diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-03-01 14:48:04 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-03-01 14:48:04 +0000 |
commit | 45a138c326da72890bf889a3670aad503ef4aa1e (patch) | |
tree | fa0c9a8497d0b33f78a9f19212152a61392825cc /src/prop/minisat | |
parent | 8c0b2d6db32103268f84d89c0d0545c7eb504069 (diff) |
Partial merge from kind-backend branch, including Minisat and CNF work to
support incrementality.
Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.
Expected performance change negligible; slightly better on memory:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 49 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 6 |
2 files changed, 50 insertions, 5 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 3fe9db10c..678fe28dc 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -714,10 +714,11 @@ CRef Solver::propagate(TheoryCheckType type) } void Solver::propagateTheory() { - - SatClause propagatedLiteralsClause; + SatClause propagatedLiteralsClause; + // Doesn't actually call propagate(); that's done in theoryCheck() now that combination + // is online. This just incorporates those propagations previously discovered. proxy->theoryPropagate(propagatedLiteralsClause); - + vec<Lit> propagatedLiterals; DPLLMinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals); @@ -885,10 +886,22 @@ void Solver::removeClausesAboveLevel(vec<CRef>& cs, int level) for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; if (c.level() > level) { - Debug("minisat") << "removeClausesAboveLevel(" << level << "): removing level-" << c.level() << " clause: " << c << std::endl; + if(Debug.isOn("minisat")) { + Debug("minisat") << "removeClausesAboveLevel(" << level << "): removing level-" << c.level() << " clause: " << c << ":"; + for(int i = 0; i < c.size(); ++i) { + Debug("minisat") << " " << c[i]; + } + Debug("minisat") << std::endl; + } removeClause(cs[i]); } else { - Debug("minisat") << "removeClausesAboveLevel(" << level << "): leaving level-" << c.level() << " clause: " << c << std::endl; + if(Debug.isOn("minisat")) { + Debug("minisat") << "removeClausesAboveLevel(" << level << "): leaving level-" << c.level() << " clause: " << c << ":"; + for(int i = 0; i < c.size(); ++i) { + Debug("minisat") << " " << c[i]; + } + Debug("minisat") << std::endl; + } cs[j++] = cs[i]; } } @@ -1328,16 +1341,25 @@ void Solver::push() Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl; trail_user.push(lit_Undef); trail_ok.push(ok); + trail_user_lim.push(trail.size()); + assert(trail_user_lim.size() == assertionLevel); + Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl; } void Solver::pop() { assert(enable_incremental); + Debug("minisat") << "MINISAT POP at level " << decisionLevel() << " (context " << context->getLevel() << "), popping trail..." << std::endl; popTrail(); + Debug("minisat") << "MINISAT POP now at " << decisionLevel() << " (context " << context->getLevel() << ")" << std::endl; + + assert(decisionLevel() == 0); + assert(trail_user_lim.size() == assertionLevel); --assertionLevel; + Debug("minisat") << "MINISAT POP assertionLevel is now down to " << assertionLevel << ", trail.size is " << trail.size() << ", need to get down to " << trail_user_lim.last() << std::endl; 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 @@ -1346,6 +1368,23 @@ void Solver::pop() Debug("minisat") << "in user pop, at " << trail_lim.size() << " : " << assertionLevel << std::endl; + int downto = trail_user_lim.last(); + while(downto < trail.size()) { + Debug("minisat") << "== unassigning " << trail.last() << std::endl; + Var x = var(trail.last()); + if(intro_level(x) != -1) {// might be unregistered + assigns [x] = l_Undef; + vardata[x].trail_index = -1; + polarity[x] = sign(trail.last()); + insertVarOrder(x); + } + trail.pop(); + } + qhead = trail.size(); + Debug("minisat") << "MINISAT POP assertionLevel is now down to " << assertionLevel << ", trail.size is " << trail.size() << ", should be at " << trail_user_lim.last() << std::endl; + assert(trail_user_lim.last() == qhead); + trail_user_lim.pop(); + // 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) { diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 426268b4b..c0dd00166 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -191,6 +191,10 @@ public: int nVars () const; // The current number of variables. int nFreeVars () const; + // Debugging SMT explanations + // + bool properExplanation(Lit l, Lit expl) const; // returns true if expl can be used to explain l---i.e., both assigned and trail_index(expl) < trail_index(l) + // Resource contraints: // void setConfBudget(int64_t x); @@ -282,6 +286,7 @@ protected: 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<int> trail_user_lim; // Separator indices for different user levels in 'trail'. 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). @@ -462,6 +467,7 @@ inline int Solver::nClauses () const { return clauses_persisten inline int Solver::nLearnts () const { return clauses_removable.size(); } inline int Solver::nVars () const { return vardata.size(); } inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); } +inline bool Solver::properExplanation(Lit l, Lit expl) const { return value(l) == l_True && value(expl) == l_True && trail_index(var(expl)) < trail_index(var(l)); } inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; } inline void Solver::setDecisionVar(Var v, bool b) { |