shared_context.h

Go to the documentation of this file.

// 
// Copyright (c) 2010-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_SHARED_CONTEXT_H_INCLUDED
#define CLASP_SHARED_CONTEXT_H_INCLUDED
#ifdef _MSC_VER
#pragma warning (disable : 4200) // nonstandard extension used : zero-sized array
#pragma once
#endif

#include <clasp/literal.h>
#include <clasp/constraint.h>
#include <clasp/util/left_right_sequence.h>
#include <clasp/util/misc_types.h>
#include <clasp/util/atomic.h>
#include <clasp/solver_strategies.h>
namespace Clasp {
class Solver;
class ClauseInfo;
class Assignment;
class SharedContext;
class SharedLiterals;
class SharedDependencyGraph;
struct SolverStats;


class SatPreprocessor {
public:
        class Clause {
        public:
                static Clause*  newClause(const Literal* lits, uint32 size);
                static uint64   abstractLit(Literal p)      { return uint64(1) << ((p.var()-1) & 63);  }
                uint32          size()                const { return size_;       }
                const Literal&  operator[](uint32 x)  const { return lits_[x];    }
                bool            inQ()                 const { return inQ_ != 0;   }
                uint64          abstraction()         const { return data_.abstr; }
                Clause*         next()                const { return data_.next;  }
                bool            marked()              const { return marked_ != 0;}
                Literal&        operator[](uint32 x)        { return lits_[x];    }    
                void            setInQ(bool b)              { inQ_    = (uint32)b;}
                void            setMarked(bool b)           { marked_ = (uint32)b;}
                uint64&         abstraction()               { return data_.abstr; }
                Clause*         linkRemoved(Clause* next)   { data_.next = next; return this; }
                void            strengthen(Literal p);
                void            simplify(Solver& s);
                void            destroy();
        private:
                Clause(const Literal* lits, uint32 size);
                union {
                        uint64  abstr;      // abstraction of literals
                        Clause* next;       // next removed clause
                }       data_;
                uint32  size_   : 30; // size of the clause
                uint32  inQ_    : 1;  // in todo-queue?
                uint32  marked_ : 1;  // a marker flag
                Literal lits_[1];     // literals of the clause: [lits_[0], lits_[size_])
        };
        
        SatPreprocessor() : ctx_(0), elimTop_(0), seen_(1,1) {}
        virtual ~SatPreprocessor();


        virtual SatPreprocessor* clone() = 0;

        uint32 numClauses() const { return (uint32)clauses_.size(); }

        bool addClause(const LitVec& cl) { return addClause(!cl.empty() ? &cl[0] : 0, cl.size()); }
        bool addClause(const Literal* clause, uint32 size);

        bool preprocess(SharedContext& ctx, SatPreParams& opts);
        bool preprocess(SharedContext& ctx);

        void cleanUp(bool discardEliminated = false);

