From 1ea434616c48b92189e77b37b3e82dbbee0e0ccc Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Tue, 30 Aug 2011 02:19:58 +0000 Subject: [PATCH] Fixin the SAT solver for Andy. Even if a SAT lemma is added, a FULL-CHECK will be reissued. Some unexpected slowdowns, but not too much. --- src/prop/minisat/core/Solver.cc | 5 +++++ src/prop/minisat/core/Solver.h | 3 +++ 2 files changed, 8 insertions(+) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index a5774ee7b..7ca117c2e 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -579,6 +579,7 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) CRef Solver::propagate(TheoryCheckType type) { CRef confl = CRef_Undef; + recheck = false; ScopedBool scoped_bool(minisat_busy, true); @@ -597,6 +598,7 @@ CRef Solver::propagate(TheoryCheckType type) theoryCheck(CVC4::theory::Theory::FULL_EFFORT); // If there are lemmas (or conflicts) update them if (lemmas.size() > 0) { + recheck = true; return updateLemmas(); } } @@ -914,6 +916,9 @@ lbool Solver::search(int nof_conflicts) if (!order_heap.empty() || qhead < trail.size()) { check_type = CHECK_WITH_PROPAGATION_STANDARD; continue; + } else if (recheck) { + // There some additional stuff added, so we go for another full-check + continue; } else { // Yes, we're truly satisfiable return l_True; diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 8eb82d9f1..1141e53c4 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -71,6 +71,9 @@ protected: /** Is the lemma removable */ vec lemmas_removable; + /** Do a another check if FULL_EFFORT was the last one */ + bool recheck; + /** Shrink 'cs' to contain only clauses below given level */ void removeClausesAboveLevel(vec& cs, int level); -- 2.30.2