From 5efc0cd28524a45b8fb25c4b1c0f8c42830fc3ef Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Wed, 3 Mar 2010 23:39:43 +0000 Subject: [PATCH] Some SAT stuff, not doing anything special yet, just to keep it in sync. --- src/prop/minisat/Makefile.am | 2 +- src/prop/minisat/core/Solver.C | 56 +++++++++++++++++++++---- src/prop/minisat/core/Solver.h | 28 ++++++++----- src/prop/minisat/simp/SimpSolver.C | 5 ++- src/prop/minisat/simp/SimpSolver.h | 5 ++- src/prop/prop_engine.cpp | 9 ++-- src/prop/prop_engine.h | 6 ++- src/prop/sat.h | 66 +++++++++++++++++++++++------- src/smt/smt_engine.cpp | 2 +- 9 files changed, 136 insertions(+), 43 deletions(-) diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am index 9cde8ae2d..366cc34c8 100644 --- a/src/prop/minisat/Makefile.am +++ b/src/prop/minisat/Makefile.am @@ -1,6 +1,6 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ - -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include + -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../.. -I@srcdir@/../../include AM_CXXFLAGS = -Wall -fvisibility=hidden -DNDEBUG noinst_LTLIBRARIES = libminisat.la diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C index e99870654..771d79f62 100644 --- a/src/prop/minisat/core/Solver.C +++ b/src/prop/minisat/core/Solver.C @@ -19,6 +19,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Solver.h" #include "Sort.h" +#include "prop/sat.h" #include //================================================================================================= @@ -28,10 +29,14 @@ namespace CVC4 { namespace prop { namespace minisat { -Solver::Solver() : +Solver::Solver(SatSolver* proxy, context::Context* context) : + + // SMT stuff + proxy(proxy) + , context(context) // Parameters: (formerly in 'SearchParams') - var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02) + , var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02) , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1.1) // More parameters: @@ -159,14 +164,20 @@ bool Solver::satisfied(const Clause& c) const { // void Solver::cancelUntil(int level) { if (decisionLevel() > level){ - for (int c = trail.size()-1; c >= trail_lim[level]; c--){ + // Pop the SMT context + for (int l = trail_lim.size() - level; l > 0; --l) + context->pop(); + // Now the minisat stuff + for (int c = trail.size()-1; c >= trail_lim[level]; c--) { Var x = var(trail[c]); assigns[x] = toInt(l_Undef); - insertVarOrder(x); } + insertVarOrder(x); + } qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); trail_lim.shrink(trail_lim.size() - level); - } } + } +} //================================================================================================= @@ -390,9 +401,40 @@ void Solver::uncheckedEnqueue(Lit p, Clause* from) } +Clause* Solver::propagate() +{ + Clause* confl = NULL; + + while(qhead < trail.size()) { + confl = propagateBool(); + if (confl != NULL) break; + confl = propagateTheory(); + if (confl != NULL) break; + } + + return confl; +} + /*_________________________________________________________________________________________________ | -| propagate : [void] -> [Clause*] +| propagateTheory : [void] -> [Clause*] +| +| Description: +| Propagates all enqueued theory facts. If a conflict arises, the conflicting clause is returned, +| otherwise NULL. +| +| Note: the propagation queue might be NOT empty +|________________________________________________________________________________________________@*/ +Clause* Solver::propagateTheory() +{ + SatClause clause; + proxy->theoryCheck(clause); + return NULL; +} + +/*_________________________________________________________________________________________________ +| +| propagateBool : [void] -> [Clause*] | | Description: | Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, @@ -401,7 +443,7 @@ void Solver::uncheckedEnqueue(Lit p, Clause* from) | Post-conditions: | * the propagation queue is empty, even if there was a conflict. |________________________________________________________________________________________________@*/ -Clause* Solver::propagate() +Clause* Solver::propagateBool() { Clause* confl = NULL; int num_props = 0; diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 44499246e..c593d8b2c 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -17,11 +17,12 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#include "cvc4_private.h" - #ifndef __CVC4__PROP__MINISAT__SOLVER_H #define __CVC4__PROP__MINISAT__SOLVER_H +#include "cvc4_private.h" +#include "context/context.h" + #include #include @@ -32,27 +33,34 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "SolverTypes.h" - //================================================================================================= // Solver -- the main class: namespace CVC4 { namespace prop { -class SatSolverProxy; +class SatSolver; namespace minisat { class Solver { /** The only CVC4 entry point to the private solver data */ - friend class CVC4::prop::SatSolverProxy; + friend class CVC4::prop::SatSolver; + +protected: + + /** The pointer to the proxy that provides interfaces to the SMT engine */ + SatSolver* proxy; + + /** The context from the SMT solver */ + context::Context* context; public: // Constructor/Destructor: // - Solver(); + Solver(SatSolver* proxy, context::Context* context); CVC4_PUBLIC ~Solver(); // Problem specification: @@ -165,7 +173,9 @@ protected: void newDecisionLevel (); // Begins a new decision level. void uncheckedEnqueue (Lit p, Clause* from = NULL); // Enqueue a literal. Assumes value of literal is undefined. bool enqueue (Lit p, Clause* from = NULL); // Test if fact 'p' contradicts current state, enqueue otherwise. - Clause* propagate (); // Perform unit propagation. Returns possibly conflicting clause. + Clause* propagate (); // Perform Boolean and Theory. Returns possibly conflicting clause. + Clause* propagateBool (); // Perform Boolean propagation. Returns possibly conflicting clause. + Clause* propagateTheory (); // Perform Theory propagation. Returns possibly conflicting clause. void cancelUntil (int level); // Backtrack until a certain level. void analyze (Clause* confl, vec& out_learnt, int& out_btlevel); // (bt = backtrack) void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? @@ -217,11 +227,9 @@ protected: return (int)(drand(seed) * size); } }; - //================================================================================================= // Implementation of inline methods: - inline void Solver::insertVarOrder(Var x) { if (!order_heap.inHeap(x) && decision_var[x]) order_heap.insert(x); } @@ -247,7 +255,7 @@ inline void Solver::claBumpActivity (Clause& c) { inline bool Solver::enqueue (Lit p, Clause* from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); } inline bool Solver::locked (const Clause& c) const { return reason[var(c[0])] == &c && value(c[0]) == l_True; } -inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } +inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); context->push(); } inline int Solver::decisionLevel () const { return trail_lim.size(); } inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level[x] & 31); } diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C index 063332e74..124849155 100644 --- a/src/prop/minisat/simp/SimpSolver.C +++ b/src/prop/minisat/simp/SimpSolver.C @@ -28,8 +28,9 @@ namespace CVC4 { namespace prop { namespace minisat { -SimpSolver::SimpSolver() : - grow (0) +SimpSolver::SimpSolver(SatSolver* proxy, context::Context* context) : + Solver(proxy, context) + , grow (0) , asymm_mode (false) , redundancy_check (false) , merges (0) diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 223b21998..67d0d2b95 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -30,13 +30,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA namespace CVC4 { namespace prop { + +class SatSolver; + namespace minisat { class SimpSolver : public Solver { public: // Constructor/Destructor: // - SimpSolver(); + SimpSolver(SatSolver* proxy, context::Context* context); CVC4_PUBLIC ~SimpSolver(); // Problem specification: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 76be5d6d8..32be206b0 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -26,20 +26,21 @@ #include using namespace std; +using namespace CVC4::context; namespace CVC4 { namespace prop { PropEngine::PropEngine(const Options* opts, DecisionEngine* de, - TheoryEngine* te) + TheoryEngine* te, Context* context) : d_inCheckSat(false), d_options(opts), d_decisionEngine(de), - d_theoryEngine(te) + d_theoryEngine(te), + d_context(context) { Debug("prop") << "Constructing the PropEngine" << endl; - d_satSolver = new SatSolver(); - SatSolverProxy::initSatSolver(d_satSolver, d_options); + d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options); d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver); } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index f57161fde..0c3916162 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -53,7 +53,9 @@ class PropEngine { /** The theory engine we will be using */ TheoryEngine *d_theoryEngine; - /** The SAT solver*/ + context::Context* d_context; + + /** The SAT solver proxy */ SatSolver* d_satSolver; /** List of all of the assertions that need to be made */ @@ -67,7 +69,7 @@ public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(const Options*, DecisionEngine*, TheoryEngine*); + PropEngine(const Options*, DecisionEngine*, TheoryEngine*, context::Context*); /** * Destructor. diff --git a/src/prop/sat.h b/src/prop/sat.h index 65752f20b..1cd5d0bfe 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -14,6 +14,8 @@ **/ #include "cvc4_private.h" +#include "context/context.h" +#include "theory/theory_engine.h" #ifndef __CVC4__PROP__SAT_H #define __CVC4__PROP__SAT_H @@ -28,10 +30,12 @@ #include "prop/minisat/simp/SimpSolver.h" namespace CVC4 { + +class TheoryEngine; + namespace prop { -/** The solver we are using */ -typedef minisat::SimpSolver SatSolver; +class PropEngine; /** Type of the SAT variables */ typedef minisat::Var SatVariable; @@ -74,24 +78,56 @@ inline std::ostream& operator << (std::ostream& out, const SatClause& clause) { * It's only accessible from the PropEngine, and should be treated with major * care. */ -class SatSolverProxy { +class SatSolver { + + /** The prop engine we are using */ + PropEngine* d_propEngine; + + /** The theory engine we are using */ + TheoryEngine* d_theoryEngine; - /** Only the prop engine can modify the internals of the SAT solver */ - friend class PropEngine; + /** Context we will be using to synchronzie the sat solver */ + context::Context* d_context; - private: + /** Minisat solver */ + minisat::SimpSolver* d_minisat; - /** - * Initializes the given sat solver with the given options. - * @param satSolver the SAT solver - * @param options the options - */ - inline static void initSatSolver(SatSolver* satSolver, - const Options* options) { + /** Remember the options */ + Options* d_options; + + 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 - satSolver->verbosity = (options->verbosity > 0) ? 1 : -1; + d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1; // Do not delete the satisfied clauses, just the learnt ones - satSolver->remove_satisfied = false; + d_minisat->remove_satisfied = false; + } + + ~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) { } }; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ae676e48d..c45314a55 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -33,7 +33,7 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : NodeManagerScope nms(d_nodeManager); d_decisionEngine = new DecisionEngine; d_theoryEngine = new TheoryEngine(this, d_ctxt); - d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine); + d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine, d_ctxt); } SmtEngine::~SmtEngine() { -- 2.30.2