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/minisat/simp | |
| 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/minisat/simp')
| -rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 6 |
1 files changed, 3 insertions, 3 deletions
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)) |