        void extendModel(ValueVec& m, LitVec& open);
        struct Stats {
                Stats() : clRemoved(0), clAdded(0), litsRemoved(0) {}
                uint32 clRemoved;
                uint32 clAdded;
                uint32 litsRemoved;
        } stats;
        typedef SatPreParams Options;
protected:
        typedef PodVector<Clause*>::type  ClauseList;
        virtual bool  initPreprocess(SatPreParams& opts) = 0;
        virtual bool  doPreprocess() = 0;
        virtual void  doExtendModel(ValueVec& m, LitVec& open) = 0;
        virtual void  doCleanUp() = 0;
        Clause*       clause(uint32 clId)       { return clauses_[clId]; }
        const Clause* clause(uint32 clId) const { return clauses_[clId]; }
        void          freezeSeen();
        void          discardClauses(bool discardEliminated);
        void          setClause(uint32 clId, const LitVec& cl) {
                clauses_[clId] = Clause::newClause(&cl[0], (uint32)cl.size());
        }
        void          destroyClause(uint32 clId){
                clauses_[clId]->destroy();
                clauses_[clId] = 0;
                ++stats.clRemoved;
        }
        void          eliminateClause(uint32 id){
                elimTop_     = clauses_[id]->linkRemoved(elimTop_);
                clauses_[id] = 0;
                ++stats.clRemoved;
        }
        SharedContext*  ctx_;     // current context
        Clause*         elimTop_; // stack of blocked/eliminated clauses
private:
        SatPreprocessor(const SatPreprocessor&);
        SatPreprocessor& operator=(const SatPreprocessor&);
        ClauseList clauses_; // initial non-unit clauses
        LitVec     units_;   // initial unit clauses
        Range32    seen_;    // vars seen in previous step
};


// Problem statistics

struct ProblemStats {
        ProblemStats() { reset(); }
        uint32  vars;
        uint32  vars_eliminated;
        uint32  vars_frozen;
        uint32  constraints;
        uint32  constraints_binary;
        uint32  constraints_ternary;
        uint32  complexity;
        void    reset() { std::memset(this, 0, sizeof(*this)); }
        uint32  numConstraints() const   { return constraints + constraints_binary + constraints_ternary; }
        void diff(const ProblemStats& o) {
                vars               = std::max(vars, o.vars)-std::min(vars, o.vars);
                vars_eliminated    = std::max(vars_eliminated, o.vars_eliminated)-std::min(vars_eliminated, o.vars_eliminated);
                vars_frozen        = std::max(vars_frozen, o.vars_frozen)-std::min(vars_frozen, o.vars_frozen);
                constraints        = std::max(constraints, o.constraints) - std::min(constraints, o.constraints);
                constraints_binary = std::max(constraints_binary, o.constraints_binary) - std::min(constraints_binary, o.constraints_binary);
                constraints_ternary= std::max(constraints_ternary, o.constraints_ternary) - std::min(constraints_ternary, o.constraints_ternary);
        }
        double operator[](const char* key) const;
        static const char* keys(const char* = 0);
};

struct VarInfo {
        enum FLAG {
                MARK_P = 0x1u, // mark for positive literal
                MARK_N = 0x2u, // mark for negative literal
                NANT   = 0x4u, // var in NAnt(P)?
                PROJECT= 0x8u, // do we project on this var?
                BODY   = 0x10u,// is this var representing a body?
                EQ     = 0x20u,// is the var representing both a body and an atom?
                DISJ   = 0x40u,// in non-hcf disjunction?
                FROZEN = 0x80u // is the variable frozen?
        };
        VarInfo() : rep(0) {}

        VarType type()          const { return has(VarInfo::EQ) ? Var_t::atom_body_var : VarType(Var_t::atom_var + has(VarInfo::BODY)); }
        bool    nant()          const { return has(VarInfo::NANT); }
        bool    project()       const { return has(VarInfo::PROJECT);}
        bool    inDisj()        const { return has(VarInfo::DISJ);}
        bool    frozen()        const { return has(VarInfo::FROZEN); }

        bool    preferredSign() const { return !has(VarInfo::BODY); }
        
        bool    has(FLAG f)     const { return (rep & flag(f)) != 0; }
        bool    has(uint32 f)   const { return (rep & f) != 0;       }
        void    set(FLAG f)           { rep |= flag(f); }
        void    toggle(FLAG f)        { rep ^= flag(f); }
        static uint8 flag(FLAG x)     { return uint8(x); }
        uint8 rep;
};

class ShortImplicationsGraph {
public:
        ShortImplicationsGraph();
        ~ShortImplicationsGraph();
        enum ImpType { binary_imp = 2, ternary_imp = 3 };
        
        void resize(uint32 nodes);

        void markShared(bool b) { shared_ = b; }

        bool add(ImpType t, bool learnt, const Literal* lits);
        

        void removeTrue(const Solver& s, Literal p);
        

        bool   propagate(Solver& s, Literal p) const;
        bool   propagateBin(Assignment& out, Literal p, uint32 dl) const;
        bool   reverseArc(const Solver& s, Literal p, uint32 maxLev, Antecedent& out) const;
        
        uint32 numBinary() const { return bin_[0]; }
        uint32 numTernary()const { return tern_[0]; }
        uint32 numLearnt() const { return bin_[1] + tern_[1]; }
        uint32 numEdges(Literal p) const;
        uint32 size() const      { return graph_.size(); }

