diff options
Diffstat (limited to 'src/prop/minisat/simp/SimpSolver.cc')
| -rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 235c97e8f..5bdaea950 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -160,7 +160,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) -bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) +bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) { #ifndef NDEBUG if (use_simplification) { @@ -174,7 +174,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id) if (use_rcheck && implied(ps)) return true; - if (!Solver::addClause_(ps, removable, proof_id)) + if (!Solver::addClause_(ps, removable, id)) return false; if (use_simplification && clauses_persistent.size() == nclauses + 1){ @@ -541,12 +541,14 @@ bool SimpSolver::eliminateVar(Var v) for (int i = 0; i < cls.size(); i++) removeClause(cls[i]); + ClauseId id = ClauseIdUndef; // 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++) { bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable(); - if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable, uint64_t(-1))) { + if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && + !addClause_(resolvent, removable, id)) { return false; } } @@ -585,8 +587,8 @@ bool SimpSolver::substitute(Var v, Lit x) } removeClause(cls[i]); - - if (!addClause_(subst_clause, c.removable(), uint64_t(-1))) { + ClauseId id = ClauseIdUndef; + if (!addClause_(subst_clause, c.removable(), id)) { return ok = false; } } |