diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-04-11 16:31:03 +0000 |
commit | d01d291be3213368985f28d0072905c4f033d5ff (patch) | |
tree | 8524a2b6a00c012221ecca9266c3ab9fb11989ed /src/prop/bvminisat | |
parent | 889853e225687dfef36b15ca1dccf74682e0fd66 (diff) |
merge from arrays-clark branch
Diffstat (limited to 'src/prop/bvminisat')
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 15 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 2 |
2 files changed, 8 insertions, 9 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 238a9cbf7..7e6f4fd93 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -153,7 +153,10 @@ Var Solver::newVar(bool sign, bool dvar) bool Solver::addClause_(vec<Lit>& ps) { - assert(decisionLevel() == 0); + if (decisionLevel() > 0) { + cancelUntil(0); + } + if (!ok) return false; // Check if clause is satisfied and remove false/duplicate literals: @@ -500,6 +503,7 @@ lbool Solver::assertAssumption(Lit p, bool propagate) { only_bcp = true; ccmin_mode = 0; lbool result = search(-1, UIP_FIRST); + return result; } else { return l_True; } @@ -842,14 +846,7 @@ lbool Solver::solve_() model.clear(); conflict.clear(); - ccmin_mode = 2; - - // reduce the database - reduceDB(); - - // this is a new search, reset the parameters - restart_first = opt_restart_first; - restart_inc = opt_restart_inc; + ccmin_mode = 0; if (!ok) return l_False; diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 33d1900c9..c7346d7f7 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -148,6 +148,8 @@ public: // void addMarkerLiteral(Var var) { + // make sure it wasn't already marked + Assert(marker[var] == 0); marker[var] = 1; } |