diff options
Diffstat (limited to 'src/prop/bvminisat')
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 2 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 8 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 10 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 9 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 16 |
5 files changed, 41 insertions, 4 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 124fc35f1..4868db6f5 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -73,7 +73,7 @@ SatValue BVMinisatSatSolver::assertAssumption(SatLiteral lit, bool propagate) { return toSatLiteralValue(d_minisat->assertAssumption(toMinisatLit(lit), propagate)); } -void BVMinisatSatSolver::notify() { +void BVMinisatSatSolver::contextNotifyPop() { while (d_assertionsCount > d_assertionsRealCount) { popAssumption(); d_assertionsCount --; diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index cd2a2c6b9..60cdd1c28 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -54,6 +54,10 @@ private: context::CDO<unsigned> d_assertionsRealCount; context::CDO<unsigned> d_lastPropagation; +protected: + + void contextNotifyPop(); + public: BVMinisatSatSolver() : @@ -70,10 +74,12 @@ public: SatVariable newVar(bool theoryAtom = false); + SatVariable trueVar() { return d_minisat->trueVar(); } + SatVariable falseVar() { return d_minisat->falseVar(); } + void markUnremovable(SatLiteral lit); void interrupt(); - void notify(); SatValue solve(); SatValue solve(long unsigned int&); diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index e24fcac1a..c96b6e4b2 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -119,7 +119,15 @@ Solver::Solver(CVC4::context::Context* c) : , propagation_budget (-1) , asynch_interrupt (false) , clause_added(false) -{} +{ + // Create the constant variables + varTrue = newVar(true, false); + varFalse = newVar(false, false); + + // Assert the constants + uncheckedEnqueue(mkLit(varTrue, false)); + uncheckedEnqueue(mkLit(varFalse, true)); +} Solver::~Solver() diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index c323bfe2b..ae5efd81e 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -64,6 +64,12 @@ class Solver { /** Cvc4 context */ CVC4::context::Context* c; + /** True constant */ + Var varTrue; + + /** False constant */ + Var varFalse; + public: // Constructor/Destructor: @@ -76,6 +82,9 @@ public: // Problem specification: // Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. + Var trueVar() const { return varTrue; } + Var falseVar() const { return varFalse; } + bool addClause (const vec<Lit>& ps); // Add a clause to the solver. bool addEmptyClause(); // Add the empty clause, making the solver contradictory. diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index c8ce13410..59820e9e3 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -63,11 +63,25 @@ SimpSolver::SimpSolver(CVC4::context::Context* c) : , bwdsub_assigns (0) , n_touched (0) { - CVC4::StatisticsRegistry::registerStat(&total_eliminate_time); + CVC4::StatisticsRegistry::registerStat(&total_eliminate_time); vec<Lit> dummy(1,lit_Undef); ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below. bwdsub_tmpunit = ca.alloc(dummy); remove_satisfied = false; + + // add the initialization for all the internal variables + for (int i = frozen.size(); i < vardata.size(); ++ i) { + frozen .push(1); + eliminated.push(0); + if (use_simplification){ + n_occ .push(0); + n_occ .push(0); + occurs .init(i); + touched .push(0); + elim_heap .insert(i); + } + } + } |