A better mechanism for handling BV terms with aliases: inject the alias at the decl_bblast step, instead of having an individual "with alias" rule for each BV operation

2 files changed, 29 insertions, 281 deletions

diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf
index d8ce7be22..3cc1ec296 100644
--- a/proofs/signatures/th_bv_bitblast.plf
+++ b/proofs/signatures/th_bv_bitblast.plf
@@ -35,6 +35,16 @@
 	 (! u (! v (bblast_term n t b) (holds cln))
 		   (holds cln))))))))
 
+(declare decl_bblast_with_alias
+	 (! n mpz
+	 (! b bblt
+	 (! t (term (BitVec n))
+	 (! a (term (BitVec n))
+	 (! bb (bblast_term n t b)
+	 (! e (th_holds (= _ t a))
+	 (! s (^ (bblt_len b) n)
+	 (! u (! v (bblast_term n a b) (holds cln))
+		   (holds cln))))))))))
 
 ; a predicate to represent the n^th bit of a bitvector term
 (declare bitof
@@ -103,53 +113,6 @@
                        (! c (^ (bblast_concat xb yb ) rb)
                            (bblast_term n (concat n m m1 x y) rb)))))))))))))
 
-(declare bv_bbl_concat_alias_1 (! n mpz
-     	    	               (! m mpz
-		               (! m1 mpz
-                               (! x (term (BitVec m))
-		               (! y (term (BitVec m1))
-		               (! xb bblt
-		               (! yb bblt
-		               (! rb bblt
-       		               (! a (term (BitVec m))
-		               (! e (th_holds (= _ x a))
-		               (! xbb (bblast_term m x xb)
-		               (! ybb (bblast_term m1 y yb)
-                               (! c (^ (bblast_concat xb yb) rb)
-                                   (bblast_term n (concat n m m1 a y) rb)))))))))))))))
-
-(declare bv_bbl_concat_alias_2 (! n mpz
-     	    	               (! m mpz
-		               (! m1 mpz
-                               (! x (term (BitVec m))
-		               (! y (term (BitVec m1))
-		               (! xb bblt
-		               (! yb bblt
-		               (! rb bblt
-		               (! xbb (bblast_term m x xb)
-       		               (! a (term (BitVec m1))
-		               (! e (th_holds (= _ y a))
-		               (! ybb (bblast_term m1 y yb)
-                               (! c (^ (bblast_concat xb yb) rb)
-                                   (bblast_term n (concat n m m1 x a) rb)))))))))))))))
-
-(declare bv_bbl_concat_alias_1_2 (! n mpz
-     	    	                 (! m mpz
-		                 (! m1 mpz
-                                 (! x (term (BitVec m))
-		                 (! y (term (BitVec m1))
-		                 (! xb bblt
-		                 (! yb bblt
-		                 (! rb bblt
-       		                 (! a1 (term (BitVec m))
-		                 (! e (th_holds (= _ x a1))
-		                 (! xbb (bblast_term m x xb)
-       		                 (! a2 (term (BitVec m1))
-		                 (! e (th_holds (= _ y a2))
-		                 (! ybb (bblast_term m1 y yb)
-                                 (! c (^ (bblast_concat xb yb) rb)
-                                     (bblast_term n (concat n m m1 a1 a2) rb)))))))))))))))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST EXTRACT
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -178,19 +141,6 @@
 			(! c ( ^ (bblast_extract xb i j m) rb)
                            (bblast_term n (extract n i j m x) rb)))))))))))
 
-(declare bv_bbl_extract_alias (! n mpz
-  			      (! i mpz
-			      (! j mpz
-			      (! m mpz
-                       	      (! x (term (BitVec m))
-		       	      (! xb bblt
-		       	      (! rb bblt
-			      (! a (term (BitVec m))
-		              (! e (th_holds (= _ x a))
-		       	      (! xbb (bblast_term m x xb)
-			      (! c ( ^ (bblast_extract xb i j m) rb)
-                                 (bblast_term n (extract n i j m a) rb)))))))))))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST ZERO/SIGN EXTEND
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -226,18 +176,6 @@
 			(! c ( ^ (bblast_sextend xb k m) rb)
                            (bblast_term n (sign_extend n k m x) rb))))))))))
 
