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 | |
parent | 889853e225687dfef36b15ca1dccf74682e0fd66 (diff) |
merge from arrays-clark branch
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 15 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 2 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 4 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 5 |
4 files changed, 17 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; } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 7d4cb7b1c..abe22cb48 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -86,6 +86,10 @@ PropEngine::~PropEngine() { delete d_satSolver; } +void PropEngine::processAssertionsStart() { + d_theoryEngine->preprocessStart(); +} + void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "assertFormula(" << node << ")" << endl; diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 91b9a61e6..93c35bbf3 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -170,6 +170,11 @@ public: void shutdown() { } /** + * Signal that a new round of assertions is ready so we can notify the theory engine + */ + void processAssertionsStart(); + + /** * Converts the given formula to CNF and assert the CNF to the SAT solver. * The formula is asserted permanently for the current context. * @param node the formula to assert |