bv2int: new options for bvand translation (#5096)

Currently, (bvand x y) is translated into a sum of ITEs.
This PR introduces two more options for the translation of (bvand x y):

bv: cast the integer translations of x and y back to bit-vectors, do a bvand, and cast the result to integers.
iand: use the builtin iand operator.
These options are added to many of the tests, and some new tests are added.
In addition, some tests are cleaned up (e.g., removing --no-check-unsat-cores for satisfiable benchmarks).
Finally, some tests are moved from regress0 to regress2 because they take several seconds to complete (2 -- 10 seconds).

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 4e1a89259b02bf7455d8466e5256400714e8bafb..683fe61bd46687efdd7bc6a18c4eb18e60d2f84c 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -642,6 +642,12 @@ header = "options/smt_options.h"
 [[option.mode.SUM]]
   name = "sum"
   help = "Generate a sum expression for each bvand instance, based on the value in --solbv-bv-as-int-granularity"
+[[option.mode.IAND]]
+  name = "iand"
+  help = "Translate bvand to the iand operator (experimental)"
+[[option.mode.BV]]
+  name = "bv"
+  help = "Translate bvand back to bit-vectors"
 
 [[option]]
   name       = "BVAndIntegerGranularity"

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index aa1b5ac5b7fdde83c0aee3ea98645c1db97f0c30..9ee4e2b7db97854dabfa3aa056119212fb021d25 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -169,7 +169,8 @@ Node BVToInt::eliminationPass(Node n)
   {
     current = toVisit.back();
     // assert that the node is binarized
-    kind::Kind_t k = current.getKind();
+    // The following variable is only used in assertions
+    CVC4_UNUSED kind::Kind_t k = current.getKind();
     uint64_t numChildren = current.getNumChildren();
     Assert((numChildren == 2)
            || !(k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT
@@ -350,7 +351,8 @@ Node BVToInt::translateWithChildren(Node original,
   // ultbv and sltbv were supposed to be eliminated before this point.
   Assert(oldKind != kind::BITVECTOR_ULTBV);
   Assert(oldKind != kind::BITVECTOR_SLTBV);
-  uint64_t originalNumChildren = original.getNumChildren();
+  // The following variable will only be used in assertions.
+  CVC4_UNUSED uint64_t originalNumChildren = original.getNumChildren();
   Node returnNode;
   switch (oldKind)
   {
@@ -414,15 +416,43 @@ Node BVToInt::translateWithChildren(Node original,
     }
     case kind::BITVECTOR_AND:
     {
-      // Construct an ite, based on granularity.
+      // We support three configurations:
+      // 1. translating to IAND
+      // 2. translating back to BV (using BITVECTOR_TO_NAT and INT_TO_BV
+      // operators)
+      // 3. translating into a sum
       uint64_t bvsize = original[0].getType().getBitVectorSize();
-      Assert(translated_children.size() == 2);
-      Node newNode = createBitwiseNode(translated_children[0],
+      if (options::solveBVAsInt() == options::SolveBVAsIntMode::IAND)
+      {
+        Node iAndOp = d_nm->mkConst(IntAnd(bvsize));
+        returnNode = d_nm->mkNode(
+            kind::IAND, iAndOp, translated_children[0], translated_children[1]);
+      }
+      else if (options::solveBVAsInt() == options::SolveBVAsIntMode::BV)
+      {
+        // translate the children back to BV
+        Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize));
+        Node x = translated_children[0];
+        Node y = translated_children[1];
+        Node bvx = d_nm->mkNode(intToBVOp, x);
+        Node bvy = d_nm->mkNode(intToBVOp, y);
+        // perform bvand on the bit-vectors
+        Node bvand = d_nm->mkNode(kind::BITVECTOR_AND, bvx, bvy);
+        // translate the result to integers
+        returnNode = d_nm->mkNode(kind::BITVECTOR_TO_NAT, bvand);
+      }
+      else
+      {
+        Assert(options::solveBVAsInt() == options::SolveBVAsIntMode::SUM);
+        // Construct a sum of ites, based on granularity.
+        Assert(translated_children.size() == 2);
+        Node newNode = createBitwiseNode(translated_children[0],
                                        translated_children[1],
                                        bvsize,
                                        options::BVAndIntegerGranularity(),
                                        &oneBitAnd);
-      returnNode = newNode;
+        returnNode = newNode;
+      }
       break;
     }
     case kind::BITVECTOR_SHL:

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 87b3c73109062d9d3819b1059aa3ea31e8b68750..bc45a3105a94508bd440e7adea511c180d878bee 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -220,12 +220,8 @@ set(regress_0_tests
   regress0/bv/bv-to-bool1.smtv1.smt2
   regress0/bv/bv-to-bool2.smt2
   regress0/bv/bv_to_int1.smt2
-  regress0/bv/bv_to_int2.smt2
-  regress0/bv/bv_to_int_bvmul1.smt2
   regress0/bv/bv_to_int_bvmul2.smt2
-  regress0/bv/bv_to_int_bitwise.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf.smt2
-  regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
   regress0/bv/bv_to_int_elim_err.smt2
   regress0/bv/bv_to_int_zext.smt2
@@ -2102,7 +2098,11 @@ set(regress_2_tests
   regress2/bug765.smt2
   regress2/bug812.smt2
   regress2/bv/opStructure_MBA_6.scrambled.min.smt2
+  regress2/bv_to_int2.smt2
   regress2/bv_to_int_ashr.smt2
+  regress2/bv_to_int_bitwise.smt2
+  regress2/bv_to_int_bvmul1.smt2
+  regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
   regress2/bv_to_int_inc1.smt2
   regress2/bv_to_int_mask_array_1.smt2
   regress2/bv_to_int_mask_array_2.smt2
@@ -2201,8 +2201,12 @@ set(regress_3_tests
   regress3/bmc-ibm-5.smtv1.smt2
   regress3/bmc-ibm-7.smtv1.smt2
   regress3/bv_to_int_and_or.smt2
+  regress3/bv_to_int_bench_9839.smt2.minimized.smt2
   regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2
+  regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2
   regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2
+  regress3/bv_to_int_quant1.smt2
+  regress3/bv_to_int_quant2.smt2
   regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2
   regress3/eq_diamond14.smtv1.smt2
   regress3/friedman_n6_i4.smtv1.smt2

diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2
index 970a9fd7526e2234e6328017d6fc52e710da3494..9111ac25c01b3819b247982ea1f9bf4cc5c5ce8a 100644 (file)
--- a/test/regress/regress0/bv/bv_to_int1.smt2
+++ b/test/regress/regress0/bv/bv_to_int1.smt2
@@ -1,7 +1,7 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun x () (_ BitVec 4))

diff --git a/test/regress/regress0/bv/bv_to_int2.smt2 b/test/regress/regress0/bv/bv_to_int2.smt2
deleted file mode 100644 (file)
index d60f490..0000000
--- a/test/regress/regress0/bv/bv_to_int2.smt2
+++ /dev/null
@@ -1,10 +0,0 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8   --no-check-unsat-cores
-; EXPECT: sat
-(set-logic QF_BV)
-(declare-fun a () (_ BitVec 8))
-(declare-fun b () (_ BitVec 8))
-(assert (bvult (bvshl a b) (bvlshr a b)))
-
-(check-sat)

diff --git a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 b/test/regress/regress0/bv/bv_to_int_bitwise.smt2
deleted file mode 100644 (file)
index 4445517..0000000
--- a/test/regress/regress0/bv/bv_to_int_bitwise.smt2
+++ /dev/null
@@ -1,9 +0,0 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5   --no-check-unsat-cores
-; EXPECT: unsat
-(set-logic QF_BV)
-(declare-fun s () (_ BitVec 4))
-(declare-fun t () (_ BitVec 4))
-(assert (not (= (bvlshr s (bvor (bvand t #b0000) s)) #b0000)))
-(check-sat)
-(exit)

diff --git a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
deleted file mode 100644 (file)
index e214152..0000000
--- a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
+++ /dev/null
@@ -1,11 +0,0 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8   --no-check-unsat-cores
-; EXPECT: sat
-(set-logic QF_BV)
-(declare-fun a () (_ BitVec 8))
-(declare-fun b () (_ BitVec 8))
-(assert (bvult (bvmul a b) (bvudiv a b)))
-(assert (bvugt a (_ bv0 8)))
-
-(check-sat)

diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
index 4bbe5685eaf26353e75ba4622191abd09a95e410..91e0c45fd9df805524a4f5e162c68da32aa98e72 100644 (file)
--- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T4_180 () (_ BitVec 32))

diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
index 5879542eb68c294ab1042720acdc756688b1d668..3e545ef03372c884ec91f4a8b9d946ba57133924 100644 (file)
--- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (declare-fun a () (_ BitVec 4))

diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2
deleted file mode 100644 (file)
index 6196b2b..0000000
--- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2
+++ /dev/null
@@ -1,81 +0,0 @@
-;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-models --no-produce-unsat-cores
-;EXPECT: unsat
-
-(set-logic QF_UFBV)
-(declare-fun z$n0s32 () (_ BitVec 32))
-(declare-fun dataOut () (_ BitVec 32))
-(declare-fun z$2 () (_ BitVec 1))
-(declare-fun stageOne () (_ BitVec 32))
-(declare-fun z$4 () (_ BitVec 1))
-(declare-fun stageTwo () (_ BitVec 32))
-(declare-fun z$6 () (_ BitVec 1))
-(declare-fun tmp_stageOne () (_ BitVec 32))
-(declare-fun z$8 () (_ BitVec 1))
-(declare-fun tmp_stageTwo () (_ BitVec 32))
-(declare-fun z$10 () (_ BitVec 1))
-(declare-fun reset_ () (_ BitVec 1))
-(declare-fun z$14 () (_ BitVec 1))
-(declare-fun Add_32_32_32 ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
-(declare-fun z$15 () (_ BitVec 32))
-(declare-fun z$17 () (_ BitVec 32))
-(declare-fun dataOut$next () (_ BitVec 32))
-(declare-fun z$19 () (_ BitVec 1))
-(declare-fun c1 () (_ BitVec 32))
-(declare-fun dataIn () (_ BitVec 32))
-(declare-fun z$23 () (_ BitVec 32))
-(declare-fun stageOne$next () (_ BitVec 32))
-(declare-fun z$25 () (_ BitVec 1))
-(declare-fun c2 () (_ BitVec 32))
-(declare-fun z$28 () (_ BitVec 32))
-(declare-fun stageTwo$next () (_ BitVec 32))
-(declare-fun z$30 () (_ BitVec 1))
-(declare-fun tmp_stageOne$next () (_ BitVec 32))
-(declare-fun z$32 () (_ BitVec 1))
-(declare-fun tmp_stageTwo$next () (_ BitVec 32))
-(declare-fun z$34 () (_ BitVec 1))
-(declare-fun z$35 () (_ BitVec 1))
-(declare-fun z$55 () (_ BitVec 32))
-(declare-fun z$57 () (_ BitVec 1))
-(declare-fun z$58 () (_ BitVec 1))
-(declare-fun z$59 () (_ BitVec 1))
-(declare-fun prop$next () (_ BitVec 1))
-(declare-fun z$61 () (_ BitVec 1))
-(declare-fun z$54 () (_ BitVec 1))
-(declare-fun z$63 () (_ BitVec 1))
-(assert
- (= z$15 (Add_32_32_32 stageTwo stageOne)))
-(assert
- (= z$17 (ite (= z$14 (_ bv1 1)) z$15 z$n0s32)))
-(assert
- (= z$19 (ite (= dataOut$next z$17) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$25 (ite (= stageOne$next z$23) (_ bv1 1) (_ bv0 1))))
-
- 
-(assert
- (= z$32 (ite (= tmp_stageOne$next stageOne) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$34 (ite (= tmp_stageTwo$next stageTwo) (_ bv1 1) (_ bv0 1))))
-(assert
- (let (($x130 (and (= z$19 (_ bv1 1)) (= z$25 (_ bv1 1)) (= z$30 (_ bv1 1)) (= z$32 (_ bv1 1)) (= z$34 (_ bv1 1)))))
- (= z$35 (ite $x130 (_ bv1 1) (_ bv0 1)))))
-(assert
- (= z$55 (Add_32_32_32 tmp_stageTwo$next tmp_stageOne$next)))
-(assert
- (= z$57 (ite (= dataOut$next z$55) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$58 (ite (= dataOut$next z$n0s32) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$59 (ite (or (= z$57 (_ bv1 1)) (= z$58 (_ bv1 1))) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$61 (ite (= prop$next z$59) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$54 (ite (= prop$next (_ bv0 1)) (_ bv1 1) (_ bv0 1))))
-(assert
- (let (($x52 (= z$2 (_ bv1 1))))
- (let (($x165 (and $x52 (= z$4 (_ bv1 1)) (= z$6 (_ bv1 1)) (= z$8 (_ bv1 1)) (= z$10 (_ bv1 1)) (= z$35 (_ bv1 1)) (= z$61 (_ bv1 1)) (= z$54 (_ bv1 1)))))
- (= z$63 (ite $x165 (_ bv1 1) (_ bv0 1))))))
-(assert
- (= z$63 (_ bv1 1)))
-(check-sat)
-(exit)

diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
index f43c8c860948d2ec95053aa58e04bc8affaaf8f1..0a0ec7b2013d68e3191fe2aebeb3a8959d7dfaea 100644 (file)
--- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (declare-sort S 0)

diff --git a/test/regress/regress2/bv_to_int2.smt2 b/test/regress/regress2/bv_to_int2.smt2
new file mode 100644 (file)
index 0000000..4c1ca0c
--- /dev/null
+++ b/test/regress/regress2/bv_to_int2.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(assert (bvult (bvshl a b) (bvlshr a b)))
+
+(check-sat)

diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2
index 11952839f39b62b68a2884ccf184267d76939724..5516f974baa86bba83d2a67e89a096b7848f05cc 100644 (file)
--- a/test/regress/regress2/bv_to_int_ashr.smt2
+++ b/test/regress/regress2/bv_to_int_ashr.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))

diff --git a/test/regress/regress2/bv_to_int_bitwise.smt2 b/test/regress/regress2/bv_to_int_bitwise.smt2
new file mode 100644 (file)
index 0000000..373f9c3
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_bitwise.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=iand --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun s () (_ BitVec 4))
+(declare-fun t () (_ BitVec 4))
+(assert (not (= (bvlshr s (bvor (bvand t #b0000) s)) #b0000)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress2/bv_to_int_bvmul1.smt2 b/test/regress/regress2/bv_to_int_bvmul1.smt2
new file mode 100644 (file)
index 0000000..cfd5c4b
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_bvmul1.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(assert (bvult (bvmul a b) (bvudiv a b)))
+(assert (bvugt a (_ bv0 8)))
+
+(check-sat)

diff --git a/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
new file mode 100644 (file)
index 0000000..babf9af
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
@@ -0,0 +1,80 @@
+;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-unsat-cores
+;EXPECT: unsat
+(set-logic QF_UFBV)
+(declare-fun z$n0s32 () (_ BitVec 32))
+(declare-fun dataOut () (_ BitVec 32))
+(declare-fun z$2 () (_ BitVec 1))
+(declare-fun stageOne () (_ BitVec 32))
+(declare-fun z$4 () (_ BitVec 1))
+(declare-fun stageTwo () (_ BitVec 32))
+(declare-fun z$6 () (_ BitVec 1))
+(declare-fun tmp_stageOne () (_ BitVec 32))
+(declare-fun z$8 () (_ BitVec 1))
+(declare-fun tmp_stageTwo () (_ BitVec 32))
+(declare-fun z$10 () (_ BitVec 1))
+(declare-fun reset_ () (_ BitVec 1))
+(declare-fun z$14 () (_ BitVec 1))
+(declare-fun Add_32_32_32 ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
+(declare-fun z$15 () (_ BitVec 32))
+(declare-fun z$17 () (_ BitVec 32))
+(declare-fun dataOut$next () (_ BitVec 32))
+(declare-fun z$19 () (_ BitVec 1))
+(declare-fun c1 () (_ BitVec 32))
+(declare-fun dataIn () (_ BitVec 32))
+(declare-fun z$23 () (_ BitVec 32))
+(declare-fun stageOne$next () (_ BitVec 32))
+(declare-fun z$25 () (_ BitVec 1))
+(declare-fun c2 () (_ BitVec 32))
+(declare-fun z$28 () (_ BitVec 32))
+(declare-fun stageTwo$next () (_ BitVec 32))
+(declare-fun z$30 () (_ BitVec 1))
+(declare-fun tmp_stageOne$next () (_ BitVec 32))
+(declare-fun z$32 () (_ BitVec 1))
+(declare-fun tmp_stageTwo$next () (_ BitVec 32))
+(declare-fun z$34 () (_ BitVec 1))
+(declare-fun z$35 () (_ BitVec 1))
+(declare-fun z$55 () (_ BitVec 32))
+(declare-fun z$57 () (_ BitVec 1))
+(declare-fun z$58 () (_ BitVec 1))
+(declare-fun z$59 () (_ BitVec 1))
+(declare-fun prop$next () (_ BitVec 1))
+(declare-fun z$61 () (_ BitVec 1))
+(declare-fun z$54 () (_ BitVec 1))
+(declare-fun z$63 () (_ BitVec 1))
+(assert
+ (= z$15 (Add_32_32_32 stageTwo stageOne)))
+(assert
+ (= z$17 (ite (= z$14 (_ bv1 1)) z$15 z$n0s32)))
+(assert
+ (= z$19 (ite (= dataOut$next z$17) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$25 (ite (= stageOne$next z$23) (_ bv1 1) (_ bv0 1))))
+
+ 
+(assert
+ (= z$32 (ite (= tmp_stageOne$next stageOne) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$34 (ite (= tmp_stageTwo$next stageTwo) (_ bv1 1) (_ bv0 1))))
+(assert
+ (let (($x130 (and (= z$19 (_ bv1 1)) (= z$25 (_ bv1 1)) (= z$30 (_ bv1 1)) (= z$32 (_ bv1 1)) (= z$34 (_ bv1 1)))))
+ (= z$35 (ite $x130 (_ bv1 1) (_ bv0 1)))))
+(assert
+ (= z$55 (Add_32_32_32 tmp_stageTwo$next tmp_stageOne$next)))
+(assert
+ (= z$57 (ite (= dataOut$next z$55) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$58 (ite (= dataOut$next z$n0s32) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$59 (ite (or (= z$57 (_ bv1 1)) (= z$58 (_ bv1 1))) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$61 (ite (= prop$next z$59) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$54 (ite (= prop$next (_ bv0 1)) (_ bv1 1) (_ bv0 1))))
+(assert
+ (let (($x52 (= z$2 (_ bv1 1))))
+ (let (($x165 (and $x52 (= z$4 (_ bv1 1)) (= z$6 (_ bv1 1)) (= z$8 (_ bv1 1)) (= z$10 (_ bv1 1)) (= z$35 (_ bv1 1)) (= z$61 (_ bv1 1)) (= z$54 (_ bv1 1)))))
+ (= z$63 (ite $x165 (_ bv1 1) (_ bv0 1))))))
+(assert
+ (= z$63 (_ bv1 1)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress2/bv_to_int_inc1.smt2 b/test/regress/regress2/bv_to_int_inc1.smt2
index 0d09a7252a6fbcda1e4fd4411607af063416be35..4b22c8ed80e6bc3da3f2456000dd3d33a1d571bf 100644 (file)
--- a/test/regress/regress2/bv_to_int_inc1.smt2
+++ b/test/regress/regress2/bv_to_int_inc1.smt2
@@ -1,4 +1,6 @@
 ; COMMAND-LINE: --incremental --solve-bv-as-int=sum
+; COMMAND-LINE: --incremental --solve-bv-as-int=iand
+; COMMAND-LINE: --incremental --solve-bv-as-int=bv
 ; EXPECT sat
 ; EXPECT sat
 ; EXPECT unsat

diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2
index 970f27fb97624b7348d6a6909f922161245c4c73..b1c8b95096b6cc231b83d76638e3223a9edb719d 100644 (file)
--- a/test/regress/regress2/bv_to_int_mask_array_1.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2
@@ -1,4 +1,6 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=iand --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-fun A () (Array Int Int))

diff --git a/test/regress/regress2/bv_to_int_mask_array_2.smt2 b/test/regress/regress2/bv_to_int_mask_array_2.smt2
index 0960b935930f80c8bd570e196ca12c089391309c..c054f9693bfd86d36ef10f46d86eb4a40caaefeb 100644 (file)
--- a/test/regress/regress2/bv_to_int_mask_array_2.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_2.smt2
@@ -1,4 +1,6 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=iand
+; COMMAND-LINE: --solve-bv-as-int=bv
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun A () (Array Int Int))

diff --git a/test/regress/regress2/bv_to_int_mask_array_3.smt2 b/test/regress/regress2/bv_to_int_mask_array_3.smt2
index 329ee715ae560a6f4d6441a768b872a5b85d6aef..37582d9d838bbb0c1a63e16af0d442b914cfbf1a 100644 (file)
--- a/test/regress/regress2/bv_to_int_mask_array_3.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun A () (Array (_ BitVec 4) (_ BitVec 4)))

diff --git a/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2
new file mode 100644 (file)
index 0000000..aeacda3
--- /dev/null
+++ b/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE:  --solve-bv-as-int=bv 
+; COMMAND-LINE:  --bvand-integer-granularity=1 --solve-bv-as-int=sum     
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun _substvar_1171_ () (_ BitVec 32))
+(assert (bvsge ((_ sign_extend 0) _substvar_1171_) (_ bv0 32)))
+(check-sat)
+(exit)

diff --git a/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2
index a2c964e9a6e79fc87fe39edc4b0ce16ed91e89b5..67f8f69ad4ce5ace6f8df1103469c11e36b23a07 100644 (file)
--- a/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2
+++ b/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum --no-check-models
-; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=2 --solve-bv-as-int=sum --no-check-models
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum      --no-check-models
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=2 --solve-bv-as-int=sum      --no-check-models
 ; EXPECT: sat
 (set-logic BV)
 (declare-fun s () (_ BitVec 3))

diff --git a/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2
new file mode 100644 (file)
index 0000000..3008838
--- /dev/null
+++ b/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE:  --solve-bv-as-int=bv 
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum     
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=iand --iand-mode=sum    
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=iand --iand-mode=bitwise    
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=iand    
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=2 --solve-bv-as-int=sum     
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun t () (_ BitVec 4))
+(declare-fun s () (_ BitVec 4))
+(assert (bvult (_ bv8 4) (bvadd (_ bv8 4) (bvlshr t s))))
+(assert (forall ((x (_ BitVec 4))) (bvule (bvadd (_ bv8 4) (bvlshr x s)) (_ bv8 4))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2
index 22656d17f4abcd8ceec1894aa5e3c6149809fe08..1db79b1e9e8cd0c09f882d20da7ff0688c3674f7 100644 (file)
--- a/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2
+++ b/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE:  --solve-bv-as-int=bv --no-check-unsat-cores
 ; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum  --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic BV)

diff --git a/test/regress/regress3/bv_to_int_quant1.smt2 b/test/regress/regress3/bv_to_int_quant1.smt2
new file mode 100644 (file)
index 0000000..22656d1
--- /dev/null
+++ b/test/regress/regress3/bv_to_int_quant1.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum  --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic BV)
+(declare-fun s () (_ BitVec 4))
+(assert (bvult s (_ bv4 4)))
+(assert (forall ((x (_ BitVec 4))) (= (bvlshr x s) (_ bv0 4))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress3/bv_to_int_quant2.smt2 b/test/regress/regress3/bv_to_int_quant2.smt2
new file mode 100644 (file)
index 0000000..c2bf6d9
--- /dev/null
+++ b/test/regress/regress3/bv_to_int_quant2.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=sum --no-check-models
+; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=bv --no-check-models
+; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=iand --no-check-models
+; EXPECT: sat
+(set-logic BV)
+(declare-fun s () (_ BitVec 4))
+(assert (bvult s (_ bv4 4)))
+(assert (forall ((x (_ BitVec 4))) (= (bvand x s) (_ bv0 4))))
+(check-sat)
+(exit)

diff --git a/test/regress/regress3/bv_to_int_signed_sub_or.smt2 b/test/regress/regress3/bv_to_int_signed_sub_or.smt2
new file mode 100644 (file)
index 0000000..50cce45
--- /dev/null
+++ b/test/regress/regress3/bv_to_int_signed_sub_or.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores
+; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum --no-check-unsat-cores
+; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores
+; COMMAND-LINE: --bvand-integer-granularity=2 --solve-bv-as-int=sum --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun s () (_ BitVec 4))
+(declare-fun t () (_ BitVec 4))
+(assert (bvsgt s t))
+(assert (bvsge t (bvsub t (bvor (bvor s t) (bvneg s)))))
+(check-sat)
+(exit)