diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-08 02:33:37 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-08 02:33:37 +0000 |
commit | 752b00bc94385fd4b54becb072fca3814f34fd4c (patch) | |
tree | 5636548d4e874275d6348fd6fd9f03b074e65d33 /src/prop | |
parent | f632dfe4fe36f49361bebbf843992f658bac28ef (diff) |
Removing QUICK_CHECK, and other unused ones, from the Theory::Effort.
Seems to be working better <http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3749&category=&p=5&reference_id=3739>, and should fix the failing cases in the regressions.
Removing one test case from the integer regress0.
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 66 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 12 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 6 |
3 files changed, 35 insertions, 49 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 678fe28dc..9f3285fff 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -248,7 +248,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) Debug("minisat") << "got new unit " << ps[0] << " at assertion level " << assertionLevel << std::endl; trail_user.push(ps[0]); } - return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef); + return ok = (propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef); } else return ok; } else { CRef cr = ca.alloc(assertionLevel, ps, false); @@ -654,8 +654,8 @@ CRef Solver::propagate(TheoryCheckType type) ScopedBool scoped_bool(minisat_busy, true); - // If we are not in the quick mode add the lemmas that were left begind - if (type != CHECK_WITHOUTH_PROPAGATION_QUICK && lemmas.size() > 0) { + // If we are not in the quick mode add the lemmas that were left behind + if (type != CHECK_WITHOUTH_THEORY && lemmas.size() > 0) { confl = updateLemmas(); if (confl != CRef_Undef) { return confl; @@ -664,9 +664,9 @@ CRef Solver::propagate(TheoryCheckType type) // If this is the final check, no need for Boolean propagation and // theory propagation - if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) { + if (type == CHECK_FINAL) { // Do the theory check - theoryCheck(CVC4::theory::Theory::FULL_EFFORT); + theoryCheck(CVC4::theory::Theory::EFFORT_FULL); // If there are lemmas (or conflicts) update them if (lemmas.size() > 0) { recheck = true; @@ -677,38 +677,24 @@ CRef Solver::propagate(TheoryCheckType type) } } - // The effort we will be using to theory check - CVC4::theory::Theory::Effort effort = type == CHECK_WITHOUTH_PROPAGATION_QUICK ? - CVC4::theory::Theory::QUICK_CHECK : - CVC4::theory::Theory::STANDARD; - // Keep running until we have checked everything, we // have no conflict and no new literals have been asserted - do { - do { - // Propagate on the clauses - confl = propagateBool(); - - // If no conflict, do the theory check - if (confl == CRef_Undef) { - // Do the theory check - theoryCheck(effort); - // If there are lemmas (or conflicts) update them - if (lemmas.size() > 0) { - confl = updateLemmas(); - } - } - } while (confl == CRef_Undef && qhead < trail.size()); - - // If still consistent do some theory propagation - if (confl == CRef_Undef && type == CHECK_WITH_PROPAGATION_STANDARD) { - propagateTheory(); - if (lemmas.size() > 0) { - confl = updateLemmas(); - } + do { + // Propagate on the clauses + confl = propagateBool(); + + // If no conflict, do the theory check + if (confl == CRef_Undef && type != CHECK_WITHOUTH_THEORY) { + // Do the theory check + theoryCheck(CVC4::theory::Theory::EFFORT_STANDARD); + // Pick up the theory propagated literals + propagateTheory(); + // If there are lemmas (or conflicts) update them + if (lemmas.size() > 0) { + confl = updateLemmas(); + } } - - } while (confl == CRef_Undef && qhead < trail.size()); + } while (confl == CRef_Undef && qhead < trail.size()); return confl; } @@ -931,7 +917,7 @@ bool Solver::simplify() { assert(decisionLevel() == 0); - if (!ok || propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef) + if (!ok || propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef) return ok = false; if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) @@ -972,7 +958,7 @@ lbool Solver::search(int nof_conflicts) vec<Lit> learnt_clause; starts++; - TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD; + TheoryCheckType check_type = CHECK_WITH_THEORY; for (;;) { // Propagate and call the theory solvers @@ -1025,14 +1011,14 @@ lbool Solver::search(int nof_conflicts) } // We have a conflict so, we are going back to standard checks - check_type = CHECK_WITH_PROPAGATION_STANDARD; + check_type = CHECK_WITH_THEORY; } else { // If this was a final check, we are satisfiable - if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL) { + if (check_type == CHECK_FINAL) { // Unless a lemma has added more stuff to the queues if (!order_heap.empty() || qhead < trail.size()) { - check_type = CHECK_WITH_PROPAGATION_STANDARD; + check_type = CHECK_WITH_THEORY; continue; } else if (recheck) { // There some additional stuff added, so we go for another full-check @@ -1086,7 +1072,7 @@ lbool Solver::search(int nof_conflicts) if (next == lit_Undef) { // We need to do a full theory check to confirm - check_type = CHECK_WITHOUTH_PROPAGATION_FINAL; + check_type = CHECK_FINAL; continue; } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index c0dd00166..8a5472725 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -303,12 +303,12 @@ protected: vec<bool> theory; // Is the variable representing a theory atom enum TheoryCheckType { - // Quick check, but don't perform theory propagation - CHECK_WITHOUTH_PROPAGATION_QUICK, - // Check and perform theory propagation - CHECK_WITH_PROPAGATION_STANDARD, - // The SAT problem is satisfiable, perform a full theory check - CHECK_WITHOUTH_PROPAGATION_FINAL + // Quick check, but don't perform theory reasoning + CHECK_WITHOUTH_THEORY, + // Check and perform theory reasoning + CHECK_WITH_THEORY, + // The SAT abstraction of the problem is satisfiable, perform a full theory check + CHECK_FINAL }; // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 2b5468186..2cacfbcc0 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -214,7 +214,7 @@ bool SimpSolver::strengthenClause(CRef cr, Lit l) updateElimHeap(var(l)); } - return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef : true; + return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef : true; } @@ -321,7 +321,7 @@ bool SimpSolver::implied(const vec<Lit>& c) uncheckedEnqueue(~c[i]); } - bool result = propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef; + bool result = propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef; cancelUntil(0); return result; } @@ -410,7 +410,7 @@ bool SimpSolver::asymm(Var v, CRef cr) else l = c[i]; - if (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != CRef_Undef){ + if (propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef){ cancelUntil(0); asymm_lits++; if (!strengthenClause(cr, l)) |