Letification of BV constants

3 files changed, 60 insertions, 17 deletions

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 2da0d5362..3c96f7cf3 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -16,6 +16,7 @@
 **/
 
 #include "options/bv_options.h"
+#include "options/proof_options.h"
 #include "proof/array_proof.h"
 #include "proof/bitvector_proof.h"
 #include "proof/clause_id.h"
@@ -41,6 +42,7 @@ BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proo
   , d_resolutionProof(NULL)
   , d_cnfProof(NULL)
   , d_bitblaster(NULL)
+  , d_useConstantLetification(false)
 {}
 
 void BitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) {
@@ -117,6 +119,14 @@ void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) {
 void BitVectorProof::registerTerm(Expr term) {
   Debug("pf::bv") << "BitVectorProof::registerTerm( " << term << " )" << std::endl;
 
+  if (options::lfscLetification() && term.isConst()) {
+    if (d_constantLetMap.find(term) == d_constantLetMap.end()) {
+      std::ostringstream name;
+      name << "letBvc" << d_constantLetMap.size();
+      d_constantLetMap[term] = name.str();
+    }
+  }
+
   d_usedBB.insert(term);
 
   if (Theory::isLeafOf(term, theory::THEORY_BV) &&
@@ -384,16 +394,21 @@ void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const ProofLetM
 
 void LFSCBitVectorProof::printConstant(Expr term, std::ostream& os) {
   Assert (term.isConst());
-  os <<"(a_bv " << utils::getSize(term)<<" ";
-  std::ostringstream paren;
-  int size = utils::getSize(term);
-  for (int i = size - 1; i >= 0; --i) {
-    os << "(bvc ";
-    os << (utils::getBit(term, i) ? "b1" : "b0") <<" ";
-    paren << ")";
+  os << "(a_bv " << utils::getSize(term) << " ";
+
+  if (d_useConstantLetification) {
+    os << d_constantLetMap[term] << ")";
+  } else {
+    std::ostringstream paren;
+    int size = utils::getSize(term);
+    for (int i = size - 1; i >= 0; --i) {
+      os << "(bvc ";
+      os << (utils::getBit(term, i) ? "b1" : "b0") <<" ";
+      paren << ")";
+    }
+    os << " bvn)";
+    os << paren.str();
   }
-  os << " bvn)";
-  os << paren.str();
 }
 
 void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map) {
@@ -653,7 +668,26 @@ void LFSCBitVectorProof::printTermDeclarations(std::ostream& os, std::ostream& p
 }
 
 void LFSCBitVectorProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) {
-  // Nothing to do here at this point.
+  if (options::lfscLetification()) {
+    os << std::endl << ";; BV const letification\n" << std::endl;
+    std::map<Expr,std::string>::const_iterator it;
+    for (it = d_constantLetMap.begin(); it != d_constantLetMap.end(); ++it) {
+      os << "\n(@ " << it->second << " ";
+      std::ostringstream localParen;
+      int size = utils::getSize(it->first);
+      for (int i = size - 1; i >= 0; --i) {
+        os << "(bvc ";
+        os << (utils::getBit(it->first, i) ? "b1" : "b0") << " ";
+        localParen << ")";
+      }
+      os << "bvn";
+      os << localParen.str();
+      paren << ")";
+    }
+    os << std::endl;
+
+    d_useConstantLetification = true;
+  }
 }
 
 void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
@@ -700,15 +734,20 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
     os << "(bv_bbl_const "<< utils::getSize(term) <<" _ ";
     std::ostringstream paren;
     int size = utils::getSize(term);
-    for (int i = size - 1; i>= 0; --i) {
-      os << "(bvc ";
-      os << (utils::getBit(term, i) ? "b1" : "b0") <<" ";
-      paren << ")";
+    if (d_useConstantLetification) {
+      os << d_constantLetMap[term] << ")";
+    } else {
+      for (int i = size - 1; i>= 0; --i) {
+        os << "(bvc ";
+        os << (utils::getBit(term, i) ? "b1" : "b0") <<" ";
+        paren << ")";
+      }
+      os << " bvn)";
+      os << paren.str();
     }
-    os << " bvn)";
-    os << paren.str();
     return;
   }
+
   case kind::BITVECTOR_AND :
   case kind::BITVECTOR_OR :
   case kind::BITVECTOR_XOR :
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 8d0871ef8..f89774945 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -81,6 +81,10 @@ protected:
   bool d_isAssumptionConflict;
   theory::bv::TBitblaster<Node>* d_bitblaster;
   std::string getBBTermName(Expr expr);
+
+  std::map<Expr,std::string> d_constantLetMap;
+  bool d_useConstantLetification;
+
 public:
   BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine);
 
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 1b4fbcc47..e5e00f117 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -384,7 +384,7 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) {
           if (lemma[i] == *lemmaIt)
             found = true;
         }
-        Assert(found);
+        AlwaysAssert(found);
       }
     }
   }