diff options
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/Makefile.am | 2 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.C | 56 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 28 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.C | 5 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.h | 5 |
5 files changed, 75 insertions, 21 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 <cmath> //================================================================================================= @@ -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 <cstdio> #include <cassert> @@ -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<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack) void analyzeFinal (Lit p, vec<Lit>& 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: |