diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-27 14:14:38 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-27 14:14:38 -0700 |
commit | ed7bc3afb8c6ee663b3d535674513c7ff4376050 (patch) | |
tree | ffaf84ebac8a9abec6156eb021dfeedf216f9e23 /src/proof/bitvector_proof.cpp | |
parent | 11110b87cb70d9c4a6dc486319adbb7dfa59fedb (diff) |
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.
Diffstat (limited to 'src/proof/bitvector_proof.cpp')
-rw-r--r-- | src/proof/bitvector_proof.cpp | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 0c3f0704c..8f001ffa1 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -15,11 +15,12 @@ **/ +#include "proof/bitvector_proof.h" #include "options/bv_options.h" #include "options/proof_options.h" #include "proof/array_proof.h" -#include "proof/bitvector_proof.h" #include "proof/clause_id.h" +#include "proof/lfsc_proof_printer.h" #include "proof/proof_output_channel.h" #include "proof/proof_utils.h" #include "proof/sat_proof_implementation.h" @@ -48,16 +49,15 @@ BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv, void BitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) { Assert (d_resolutionProof == NULL); - d_resolutionProof = new LFSCBVSatProof(solver, &d_fakeContext, "bb", true); + d_resolutionProof = new BVSatProof(solver, &d_fakeContext, "bb", true); } theory::TheoryId BitVectorProof::getTheoryId() { return theory::THEORY_BV; } void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream, context::Context* cnf) { + Assert (d_resolutionProof != NULL); Assert (d_cnfProof == NULL); d_cnfProof = new LFSCCnfProof(cnfStream, cnf, "bb"); - Assert (d_resolutionProof != NULL); - d_resolutionProof->setCnfProof(d_cnfProof); // true and false have to be setup in a special way Node true_node = NodeManager::currentNM()->mkConst<bool>(true); @@ -515,7 +515,8 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::os Expr lem = utils::mkOr(lemma); Assert (d_bbConflictMap.find(lem) != d_bbConflictMap.end()); ClauseId lemma_id = d_bbConflictMap[lem]; - d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren); + proof::LFSCProofPrinter::printAssumptionsResolution( + d_resolutionProof, lemma_id, os, lemma_paren); os <<lemma_paren.str(); } else { @@ -615,7 +616,8 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::os } ClauseId lemma_id = it->second; - d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren); + proof::LFSCProofPrinter::printAssumptionsResolution( + d_resolutionProof, lemma_id, os, lemma_paren); os <<lemma_paren.str(); return; @@ -1039,7 +1041,7 @@ void LFSCBitVectorProof::printResolutionProof(std::ostream& os, } os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl; - d_resolutionProof->printResolutions(os, paren); + proof::LFSCProofPrinter::printResolutions(d_resolutionProof, os, paren); } std::string LFSCBitVectorProof::assignAlias(Expr expr) { |