clause.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_CLAUSE_H_INCLUDED
#define CLASP_CLAUSE_H_INCLUDED

#ifdef _MSC_VER
#pragma warning (disable : 4200) // nonstandard extension used : zero-sized array
#pragma once
#endif

#include <clasp/solver_types.h>
#include <clasp/util/atomic.h>
namespace Clasp { 

class SharedLiterals {
public:

        static SharedLiterals* newShareable(const LitVec& lits, ConstraintType t, uint32 numRefs = 1) {
                return newShareable(!lits.empty() ? &lits[0]:0, static_cast<uint32>(lits.size()), t, numRefs);
        }
        static SharedLiterals* newShareable(const Literal* lits, uint32 size, ConstraintType t, uint32 numRefs = 1);
        
        const Literal* begin() const { return lits_; }
        const Literal* end()   const { return lits_+size(); }
        uint32         size()  const { return size_type_ >> 2; }
        ConstraintType type()  const { return ConstraintType( size_type_ & uint32(3) ); }

        uint32 simplify(Solver& s);

        void            release();
  SharedLiterals* share();
        bool            unique()   const { return refCount_ <= 1; }
        uint32          refCount() const { return refCount_; }
private:
        void destroy();
        SharedLiterals(const Literal* lits, uint32 size, ConstraintType t, uint32 numRefs);
        SharedLiterals(const SharedLiterals&);
        SharedLiterals& operator=(const SharedLiterals&);
        Clasp::atomic<int32> refCount_;
        uint32               size_type_;
        Literal              lits_[0];
};


class ClauseCreator {
public:

        explicit ClauseCreator(Solver* s = 0);
        void setSolver(Solver& s)         { solver_ = &s; }
        void addDefaultFlags(uint32 f)    { flags_ |= f; }
        void reserve(LitVec::size_type s) { literals_.reserve(s); }
        void clear()                      { literals_.clear(); }


        enum Status {
                // BASE STATUS
                status_open         = 0,  
                status_sat          = 1,  
                status_unsat        = 2,  
                status_unit         = 4,  
                // COMPLEX STATUS
                status_sat_asserting= 5,  
                status_asserting    = 6,  
                status_subsumed     = 9,  
                status_empty        = 10, 
        };
        struct Result {
                explicit Result(ClauseHead* loc = 0, Status st = status_open)
                        : local(loc)
                        , status(st) {}
                ClauseHead*     local;
                Status          status;
                bool     ok()   const { return (status & status_unsat) == 0; }
                bool     unit() const { return (status & status_unit) != 0; }
                operator bool() const { return ok(); }
        };

        ClauseCreator& start(ConstraintType t = Constraint_t::static_constraint);
        ClauseCreator& setActivity(uint32 a)      { extra_.setActivity(a);  return *this; }
        ClauseCreator& setLbd(uint32 lbd)         { extra_.setLbd(lbd); return *this; }
        ClauseCreator& add(const Literal& p)      { literals_.push_back(p); return *this; }
        ClauseRep      prepare(bool fullSimplify);
        uint32         size()    const { return (uint32)literals_.size(); }
        Literal&       operator[](uint32 i)       { return literals_[i]; }
        Literal        operator[](uint32 i) const { return literals_[i]; }
        const LitVec&  lits()    const { return literals_; }
        LitVec&        lits()          { return literals_; }
        ConstraintType type()    const { return extra_.type(); }
        ClauseInfo     info()    const { return extra_; }

        Result end(uint32 flags = clause_not_sat | clause_not_conflict);


        enum CreateFlag {
                // REPRESENTATION
                clause_no_add        = 1,  
                clause_explicit      = 2,  
                // STATUS
                clause_not_sat       = 4,  
                clause_not_root_sat  = 8,  
                clause_not_conflict  = 16, 
                // INTEGRATE
                clause_no_release    = 32, 
                clause_int_lbd       = 64, 
                // PREPARE
                clause_no_prepare    = 128,
                clause_force_simplify= 256,
                clause_no_heuristic  = 512 
        };      
        static Status    status(const Solver& s, const Literal* clause_begin, const Literal* clause_end);
        static Status    status(const Solver& s, const ClauseRep& c);
        

        static uint32    watchOrder(const Solver& s, Literal p);
        

        static ClauseRep prepare(Solver& s, LitVec& lits, uint32 flags, const ClauseInfo& info = ClauseInfo());


        static Result create(Solver& s, LitVec& lits, uint32 flags, const ClauseInfo& info = ClauseInfo());
        static Result create(Solver& s, const ClauseRep& rep, uint32 flags);

        static Result integrate(Solver& s, SharedLiterals* clause, uint32 flags, ConstraintType t);
        static Result integrate(Solver& s, SharedLiterals* clause, uint32 flags);
private:        
        static ClauseRep   prepare(Solver& s, const Literal* in, uint32 inSize, const ClauseInfo& e, uint32 flags, Literal* out, uint32 outMax = UINT32_MAX);
        static Result      create_prepared(Solver& s, const ClauseRep& pc, uint32 flags);
        static ClauseHead* newProblemClause(Solver& s, const ClauseRep& clause, uint32 flags);
        static ClauseHead* newLearntClause(Solver& s, const ClauseRep& clause, uint32 flags);
        static ClauseHead* newUnshared(Solver& s, SharedLiterals* clause, const Literal* w, const ClauseInfo& e);
        static bool        ignoreClause(const Solver& s, const ClauseRep& cl, Status st, uint32 modeFlags);
        Solver*    solver_;   // solver in which new clauses are stored
        LitVec     literals_; // literals of the new clause
        ClauseInfo extra_;    // extra info 
        uint32     flags_;    // default flags to be used in end()
};

class Clause : public ClauseHead {
public:
        typedef Constraint::PropResult   PropResult;
        enum { MAX_SHORT_LEN = 5 };
        
