A better mechanism for handling BV terms with aliases: inject the alias at the decl_b...

diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf
index d8ce7be223a0299a10892080891f6c1588be4ccf..3cc1ec296591084e0520f28cb31abab8cc2506ac 100644 (file)
--- 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 268712f2a8ee07418d2f2826352a1329ed19e490..3fe426f15a9a81b99c5a5d9d421bcabb1d9ef32c 100644 (file)
--- 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();