constraint.h

Go to the documentation of this file.

// 
// Copyright (c) 2006-2012, Benjamin Kaufmann
// 
// This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 
// 
// Clasp is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
// 
// Clasp is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
// 
// You should have received a copy of the GNU General Public License
// along with Clasp; if not, write to the Free Software
// Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
//
#ifndef CLASP_CONSTRAINT_H_INCLUDED
#define CLASP_CONSTRAINT_H_INCLUDED

#ifdef _MSC_VER
#pragma once
#endif

#include <clasp/literal.h>
#include <utility>  // std::pair
#include <cassert>

namespace Clasp {

class  SharedContext;
class  Solver;
class  ClauseHead;
struct CCMinRecursive;


struct Constraint_t {
        enum Type { 
                static_constraint = 0, 
                learnt_conflict   = 1, 
                learnt_loop       = 2, 
                learnt_other      = 3, 
                max_value         = learnt_other
        };
        struct Set {
                Set() : m(0) {}
                bool inSet(Type t) const { return (m & (uint32(1)<<t)) != 0; }
                void addSet(Type t)      { m |= (uint32(1)<<t); }
                uint32 m;
        };
};  
typedef Constraint_t::Type ConstraintType;
typedef Constraint_t::Set  TypeSet;
struct Activity {
        enum { LBD_SHIFT = 7, MAX_LBD = (1 << LBD_SHIFT)-1, MAX_ACT = (1 << (32-LBD_SHIFT))-1 };
        Activity(uint32 act, uint32 lbd) : rep( (act << LBD_SHIFT) | lbd ) {}
        uint32 activity() const { return rep >> LBD_SHIFT; }
        uint32 lbd()      const { return rep & uint32(MAX_LBD); }
        void   bumpAct()        { if (rep < uint32(MAX_ACT<<LBD_SHIFT)) rep += (1<<LBD_SHIFT); }
        void   setLbd(uint32 x) { rep &= ~uint32(MAX_LBD); rep |= x; }
        uint32 rep;
};


class Constraint {
public:
        struct PropResult {
                explicit PropResult(bool a_ok = true, bool a_keepWatch = true) : ok(a_ok), keepWatch(a_keepWatch) {}
                bool ok;         
                bool keepWatch;  
        };
        Constraint();

        virtual Constraint* cloneAttach(Solver& other) = 0;
        
        virtual void destroy(Solver* s = 0, bool detach = false);


        virtual ConstraintType type() const;

        virtual PropResult propagate(Solver& s, Literal p, uint32& data) = 0;

        virtual void reason(Solver& s, Literal p, LitVec& lits) = 0;

        virtual bool minimize(Solver& s, Literal p, CCMinRecursive* rec);


        virtual void undoLevel(Solver& s);

        virtual bool simplify(Solver& s, bool reinit = false);

        virtual uint32 estimateComplexity(const Solver& s) const;


        virtual ClauseHead* clause();


        virtual bool valid(Solver& s);
protected:
        virtual ~Constraint();
private:
        Constraint(const Constraint&);
        Constraint& operator=(const Constraint&);
};


class LearntConstraint : public Constraint {
public:
        LearntConstraint();

        ConstraintType type() const;

        virtual bool locked(const Solver& s) const = 0;


        virtual Activity activity() const;
        
        virtual void decreaseActivity();
        virtual void resetActivity(Activity hint);
        

        virtual uint32 isOpen(const Solver& s, const TypeSet& t, LitVec& freeLits) = 0;
protected:
        ~LearntConstraint();
};


class PostPropagator : public Constraint {
public:
        PostPropagator();
        virtual ~PostPropagator();
        using Constraint::propagate;  // Enable overloading!

        PostPropagator* next; // main propagation lists of post propagators
        enum Priority {
                priority_class_simple    = 0,    
                priority_reserved_msg    = 0,    
                priority_reserved_ufs    = 10,   
                priority_reserved_look   = 1023, 
                priority_class_general   = 1024, 
        };


        virtual uint32 priority() const = 0;


        virtual bool   init(Solver& s);
        

        virtual bool   propagateFixpoint(Solver& s, PostPropagator* ctx) = 0;


        virtual void   reset();


        virtual bool   isModel(Solver& s);
protected:
        Constraint* cloneAttach(Solver&) { return 0; }
        // Constraint interface - noops
        PropResult propagate(Solver&, Literal, uint32&);
  void       reason(Solver&, Literal, LitVec& );
private:
        PostPropagator(const PostPropagator&);
        PostPropagator& operator=(const PostPropagator&);
};

class MessageHandler : public PostPropagator {
public:
        MessageHandler();
        virtual bool   handleMessages() = 0;
        virtual uint32 priority()const { return PostPropagator::priority_reserved_msg; }
        virtual bool   propagateFixpoint(Solver&, PostPropagator*) { return handleMessages(); }
};



class Antecedent {
public:
        enum Type { generic_constraint = 0, ternary_constraint = 1, binary_constraint = 2};

        Antecedent() : data_(0) {}
        

        Antecedent(const Literal& p) {
                // first lit is stored in high dword
                data_ = (((uint64)p.index()) << 33) + binary_constraint;
                assert(type() == binary_constraint && firstLiteral() == p);
        }
        

        Antecedent(const Literal& p, const Literal& q) {
                // first lit is stored in high dword
                // second lit is stored in low dword
                data_ = (((uint64)p.index()) << 33) + (((uint64)q.index()) << 2) + ternary_constraint;
                assert(type() == ternary_constraint && firstLiteral() == p && secondLiteral() == q);
        }


        Antecedent(Constraint* con) : data_((uintp)con) {
                assert(type() == generic_constraint && constraint() == con);
        }

        bool isNull() const {
                return data_ == 0;
        }

        Type type() const {
                return Type( data_ & 3 );
        }
        
        bool learnt() const { return data_ && (data_ & 3u) == 0 && constraint()->type() != Constraint_t::static_constraint; }
        

        Constraint* constraint() const {
                assert(type() == generic_constraint);
                return (Constraint*)(uintp)data_;
        }
        

        Literal firstLiteral() const {
                assert(type() != generic_constraint);
                return Literal::fromIndex(static_cast<uint32>(data_ >> 33));
        }
        

        Literal secondLiteral() const {
                assert(type() == ternary_constraint);
                return Literal::fromIndex( static_cast<uint32>(data_>>1) >> 1 );
        }


        void reason(Solver& s, Literal p, LitVec& lits) const {
                assert(!isNull());
                Type t = type();
                if (t == generic_constraint) {
                        constraint()->reason(s, p, lits);
                }
                else {
                        lits.push_back(firstLiteral());
                        if (t == ternary_constraint) {
                                lits.push_back(secondLiteral());
                        }
                }
        }
        template <class S>
        bool minimize(S& s, Literal p, CCMinRecursive* rec) const {
                assert(!isNull());
                Type t = type();
                if (t == generic_constraint) {
                        return constraint()->minimize(s, p, rec);
                }
                else {
                        return s.ccMinimize(firstLiteral(), rec)
                                && (t != ternary_constraint || s.ccMinimize(secondLiteral(), rec));
                }
        }

        bool operator==(const Constraint* con) const {
                return static_cast<uintp>(data_) == reinterpret_cast<uintp>(con);
        }


        static bool checkPlatformAssumptions();

        uint64  asUint() const { return data_; }
        uint64& asUint()       { return data_; }
private:
        uint64 data_;
};


class PlatformError : public ClaspError {
public:
        explicit PlatformError(const char* msg);
};

}
#endif