diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-02-25 18:23:10 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-02-25 18:23:10 +0000 |
commit | 7aa55e0d38e73a02b11ad0c5a60196b610674050 (patch) | |
tree | c59def0ed00dcde29a5a6498cf74ac87dc3a2a6f /src/prop/sat.h | |
parent | d8da6a3644d1cdbe62d44a8eb80068da4d1d2855 (diff) |
Refactored CnfStream to work with the bv theory Bitblaster:
* separated SatSolverInput interface class into two classes:
- TheoryProxy for the sat solver to communicate with the theories
- SatSolverInterface abstract class to communicate with the sat solver
* instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation
* added abstract classes for DPLLSatSolver and BVSatSolver different interfaces
Replaced TheoryBV with bitblasting implementation:
* all operators bitblasted
* only operator elimination rewrite rules so far
Diffstat (limited to 'src/prop/sat.h')
-rw-r--r-- | src/prop/sat.h | 303 |
1 files changed, 33 insertions, 270 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h index 3f3166c14..a6bdcb309 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -29,6 +29,8 @@ #include "util/options.h" #include "util/stats.h" +#include "prop/sat_module.h" + #ifdef __CVC4_USE_MINISAT #include "prop/minisat/core/Solver.h" @@ -48,82 +50,10 @@ class CnfStream; /* Definitions of abstract types and conversion functions for SAT interface */ -#ifdef __CVC4_USE_MINISAT - -/** Type of the SAT variables */ -typedef Minisat::Var SatVariable; - -/** Type of the SAT literals */ -typedef Minisat::Lit SatLiteral; - -/** Type of the SAT clauses */ -typedef Minisat::vec<SatLiteral> SatClause; - -/** Type of a SAT variable assignment (T, F, unknown) */ -typedef Minisat::lbool SatLiteralValue; - /** - * Returns the variable of the literal. - * @param lit the literal + * The proxy class that allows the SatSolver to communicate with the theories */ -inline SatVariable literalToVariable(SatLiteral lit) { - return Minisat::var(lit); -} - -inline SatLiteral variableToLiteral(SatVariable var) { - return Minisat::mkLit(var); -} - -inline bool literalSign(SatLiteral lit) { - return Minisat::sign(lit); -} - -static inline size_t -hashSatLiteral(const SatLiteral& literal) { - return (size_t) Minisat::toInt(literal); -} - -inline std::string stringOfLiteralValue(SatLiteralValue val) { - if( val == l_False ) { - return "0"; - } else if (val == l_True ) { - return "1"; - } else { // unknown - return "_"; - } -} -#endif /* __CVC4_USE_MINISAT */ - -/** Interface encapsulating the "input" to the solver, e.g., from the - * CNF converter. - * - * TODO: Is it possible to push the typedefs of SatClause and SatVariable - * into here, somehow? - */ -class SatInputInterface { -public: - /** Virtual destructor to make g++ happy */ - virtual ~SatInputInterface() { } - /** Assert a clause in the solver. */ - virtual void addClause(SatClause& clause, bool removable) = 0; - /** Create a new boolean variable in the solver. */ - virtual SatVariable newVar(bool theoryAtom = false) = 0; - /** Get the current user assertion level of the solver */ - virtual int getAssertionLevel() const = 0; - /** Unregister the variable (of the literal) from solving */ - virtual void unregisterVar(SatLiteral lit) = 0; - /** Register the variable (of the literal) for solving */ - virtual void renewVar(SatLiteral lit, int level = -1) = 0; - /** Interrupt the solver */ - virtual void interrupt() = 0; -}; - -/** - * The proxy class that allows us to modify the internals of the SAT solver. - * It's only accessible from the PropEngine, and should be treated with major - * care. - */ -class SatSolver : public SatInputInterface { +class TheoryProxy { /** The prop engine we are using */ PropEngine* d_propEngine; @@ -143,96 +73,20 @@ class SatSolver : public SatInputInterface { */ std::hash_set<Node, NodeHashFunction> d_shared; - /* Pointer to the concrete SAT solver. Including this via the - preprocessor saves us a level of indirection vs, e.g., defining a - sub-class for each solver. */ - -#ifdef __CVC4_USE_MINISAT - - /** Minisat solver */ - Minisat::SimpSolver* d_minisat; - - class Statistics { - private: - ReferenceStat<uint64_t> d_statStarts, d_statDecisions; - ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations; - ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals; - ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals; - ReferenceStat<uint64_t> d_statTotLiterals; - public: - Statistics() : - d_statStarts("sat::starts"), - d_statDecisions("sat::decisions"), - d_statRndDecisions("sat::rnd_decisions"), - d_statPropagations("sat::propagations"), - d_statConflicts("sat::conflicts"), - d_statClausesLiterals("sat::clauses_literals"), - d_statLearntsLiterals("sat::learnts_literals"), - d_statMaxLiterals("sat::max_literals"), - d_statTotLiterals("sat::tot_literals") - { - StatisticsRegistry::registerStat(&d_statStarts); - StatisticsRegistry::registerStat(&d_statDecisions); - StatisticsRegistry::registerStat(&d_statRndDecisions); - StatisticsRegistry::registerStat(&d_statPropagations); - StatisticsRegistry::registerStat(&d_statConflicts); - StatisticsRegistry::registerStat(&d_statClausesLiterals); - StatisticsRegistry::registerStat(&d_statLearntsLiterals); - StatisticsRegistry::registerStat(&d_statMaxLiterals); - StatisticsRegistry::registerStat(&d_statTotLiterals); - } - ~Statistics() { - StatisticsRegistry::unregisterStat(&d_statStarts); - StatisticsRegistry::unregisterStat(&d_statDecisions); - StatisticsRegistry::unregisterStat(&d_statRndDecisions); - StatisticsRegistry::unregisterStat(&d_statPropagations); - StatisticsRegistry::unregisterStat(&d_statConflicts); - StatisticsRegistry::unregisterStat(&d_statClausesLiterals); - StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); - StatisticsRegistry::unregisterStat(&d_statMaxLiterals); - StatisticsRegistry::unregisterStat(&d_statTotLiterals); - } - void init(Minisat::SimpSolver* d_minisat){ - d_statStarts.setData(d_minisat->starts); - d_statDecisions.setData(d_minisat->decisions); - d_statRndDecisions.setData(d_minisat->rnd_decisions); - d_statPropagations.setData(d_minisat->propagations); - d_statConflicts.setData(d_minisat->conflicts); - d_statClausesLiterals.setData(d_minisat->clauses_literals); - d_statLearntsLiterals.setData(d_minisat->learnts_literals); - d_statMaxLiterals.setData(d_minisat->max_literals); - d_statTotLiterals.setData(d_minisat->tot_literals); - } - }; - Statistics d_statistics; - -#endif /* __CVC4_USE_MINISAT */ - -protected: - public: - /** Hash function for literals */ - struct SatLiteralHashFunction { - inline size_t operator()(const SatLiteral& literal) const; - }; - - SatSolver(PropEngine* propEngine, - TheoryEngine* theoryEngine, - context::Context* context); - - virtual ~SatSolver(); + TheoryProxy(PropEngine* propEngine, + TheoryEngine* theoryEngine, + context::Context* context, + CnfStream* cnfStream); - SatLiteralValue solve(unsigned long& resource); + ~TheoryProxy(); - void addClause(SatClause& clause, bool removable); - - SatVariable newVar(bool theoryAtom = false); void theoryCheck(theory::Theory::Effort effort); void explainPropagation(SatLiteral l, SatClause& explanation); - void theoryPropagate(std::vector<SatLiteral>& output); + void theoryPropagate(SatClause& output); void enqueueTheoryLiteral(const SatLiteral& l); @@ -240,20 +94,6 @@ public: bool theoryNeedCheck() const; - void setCnfStream(CnfStream* cnfStream); - - /** Call value() during the search.*/ - SatLiteralValue value(SatLiteral l); - - /** Call modelValue() when the search is done.*/ - SatLiteralValue modelValue(SatLiteral l); - - int getAssertionLevel() const; - - void push(); - - void pop(); - void removeClausesAboveLevel(int level); /** @@ -265,8 +105,6 @@ public: void renewVar(SatLiteral lit, int level = -1); - void interrupt(); - TNode getNode(SatLiteral lit); void notifyRestart(); @@ -283,114 +121,26 @@ public: /* Functions that delegate to the concrete SAT solver. */ -#ifdef __CVC4_USE_MINISAT - -inline SatSolver::SatSolver(PropEngine* propEngine, - TheoryEngine* theoryEngine, - context::Context* context) : +inline TheoryProxy::TheoryProxy(PropEngine* propEngine, + TheoryEngine* theoryEngine, + context::Context* context, + CnfStream* cnfStream) : d_propEngine(propEngine), - d_cnfStream(NULL), + d_cnfStream(cnfStream), d_theoryEngine(theoryEngine), - d_context(context), - d_statistics() -{ - // Create the solver - d_minisat = new Minisat::SimpSolver(this, d_context, - Options::current()->incrementalSolving); - // Setup the verbosity - d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1; - - // Setup the random decision parameters - d_minisat->random_var_freq = Options::current()->satRandomFreq; - d_minisat->random_seed = Options::current()->satRandomSeed; - - // Give access to all possible options in the sat solver - d_minisat->var_decay = Options::current()->satVarDecay; - d_minisat->clause_decay = Options::current()->satClauseDecay; - d_minisat->restart_first = Options::current()->satRestartFirst; - d_minisat->restart_inc = Options::current()->satRestartInc; - - d_statistics.init(d_minisat); -} - -inline SatSolver::~SatSolver() { - delete d_minisat; -} - -inline SatLiteralValue SatSolver::solve(unsigned long& resource) { - Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; - if(resource == 0) { - d_minisat->budgetOff(); - } else { - d_minisat->setConfBudget(resource); - } - Minisat::vec<SatLiteral> empty; - unsigned long conflictsBefore = d_minisat->conflicts; - SatLiteralValue result = d_minisat->solveLimited(empty); - d_minisat->clearInterrupt(); - resource = d_minisat->conflicts - conflictsBefore; - Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl; - return result; -} - -inline void SatSolver::addClause(SatClause& clause, bool removable) { - d_minisat->addClause(clause, removable); -} - -inline SatVariable SatSolver::newVar(bool theoryAtom) { - return d_minisat->newVar(true, true, theoryAtom); -} - -inline SatLiteralValue SatSolver::value(SatLiteral l) { - return d_minisat->value(l); -} - -inline SatLiteralValue SatSolver::modelValue(SatLiteral l) { - return d_minisat->modelValue(l); -} - -inline void SatSolver::push() { - d_minisat->push(); -} - -inline void SatSolver::pop() { - d_minisat->pop(); -} - -inline int SatSolver::getAssertionLevel() const { - return d_minisat->getAssertionLevel(); -} - -inline void SatSolver::unregisterVar(SatLiteral lit) { - d_minisat->unregisterVar(lit); -} - -inline void SatSolver::renewVar(SatLiteral lit, int level) { - d_minisat->renewVar(lit, level); -} - -inline void SatSolver::interrupt() { - d_minisat->interrupt(); -} - -#endif /* __CVC4_USE_MINISAT */ - -inline size_t -SatSolver::SatLiteralHashFunction::operator()(const SatLiteral& literal) const { - return hashSatLiteral(literal); -} + d_context(context) +{} }/* CVC4::prop namespace */ inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { - const char * s = (prop::literalSign(lit)) ? "~" : " "; - out << s << prop::literalToVariable(lit); + out << lit.toString(); return out; } inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) { out << "clause:"; - for(int i = 0; i < clause.size(); ++i) { + for(unsigned i = 0; i < clause.size(); ++i) { out << " " << clause[i]; } out << ";"; @@ -398,10 +148,23 @@ inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& claus } inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) { - out << prop::stringOfLiteralValue(val); + std::string str; + switch(val) { + case prop::SatValUnknown: + str = "_"; + case prop::SatValTrue: + str = "1"; + case prop::SatValFalse: + str = "0"; + default: + str = "Error"; + + out << str; return out; } +} /* prop namespace */ + }/* CVC4 namespace */ #endif /* __CVC4__PROP__SAT_H */ |