        static void* alloc(Solver& s, uint32 mLits, bool learnt);
        

        static ClauseHead*  newClause(Solver& s, const ClauseRep& rep) {
                return newClause(alloc(s, rep.size, rep.info.learnt()), s, rep);
        }

        static ClauseHead*  newClause(void* mem, Solver& s, const ClauseRep& rep);


        static ClauseHead*  newContractedClause(Solver& s, const ClauseRep& rep, uint32 tailPos, bool extend);
        

        static ClauseHead* newShared(Solver& s, SharedLiterals* lits, const ClauseInfo& e, const Literal head[3], bool addRef = true);

        // Constraint-Interface
        
        Constraint* cloneAttach(Solver& other);

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

        bool minimize(Solver& m, Literal p, CCMinRecursive* r);

        bool isReverseReason(const Solver& s, Literal p, uint32 maxL, uint32 maxN);


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

        void destroy(Solver* s = 0, bool detach = false);
        
        // LearntConstraint interface

        uint32 isOpen(const Solver& s, const TypeSet& t, LitVec& freeLits);
        
        // clause interface
        BoolPair strengthen(Solver& s, Literal p, bool allowToShort);
        void     detach(Solver&);
        uint32   size()                 const;
        void     toLits(LitVec& out)    const;
        bool     contracted()           const { return data_.local.contracted(); }
        bool     isSmall()              const { return data_.local.isSmall(); }
        bool     strengthened()         const { return data_.local.strengthened(); }
        uint32   computeAllocSize()     const;
private:
        Clause(Solver& s, const ClauseRep& rep, uint32 tail = UINT32_MAX, bool extend = false);
        Clause(Solver& s, const Clause& other);
        typedef std::pair<Literal*, Literal*> LitRange;
        void         undoLevel(Solver& s);
        bool         updateWatch(Solver& s, uint32 pos);
        Literal*     removeFromTail(Solver& s, Literal* it, Literal* end);
        Literal*     longEnd()   { return head_+data_.local.size(); }
        LitRange     tail() {
                if (!isSmall()) { return LitRange(head_+ClauseHead::HEAD_LITS, longEnd()); }
                uint32 ts = (data_.lits[0] != 2) + (data_.lits[1] != 2);
                return LitRange((Literal*)data_.lits, (Literal*)(data_.lits + ts));
        }
};


class LoopFormula : public LearntConstraint {
public:
        static LoopFormula* newLoopFormula(Solver& s, Literal* bodyLits, uint32 numBodies, uint32 bodyToWatch, uint32 numAtoms, const Activity& act);


        void addAtom(Literal atom, Solver& s);
        
        void updateHeuristic(Solver& s);
        
        uint32 size() const;
        
        // Constraint interface
        Constraint* cloneAttach(Solver&) { return 0; }
        PropResult  propagate(Solver& s, Literal p, uint32& data);
        void reason(Solver&, Literal p, LitVec& lits);
        bool minimize(Solver& s, Literal p, CCMinRecursive* ccMin);
        bool simplify(Solver& s, bool = false);
        void destroy(Solver* = 0, bool = false);
        
        // LearntConstraint interface
        bool locked(const Solver& s) const;
        
        uint32 isOpen(const Solver& s, const TypeSet& t, LitVec& freeLits);
        

        Activity activity() const { return act_; }
        
        void decreaseActivity()          { act_ = Activity(act_.activity()>>1, act_.lbd()); }
        void resetActivity(Activity hint){ act_ = hint; }
        
        ConstraintType type() const { return Constraint_t::learnt_loop; }
private:
        LoopFormula(Solver& s, uint32 size, Literal* bodyLits, uint32 numBodies, uint32 bodyToWatch, const Activity& a);
        bool watchable(const Solver& s, uint32 idx);
        bool isTrue(const Solver& s, uint32 idx);
        Activity act_;     // Activity of constraint 
        uint32   end_;     // position of second sentinel
        uint32   size_;    // size of lits_
        uint32   other_;   // stores the position of a literal that was recently true
        Literal  lits_[0]; // S B1...Bm ai S a1...an
};

namespace mt {


class SharedLitsClause : public ClauseHead {
public:

        static ClauseHead* newClause(Solver& s, SharedLiterals* shared_lits, const ClauseInfo& e, const Literal* lits, bool addRef = true);
        
        Constraint*    cloneAttach(Solver& other);
        void           reason(Solver& s, Literal p, LitVec& out);
        bool           minimize(Solver& s, Literal p, CCMinRecursive* rec);
        bool           isReverseReason(const Solver& s, Literal p, uint32 maxL, uint32 maxN);
        bool           simplify(Solver& s, bool);
        void           destroy(Solver* s, bool detach);
        uint32         isOpen(const Solver& s, const TypeSet& t, LitVec& freeLits);
        uint32         size() const;
        void           toLits(LitVec& out) const;
private:
        SharedLitsClause(Solver& s, SharedLiterals* x, const Literal* lits, const ClauseInfo&,  bool addRef);
        bool     updateWatch(Solver& s, uint32 pos);
        BoolPair strengthen(Solver& s, Literal p, bool allowToShort);
};
}

}
#endif