diff options
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 62 | ||||
| -rw-r--r-- | src/prop/minisat/core/Solver.h | 4 | ||||
| -rw-r--r-- | src/prop/prop_engine.cpp | 11 | ||||
| -rw-r--r-- | src/prop/prop_engine.h | 1 | ||||
| -rw-r--r-- | src/theory/theory_engine.h | 2 |
5 files changed, 39 insertions, 41 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index a24772581..4817ec1f5 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -56,7 +56,7 @@ Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bo , assertionLevel(0) , enable_incremental(enable_incremental) , problem_extended(false) - , in_propagate(false) + , in_solve(false) // Parameters (user settable): // , verbosity (0) @@ -135,7 +135,7 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) theory .push(theoryAtom); // We have extended the problem - if (in_propagate) { + if (in_solve) { problem_extended = true; insertVarOrder(v); } @@ -256,7 +256,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type) } } - if (in_propagate && type == CLAUSE_LEMMA) { + if (type == CLAUSE_LEMMA) { problem_extended = true; } @@ -620,15 +620,12 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) CRef Solver::propagate(TheoryCheckType type) { - in_propagate = true; - CRef confl = CRef_Undef; // If this is the final check, no need for Boolean propagation and // theory propagation if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) { confl = theoryCheck(CVC4::theory::Theory::FULL_EFFORT); - in_propagate = false; return confl; } @@ -655,8 +652,6 @@ CRef Solver::propagate(TheoryCheckType type) } } while (new_assertions); - in_propagate = false; - return confl; } @@ -916,7 +911,26 @@ lbool Solver::search(int nof_conflicts) TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD; for (;;){ - problem_extended = false; + + // If we have more assertions from lemmas, we continue + if (problem_extended) { + + Debug("minisat::lemmas") << "Problem extended with lemmas, adding propagations." << endl; + + for (int i = 0, i_end = lemma_propagated_literals.size(); i < i_end; ++ i) { + if (value(var(lemma_propagated_literals[i])) == l_Undef) { + Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << endl; + uncheckedEnqueue(lemma_propagated_literals[i], lemma_propagated_reasons[i]); + } + } + + lemma_propagated_literals.clear(); + lemma_propagated_reasons.clear(); + + check_type = CHECK_WITH_PROPAGATION_STANDARD; + problem_extended = false; + } + CRef confl = propagate(check_type); if (confl != CRef_Undef){ // CONFLICT @@ -959,27 +973,10 @@ lbool Solver::search(int nof_conflicts) // We have a conflict so, we are going back to standard checks check_type = CHECK_WITH_PROPAGATION_STANDARD; }else{ - // NO CONFLICT - - // If we have more assertions from lemmas, we continue - if (problem_extended) { - - Debug("minisat::lemmas") << "Problem extended with lemmas, adding propagations." << endl; - - for (int i = 0, i_end = lemma_propagated_literals.size(); i < i_end; ++ i) { - if (value(var(lemma_propagated_literals[i])) == l_Undef) { - Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << endl; - uncheckedEnqueue(lemma_propagated_literals[i], lemma_propagated_reasons[i]); - } - } - - lemma_propagated_literals.clear(); - lemma_propagated_reasons.clear(); - - check_type = CHECK_WITH_PROPAGATION_STANDARD; + // NO CONFLICT + if (problem_extended) continue; - } // If this was a final check, we are satisfiable if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL) @@ -1082,9 +1079,14 @@ lbool Solver::solve_() { Debug("minisat") << "nvars = " << nVars() << endl; + in_solve = true; + model.clear(); conflict.clear(); - if (!ok) return l_False; + if (!ok){ + in_solve = false; + return l_False; + } solves++; @@ -1126,6 +1128,8 @@ lbool Solver::solve_() // Cancel the trail downto previous push popTrail(); + in_solve = false; + return status; } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 7050f2d10..5c0f0f9a3 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -79,8 +79,8 @@ protected: /** Shrink 'cs' to contain only clauses below given level */ void removeClausesAboveLevel(vec<CRef>& cs, int level); - /** True if we are inside the propagate method */ - bool in_propagate; + /** True if we are currently solving. */ + bool in_solve; public: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index f3caead8b..ab1afceba 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -81,19 +81,14 @@ void PropEngine::assertFormula(TNode node) { } void PropEngine::assertLemma(TNode node) { - Assert(d_inCheckSat, "Sat solver should be in solve()!"); + //Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; + + //TODO This comment is now false // Assert as removable d_cnfStream->convertAndAssert(node, true, false); } -void PropEngine::assertSafeLemma(TNode node) { - if(d_inCheckSat){ - assertLemma(node); - }else{ - assertFormula(node); - } -} void PropEngine::printSatisfyingAssignment(){ const CnfStream::TranslationCache& transCache = diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index c0483e943..b43c2d859 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -103,7 +103,6 @@ public: * @param node the formula to assert */ void assertLemma(TNode node); - void assertSafeLemma(TNode node); /** * Checks the current context for satisfiability. diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 813b38d93..7958d977e 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -318,7 +318,7 @@ public: } inline void newLemma(TNode node) { - d_propEngine->assertSafeLemma(preprocess(node)); + d_propEngine->assertLemma(preprocess(node)); } /** |