-(declare bv_bbl_sign_extend_alias (! n mpz
-   			          (! k mpz
-			          (! m mpz
-                       	          (! x (term (BitVec m))
-		       	          (! xb bblt
-		       	          (! rb bblt
-				  (! a (term (BitVec m))
-		                  (! e (th_holds (= _ x a))
-		       	          (! xbb (bblast_term m x xb)
-			          (! c ( ^ (bblast_sextend xb k m) rb)
-                                     (bblast_term n (sign_extend n k m a) rb))))))))))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST BVAND
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -382,19 +320,6 @@
                       (! c (^ (bblast_bvadd xb yb false) rb)
                            (bblast_term n (bvadd n x y) rb)))))))))))
 
-(declare bv_bbl_bvadd_alias_1 (! n mpz
-	                      (! x (term (BitVec n))
-		              (! y (term (BitVec n))
-        		      (! xb bblt
-        		      (! yb bblt
-	        	      (! rb bblt
-			      (! a (term (BitVec n))
-		              (! e (th_holds (= _ x a))
-		              (! xbb (bblast_term n x xb)
-        		      (! ybb (bblast_term n y yb)
-                              (! c (^ (bblast_bvadd xb yb false) rb)
-                                   (bblast_term n (bvadd n a y) rb)))))))))))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST BVNEG
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -556,94 +481,6 @@
          (! c (^ (bblast_eq by bx) f)
             (th_holds (iff (= (BitVec n) x y) f))))))))))))
 
-(declare bv_bbl_=_alias_1
-	 (! n mpz
-	 (! x (term (BitVec n))
-         (! y (term (BitVec n))
-         (! bx bblt
-         (! by bblt
-         (! f formula
- 	 (! a (term (BitVec n))
- 	 (! e (th_holds (= _ x a))
-         (! bbx (bblast_term n x bx)
-         (! bby (bblast_term n y by)
-         (! c (^ (bblast_eq bx by) f)
-            (th_holds (iff (= (BitVec n) a y) f))))))))))))))
-
-(declare bv_bbl_=_alias_1_swap
-	 (! n mpz
-	 (! x (term (BitVec n))
-         (! y (term (BitVec n))
-         (! bx bblt
-         (! by bblt
-         (! f formula
- 	 (! a (term (BitVec n))
- 	 (! e (th_holds (= _ x a))
-         (! bbx (bblast_term n x bx)
-         (! bby (bblast_term n y by)
-         (! c (^ (bblast_eq by bx) f)
-            (th_holds (iff (= (BitVec n) a y) f))))))))))))))
-
-(declare bv_bbl_=_alias_2
-	 (! n mpz
-	 (! x (term (BitVec n))
-         (! y (term (BitVec n))
-         (! bx bblt
-         (! by bblt
-         (! f formula
-         (! bbx (bblast_term n x bx)
- 	 (! a (term (BitVec n))
- 	 (! e (th_holds (= _ y a))
-         (! bby (bblast_term n y by)
-         (! c (^ (bblast_eq bx by) f)
-            (th_holds (iff (= (BitVec n) x a) f))))))))))))))
-
-(declare bv_bbl_=_alias_2_swap
-	 (! n mpz
-	 (! x (term (BitVec n))
-         (! y (term (BitVec n))
-         (! bx bblt
-         (! by bblt
-         (! f formula
-         (! bbx (bblast_term n x bx)
- 	 (! a (term (BitVec n))
- 	 (! e (th_holds (= _ y a))
-         (! bby (bblast_term n y by)
-         (! c (^ (bblast_eq by bx) f)
-            (th_holds (iff (= (BitVec n) x a) f))))))))))))))
-
-(declare bv_bbl_=_alias_1_2
-	 (! n mpz
-	 (! x (term (BitVec n))
-         (! y (term (BitVec n))
-         (! bx bblt
-         (! by bblt
-         (! f formula
- 	 (! a1 (term (BitVec n))
- 	 (! e1 (th_holds (= _ x a1))
-         (! bbx (bblast_term n x bx)
- 	 (! a2 (term (BitVec n))
- 	 (! e2 (th_holds (= _ y a2))
-         (! bby (bblast_term n y by)
-         (! c (^ (bblast_eq bx by) f)
-            (th_holds (iff (= (BitVec n) a1 a2) f))))))))))))))))
-
-(declare bv_bbl_=_alias_1_2_swap
-	 (! n mpz
-	 (! x (term (BitVec n))
-         (! y (term (BitVec n))
-         (! bx bblt
-         (! by bblt
-         (! f formula
- 	 (! a1 (term (BitVec n))
- 	 (! e1 (th_holds (= _ x a1))
-         (! bbx (bblast_term n x bx)
- 	 (! a2 (term (BitVec n))
- 	 (! e2 (th_holds (= _ y a2))
-         (! bby (bblast_term n y by)
-         (! c (^ (bblast_eq by bx) f)
-            (th_holds (iff (= (BitVec n) a1 a2) f))))))))))))))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST BVULT
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -669,50 +506,6 @@
          (! c (^ (bblast_bvult bx by (mp_add n (~1))) f)
             (th_holds (iff (bvult n x y) f))))))))))))
 
