diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 16:59:28 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 17:58:14 -0400 |
| commit | 2dbe1f150d30f0fb0c8522f891104270ce09db4c (patch) | |
| tree | 1305f3de890f4353c3b5695a93ab7e2419760617 /src/prop/minisat/simp/SimpSolver.cc | |
| parent | 4ec2c8eb8b8a50dc743119100767e101f19305f6 (diff) | |
Unsat core infrastruture and API (SMT-LIB compliance to come).
Diffstat (limited to 'src/prop/minisat/simp/SimpSolver.cc')
| -rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 8 |
1 files changed, 4 insertions, 4 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; } } |