        template <class OP>
        bool forEach(Literal p, const OP& op) const {
                const ImplicationList& x = graph_[p.index()];
                if (x.empty()) return true;
                ImplicationList::const_right_iterator rEnd = x.right_end(); // prefetch
                for (ImplicationList::const_left_iterator it = x.left_begin(), end = x.left_end(); it != end; ++it) {
                        if (!op.unary(p, *it)) { return false; }
                }
                for (ImplicationList::const_right_iterator it = x.right_begin(); it != rEnd; ++it) {
                        if (!op.binary(p, it->first, it->second)) { return false; }
                }
#if WITH_THREADS
                for (Block* b = (x).learnt; b ; b = b->next) {
                        p.watch(); bool r = true;
                        for (Block::const_iterator imp = b->begin(), endOf = b->end(); imp != endOf; ) {
                                if (!imp->watched()) { r = op.binary(p, imp[0], imp[1]); imp += 2; }
                                else                 { r = op.unary(p, imp[0]);          imp += 1; }
                                if (!r)              { return false; }
                        }
                }
#endif
                return true;
        }
private:
        ShortImplicationsGraph(const ShortImplicationsGraph&);
        ShortImplicationsGraph& operator=(ShortImplicationsGraph&);
        struct Propagate;
        struct ReverseArc;
#if WITH_THREADS
        struct Block {
                typedef Clasp::atomic<uint32> atomic_size;
                typedef Clasp::atomic<Block*> atomic_ptr;
                typedef const Literal*      const_iterator;
                typedef       Literal*      iterator;
                enum { block_cap = (64 - (sizeof(atomic_size)+sizeof(atomic_ptr)))/sizeof(Literal) };
                explicit Block();
                const_iterator  begin() const { return data; }
                const_iterator  end()   const { return data+size(); }
                iterator        end()         { return data+size(); }
                uint32          size()  const { return size_lock >> 1; }
                bool tryLock(uint32& lockedSize);
                void addUnlock(uint32 lockedSize, const Literal* x, uint32 xs);
                atomic_ptr  next;
                atomic_size size_lock;
                Literal     data[block_cap];
        };
        typedef Block::atomic_ptr SharedBlockPtr;
        typedef bk_lib::left_right_sequence<Literal, std::pair<Literal,Literal>, 64-sizeof(SharedBlockPtr)> ImpListBase;
        struct ImplicationList : public ImpListBase {
                ImplicationList() : ImpListBase() { learnt = 0; }
                ImplicationList(const ImplicationList& other) : ImpListBase(other), learnt(other.learnt) {}
                ~ImplicationList();
                bool hasLearnt(Literal q, Literal r = negLit(0)) const;
                void addLearnt(Literal q, Literal r = negLit(0));
                void simplifyLearnt(const Solver& s);
                bool empty() const { return ImpListBase::empty() && learnt == 0; }
                void move(ImplicationList& other);
                void clear(bool b);
                SharedBlockPtr learnt; 
        };
#else
        typedef bk_lib::left_right_sequence<Literal, std::pair<Literal,Literal>, 64> ImplicationList;
#endif
        ImplicationList& getList(Literal p) { return graph_[p.index()]; }
        void remove_bin(ImplicationList& w, Literal p);
        void remove_tern(ImplicationList& w, Literal p);
        typedef PodVector<ImplicationList>::type ImpLists;
        ImpLists   graph_;     // one implication list for each literal
        uint32     bin_[2];    // number of binary constraints (0: problem / 1: learnt)
        uint32     tern_[2];   // number of ternary constraints(0: problem / 1: learnt)
        bool       shared_;
};

class Distributor {
public:
        struct Policy {
                enum Types { 
                        no       = 0,
                        conflict = Constraint_t::learnt_conflict,
                        loop     = Constraint_t::learnt_loop,
                        all      = conflict | loop,
                        implicit = all + 1
                };
                Policy(uint32 a_sz = 0, uint32 a_lbd = 0, uint32 a_type = 0) : size(a_sz), lbd(a_lbd), types(a_type) {}
                uint32 size  : 22; 
                uint32 lbd   :  7; 
                uint32 types :  3; 
        };
        static  uint64  mask(uint32 i)             { return uint64(1) << i; }
        static  uint32  initSet(uint32 sz)         { return (uint64(1) << sz) - 1; }
        static  bool    inSet(uint64 s, uint32 id) { return (s & mask(id)) != 0; }
        explicit Distributor(const Policy& p);
        virtual ~Distributor();
        bool            isCandidate(uint32 size, uint32 lbd, uint32 type) const {
                return size <= policy_.size && lbd <= policy_.lbd && ((type & policy_.types) != 0);
        }
        virtual void    publish(const Solver& source, SharedLiterals* lits) = 0;
        virtual uint32  receive(const Solver& in, SharedLiterals** out, uint32 maxOut) = 0;
private:
        Distributor(const Distributor&);
        Distributor& operator=(const Distributor&);
        Policy policy_;
};


class SharedContext {
public:
        typedef SharedDependencyGraph SDG;
        typedef PodVector<Solver*>::type       SolverVec;
        typedef SingleOwnerPtr<SDG>            SccGraph;
        typedef Configuration*                 ConfigPtr;
        typedef SingleOwnerPtr<Distributor>    DistrPtr;
        typedef const ProblemStats&            StatsRef;
        typedef SymbolTable&                   SymbolsRef;
        typedef LitVec::size_type              size_type;
        typedef ShortImplicationsGraph         ImpGraph;
        typedef const ImpGraph&                ImpGraphRef;
        typedef EventHandler*                  LogPtr;
        typedef SingleOwnerPtr<SatPreprocessor>SatPrePtr;
        enum InitMode   { init_share_symbols, init_copy_symbols };