-(declare bv_bbl_bvult_alias_1
-	 (! n mpz
-	 (! x (term (BitVec n))
-         (! y (term (BitVec n))
-         (! bx bblt
-         (! by bblt
-         (! f formula
- 	 (! a1 (term (BitVec n))
- 	 (! e1 (th_holds (= _ x a1))
-         (! bbx (bblast_term n x bx)
-         (! bby (bblast_term n y by)
-         (! c (^ (bblast_bvult bx by (mp_add n (~1))) f)
-            (th_holds (iff (bvult n a1 y) f))))))))))))))
-
-(declare bv_bbl_bvult_alias_2
-	 (! n mpz
-	 (! x (term (BitVec n))
-         (! y (term (BitVec n))
-         (! bx bblt
-         (! by bblt
-         (! f formula
-         (! bbx (bblast_term n x bx)
- 	 (! a2 (term (BitVec n))
- 	 (! e2 (th_holds (= _ y a2))
-         (! bby (bblast_term n y by)
-         (! c (^ (bblast_bvult bx by (mp_add n (~1))) f)
-            (th_holds (iff (bvult n x a2) f))))))))))))))
-
-(declare bv_bbl_bvult_alias_1_2
-	 (! n mpz
-	 (! x (term (BitVec n))
-         (! y (term (BitVec n))
-         (! bx bblt
-         (! by bblt
-         (! f formula
- 	 (! a1 (term (BitVec n))
- 	 (! e1 (th_holds (= _ x a1))
-         (! bbx (bblast_term n x bx)
- 	 (! a2 (term (BitVec n))
- 	 (! e2 (th_holds (= _ y a2))
-         (! bby (bblast_term n y by)
-         (! c (^ (bblast_bvult bx by (mp_add n (~1))) f)
-            (th_holds (iff (bvult n a1 a2) f))))))))))))))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; BITBLAST BVSLT
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -740,34 +533,6 @@
          (! c (^ (bblast_bvslt bx by n) f)
             (th_holds (iff (bvslt n x y) f))))))))))))
 
-(declare bv_bbl_bvslt_alias_1
-	 (! n mpz
-	 (! x (term (BitVec n))
-         (! y (term (BitVec n))
-         (! bx bblt
-         (! by bblt
-         (! f formula
- 	 (! a (term (BitVec n))
- 	 (! e (th_holds (= _ x a))
-         (! bbx (bblast_term n x bx)
-         (! bby (bblast_term n y by)
-         (! c (^ (bblast_bvslt bx by n) f)
-            (th_holds (iff (bvslt n a y) f))))))))))))))
-
-(declare bv_bbl_bvslt_alias_2
-	 (! n mpz
-	 (! x (term (BitVec n))
-         (! y (term (BitVec n))
-         (! bx bblt
-         (! by bblt
-         (! f formula
-         (! bbx (bblast_term n x bx)
- 	 (! a (term (BitVec n))
- 	 (! e (th_holds (= _ y a))
-         (! bby (bblast_term n y by)
-         (! c (^ (bblast_bvslt bx by n) f)
-            (th_holds (iff (bvslt n x a) f))))))))))))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;;           BITBLASTING CONNECTORS
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 268712f2a..3fe426f15 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -677,7 +677,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
   if (Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst()) {
     // A term is a leaf if it has no children, or if it belongs to another theory
     os << "(bv_bbl_var " << utils::getSize(term) << " " << d_exprToVariableName[term];
-    os << " _ )";
+    os << " _)";
     return;
   }
 
@@ -711,27 +711,15 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
     for (int i = term.getNumChildren() - 1; i > 0; --i) {
       os <<"(bv_bbl_"<< utils::toLFSCKind(kind);
 
-      if (i > 1) {
-        // This is not the inner-most operation; only child i+1 can be aliased
-        if (hasAlias(term[i])) {os << "_alias_2";}
-      } else {
-        // This is the inner-most operation; both children can be aliased
-        if (hasAlias(term[i-1]) || hasAlias(term[i])) {os << "_alias";}
-        if (hasAlias(term[i-1])) {os << "_1";}
-        if (hasAlias(term[i])) {os << "_2";}
-      }
-
       if (kind == kind::BITVECTOR_CONCAT) {
         os << " " << utils::getSize(term) << " _";
       }
       os << " _ _ _ _ _ _ ";
     }
 
-    if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";}
     os << getBBTermName(term[0]) << " ";
 
     for (unsigned i = 1; i < term.getNumChildren(); ++i) {
-      if (hasAlias(term[i])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[i]]] << " ";}
       os << getBBTermName(term[i]);
       os << ") ";
     }
