From ed7bc3afb8c6ee663b3d535674513c7ff4376050 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 27 Aug 2018 14:14:38 -0700 Subject: Resolution proof: separate printing from proof (#1964) Currently, we have an LFSCSatProof which inherits from TSatProof and implements printing the proof. The seperation is not clean (e.g. clauseName is used for printing only but is in TSatProof) and the inheritance does not add any value while making dependencies more confusing. The plan is that TSatProof becomes a self-contained part that the MiniSat implementations generate and ProofManager prints out. This commit is a first step in that direction. For SAT solvers with native capabilities for producing proofs, we would simply implement a different LFSC printer of their proof representation without changing the SAT solver itself. The inheritance would make this awkward to deal with. Additionally, the commit cleans up some unused functions and adjusts the visibility of TSatProof methods and members. --- src/proof/proof_manager.cpp | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) (limited to 'src/proof/proof_manager.cpp') diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index f2205e2ed..cc5332cfd 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -24,6 +24,7 @@ #include "proof/bitvector_proof.h" #include "proof/clause_id.h" #include "proof/cnf_proof.h" +#include "proof/lfsc_proof_printer.h" #include "proof/proof_utils.h" #include "proof/sat_proof_implementation.h" #include "proof/theory_proof.h" @@ -87,7 +88,7 @@ const Proof& ProofManager::getProof(SmtEngine* smt) Assert(currentPM()->d_format == LFSC); currentPM()->d_fullProof.reset(new LFSCProof( smt, - static_cast(getSatProof()), + static_cast(getSatProof()), static_cast(getCnfProof()), static_cast(getTheoryProofEngine()))); } @@ -141,18 +142,17 @@ SkolemizationManager* ProofManager::getSkolemizationManager() { void ProofManager::initSatProof(Minisat::Solver* solver) { Assert (currentPM()->d_satProof == NULL); Assert(currentPM()->d_format == LFSC); - currentPM()->d_satProof = new LFSCCoreSatProof(solver, d_context, ""); + currentPM()->d_satProof = new CoreSatProof(solver, d_context, ""); } void ProofManager::initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx) { ProofManager* pm = currentPM(); + Assert(pm->d_satProof != NULL); Assert (pm->d_cnfProof == NULL); Assert (pm->d_format == LFSC); CnfProof* cnf = new LFSCCnfProof(cnfStream, ctx, ""); pm->d_cnfProof = cnf; - Assert(pm-> d_satProof != NULL); - pm->d_satProof->setCnfProof(cnf); // true and false have to be setup in a special way Node true_node = NodeManager::currentNM()->mkConst(true); @@ -541,16 +541,14 @@ void ProofManager::setLogic(const LogicInfo& logic) { d_logic = logic; } - - LFSCProof::LFSCProof(SmtEngine* smtEngine, - LFSCCoreSatProof* sat, + CoreSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProofEngine* theory) - : d_satProof(sat) - , d_cnfProof(cnf) - , d_theoryProof(theory) - , d_smtEngine(smtEngine) + : d_satProof(sat), + d_cnfProof(cnf), + d_theoryProof(theory), + d_smtEngine(smtEngine) {} void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) const @@ -732,11 +730,12 @@ void LFSCProof::toStream(std::ostream& out) const Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl; if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) { - ProofManager::getBitVectorProof()->getSatProof()->printResolutionEmptyClause(out, paren); + proof::LFSCProofPrinter::printResolutionEmptyClause( + ProofManager::getBitVectorProof()->getSatProof(), out, paren); } else { // print actual resolution proof - d_satProof->printResolutions(out, paren); - d_satProof->printResolutionEmptyClause(out, paren); + proof::LFSCProofPrinter::printResolutions(d_satProof, out, paren); + proof::LFSCProofPrinter::printResolutionEmptyClause(d_satProof, out, paren); } out << paren.str(); -- cgit v1.2.3