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

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index bd5b00728af8249f7bc5860faaabc45d14c12b63..a808ecd3cea7bb9bc030c91900a38b82f32df5a5 100644 (file)
--- 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 c9e98d1704596b36515feed93fb5d0e259f0898c..9eb39e2e2a60df8e79a753969da9eef030212b94 100644 (file)
--- 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 5b26432dd19fc253d8e416a1cd7b223428a4fbed..9878972bfb7711c7c72bb69652f0cc210684ea45 100644 (file)
--- 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 33d5a1c8041b8e8e29a42aaad397323182d02715..019918c2f2cb57878b4685e880921eb80f7f8ac6 100644 (file)
--- 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 9b96b38c4e2da6a5994b6f3f7331676dd29f230c..218fd746b195fa65d08fe179535197aaeb39048b 100644 (file)
--- 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 eeca505fe431c4033a0ffe32bacede7335e69136..b1aaa7d6499bc4e5aba4f00787b4af0d464992c6 100644 (file)
--- 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 8e0ba0016e8d839651484acbd9bb5c1f2ea06153..d732b9ff08291eb0e611d7dbe7ad59ea200f307d 100644 (file)
--- 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)