@@ -751,15 +739,11 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
   case kind::BITVECTOR_EXTRACT : {
     os <<"(bv_bbl_"<<utils::toLFSCKind(kind);
 
-    if (hasAlias(term[0])) {os << "_alias";};
-
     os << " " << utils::getSize(term) << " ";
     os << utils::getExtractHigh(term) << " ";
     os << utils::getExtractLow(term) << " ";
     os << " _ _ _ _ ";
 
-    if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";}
-
     os << getBBTermName(term[0]);
     os <<")";
     return;
@@ -767,8 +751,8 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
   case kind::BITVECTOR_REPEAT :
   case kind::BITVECTOR_ZERO_EXTEND :
   case kind::BITVECTOR_SIGN_EXTEND : {
-    os <<"(bv_bbl_" <<utils::toLFSCKind(kind) << (hasAlias(term[0]) ? "_alias " : " ");
-    os << utils::getSize(term) <<" ";
+    os << "(bv_bbl_" << utils::toLFSCKind(kind) << " ";
+    os << utils::getSize(term) << " ";
     if (term.getKind() == kind::BITVECTOR_REPEAT) {
       unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount;
       os << amount;
@@ -784,7 +768,6 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
     }
 
     os <<" _ _ _ _ ";
-    if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";}
     os << getBBTermName(term[0]);
     os <<")";
     return;
@@ -838,23 +821,14 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool
 
     os << "(bv_bbl_" << utils::toLFSCKind(atom.getKind());
 
-    if (hasAlias(atom[0]) || hasAlias(atom[1])) {os << "_alias";}
-    if (hasAlias(atom[0])) {os << "_1";}
-    if (hasAlias(atom[1])) {os << "_2";}
-
     if (swap) {os << "_swap";}
 
     os << " _ _ _ _ _ _ ";
-
-    if (hasAlias(atom[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[0]]] << " ";}
     os << getBBTermName(atom[0]);
-
     os << " ";
-
-    if (hasAlias(atom[1])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[1]]] << " ";}
     os << getBBTermName(atom[1]);
-
     os << ")";
+
     return;
   }
   default:
@@ -867,12 +841,10 @@ void LFSCBitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os
 
   os << "(bv_bbl_=_false";
   os << " _ _ _ _ _ _ ";
-  if (hasAlias(atom[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[0]]] << " ";}
   os << getBBTermName(atom[0]);
 
   os << " ";
 
-  if (hasAlias(atom[1])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[1]]] << " ";}
   os << getBBTermName(atom[1]);
 
   os << ")";
@@ -905,10 +877,21 @@ void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren)
         options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER)
       continue;
 
-    os << "(decl_bblast _ _ _ ";
-    printTermBitblasting(*it, os);
-    os << "(\\ "<< getBBTermName(*it) << "\n";
-    paren << "))";
+    // Is this term has an alias, we inject it through the decl_bblast statement
+    if (hasAlias(*it)) {
+      os << "(decl_bblast_with_alias _ _ _ _ ";
+      printTermBitblasting(*it, os);
+      os << " " << d_aliasToBindDeclaration[d_assignedAliases[*it]] << " ";
+      os << "(\\ "<< getBBTermName(*it);
+      os << "\n";
+      paren <<"))";
+    } else {
+      os << "(decl_bblast _ _ _ ";
+      printTermBitblasting(*it, os);
+      os << "(\\ "<< getBBTermName(*it);
+      os << "\n";
+      paren <<"))";
+    }
   }
   // bit-blast atoms
   ExprToExpr::const_iterator ait = d_bbAtoms.begin();