diff options
author | lianah <lianahady@gmail.com> | 2013-05-10 15:52:37 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-05-10 15:52:45 -0400 |
commit | f84120cd5311450de2075a91356524d4e20d457c (patch) | |
tree | 1a9220eee3d0063b76794bca414a26132007d8dd /src/prop | |
parent | 7f13c0713accdefa46ce2a43dbeae8c46255bea1 (diff) |
fixes to the proof system so it works with theory lemmas and explanations
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 6196ca357..4cce83fef 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -261,6 +261,7 @@ CRef Solver::reason(Var x) { // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); + PROOF (ProofManager::getSatProof()->registerClause(real_reason, true); ); vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x)); clauses_removable.push(real_reason); attachClause(real_reason); @@ -298,7 +299,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) continue; } // If a literals is false at 0 level (both sat and user level) we also ignore it - if (value(ps[i]) == l_False) { + if (value(ps[i]) == l_False && !PROOF_ON() ) { if (level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) { continue; } else { @@ -789,7 +790,8 @@ CRef Solver::propagate(TheoryCheckType type) // If there are lemmas (or conflicts) update them if (lemmas.size() > 0) { recheck = true; - return updateLemmas(); + confl = updateLemmas(); + return confl; } else { recheck = proxy->theoryNeedCheck(); return confl; @@ -801,7 +803,6 @@ CRef Solver::propagate(TheoryCheckType type) do { // Propagate on the clauses confl = propagateBool(); - // If no conflict, do the theory check if (confl == CRef_Undef && type != CHECK_WITHOUTH_THEORY) { // Do the theory check @@ -836,7 +837,6 @@ CRef Solver::propagate(TheoryCheckType type) } } } while (confl == CRef_Undef && qhead < trail.size()); - return confl; } @@ -1579,6 +1579,7 @@ CRef Solver::updateLemmas() { vec<Lit>& lemma = lemmas[i]; // If it's an empty lemma, we have a conflict at zero level if (lemma.size() == 0) { + Assert (! PROOF_ON()); conflict = CRef_Lazy; backtrackLevel = 0; Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl; @@ -1628,6 +1629,7 @@ CRef Solver::updateLemmas() { } lemma_ref = ca.alloc(clauseLevel, lemma, removable); + PROOF (ProofManager::getSatProof()->registerClause(lemma_ref, true); ); if (removable) { clauses_removable.push(lemma_ref); } else { @@ -1647,6 +1649,7 @@ CRef Solver::updateLemmas() { } else { Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl; conflict = CRef_Lazy; + PROOF(ProofManager::getSatProof()->storeUnitConflict(lemma[0]);); } } else { Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; |