diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-08 21:08:40 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-08 21:08:40 +0000 |
commit | b1d9707979074abb8fed7ad4e8a2b15648c69324 (patch) | |
tree | 236c83135c62a7499d1039fff94037950e05061e /src/prop/sat.h | |
parent | 7b19de6b01d9a896560c39c9ef4a3731cf29b19d (diff) |
some more sat stuff for tim: assertions now go to theory_uf
Diffstat (limited to 'src/prop/sat.h')
-rw-r--r-- | src/prop/sat.h | 172 |
1 files changed, 112 insertions, 60 deletions
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; @@ -47,6 +46,67 @@ typedef minisat::Lit SatLiteral; typedef minisat::vec<SatLiteral> 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 */ |