diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-13 05:30:30 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-13 05:30:30 +0000 |
commit | 8394cecaf2b1a261b44af54501ef1a433cdbadc2 (patch) | |
tree | d4af6dec9e07b2406a84785eea73a1480c91580f | |
parent | 7730b9562b11d13236ce566f15ede0cb3416fe21 (diff) |
Minor refactorings to PropEngine, SatSolver
-rw-r--r-- | .cproject | 2 | ||||
-rw-r--r-- | src/parser/bounded_token_buffer.cpp | 2 | ||||
-rw-r--r-- | src/prop/Makefile.am | 1 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 3 | ||||
-rw-r--r-- | src/prop/sat.cpp | 43 | ||||
-rw-r--r-- | src/prop/sat.h | 162 |
6 files changed, 122 insertions, 91 deletions
@@ -44,7 +44,7 @@ </toolChain> </folderInfo> <sourceEntries> -<entry excluding="parser|smt2" flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="sourcePath" name=""/> +<entry excluding="prop|parser|smt2" flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="sourcePath" name=""/> </sourceEntries> </configuration> </storageModule> 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; @@ -46,6 +55,25 @@ typedef minisat::Lit SatLiteral; typedef minisat::vec<SatLiteral> 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 * care. @@ -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 */ |