From 192c5592424e5db0afc72e7316c4698949a2f7e5 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 30 Sep 2011 03:33:56 +0000 Subject: [PATCH] more push/pop infrastructure, some SAT stuff --- src/prop/minisat/core/Solver.cc | 96 ++++++++++++------------ src/prop/minisat/core/Solver.h | 1 - src/prop/minisat/simp/SimpSolver.cc | 2 + src/theory/theory_engine.cpp | 2 +- test/regress/regress0/push-pop/units.cvc | 20 +++++ 5 files changed, 72 insertions(+), 49 deletions(-) create mode 100644 test/regress/regress0/push-pop/units.cvc diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index f3a85ed5e..7b5ba9286 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -143,7 +143,7 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) watches .init(mkLit(v, false)); watches .init(mkLit(v, true )); assigns .push(l_Undef); - vardata .push(mkVarData(CRef_Undef, 0, assertionLevel, 0)); + vardata .push(mkVarData(CRef_Undef, 0, assertionLevel, -1)); activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0); seen .push(0); polarity .push(sign); @@ -158,6 +158,8 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) variables_to_register.push(VarIntroInfo(v, decisionLevel())); } + Debug("minisat") << "new var " << v << std::endl; + return v; } @@ -173,7 +175,7 @@ CRef Solver::reason(Var x) { // Get the explanation from the theory SatClause explanation; proxy->explainPropagation(l, explanation); - + // Sort the literals by trail index level lemma_lt lt(*this); sort(explanation, lt); @@ -245,19 +247,20 @@ bool Solver::addClause_(vec& ps, bool removable) void Solver::attachClause(CRef cr) { const Clause& c = ca[cr]; - Debug("minisat") << "Solver::attachClause(" << c << ")" << std::endl; + Debug("minisat") << "Solver::attachClause(" << c << "): level " << c.level() << std::endl; Assert(c.size() > 1); watches[~c[0]].push(Watcher(cr, c[1])); watches[~c[1]].push(Watcher(cr, c[0])); if (c.removable()) learnts_literals += c.size(); - else clauses_literals += c.size(); } + else clauses_literals += c.size(); +} void Solver::detachClause(CRef cr, bool strict) { const Clause& c = ca[cr]; Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl; assert(c.size() > 1); - + if (strict){ remove(watches[~c[0]], Watcher(cr, c[1])); remove(watches[~c[1]], Watcher(cr, c[0])); @@ -277,7 +280,7 @@ void Solver::removeClause(CRef cr) { detachClause(cr); // Don't leave pointers to free'd memory! if (locked(c)) vardata[var(c[0])].reason = CRef_Undef; - c.mark(1); + c.mark(1); ca.free(cr); } @@ -292,7 +295,7 @@ bool Solver::satisfied(const Clause& c) const { // Revert to the state at given level (keeping all assignment at 'level' but not beyond). // void Solver::cancelUntil(int level) { - Debug("minisat") << "minisat::cancelUntil(" << level << std::endl; + Debug("minisat") << "minisat::cancelUntil(" << level << ")" << std::endl; if (decisionLevel() > level){ // Pop the SMT context @@ -307,7 +310,8 @@ void Solver::cancelUntil(int level) { assigns [x] = l_Undef; 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]); trail_lim.shrink(trail_lim.size() - level); @@ -322,21 +326,7 @@ void Solver::cancelUntil(int level) { } void Solver::popTrail() { - // If we're not incremental, just pop until level 0 - if (!enable_incremental) { - cancelUntil(0); - } else { - // Otherwise pop until the last recorded level 0 trail index - int target_size = trail_user_lim.last(); - for (int c = trail.size()-1; c >= target_size; c--){ - Var x = var(trail[c]); - assigns [x] = l_Undef; - if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) - polarity[x] = sign(trail[c]); - insertVarOrder(x); } - qhead = target_size; - trail.shrink(trail.size() - target_size); - } + cancelUntil(0); } //================================================================================================= @@ -588,6 +578,7 @@ void Solver::analyzeFinal(Lit p, vec& out_conflict) 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()); @@ -812,11 +803,15 @@ void Solver::removeClausesAboveLevel(vec& cs, int level) int i, j; for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; - if (c.level() > level) + if (c.level() > level) { + Debug("minisat") << "removeClausesAboveLevel(" << level << "): removing level-" << c.level() << " clause: " << c << std::endl; removeClause(cs[i]); - else + } else { + Debug("minisat") << "removeClausesAboveLevel(" << level << "): leaving level-" << c.level() << " clause: " << c << std::endl; cs[j++] = cs[i]; + } } + Debug("minisat") << "removeClausesAboveLevel(" << level << "): removed " << i - j << " clauses in all, left " << j << std::endl; cs.shrink(i - j); } @@ -1099,9 +1094,6 @@ lbool Solver::solve_() }else if (status == l_False && conflict.size() == 0) ok = false; - // Cancel the trail downto previous push - //popTrail(); - return status; } @@ -1237,38 +1229,42 @@ void Solver::garbageCollect() void Solver::push() { - if (enable_incremental) { - ++ assertionLevel; - trail_user_lim.push(trail.size()); - } + assert(enable_incremental); + + Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl; + ++assertionLevel; } void Solver::pop() { - if (enable_incremental) { - -- assertionLevel; - // Remove all the clauses asserted (and implied) above the new base level - removeClausesAboveLevel(clauses_removable, assertionLevel); - removeClausesAboveLevel(clauses_persistent, assertionLevel); - - // Pop the user trail size - popTrail(); - trail_user_lim.pop(); - - // Notify the cnf - proxy->removeClausesAboveLevel(assertionLevel); - } + assert(enable_incremental); + + --assertionLevel; + + Debug("minisat") << "in user pop, reducing assertion level to " << assertionLevel << " and removing clauses above this from db" << std::endl; + + // Remove all the clauses asserted (and implied) above the new base level + removeClausesAboveLevel(clauses_removable, assertionLevel); + removeClausesAboveLevel(clauses_persistent, assertionLevel); + + // Pop the user trail size + popTrail(); + + // Notify the cnf + proxy->removeClausesAboveLevel(assertionLevel); } void Solver::unregisterVar(Lit lit) { + Debug("minisat") << "unregisterVar " << lit << std::endl; Var v = var(lit); vardata[v].intro_level = -1; setDecisionVar(v, false); } void Solver::renewVar(Lit lit, int level) { + Debug("minisat") << "renewVar " << lit << " " << level << std::endl; Var v = var(lit); - vardata[v].intro_level = level == -1 ? getAssertionLevel() : level; + vardata[v].intro_level = (level == -1 ? getAssertionLevel() : level); setDecisionVar(v, true); } @@ -1300,6 +1296,7 @@ CRef Solver::updateLemmas() { sort(lemma, lt); // See if the lemma propagates something if (lemma.size() == 1 || value(lemma[1]) == l_False) { + Debug("minisat::lemmas") << "found unit " << lemma.size() << std::endl; // This lemma propagates, see which level we need to backtrack to int currentBacktrackLevel = lemma.size() == 1 ? 0 : level(var(lemma[1])); // Even if the first literal is true, we should propagate it at this level (unless it's set at a lower level) @@ -1337,7 +1334,7 @@ CRef Solver::updateLemmas() { attachClause(lemma_ref); } - // If the lemma is propagating enqueue it's literal (or set the conflict) + // If the lemma is propagating enqueue its literal (or set the conflict) if (conflict == CRef_Undef && value(lemma[0]) != l_True) { if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) { if (value(lemma[0]) == l_False) { @@ -1358,7 +1355,12 @@ CRef Solver::updateLemmas() { // } // Debug("minisat::lemmas") << std::endl; // } + Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; uncheckedEnqueue(lemma[0], lemma_ref); + if(assertionLevel > 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; + } } } } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 8e5e05b1c..345a00e52 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -278,7 +278,6 @@ protected: vec decision; // Declares if a variable is eligible for selection in the decision heuristic. vec trail; // Assignment stack; stores all assigments made in the order they were made. vec trail_lim; // Separator indices for different decision levels in 'trail'. - vec trail_user_lim; // Separator indices for different user push levels in 'trail'. vec 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 271aabb52..f8292c072 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -94,6 +94,8 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool theoryAtom) { lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) { + popTrail(); + vec extra_frozen; lbool result = l_True; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 689ca4cdd..a3b91c132 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -199,7 +199,7 @@ void TheoryEngine::combineTheories() { CVC4_FOR_EACH_THEORY; - // Now add splitters for the ones we are interested in + // Now add splitters for the ones we are interested in for (unsigned i = 0; i < careGraph.size(); ++ i) { const CarePair& carePair = careGraph[i]; diff --git a/test/regress/regress0/push-pop/units.cvc b/test/regress/regress0/push-pop/units.cvc new file mode 100644 index 000000000..9bdfdaadb --- /dev/null +++ b/test/regress/regress0/push-pop/units.cvc @@ -0,0 +1,20 @@ +% COMMAND-LINE: --incremental +x, y: BOOLEAN; +ASSERT x OR y; +% EXPECT: sat +CHECKSAT; +PUSH; + ASSERT NOT x; +% EXPECT: sat + CHECKSAT; + PUSH; + ASSERT NOT y; +% EXPECT: unsat + CHECKSAT; + POP; +% EXPECT: sat + CHECKSAT; +POP; +% EXPECT: sat +CHECKSAT; +% EXIT: 10 -- 2.30.2