diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-29 20:53:47 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-29 20:53:47 +0000 |
commit | e792bb8628ea7010fa9c452bf1aa7ba1b60291a3 (patch) | |
tree | ddc12f92092627b7aee2a63dca8dd66279b2970e /src/prop/minisat | |
parent | e7e9c10006b5b243a73832ed97c5dec79df6c90a (diff) |
Merging the unate-propagator branch into the trunk. This is a big update so expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/core/Solver.C | 111 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 23 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.C | 6 |
3 files changed, 109 insertions, 31 deletions
diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C index 8533e191b..1667af20d 100644 --- a/src/prop/minisat/core/Solver.C +++ b/src/prop/minisat/core/Solver.C @@ -29,6 +29,28 @@ namespace CVC4 { namespace prop { namespace minisat { +Clause* Solver::lazy_reason = reinterpret_cast<Clause*>(1); + +Clause* Solver::getReason(Lit l) +{ + if (reason[var(l)] != lazy_reason) return reason[var(l)]; + // Get the explanation from the theory + SatClause explanation; + if (value(l) == l_True) { + proxy->explainPropagation(l, explanation); + assert(explanation[0] == l); + } else { + proxy->explainPropagation(~l, explanation); + assert(explanation[0] == ~l); + } + Clause* real_reason = Clause_new(explanation, true); + reason[var(l)] = real_reason; + // Add it to the database + learnts.push(real_reason); + attachClause(*real_reason); + return real_reason; +} + Solver::Solver(SatSolver* proxy, context::Context* context) : // SMT stuff @@ -122,7 +144,7 @@ bool Solver::addClause(vec<Lit>& ps, ClauseType type) assert(type != CLAUSE_LEMMA); assert(value(ps[0]) == l_Undef); uncheckedEnqueue(ps[0]); - return ok = (propagate() == NULL); + return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == NULL); }else{ Clause* c = Clause_new(ps, false); clauses.push(c); @@ -282,7 +304,7 @@ void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel) // Select next clause to look at: while (!seen[var(trail[index--])]); p = trail[index+1]; - confl = reason[var(p)]; + confl = getReason(p); seen[var(p)] = 0; pathC--; @@ -299,12 +321,12 @@ void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel) out_learnt.copyTo(analyze_toclear); for (i = j = 1; i < out_learnt.size(); i++) - if (reason[var(out_learnt[i])] == NULL || !litRedundant(out_learnt[i], abstract_level)) + if (getReason(out_learnt[i]) == NULL || !litRedundant(out_learnt[i], abstract_level)) out_learnt[j++] = out_learnt[i]; }else{ out_learnt.copyTo(analyze_toclear); for (i = j = 1; i < out_learnt.size(); i++){ - Clause& c = *reason[var(out_learnt[i])]; + Clause& c = *getReason(out_learnt[i]); for (int k = 1; k < c.size(); k++) if (!seen[var(c[k])] && level[var(c[k])] > 0){ out_learnt[j++] = out_learnt[i]; @@ -342,13 +364,13 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) analyze_stack.clear(); analyze_stack.push(p); int top = analyze_toclear.size(); while (analyze_stack.size() > 0){ - assert(reason[var(analyze_stack.last())] != NULL); + assert(getReason(analyze_stack.last()) != NULL); Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop(); for (int i = 1; i < c.size(); i++){ Lit p = c[i]; if (!seen[var(p)] && level[var(p)] > 0){ - if (reason[var(p)] != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){ + if (getReason(p) != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){ seen[var(p)] = 1; analyze_stack.push(p); analyze_toclear.push(p); @@ -415,42 +437,74 @@ void Solver::uncheckedEnqueue(Lit p, Clause* from) polarity [var(p)] = sign(p); trail.push(p); - if (theory[var(p)]) { + if (theory[var(p)] && from != lazy_reason) { // Enqueue to the theory proxy->enqueueTheoryLiteral(p); } } -Clause* Solver::propagate() +Clause* Solver::propagate(TheoryCheckType type) { Clause* confl = NULL; - while(qhead < trail.size()) { - confl = propagateBool(); - if (confl != NULL) break; - confl = propagateTheory(); - if (confl != NULL) break; + // If this is the final check, no need for Boolean propagation and + // theory propagation + if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) { + return theoryCheck(theory::Theory::FULL_EFFORT); } + // The effort we will be using to theory check + theory::Theory::Effort effort = type == CHECK_WITHOUTH_PROPAGATION_QUICK ? + theory::Theory::QUICK_CHECK : theory::Theory::STANDARD; + + // Keep running until we have checked everything, we + // have no conflict and no new literals have been asserted + bool new_assertions; + do { + new_assertions = false; + while(qhead < trail.size()) { + confl = propagateBool(); + if (confl != NULL) break; + confl = theoryCheck(effort); + if (confl != NULL) break; + } + + if (confl == NULL && type == CHECK_WITH_PROPAGATION_STANDARD) { + new_assertions = propagateTheory(); + if (!new_assertions) break; + } + } while (new_assertions); + return confl; } +bool Solver::propagateTheory() { + std::vector<Lit> propagatedLiterals; + proxy->theoryPropagate(propagatedLiterals); + const unsigned i_end = propagatedLiterals.size(); + for (unsigned i = 0; i < i_end; ++ i) { + uncheckedEnqueue(propagatedLiterals[i], lazy_reason); + } + proxy->clearPropagatedLiterals(); + return propagatedLiterals.size() > 0; +} + /*_________________________________________________________________________________________________ | -| propagateTheory : [void] -> [Clause*] +| theoryCheck: [void] -> [Clause*] | | Description: -| Propagates all enqueued theory facts. If a conflict arises, the conflicting clause is returned, -| otherwise NULL. +| Checks all enqueued theory facts for satisfiability. If a conflict arises, the conflicting +| clause is returned, otherwise NULL. | | Note: the propagation queue might be NOT empty |________________________________________________________________________________________________@*/ -Clause* Solver::propagateTheory() +Clause* Solver::theoryCheck(theory::Theory::Effort effort) { Clause* c = NULL; SatClause clause; - proxy->theoryCheck(clause); + proxy->theoryCheck(effort, clause); int clause_size = clause.size(); Assert(clause_size != 1, "Can't handle unit clause explanations"); if(clause_size > 0) { @@ -598,7 +652,7 @@ bool Solver::simplify() { assert(decisionLevel() == 0); - if (!ok || propagate() != NULL) + if (!ok || propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL) return ok = false; if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) @@ -643,9 +697,9 @@ lbool Solver::search(int nof_conflicts, int nof_learnts) starts++; bool first = true; - + TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD; for (;;){ - Clause* confl = propagate(); + Clause* confl = propagate(check_type); if (confl != NULL){ // CONFLICT conflicts++; conflictC++; @@ -671,9 +725,16 @@ lbool Solver::search(int nof_conflicts, int nof_learnts) varDecayActivity(); claDecayActivity(); + // We have a conflict so, we are going back to standard checks + check_type = CHECK_WITH_PROPAGATION_STANDARD; + }else{ // NO CONFLICT + // If this was a final check, we are satisfiable + if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL) + return l_True; + if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ // Reached bound on number of conflicts: progress_estimate = progressEstimate(); @@ -709,9 +770,11 @@ lbool Solver::search(int nof_conflicts, int nof_learnts) decisions++; next = pickBranchLit(polarity_mode, random_var_freq); - if (next == lit_Undef) - // Model found: - return l_True; + if (next == lit_Undef) { + // We need to do a full theory check to confirm + check_type = CHECK_WITHOUTH_PROPAGATION_FINAL; + continue; + } } // Increase decision level and enqueue 'next' diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 312fe44d5..2e44803e9 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define __CVC4__PROP__MINISAT__SOLVER_H #include "context/context.h" +#include "theory/theory.h" #include <cstdio> #include <cassert> @@ -161,7 +162,11 @@ protected: vec<int> trail_lim; // Separator indices for different decision levels in 'trail'. vec<Clause*> lemmas; // List of lemmas we added (context dependent) vec<int> lemmas_lim; // Separator indices for different decision levels in 'lemmas'. - vec<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. + static Clause* lazy_reason; // The mark when we need to ask the theory engine for a reason + vec<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, lazy_reason if theory propagated, or 'NULL' if none. + + Clause* getReason(Lit l); // Returns the reason, or asks the theory for an explanation + vec<int> level; // 'level[var]' contains the level at which the assignment was made. int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). int lhead; // Head of the lemma stack (for backtracking) @@ -181,6 +186,15 @@ protected: vec<Lit> analyze_toclear; vec<Lit> add_tmp; + enum TheoryCheckType { + // Quick check, but don't perform theory propagation + CHECK_WITHOUTH_PROPAGATION_QUICK, + // Check and perform theory propagation + CHECK_WITH_PROPAGATION_STANDARD, + // The SAT problem is satisfiable, perform a full theory check + CHECK_WITHOUTH_PROPAGATION_FINAL + }; + // Main internal methods: // void insertVarOrder (Var x); // Insert a variable in the decision order priority queue. @@ -188,9 +202,10 @@ protected: void newDecisionLevel (); // Begins a new decision level. void uncheckedEnqueue (Lit p, Clause* from = NULL); // Enqueue a literal. Assumes value of literal is undefined. bool enqueue (Lit p, Clause* from = NULL); // Test if fact 'p' contradicts current state, enqueue otherwise. - Clause* propagate (); // Perform Boolean and Theory. Returns possibly conflicting clause. + Clause* propagate (TheoryCheckType type); // Perform Boolean and Theory. Returns possibly conflicting clause. Clause* propagateBool (); // Perform Boolean propagation. Returns possibly conflicting clause. - Clause* propagateTheory (); // Perform Theory propagation. Returns possibly conflicting clause. + bool propagateTheory (); // Perform Theory propagation. Return true if any literals were asserted. + Clause* theoryCheck (theory::Theory::Effort effort); // Perform a theory satisfiability check. Returns possibly conflicting clause. void cancelUntil (int level); // Backtrack until a certain level. void analyze (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack) void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? @@ -216,7 +231,7 @@ protected: // Misc: // - int decisionLevel () const; // Gives the current decisionlevel. + int decisionLevel () const; // Gives the current decision level. uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels. double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C index 9aad6aea7..00f93402f 100644 --- a/src/prop/minisat/simp/SimpSolver.C +++ b/src/prop/minisat/simp/SimpSolver.C @@ -212,7 +212,7 @@ bool SimpSolver::strengthenClause(Clause& c, Lit l) updateElimHeap(var(l)); } - return c.size() == 1 ? enqueue(c[0]) && propagate() == NULL : true; + return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == NULL : true; } @@ -312,7 +312,7 @@ bool SimpSolver::implied(const vec<Lit>& c) uncheckedEnqueue(~c[i]); } - bool result = propagate() != NULL; + bool result = propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL; cancelUntil(0); return result; } @@ -394,7 +394,7 @@ bool SimpSolver::asymm(Var v, Clause& c) else l = c[i]; - if (propagate() != NULL){ + if (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) != NULL){ cancelUntil(0); asymm_lits++; if (!strengthenClause(c, l)) |