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