diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/bitvector_proof.cpp | 10 | ||||
-rw-r--r-- | src/proof/clausal_bitvector_proof.cpp | 16 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 2 | ||||
-rw-r--r-- | src/proof/resolution_bitvector_proof.cpp | 4 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 13 |
5 files changed, 21 insertions, 24 deletions
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 98f57e25f..c60cc8274 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -224,7 +224,7 @@ void BitVectorProof::printOwnedTerm(Expr term, void BitVectorProof::printEmptyClauseProof(std::ostream& os, std::ostream& paren) { - Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + Assert(options::bitblastMode() == options::BitblastMode::EAGER) << "the BV theory should only be proving bottom directly in the eager " "bitblasting mode"; } @@ -644,8 +644,8 @@ void BitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) std::vector<Expr>::const_iterator it = d_bbTerms.begin(); std::vector<Expr>::const_iterator end = d_bbTerms.end(); for (; it != end; ++it) { - if (d_usedBB.find(*it) == d_usedBB.end() && - options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) + if (d_usedBB.find(*it) == d_usedBB.end() + && options::bitblastMode() != options::BitblastMode::EAGER) continue; // Is this term has an alias, we inject it through the decl_bblast statement @@ -668,8 +668,8 @@ void BitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) ExprToExpr::const_iterator ait = d_bbAtoms.begin(); ExprToExpr::const_iterator aend = d_bbAtoms.end(); for (; ait != aend; ++ait) { - if (d_usedBB.find(ait->first) == d_usedBB.end() && - options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) + if (d_usedBB.find(ait->first) == d_usedBB.end() + && options::bitblastMode() != options::BitblastMode::EAGER) continue; os << "(th_let_pf _ "; diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp index bb9213b4b..6b0a57725 100644 --- a/src/proof/clausal_bitvector_proof.cpp +++ b/src/proof/clausal_bitvector_proof.cpp @@ -131,11 +131,8 @@ void ClausalBitVectorProof::optimizeDratProof() { TimerStat::CodeTimer optimizeDratProofTimer{ d_dratOptimizationStatistics.d_totalTime}; - if (options::bvOptimizeSatProof() - == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF - || options::bvOptimizeSatProof() - == theory::bv::BvOptimizeSatProof:: - BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA) + if (options::bvOptimizeSatProof() == options::BvOptimizeSatProof::PROOF + || options::bvOptimizeSatProof() == options::BvOptimizeSatProof::FORMULA) { Debug("bv::clausal") << "Optimizing DRAT" << std::endl; std::string formulaFilename("cvc4-dimacs-XXXXXX"); @@ -197,8 +194,7 @@ void ClausalBitVectorProof::optimizeDratProof() static_cast<int64_t>(d_binaryDratProof.tellp()) - startPos); } - if (options::bvOptimizeSatProof() - == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA) + if (options::bvOptimizeSatProof() == options::BvOptimizeSatProof::FORMULA) { std::ifstream optFormulaStream{optFormulaFilename}; const int64_t startPos = static_cast<int64_t>(optFormulaStream.tellg()); @@ -339,7 +335,7 @@ void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os, void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os, std::ostream& paren) { - Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + Assert(options::bitblastMode() == options::BitblastMode::EAGER) << "the BV theory should only be proving bottom directly in the eager " "bitblasting mode"; @@ -366,7 +362,7 @@ void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os, void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os, std::ostream& paren) { - Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + Assert(options::bitblastMode() == options::BitblastMode::EAGER) << "the BV theory should only be proving bottom directly in the eager " "bitblasting mode"; @@ -396,7 +392,7 @@ void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os, void LfscErBitVectorProof::printEmptyClauseProof(std::ostream& os, std::ostream& paren) { - Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + Assert(options::bitblastMode() == options::BitblastMode::EAGER) << "the BV theory should only be proving bottom directly in the eager " "bitblasting mode"; diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index bbf5b0064..fda3f7424 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -798,7 +798,7 @@ void LFSCProof::toStream(std::ostream& out) const CodeTimer finalProofTimer{ ProofManager::currentPM()->getStats().d_finalProofTime}; out << ";; Printing final unsat proof \n"; - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER + if (options::bitblastMode() == options::BitblastMode::EAGER && ProofManager::getBitVectorProof()) { ProofManager::getBitVectorProof()->printEmptyClauseProof(out, paren); diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp index f4ced1748..8d4b56d54 100644 --- a/src/proof/resolution_bitvector_proof.cpp +++ b/src/proof/resolution_bitvector_proof.cpp @@ -129,7 +129,7 @@ void ResolutionBitVectorProof::endBVConflict( void ResolutionBitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts) { - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + if (options::bitblastMode() == options::BitblastMode::EAGER) { Debug("pf::bv") << "Construct full proof." << std::endl; d_resolutionProof->constructProof(); @@ -513,7 +513,7 @@ void LfscResolutionBitVectorProof::printBBDeclarationAndCnf(std::ostream& os, void LfscResolutionBitVectorProof::printEmptyClauseProof(std::ostream& os, std::ostream& paren) { - Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + Assert(options::bitblastMode() == options::BitblastMode::EAGER) << "the BV theory should only be proving bottom directly in the eager " "bitblasting mode"; proof::LFSCProofPrinter::printResolutionEmptyClause( diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 8b9204a20..d95572820 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -82,23 +82,23 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { if (id == theory::THEORY_BV) { auto thBv = static_cast<theory::bv::TheoryBV*>(th); - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER - && options::bvSatSolver() == theory::bv::SAT_SOLVER_CRYPTOMINISAT) + if (options::bitblastMode() == options::BitblastMode::EAGER + && options::bvSatSolver() == options::SatSolverMode::CRYPTOMINISAT) { proof::BitVectorProof* bvp = nullptr; switch (options::bvProofFormat()) { - case theory::bv::BvProofFormat::BITVECTOR_PROOF_DRAT: + case options::BvProofFormat::DRAT: { bvp = new proof::LfscDratBitVectorProof(thBv, this); break; } - case theory::bv::BvProofFormat::BITVECTOR_PROOF_LRAT: + case options::BvProofFormat::LRAT: { bvp = new proof::LfscLratBitVectorProof(thBv, this); break; } - case theory::bv::BvProofFormat::BITVECTOR_PROOF_ER: + case options::BvProofFormat::ER: { bvp = new proof::LfscErBitVectorProof(thBv, this); break; @@ -585,7 +585,8 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, // finalizeBvConflicts(lemmas, os, paren, map); ProofManager::getBitVectorProof()->printBBDeclarationAndCnf(os, paren, map); - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + if (options::bitblastMode() == options::BitblastMode::EAGER) + { Assert(lemmas.size() == 1); // nothing more to do (no combination with eager so far) return; |