diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-06-29 20:53:47 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-06-29 20:53:47 +0000 |
| commit | e792bb8628ea7010fa9c452bf1aa7ba1b60291a3 (patch) | |
| tree | ddc12f92092627b7aee2a63dca8dd66279b2970e /src/prop/minisat/simp | |
| parent | e7e9c10006b5b243a73832ed97c5dec79df6c90a (diff) | |
Merging the unate-propagator branch into the trunk. This is a big update so expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.
Diffstat (limited to 'src/prop/minisat/simp')
| -rw-r--r-- | src/prop/minisat/simp/SimpSolver.C | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C index 9aad6aea7..00f93402f 100644 --- a/src/prop/minisat/simp/SimpSolver.C +++ b/src/prop/minisat/simp/SimpSolver.C @@ -212,7 +212,7 @@ bool SimpSolver::strengthenClause(Clause& c, Lit l) updateElimHeap(var(l)); } - return c.size() == 1 ? enqueue(c[0]) && propagate() == NULL : true; + return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == NULL : true; } @@ -312,7 +312,7 @@ bool SimpSolver::implied(const vec<Lit>& c) uncheckedEnqueue(~c[i]); } - bool result = propagate() != NULL; + bool result = propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL; cancelUntil(0); return result; } @@ -394,7 +394,7 @@ bool SimpSolver::asymm(Var v, Clause& c) else l = c[i]; - if (propagate() != NULL){ + if (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL){ cancelUntil(0); asymm_lits++; if (!strengthenClause(c, l)) |