diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
commit | de0dd1dc966b05467f1a5443ff33094262f5076a (patch) | |
tree | 46a8539229fc31226b416755e6a88c18476ecffc /src/proof/sat_proof_implementation.h | |
parent | 89ba584531115b7f6d47088d7614368ea05ab9d8 (diff) |
Revert "Merging proof branch"
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
Diffstat (limited to 'src/proof/sat_proof_implementation.h')
-rw-r--r-- | src/proof/sat_proof_implementation.h | 27 |
1 files changed, 16 insertions, 11 deletions
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index 1e01e4dce..4f3330ef7 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -543,9 +543,12 @@ ClauseId TSatProof<Solver>::registerClause(typename Solver::TCRef clause, if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); d_lemmaClauses.insert(newId); - Debug("pf::sat") << "TSatProof::registerClause registering a new lemma clause: " - << newId << " = " << *buildClause(newId) - << std::endl; + Debug("pf::sat") + << "TSatProof::registerClause registering a new lemma clause: " + << newId << " = " << *buildClause(newId) + << ". Explainer theory: " << d_cnfProof->getExplainerTheory() + << std::endl; + d_cnfProof->registerExplanationLemma(newId); } } @@ -576,10 +579,12 @@ ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit, } if (kind == THEORY_LEMMA) { Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); - Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new lemma (UNIT CLAUSE): " - << lit - << std::endl; + Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new " + "lemma (UNIT CLAUSE): " + << lit << ". Explainer theory: " + << d_cnfProof->getExplainerTheory() << std::endl; d_lemmaClauses.insert(newId); + d_cnfProof->registerExplanationLemma(newId); } } ClauseId id = d_unitId[toInt(lit)]; @@ -837,7 +842,7 @@ ClauseId TSatProof<Solver>::resolveUnit(typename Solver::TLit lit) { // clause allocator. So reload reason ptr each time. const typename Solver::TClause& initial_reason = getClause(reason_ref); size_t current_reason_size = initial_reason.size(); - for (size_t i = 0; i < current_reason_size; i++) { + for (int i = 0; i < current_reason_size; i++) { const typename Solver::TClause& current_reason = getClause(reason_ref); current_reason_size = current_reason.size(); typename Solver::TLit l = current_reason[i]; @@ -899,7 +904,7 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) { // Here, the call to resolveUnit() can reallocate memory in the // clause allocator. So reload conflict ptr each time. size_t conflict_size = getClause(conflict_ref).size(); - for (size_t i = 0; i < conflict_size; ++i) { + for (int i = 0; i < conflict_size; ++i) { const typename Solver::TClause& conflict = getClause(conflict_ref); typename Solver::TLit lit = conflict[i]; ClauseId res_id = resolveUnit(~lit); @@ -1101,12 +1106,12 @@ void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out, } if (id == this->d_emptyClauseId) { - out <<"(\\ empty empty)"; + out << "(\\empty empty)"; return; } - out << "(\\ " << this->clauseName(id) << "\n"; // bind to lemma name - paren << "))"; // closing parethesis for lemma binding and satlem + out << "(\\" << this->clauseName(id) << "\n"; // bind to lemma name + paren << "))"; // closing parethesis for lemma binding and satlem } /// LFSCSatProof class |