        explicit SharedContext();
        ~SharedContext();
        void       reset();
        void       setEventHandler(EventHandler* r) { progress_ = r; }
        void       setShareMode(ContextParams::ShareMode m);
        void       setShortMode(ContextParams::ShortMode m);
        void       setConcurrency(uint32 numSolver);
        Solver&    addSolver();

        void       enableStats(uint32 level);
        void       accuStats();
        void       setPreserveModels(bool b = true) { share_.satPreM = b ? SatPreParams::prepro_preserve_models : SatPreParams::prepro_preserve_sat; }

        void       setConfiguration(Configuration* c, bool own);
        SatPrePtr  satPrepro;  
        SccGraph   sccGraph;   

        ConfigPtr  configuration()      const { return config_.get(); }
        LogPtr     eventHandler()       const { return progress_; }
        bool       seedSolvers()        const { return share_.seed != 0; }
        uint32     concurrency()        const { return share_.count; }
        bool       preserveModels()     const { return static_cast<SatPreParams::Mode>(share_.satPreM) == SatPreParams::prepro_preserve_models; }
        bool       physicalShare(ConstraintType t) const { return (share_.shareM & (1 + (t != Constraint_t::static_constraint))) != 0; }
        bool       physicalShareProblem()          const { return (share_.shareM & ContextParams::share_problem) != 0; }
        bool       allowImplicit(ConstraintType t) const { return t != Constraint_t::static_constraint ? share_.shortM != ContextParams::short_explicit : !isShared(); }


        bool       ok()                 const;
        bool       frozen()             const { return share_.frozen;}
        bool       isShared()           const { return frozen() && concurrency() > 1; } 
        bool       isExtended()         const { return problem_.vars_frozen || symbolTable().type() == SymbolTable::map_indirect; }
        bool       hasSolver(uint32 id) const { return id < solvers_.size(); }
        Solver*    master()             const { return solver(0);    }  
        Solver*    solver(uint32 id)    const { return solvers_[id]; }
        

        uint32     numVars()            const { return static_cast<uint32>(varInfo_.size() - 1); }
        uint32     numEliminatedVars()  const { return problem_.vars_eliminated; }

        bool       validVar(Var var)    const { return var < static_cast<uint32>(varInfo_.size()); }
        VarInfo    varInfo(Var v)       const { assert(validVar(v)); return varInfo_[v]; }
        bool       eliminated(Var v)    const;
        bool       marked(Literal p)    const { return varInfo(p.var()).has(VarInfo::MARK_P + p.sign()); }
        Literal    stepLiteral()        const { return step_; }
        uint32     numConstraints()     const;
        uint32     numBinary()          const { return btig_.numBinary();  }
        uint32     numTernary()         const { return btig_.numTernary(); }
        uint32     numUnary()           const { return lastTopLevel_; }
        uint32     problemComplexity()  const;
        StatsRef   stats()              const { return problem_; }
        SymbolsRef symbolTable()        const { return symTabPtr_->symTab; }



        bool    unfreeze();
        void    cloneVars(const SharedContext& other, InitMode m = init_copy_symbols);
        void    resizeVars(uint32 maxVar) { varInfo_.resize(std::max(Var(1), maxVar)); problem_.vars = numVars(); }

