diff options
| -rw-r--r-- | src/options/options_handler.cpp | 9 | ||||
| -rw-r--r-- | src/proof/bitvector_proof.cpp | 6 | ||||
| -rw-r--r-- | src/proof/proof_manager.cpp | 3 | ||||
| -rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 4 | ||||
| -rw-r--r-- | test/regress/regress0/bv/ackermann1.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/bv/ackermann2.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/bv/bug787.smt2 | 2 |
7 files changed, 17 insertions, 11 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index bd5b00728..a808ecd3c 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1632,7 +1632,14 @@ void OptionsHandler::setProduceAssertions(std::string option, bool value) void OptionsHandler::proofEnabledBuild(std::string option, bool value) { -#ifndef CVC4_PROOF +#ifdef CVC4_PROOF + if (value && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER + && options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT) + { + throw OptionException( + "Eager BV proofs only supported when minisat is used"); + } +#else if(value) { std::stringstream ss; ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support"; diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index c9e98d170..9eb39e2e2 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -81,7 +81,9 @@ void BitVectorProof::registerTerm(Expr term) { Debug("pf::bv") << "BitVectorProof::registerTerm( " << term << " )" << std::endl; - if (options::lfscLetification() && term.isConst()) { + if (options::lfscLetification() && term.isConst() + && term.getType().isBitVector()) + { if (d_constantLetMap.find(term) == d_constantLetMap.end()) { std::ostringstream name; name << "letBvc" << d_constantLetMap.size(); @@ -624,8 +626,6 @@ 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(); - Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER); - for (; it != end; ++it) { if (d_usedBB.find(*it) == d_usedBB.end()) { Debug("pf::bv") << "\t" << *it << "\t(UNUSED)" << std::endl; diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 5b26432dd..9878972bf 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -559,8 +559,6 @@ void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) const void LFSCProof::toStream(std::ostream& out) const { - Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER); - Assert(!d_satProof->proofConstructed()); d_satProof->constructProof(); @@ -730,6 +728,7 @@ void LFSCProof::toStream(std::ostream& out) const d_theoryProof->printTheoryLemmas(used_lemmas, out, paren, globalLetMap); Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl; + out << ";; Printing final unsat proof \n"; if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) { proof::LFSCProofPrinter::printResolutionEmptyClause( ProofManager::getBitVectorProof()->getSatProof(), out, paren); diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 33d5a1c80..019918c2f 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -99,8 +99,8 @@ void EagerBitblaster::bbFormula(TNode node) void EagerBitblaster::bbAtom(TNode node) { node = node.getKind() == kind::NOT ? node[0] : node; - if (node.getKind() == kind::BITVECTOR_BITOF) return; - if (hasBBAtom(node)) + if (node.getKind() == kind::BITVECTOR_BITOF + || node.getKind() == kind::CONST_BOOLEAN || hasBBAtom(node)) { return; } diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2 index 9b96b38c4..218fd746b 100644 --- a/test/regress/regress0/bv/ackermann1.smt2 +++ b/test/regress/regress0/bv/ackermann1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores +; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores ; EXPECT: sat (set-logic QF_UFBV) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2 index eeca505fe..b1aaa7d64 100644 --- a/test/regress/regress0/bv/ackermann2.smt2 +++ b/test/regress/regress0/bv/ackermann2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores +; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_UFBV) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress1/bv/bug787.smt2 b/test/regress/regress1/bv/bug787.smt2 index 8e0ba0016..d732b9ff0 100644 --- a/test/regress/regress1/bv/bug787.smt2 +++ b/test/regress/regress1/bv/bug787.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bitblast=eager --no-check-proofs +; COMMAND-LINE: --bitblast=eager ; EXPECT: unsat (set-logic QF_BV) (set-info :status unsat) |