From: Dejan Jovanović Date: Mon, 8 Mar 2010 21:08:40 +0000 (+0000) Subject: some more sat stuff for tim: assertions now go to theory_uf X-Git-Tag: cvc5-1.0.0~9201 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b1d9707979074abb8fed7ad4e8a2b15648c69324;p=cvc5.git some more sat stuff for tim: assertions now go to theory_uf --- diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 612b00bcf..2efad3cb2 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -14,6 +14,7 @@ ** of given an equisatisfiable stream of assertions to PropEngine. **/ +#include "sat.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "expr/node.h" @@ -71,12 +72,18 @@ SatLiteral CnfStream::lookupInCache(const TNode& n) const { void CnfStream::cacheTranslation(const TNode& node, SatLiteral lit) { Debug("cnf") << "caching translation " << node << " to " << lit << endl; + // We always cash bot the node and the negation at the same time d_translationCache[node] = lit; + d_translationCache[node.notNode()] = ~lit; } -SatLiteral CnfStream::newLiteral(const TNode& node) { - SatLiteral lit = SatLiteral(d_satSolver->newVar()); +SatLiteral CnfStream::newLiteral(const TNode& node, bool theoryLiteral) { + SatLiteral lit = SatLiteral(d_satSolver->newVar(theoryLiteral)); cacheTranslation(node, lit); + if (theoryLiteral) { + d_nodeCache[lit] = node; + d_nodeCache[~lit] = node.notNode(); + } return lit; } @@ -86,7 +93,7 @@ SatLiteral TseitinCnfStream::handleAtom(const TNode& node) { Debug("cnf") << "handleAtom(" << node << ")" << endl; - SatLiteral lit = newLiteral(node); + SatLiteral lit = newLiteral(node, true); switch(node.getKind()) { case TRUE: diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 9af15ba31..93c1f529a 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -46,7 +46,12 @@ private: SatSolver *d_satSolver; /** Cache of what literal have been registered to a node. */ - __gnu_cxx::hash_map d_translationCache; + typedef __gnu_cxx::hash_map TranslationCache; + TranslationCache d_translationCache; + + /** Cache of what nodes have been registered to a literal. */ + typedef __gnu_cxx::hash_map NodeCache; + NodeCache d_nodeCache; protected: @@ -103,9 +108,11 @@ protected: * Acquires a new variable from the SAT solver to represent the node and * inserts the necessary data it into the mapping tables. * @param node a formula + * @param theoryLiteral is this literal a theory literal (i.e. theory to be + * informed when set to true/false * @return the literal corresponding to the formula */ - SatLiteral newLiteral(const TNode& node); + SatLiteral newLiteral(const TNode& node, bool theoryLiteral = false); public: @@ -131,6 +138,20 @@ public: */ virtual void convertAndAssert(const TNode& node) = 0; + /** + * Returns a node the is represented by a give SatLiteral literal. + * @param literal the literal from the sat solver + * @return the actual node + */ + Node getNode(const SatLiteral& literal) { + Node node; + NodeCache::iterator find = d_nodeCache.find(literal); + if (find != d_nodeCache.end()) { + node = find->second; + } + return node; + } + }; /* class CnfStream */ /** diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C index dd5e1e667..e3ce088b1 100644 --- a/src/prop/minisat/core/Solver.C +++ b/src/prop/minisat/core/Solver.C @@ -77,7 +77,7 @@ Solver::~Solver() // Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be // used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). // -Var Solver::newVar(bool sign, bool dvar) +Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) { int v = nVars(); watches .push(); // (list for positive literal) @@ -88,6 +88,8 @@ Var Solver::newVar(bool sign, bool dvar) activity .push(0); seen .push(0); + theory .push(theoryAtom); + polarity .push((char)sign); decision_var.push((char)dvar); @@ -394,11 +396,17 @@ void Solver::analyzeFinal(Lit p, vec& out_conflict) void Solver::uncheckedEnqueue(Lit p, Clause* from) { assert(value(p) == l_Undef); - assigns [var(p)] = toInt(lbool(!sign(p))); // <<== abstract but not uttermost effecient + assigns [var(p)] = toInt(lbool(!sign(p))); // <<== abstract but not uttermost efficient level [var(p)] = decisionLevel(); reason [var(p)] = from; + // Added for phase-caching polarity [var(p)] = sign(p); trail.push(p); + + if (theory[var(p)]) { + // Enqueue to the theory + proxy->enqueueTheoryLiteral(p); + } } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index c593d8b2c..131999e38 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -65,7 +65,7 @@ public: // Problem specification: // - Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. + Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode. bool addClause (vec& ps); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! // Solving: @@ -144,6 +144,7 @@ protected: vec > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). vec assigns; // The current assignments (lbool:s stored as char:s). vec polarity; // The preferred polarity of each variable. + vec theory; // Is the variable representing a theory atom vec decision_var; // Declares if a variable is eligible for selection in the decision heuristic. vec trail; // Assignment stack; stores all assigments made in the order they were made. vec trail_lim; // Separator indices for different decision levels in 'trail'. diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C index 124849155..a2e46e2e4 100644 --- a/src/prop/minisat/simp/SimpSolver.C +++ b/src/prop/minisat/simp/SimpSolver.C @@ -58,8 +58,8 @@ SimpSolver::~SimpSolver() } -Var SimpSolver::newVar(bool sign, bool dvar) { - Var v = Solver::newVar(sign, dvar); +Var SimpSolver::newVar(bool sign, bool dvar, bool theoryAtom) { + Var v = Solver::newVar(sign, dvar,theoryAtom); if (use_simplification){ n_occ .push(0); diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 67d0d2b95..38d51206d 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -44,7 +44,7 @@ class SimpSolver : public Solver { // Problem specification: // - Var newVar (bool polarity = true, bool dvar = true); + Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); bool addClause (vec& ps); // Variable mode: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 32be206b0..96154063d 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -12,8 +12,8 @@ ** **/ +#include "sat.h" #include "prop/prop_engine.h" -#include "prop/cnf_stream.h" #include "theory/theory_engine.h" #include "util/decision_engine.h" @@ -42,6 +42,7 @@ PropEngine::PropEngine(const Options* opts, DecisionEngine* de, Debug("prop") << "Constructing the PropEngine" << endl; d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options); d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver); + d_satSolver->setCnfStream(d_cnfStream); } PropEngine::~PropEngine() { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 0c3916162..2ddbd24fc 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -25,12 +25,12 @@ #include "util/options.h" #include "util/decision_engine.h" #include "theory/theory_engine.h" -#include "prop/sat.h" namespace CVC4 { namespace prop { class CnfStream; +class SatSolver; /** * PropEngine is the abstraction of a Sat Solver, providing methods for diff --git a/src/prop/sat.h b/src/prop/sat.h index 2468990f2..fb8930910 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -13,13 +13,11 @@ ** SAT Solver. **/ -#include "cvc4_private.h" -#include "context/context.h" -#include "theory/theory_engine.h" - #ifndef __CVC4__PROP__SAT_H #define __CVC4__PROP__SAT_H +#include "cvc4_private.h" + #define __CVC4_USE_MINISAT #ifdef __CVC4_USE_MINISAT @@ -36,6 +34,7 @@ class TheoryEngine; namespace prop { class PropEngine; +class CnfStream; /** Type of the SAT variables */ typedef minisat::Var SatVariable; @@ -46,6 +45,67 @@ typedef minisat::Lit SatLiteral; /** Type of the SAT clauses */ typedef minisat::vec SatClause; +/** + * 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 { + + /** The prop engine we are using */ + PropEngine* d_propEngine; + + /** The CNF engine we are using */ + CnfStream* d_cnfStream; + + /** The theory engine we are using */ + TheoryEngine* d_theoryEngine; + + /** Context we will be using to synchronzie the sat solver */ + context::Context* d_context; + + /** Minisat solver */ + minisat::SimpSolver* d_minisat; + + /** Remember the options */ + Options* d_options; + +public: + + /** Hash function for literals */ + struct SatLiteralHashFcn { + inline size_t operator()(const SatLiteral& literal) const; + }; + + inline SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, context::Context* context, + const Options* options); + + inline ~SatSolver(); + + inline bool solve(); + + inline void addClause(SatClause& clause); + + inline SatVariable newVar(bool theoryAtom = false); + + inline void theoryCheck(SatClause& conflict); + + inline void enqueueTheoryLiteral(const SatLiteral& l); + + inline void setCnfStream(CnfStream* cnfStream); +}; + +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ + +#include "context/context.h" +#include "theory/theory_engine.h" +#include "prop/prop_engine.h" +#include "prop/cnf_stream.h" + +namespace CVC4 { +namespace prop { + /** * Returns the variable of the literal. * @param lit the literal @@ -58,13 +118,13 @@ inline bool literalSign(SatLiteral lit) { return minisat::sign(lit); } -inline std::ostream& operator << (std::ostream& out, SatLiteral lit) { +inline std::ostream& operator <<(std::ostream& out, SatLiteral lit) { const char * s = (literalSign(lit)) ? "~" : " "; out << s << literalToVariable(lit); return out; } -inline std::ostream& operator << (std::ostream& out, const SatClause& clause) { +inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) { out << "clause:"; for(int i = 0; i < clause.size(); ++i) { out << " " << clause[i]; @@ -73,66 +133,59 @@ inline std::ostream& operator << (std::ostream& out, const SatClause& clause) { return out; } -/** - * 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 { +size_t SatSolver::SatLiteralHashFcn::operator()(const SatLiteral& literal) const { + return (size_t) minisat::toInt(literal); +} - /** The prop engine we are using */ - PropEngine* d_propEngine; +SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, + context::Context* context, const Options* options) : + d_propEngine(propEngine), + d_cnfStream(NULL), + d_theoryEngine(theoryEngine), + d_context(context) +{ + // Create the solver + d_minisat = new minisat::SimpSolver(this, d_context); + // Setup the verbosity + d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1; + // Do not delete the satisfied clauses, just the learnt ones + d_minisat->remove_satisfied = false; + // Make minisat reuse the literal values + d_minisat->polarity_mode = minisat::SimpSolver::polarity_user; +} - /** The theory engine we are using */ - TheoryEngine* d_theoryEngine; +SatSolver::~SatSolver() { + delete d_minisat; +} - /** Context we will be using to synchronzie the sat solver */ - context::Context* d_context; +bool SatSolver::solve() { + return d_minisat->solve(); +} - /** Minisat solver */ - minisat::SimpSolver* d_minisat; +void SatSolver::addClause(SatClause& clause) { + d_minisat->addClause(clause); +} - /** Remember the options */ - Options* d_options; +SatVariable SatSolver::newVar(bool theoryAtom) { + return d_minisat->newVar(true, true, theoryAtom); +} - public: - - SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, - context::Context* context, const Options* options) - : d_propEngine(propEngine), - d_theoryEngine(theoryEngine), - d_context(context) - { - // Create the solver - d_minisat = new minisat::SimpSolver(this, d_context); - // Setup the verbosity - d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1; - // Do not delete the satisfied clauses, just the learnt ones - d_minisat->remove_satisfied = false; - // Make minisat reuse the literal values - d_minisat->polarity_mode = minisat::SimpSolver::polarity_user; - } - - ~SatSolver() { - delete d_minisat; - } - - inline bool solve() { - return d_minisat->solve(); - } - - inline void addClause(SatClause& clause) { - d_minisat->addClause(clause); - } - - inline SatVariable newVar() { - return d_minisat->newVar(); - } - - inline void theoryCheck(SatClause& conflict) { - } -}; +void SatSolver::theoryCheck(SatClause& conflict) { + d_theoryEngine->check(theory::Theory::STANDARD); +} +void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) { + Node literalNode = d_cnfStream->getNode(l); + // We can get null from the prop engine if the literal is useless (i.e.) + // the expression is not in context anyomore + if(!literalNode.isNull()) { + d_theoryEngine->assertFact(literalNode); + } +} + +void SatSolver::setCnfStream(CnfStream* cnfStream) { + d_cnfStream = cnfStream; +} }/* CVC4::prop namespace */ @@ -140,5 +193,4 @@ class SatSolver { #endif - #endif /* __CVC4__PROP__SAT_H */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 076ea4d2d..5453aab93 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -60,7 +60,8 @@ class TheoryEngine { d_engine = &engine; } - void conflict(TNode, bool) throw(theory::Interrupted) { + void conflict(TNode conflictNode, bool) throw(theory::Interrupted) { + Debug("theory") << "conflict(" << conflictNode << ")" << std::endl; } void propagate(TNode, bool) throw(theory::Interrupted) { @@ -107,8 +108,22 @@ public: * @returns the theory, or NULL if the TNode is * of built-in type. */ - theory::Theory* theoryOf(TNode n) { - return theoryOfTable[n]; + theory::Theory* theoryOf(const TNode& node) { + return theoryOfTable[node]; + } + + /** + * Assert the formula to the apropriate theory. + * @param node the assertion + */ + inline void assertFact(const TNode& node) { + Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; + theory::Theory* theory = theoryOf(node); + if (theory != NULL) theory->assertFact(node); + } + + inline void check(theory::Theory::Effort effort) { + d_uf.check(effort); } };/* class TheoryEngine */