diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-08-17 15:20:19 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-08-17 15:20:19 +0000 |
commit | 32e1d3558f17d12f2631175776209a5f8cabbdd9 (patch) | |
tree | ebc20658d5375b17f13b5c83d3dc7ee078029f96 /src/prop/minisat/simp | |
parent | 41dc1b3685b9258660dab571f8f8b56deb0fb095 (diff) |
new implementation of lemmas on demand
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>
Diffstat (limited to 'src/prop/minisat/simp')
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 28 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.h | 22 |
2 files changed, 27 insertions, 23 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 8bcd9fe76..271aabb52 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -134,23 +134,23 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) -bool SimpSolver::addClause_(vec<Lit>& ps, ClauseType type) +bool SimpSolver::addClause_(vec<Lit>& ps, bool removable) { #ifndef NDEBUG for (int i = 0; i < ps.size(); i++) assert(!isEliminated(var(ps[i]))); #endif - int nclauses = clauses.size(); + int nclauses = clauses_persistent.size(); if (use_rcheck && implied(ps)) return true; - if (!Solver::addClause_(ps, type)) + if (!Solver::addClause_(ps, removable)) return false; - if (use_simplification && clauses.size() == nclauses + 1){ - CRef cr = clauses.last(); + if (use_simplification && clauses_persistent.size() == nclauses + 1){ + CRef cr = clauses_persistent.last(); const Clause& c = ca[cr]; // NOTE: the clause is added to the queue immediately and then @@ -516,9 +516,12 @@ bool SimpSolver::eliminateVar(Var v) // Produce clauses in cross product: vec<Lit>& resolvent = add_tmp; for (int i = 0; i < pos.size(); i++) - for (int j = 0; j < neg.size(); j++) - if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, CLAUSE_CONFLICT)) + for (int j = 0; j < neg.size(); j++) { + bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable(); + if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable)) { return false; + } + } // Free occurs list for this variable: occurs[v].clear(true); @@ -555,8 +558,9 @@ bool SimpSolver::substitute(Var v, Lit x) removeClause(cls[i]); - if (!addClause_(subst_clause, CLAUSE_PROBLEM)) + if (!addClause_(subst_clause, c.removable())) { return ok = false; + } } return true; @@ -669,10 +673,10 @@ void SimpSolver::cleanUpClauses() { occurs.cleanAll(); int i,j; - for (i = j = 0; i < clauses.size(); i++) - if (ca[clauses[i]].mark() == 0) - clauses[j++] = clauses[i]; - clauses.shrink(i - j); + for (i = j = 0; i < clauses_persistent.size(); i++) + if (ca[clauses_persistent[i]].mark() == 0) + clauses_persistent[j++] = clauses_persistent[i]; + clauses_persistent.shrink(i - j); } diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index a7359e28e..9b5e5d45c 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -47,12 +47,12 @@ class SimpSolver : public Solver { // Problem specification: // Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); - bool addClause (const vec<Lit>& ps, ClauseType type); - bool addEmptyClause(ClauseType type); // Add the empty clause to the solver. - bool addClause (Lit p, ClauseType type); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, ClauseType type); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, ClauseType type); // Add a ternary clause to the solver. - bool addClause_(vec<Lit>& ps, ClauseType type); + bool addClause (const vec<Lit>& ps, bool removable); + bool addEmptyClause(bool removable); // Add the empty clause to the solver. + bool addClause (Lit p, bool removable); // Add a unit clause to the solver. + bool addClause (Lit p, Lit q, bool removable); // Add a binary clause to the solver. + bool addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver. + bool addClause_(vec<Lit>& ps, bool removable); bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). // Variable mode: @@ -181,11 +181,11 @@ inline void SimpSolver::updateElimHeap(Var v) { elim_heap.update(v); } -inline bool SimpSolver::addClause (const vec<Lit>& ps, ClauseType type) { ps.copyTo(add_tmp); return addClause_(add_tmp, type); } -inline bool SimpSolver::addEmptyClause(ClauseType type) { add_tmp.clear(); return addClause_(add_tmp, type); } -inline bool SimpSolver::addClause (Lit p, ClauseType type) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, type); } -inline bool SimpSolver::addClause (Lit p, Lit q, ClauseType type) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, type); } -inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, ClauseType type) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, type); } +inline bool SimpSolver::addClause (const vec<Lit>& ps, bool removable) { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); } +inline bool SimpSolver::addEmptyClause(bool removable) { add_tmp.clear(); return addClause_(add_tmp, removable); } +inline bool SimpSolver::addClause (Lit p, bool removable) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); } +inline bool SimpSolver::addClause (Lit p, Lit q, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); } +inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); } inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } } inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; } |