diff options
Diffstat (limited to 'src/prop')
-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 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 10 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 22 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 9 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 1 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 13 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 6 |
12 files changed, 100 insertions, 8 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); + } + } + } diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 3a4fa781a..d18ec6e69 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -175,7 +175,15 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { SatLiteral lit; if (!hasLiteral(node)) { // If no literal, we'll make one - lit = SatLiteral(d_satSolver->newVar(theoryLiteral)); + if (node.getKind() == kind::CONST_BOOLEAN) { + if (node.getConst<bool>()) { + lit = SatLiteral(d_satSolver->trueVar()); + } else { + lit = SatLiteral(d_satSolver->falseVar()); + } + } else { + lit = SatLiteral(d_satSolver->newVar(theoryLiteral)); + } d_translationCache[node].literal = lit; d_translationCache[node.notNode()].literal = ~lit; } else { diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 5e1b032a3..6ee508eba 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -126,6 +126,14 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, , asynch_interrupt (false) { PROOF(ProofManager::initSatProof(this);) + + // Create the constant variables + varTrue = newVar(true, false, false); + varFalse = newVar(false, false, false); + + // Assert the constants + uncheckedEnqueue(mkLit(varTrue, false)); + uncheckedEnqueue(mkLit(varFalse, true)); } @@ -190,16 +198,26 @@ CRef Solver::reason(Var x) { // Compute the assertion level for this clause int explLevel = 0; - for (int i = 0; i < explanation.size(); ++ i) { + int i, j; + for (i = 0, j = 0; i < explanation.size(); ++ i) { int varLevel = intro_level(var(explanation[i])); if (varLevel > explLevel) { explLevel = varLevel; } Assert(value(explanation[i]) != l_Undef); Assert(i == 0 || trail_index(var(explanation[0])) > trail_index(var(explanation[i]))); + // ignore zero level literals + if (i == 0 || level(var(explanation[i])) > 0) { + explanation[j++] = explanation[i]; + } + } + explanation.shrink(i - j); + if (j == 1) { + // Add not TRUE to the clause + explanation.push(mkLit(varTrue, true)); } - // Construct the reason (level 0) + // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); vardata[x] = mkVarData(real_reason, level(x), intro_level(x), trail_index(x)); clauses_removable.push(real_reason); diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index cfeb06211..e677d7220 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -65,6 +65,13 @@ protected: /** The current assertion level (user) */ int assertionLevel; + + /** Variable representing true */ + Var varTrue; + + /** Variable representing false */ + Var varFalse; + public: /** Returns the current user assertion level */ int getAssertionLevel() const { return assertionLevel; } @@ -108,6 +115,8 @@ public: // Problem specification: // Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode. + Var trueVar() const { return varTrue; } + Var falseVar() const { return varFalse; } // Less than for literals in a lemma struct lemma_lt { diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index bed30d658..4f2a16670 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -121,7 +121,6 @@ SatVariable MinisatSatSolver::newVar(bool theoryAtom) { return d_minisat->newVar(true, true, theoryAtom); } - SatValue MinisatSatSolver::solve(unsigned long& resource) { Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; if(resource == 0) { diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 9cf75a12e..19ade8ffa 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -56,6 +56,8 @@ public: void addClause(SatClause& clause, bool removable); SatVariable newVar(bool theoryAtom = false); + SatVariable trueVar() { return d_minisat->trueVar(); } + SatVariable falseVar() { return d_minisat->falseVar(); } SatValue solve(); SatValue solve(long unsigned int&); diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 2cacfbcc0..8da3856ff 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -67,6 +67,19 @@ SimpSolver::SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* c ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below. bwdsub_tmpunit = ca.alloc(0, 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); + } + } } diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 898709c43..2865f2cb5 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -46,6 +46,12 @@ public: /** Create a new boolean variable in the solver. */ virtual SatVariable newVar(bool theoryAtom = false) = 0; + /** Create a new (or return an existing) boolean variable representing the constant true */ + virtual SatVariable trueVar() = 0; + + /** Create a new (or return an existing) boolean variable representing the constant false */ + virtual SatVariable falseVar() = 0; + /** Check the satisfiability of the added clauses */ virtual SatValue solve() = 0; |