diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-10-03 22:07:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-10-03 22:07:38 +0000 |
commit | c5000befcf95c03a42a2f73a40c3dac6dc3492be (patch) | |
tree | 4a87ace04da1c62d1474673d485843d820e5cbd8 /src/prop/minisat | |
parent | 40253236078988fecc3becd2619dd5ccad5e3077 (diff) |
user push/pop support in minisat and simplification; also bindings work
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 68 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 2 |
3 files changed, 59 insertions, 13 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 7b5ba9286..c1795a12c 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -221,7 +221,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) // Fit to size ps.shrink(i - j); - // If we are in solve or decision level > 0 if (minisat_busy || decisionLevel() > 0) { lemmas.push(); @@ -232,8 +231,15 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) if (ps.size() == 0) { return ok = false; } else if (ps.size() == 1) { - uncheckedEnqueue(ps[0]); - return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef); + if(assigns[var(ps[0])] == l_Undef) { + uncheckedEnqueue(ps[0]); + if(assertionLevel > 0) { + // remember to unset it on user pop + 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); + } else return ok; } else { CRef cr = ca.alloc(assertionLevel, ps, false); clauses_persistent.push(cr); @@ -307,10 +313,13 @@ void Solver::cancelUntil(int level) { } for (int c = trail.size()-1; c >= trail_lim[level]; c--){ Var x = var(trail[c]); - assigns [x] = l_Undef; - if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) + if(intro_level(x) != -1) {// might be unregistered + assigns [x] = l_Undef; + vardata[x].trail_index = -1; + if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) polarity[x] = sign(trail[c]); - insertVarOrder(x); + insertVarOrder(x); + } } qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); @@ -581,8 +590,16 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) Debug("minisat") << "unchecked enqueue of " << p << " (" << trail_index(var(p)) << ") trail size is " << trail.size() << " cap is " << trail.capacity() << std::endl; assert(value(p) == l_Undef); assigns[var(p)] = lbool(!sign(p)); - vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size()); - trail.push_(p); + if(trail_index(var(p)) != -1) { + // This var is already represented in the trail, presumably from + // an earlier incarnation as a unit clause (it has been + // unregistered and renewed since then) + vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail_index(var(p))); + trail[trail_index(var(p))] = p; + } else { + vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size()); + trail.push_(p); + } if (theory[var(p)]) { // Enqueue to the theory proxy->enqueueTheoryLiteral(p); @@ -1050,6 +1067,8 @@ lbool Solver::solve_() ScopedBool scoped_bool(minisat_busy, true); + popTrail(); + model.clear(); conflict.clear(); if (!ok){ @@ -1231,14 +1250,19 @@ void Solver::push() { assert(enable_incremental); - Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl; + popTrail(); ++assertionLevel; + Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl; + trail_user.push(lit_Undef); + trail_ok.push(ok); } void Solver::pop() { assert(enable_incremental); + popTrail(); + --assertionLevel; Debug("minisat") << "in user pop, reducing assertion level to " << assertionLevel << " and removing clauses above this from db" << std::endl; @@ -1247,8 +1271,26 @@ void Solver::pop() removeClausesAboveLevel(clauses_removable, assertionLevel); removeClausesAboveLevel(clauses_persistent, assertionLevel); - // Pop the user trail size - popTrail(); + Debug("minisat") << "in user pop, at " << trail_lim.size() << " : " << assertionLevel << std::endl; + + // Unset any units learned or added at this level + Debug("minisat") << "in user pop, unsetting level units for level " << assertionLevel << std::endl; + while(trail_user.last() != lit_Undef) { + Lit l = trail_user.last(); + Debug("minisat") << "== unassigning " << l << std::endl; + Var x = var(l); + assigns [x] = l_Undef; + if (phase_saving >= 1) + polarity[x] = sign(l); + insertVarOrder(x); + trail_user.pop(); + } + trail_user.pop(); + ok = trail_ok.last(); + trail_ok.pop(); + Debug("minisat") << "in user pop, done unsetting level units" << std::endl; + + Debug("minisat") << "about to removeClausesAboveLevel(" << assertionLevel << ") in CNF" << std::endl; // Notify the cnf proxy->removeClausesAboveLevel(assertionLevel); @@ -1357,9 +1399,11 @@ CRef Solver::updateLemmas() { // } Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; uncheckedEnqueue(lemma[0], lemma_ref); - if(assertionLevel > 0) { + if(lemma.size() == 1 && assertionLevel > 0) { + assert(decisionLevel() == 0); // remember to unset it on user pop Debug("minisat") << "got new unit (survived downward during updateLemmas()) " << lemma[0] << " at assertion level " << assertionLevel << std::endl; + trail_user.push(lemma[0]); } } } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 345a00e52..c5220997b 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -278,6 +278,8 @@ protected: vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic. vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made. vec<int> trail_lim; // Separator indices for different decision levels in 'trail'. + vec<Lit> trail_user; // Stack of assignments to UNdo on user pop. + vec<bool> trail_ok; // Stack of "whether we're in conflict" flags. vec<VarData> vardata; // Stores reason and level for each variable. int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'. diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index f8292c072..8c31dd377 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -57,7 +57,7 @@ SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* con , asymm_lits (0) , eliminated_vars (0) , elimorder (1) - , use_simplification (true) + , use_simplification (!enableIncremental) , occurs (ClauseDeleted(ca)) , elim_heap (ElimLt(n_occ)) , bwdsub_assigns (0) |