From 8394cecaf2b1a261b44af54501ef1a433cdbadc2 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Thu, 13 May 2010 05:30:30 +0000 Subject: [PATCH] Minor refactorings to PropEngine, SatSolver --- .cproject | 2 +- src/parser/bounded_token_buffer.cpp | 2 +- src/prop/Makefile.am | 1 + src/prop/prop_engine.cpp | 3 +- src/prop/sat.cpp | 43 ++++++++ src/prop/sat.h | 162 +++++++++++++--------------- 6 files changed, 122 insertions(+), 91 deletions(-) create mode 100644 src/prop/sat.cpp diff --git a/.cproject b/.cproject index 488d7e4d4..df8183d4e 100644 --- a/.cproject +++ b/.cproject @@ -44,7 +44,7 @@ - + diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index 8bd896cd4..53b56dcdd 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -10,7 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** An ANTLR3 bounded token stream implementation. + ** An ANTLR3 bounded token stream implementation. ** This code is largely based on the original token buffer implementation ** in libantlr3c, by Jim Idle. **/ diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 357818b32..2856cc065 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -9,6 +9,7 @@ libprop_la_SOURCES = \ prop_engine.cpp \ prop_engine.h \ sat.h \ + sat.cpp \ cnf_stream.h \ cnf_stream.cpp \ cnf_conversion.h diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index ef28a4ac6..6b28e6f99 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -12,8 +12,9 @@ ** **/ +#include "cnf_stream.h" +#include "prop_engine.h" #include "sat.h" -#include "prop/prop_engine.h" #include "theory/theory_engine.h" #include "util/decision_engine.h" diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp new file mode 100644 index 000000000..c578cf361 --- /dev/null +++ b/src/prop/sat.cpp @@ -0,0 +1,43 @@ +#include "cnf_stream.h" +#include "prop_engine.h" +#include "sat.h" +#include "context/context.h" +#include "theory/theory_engine.h" + +namespace CVC4 { +namespace prop { + +void SatSolver::theoryCheck(SatClause& conflict) { + // Try theory propagation + if (!d_theoryEngine->check(theory::Theory::FULL_EFFORT)) { + // We have a conflict, get it + Node conflictNode = d_theoryEngine->getConflict(); + Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl; + // Go through the literals and construct the conflict clause + Node::const_iterator literal_it = conflictNode.begin(); + Node::const_iterator literal_end = conflictNode.end(); + while (literal_it != literal_end) { + // Get the literal corresponding to the node + SatLiteral l = d_cnfStream->getLiteral(*literal_it); + // Add the negation to the conflict clause and continue + conflict.push(~l); + literal_it ++; + } + } +} + +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 */ +}/* CVC4 namespace */ diff --git a/src/prop/sat.h b/src/prop/sat.h index 12aa82793..d5adedd20 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -18,15 +18,20 @@ #ifndef __CVC4__PROP__SAT_H #define __CVC4__PROP__SAT_H +// Just defining this for now, since there's no other SAT solver bindings. +// Optional blocks below will be unconditionally included #define __CVC4_USE_MINISAT +#include "util/options.h" + #ifdef __CVC4_USE_MINISAT -#include "util/options.h" #include "prop/minisat/core/Solver.h" #include "prop/minisat/core/SolverTypes.h" #include "prop/minisat/simp/SimpSolver.h" +#endif /* __CVC4_USE_MINISAT */ + namespace CVC4 { class TheoryEngine; @@ -36,6 +41,10 @@ namespace prop { class PropEngine; 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; @@ -45,6 +54,25 @@ typedef minisat::Lit SatLiteral; /** Type of the SAT clauses */ typedef minisat::vec SatClause; +/** + * Returns the variable of the literal. + * @param lit the literal + */ +inline SatVariable literalToVariable(SatLiteral lit) { + return minisat::var(lit); +} + +inline bool literalSign(SatLiteral lit) { + return minisat::sign(lit); +} + +static inline size_t +hashSatLiteral(const SatLiteral& literal) { + return (size_t) minisat::toInt(literal); +} + +#endif /* __CVC4_USE_MINISAT */ + /** * 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 @@ -64,83 +92,53 @@ class SatSolver { /** Context we will be using to synchronzie the sat solver */ context::Context* d_context; + /** Remember the options */ + Options* d_options; + + /* 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; - /** Remember the options */ - Options* d_options; +#endif /* __CVC4_USE_MINISAT */ -public: +protected: +public: /** Hash function for literals */ struct SatLiteralHashFunction { inline size_t operator()(const SatLiteral& literal) const; }; - inline SatSolver(PropEngine* propEngine, + SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, context::Context* context, const Options* options); - inline ~SatSolver(); - - inline bool solve(); - - inline void addClause(SatClause& clause); + ~SatSolver(); - inline SatVariable newVar(bool theoryAtom = false); + bool solve(); + + void addClause(SatClause& clause); - inline void theoryCheck(SatClause& conflict); + SatVariable newVar(bool theoryAtom = false); - inline void enqueueTheoryLiteral(const SatLiteral& l); + void theoryCheck(SatClause& conflict); - inline void setCnfStream(CnfStream* cnfStream); + void enqueueTheoryLiteral(const SatLiteral& l); + + 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 { +/* Functions that delegate to the concrete SAT solver. */ -/** - * Returns the variable of the literal. - * @param lit the literal - */ -inline SatVariable literalToVariable(SatLiteral lit) { - return minisat::var(lit); -} - -inline bool literalSign(SatLiteral lit) { - return minisat::sign(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) { - out << "clause:"; - for(int i = 0; i < clause.size(); ++i) { - out << " " << clause[i]; - } - out << ";"; - return out; -} - -inline size_t -SatSolver::SatLiteralHashFunction::operator()(const SatLiteral& literal) const { - return (size_t) minisat::toInt(literal); -} +#ifdef __CVC4_USE_MINISAT -SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, +inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, context::Context* context, const Options* options) : d_propEngine(propEngine), d_cnfStream(NULL), @@ -157,57 +155,45 @@ SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, d_minisat->polarity_mode = minisat::SimpSolver::polarity_user; } -SatSolver::~SatSolver() { +inline SatSolver::~SatSolver() { delete d_minisat; } -bool SatSolver::solve() { +inline bool SatSolver::solve() { return d_minisat->solve(); } -void SatSolver::addClause(SatClause& clause) { +inline void SatSolver::addClause(SatClause& clause) { d_minisat->addClause(clause); } -SatVariable SatSolver::newVar(bool theoryAtom) { +inline SatVariable SatSolver::newVar(bool theoryAtom) { return d_minisat->newVar(true, true, theoryAtom); } -void SatSolver::theoryCheck(SatClause& conflict) { - // Try theory propagation - if (!d_theoryEngine->check(theory::Theory::FULL_EFFORT)) { - // We have a conflict, get it - Node conflictNode = d_theoryEngine->getConflict(); - Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl; - // Go through the literals and construct the conflict clause - Node::const_iterator literal_it = conflictNode.begin(); - Node::const_iterator literal_end = conflictNode.end(); - while (literal_it != literal_end) { - // Get the literal corresponding to the node - SatLiteral l = d_cnfStream->getLiteral(*literal_it); - // Add the negation to the conflict clause and continue - conflict.push(~l); - literal_it ++; - } - } +#endif /* __CVC4_USE_MINISAT */ + +inline size_t +SatSolver::SatLiteralHashFunction::operator()(const SatLiteral& literal) const { + return hashSatLiteral(literal); } -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); - } +inline std::ostream& operator <<(std::ostream& out, SatLiteral lit) { + const char * s = (literalSign(lit)) ? "~" : " "; + out << s << literalToVariable(lit); + return out; } -void SatSolver::setCnfStream(CnfStream* cnfStream) { - d_cnfStream = cnfStream; +inline std::ostream& operator <<(std::ostream& out, const SatClause& clause) { + out << "clause:"; + for(int i = 0; i < clause.size(); ++i) { + out << " " << clause[i]; + } + out << ";"; + return out; } }/* CVC4::prop namespace */ }/* CVC4 namespace */ -#endif - #endif /* __CVC4__PROP__SAT_H */ -- 2.30.2