diff options
Diffstat (limited to 'src/prop/minisat/simp')
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 8 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.h | 26 |
2 files changed, 19 insertions, 15 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 6dcdb76c7..71e747f72 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -159,7 +159,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) -bool SimpSolver::addClause_(vec<Lit>& ps, bool removable) +bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) { #ifndef NDEBUG if (use_simplification) { @@ -173,7 +173,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, bool removable) if (use_rcheck && implied(ps)) return true; - if (!Solver::addClause_(ps, removable)) + if (!Solver::addClause_(ps, removable, proof_id)) return false; if (use_simplification && clauses_persistent.size() == nclauses + 1){ @@ -545,7 +545,7 @@ bool SimpSolver::eliminateVar(Var v) for (int i = 0; i < pos.size(); i++) 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)) { + if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable, uint64_t(-1))) { return false; } } @@ -585,7 +585,7 @@ bool SimpSolver::substitute(Var v, Lit x) removeClause(cls[i]); - if (!addClause_(subst_clause, c.removable())) { + if (!addClause_(subst_clause, c.removable(), uint64_t(-1))) { return ok = false; } } diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 878d799a5..041309546 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 isTheoryAtom = false, bool preRegister = false, bool canErase = true); - 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 addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id); + bool addEmptyClause(bool removable, uint64_t proof_id); // Add the empty clause to the solver. + bool addClause (Lit p, bool removable, uint64_t proof_id); // Add a unit clause to the solver. + bool addClause (Lit p, Lit q, bool removable, uint64_t proof_id); // Add a binary clause to the solver. + bool addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id); // Add a ternary clause to the solver. + bool addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id); bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). // Variable mode: @@ -182,11 +182,15 @@ inline void SimpSolver::updateElimHeap(Var v) { elim_heap.update(v); } -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 bool SimpSolver::addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id) + { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, proof_id); } +inline bool SimpSolver::addEmptyClause(bool removable, uint64_t proof_id) { add_tmp.clear(); return addClause_(add_tmp, removable, proof_id); } +inline bool SimpSolver::addClause (Lit p, bool removable, uint64_t proof_id) + { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, proof_id); } +inline bool SimpSolver::addClause (Lit p, Lit q, bool removable, uint64_t proof_id) + { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, proof_id); } +inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id) + { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); } 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; } |