diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2018-12-06 18:56:56 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-12-06 18:56:56 -0800 |
commit | 14fc21fc1101587810e64b0ed78ce03622e2939d (patch) | |
tree | a01dd53fd0598b18b46654757a0c4df7b99933fb /src/proof | |
parent | 63fb4e8c33db706589fe41476c4d3358fb47164e (diff) |
Enable BV proofs when using an eager bitblaster (#2733)
* Enable BV proofs when using and eager bitblaster
Specifically:
* Removed assertions that blocked them.
* Made sure that only bitvectors were stored in the BV const let-map
* Prevented true/false from being bit-blasted by the eager bitblaster
Also:
* uncommented "no-check-proofs" from relevant tests
* Option handler logic for BV proofs
BV eager proofs only work when minisat is the sat solver being used by
the BV theory.
Added logic to the --proof hanlder to verify this or throw an option
exception.
* Bugfix for proof options handler
I forgot that proofEnabledBuild runs even if the --proof option is
negated. In my handler I now check that proofs are enabled.
* Clang-format
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/bitvector_proof.cpp | 6 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 3 |
2 files changed, 4 insertions, 5 deletions
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); |