        Var     addVar(VarType t, bool eq = false);
        void    requestStepVar();
        void    requestData(Var v);
        void    setFrozen(Var v, bool b);
        void    setNant(Var v, bool b)       { if (b != varInfo(v).has(VarInfo::NANT))    varInfo_[v].toggle(VarInfo::NANT);    }
        void    setInDisj(Var v, bool b)     { if (b != varInfo(v).has(VarInfo::DISJ))    varInfo_[v].toggle(VarInfo::DISJ);    }
        void    setProject(Var v, bool b)    { if (b != varInfo(v).has(VarInfo::PROJECT)) varInfo_[v].toggle(VarInfo::PROJECT); }
        void    setVarEq(Var v, bool b)      { if (b != varInfo(v).has(VarInfo::EQ))      varInfo_[v].toggle(VarInfo::EQ);      }
        void    mark(Literal p)              { assert(validVar(p.var())); varInfo_[p.var()].rep |= (VarInfo::MARK_P + p.sign()); }
        void    unmark(Var v)                { assert(validVar(v)); varInfo_[v].rep &= ~(VarInfo::MARK_P|VarInfo::MARK_N); }

        void    eliminate(Var v);


        Solver& startAddConstraints(uint32 constraintGuess = 100);
        
        bool    addUnary(Literal x);
        bool    addBinary(Literal x, Literal y);
        bool    addTernary(Literal x, Literal y, Literal z);
        void    add(Constraint* c);


        bool    endInit(bool attachAll = false);
        


        bool     attach(uint32 id) { return attach(*solver(id)); }
        bool     attach(Solver& s);
        
        

        void     detach(uint32 id, bool reset = false) { return detach(*solver(id), reset); }
        void     detach(Solver& s, bool reset = false);
        
        DistrPtr distributor;
        uint32   winner()             const   { return share_.winner; }
        void     setWinner(uint32 sId)        { share_.winner = std::min(sId, concurrency()); }
        
        void     simplify(bool shuffle);
        void     removeConstraint(uint32 idx, bool detach);
        

        int         addImp(ImpGraph::ImpType t, const Literal* lits, ConstraintType ct);
        uint32      numLearntShort()     const { return btig_.numLearnt(); }
        ImpGraphRef shortImplications()  const { return btig_; }
        void        simplifyShort(const Solver& s, Literal p);
        void               report(const Event& ev)                 const { if (progress_) progress_->dispatch(ev);  }
        bool               report(const Solver& s, const Model& m) const { return !progress_ || progress_->onModel(s, m); }
        void               initStats(Solver& s)                    const;
        const SolverStats& stats(const Solver& s, bool accu)       const;
private:
        SharedContext(const SharedContext&);
        SharedContext& operator=(const SharedContext&);
        void    init();
        bool    unfreezeStep();
        Literal addAuxLit();
        typedef SingleOwnerPtr<Configuration> Config;
        typedef PodVector<VarInfo>::type      VarVec;
        typedef PodVector<SolverStats*>::type StatsVec;
        struct SharedSymTab {
                SharedSymTab() : refs(1) {}
                SymbolTable symTab;
                uint32      refs;
        }*           symTabPtr_;     // pointer to shared symbol table
        ProblemStats   problem_;     // problem statistics
        VarVec         varInfo_;     // varInfo[v] stores info about variable v
        ImpGraph       btig_;        // binary-/ternary implication graph
        Config         config_;      // active configuration
        SolverVec      solvers_;     // solvers associated with this context
        LogPtr         progress_;    // event handler or 0 if not used
        Literal        step_;        // literal for tagging enumeration/step constraints
        uint32         lastTopLevel_;// size of master's top-level after last init
        struct Share {               // Additional data
                uint32 count   :12;        //   max number of objects sharing this object
                uint32 winner  :12;        //   id of solver that terminated the search
                uint32 shareM  : 3;        //   physical sharing mode
                uint32 shortM  : 1;        //   short clause mode
                uint32 frozen  : 1;        //   is adding of problem constraints allowed?
                uint32 seed    : 1;        //   set seed of new solvers
                uint32 satPreM : 1;        //   preprocessing mode
                Share() : count(1), winner(0), shareM((uint32)ContextParams::share_auto), shortM(0), frozen(0), seed(0), satPreM(0) {}
        }              share_;
        StatsVec       accu_;        // optional stats accumulator for incremental solving
};
}
#endif