diff options
Diffstat (limited to 'src/proof/clausal_bitvector_proof.cpp')
| -rw-r--r-- | src/proof/clausal_bitvector_proof.cpp | 16 |
1 files changed, 6 insertions, 10 deletions
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"; |