diff options
Diffstat (limited to 'src/prop/minisat')
-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 |
5 files changed, 44 insertions, 3 deletions
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); + } + } } |