diff options
Diffstat (limited to 'src/proof/theory_proof.cpp')
-rw-r--r-- | src/proof/theory_proof.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index cfad0a068..ee06fbfa0 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -22,12 +22,12 @@ #include "options/proof_options.h" #include "proof/arith_proof.h" #include "proof/array_proof.h" -#include "proof/bitvector_proof.h" #include "proof/clause_id.h" #include "proof/cnf_proof.h" #include "proof/proof_manager.h" #include "proof/proof_output_channel.h" #include "proof/proof_utils.h" +#include "proof/resolution_bitvector_proof.h" #include "proof/sat_proof.h" #include "proof/simplify_boolean_node.h" #include "proof/uf_proof.h" @@ -46,6 +46,9 @@ namespace CVC4 { +using proof::LFSCBitVectorProof; +using proof::ResolutionBitVectorProof; + unsigned CVC4::ProofLetCount::counter = 0; static unsigned LET_COUNT = 1; @@ -77,7 +80,8 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { } if (id == theory::THEORY_BV) { - BitVectorProof * bvp = new LFSCBitVectorProof((theory::bv::TheoryBV*)th, this); + auto bv_theory = static_cast<theory::bv::TheoryBV*>(th); + ResolutionBitVectorProof* bvp = new LFSCBitVectorProof(bv_theory, this); d_theoryProofTable[id] = bvp; return; } @@ -102,9 +106,9 @@ void TheoryProofEngine::finishRegisterTheory(theory::Theory* th) { theory::TheoryId id = th->getId(); if (id == theory::THEORY_BV) { Assert(d_theoryProofTable.find(id) != d_theoryProofTable.end()); - - BitVectorProof *bvp = (BitVectorProof *)d_theoryProofTable[id]; - ((theory::bv::TheoryBV*)th)->setProofLog( bvp ); + ResolutionBitVectorProof* bvp = + (ResolutionBitVectorProof*)d_theoryProofTable[id]; + ((theory::bv::TheoryBV*)th)->setResolutionProofLog(bvp); return; } } @@ -529,7 +533,7 @@ void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std } } - BitVectorProof* bv = ProofManager::getBitVectorProof(); + ResolutionBitVectorProof* bv = ProofManager::getBitVectorProof(); bv->finalizeConflicts(bv_lemmas); // bv->printResolutionProof(os, paren, letMap); } |