bv-to-int: use pow2 operator (#7812)

Currently, the int-blaster translates shifts using an ite whose size is the bit-width.
This PR adds an option to use the internal pow2 operator instead.

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 1e55f63d084de815667610f82e19c750f759cd67..f829068cdf28f91ef53ecc276e006ea780d4b22c 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -399,6 +399,14 @@ name   = "SMT Layer"
   name = "bitwise"
   help = "Introduce a UF operator for bvand, and eagerly add bitwise lemmas"
 
+[[option]]
+  name       = "bvToIntUsePow2"
+  category   = "undocumented"
+  long       = "bv-to-int-use-pow2"
+  type       = "bool"
+  default    = "false"
+  help       = "use internal pow2 operator when translating shift notes"
+
 [[option]]
   name       = "BVAndIntegerGranularity"
   category   = "expert"

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index 58c12ceffa1896cc5fd6ea85c2d057f6708f9cba..ec76d82f9026bcefcdc570a5789789b7bc5ec5d1 100644 (file)
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -882,6 +882,25 @@ Node IntBlaster::createShiftNode(std::vector<Node> children,
   Node y = children[1];
   // shifting by const is eliminated by the theory rewriter
   Assert(!y.isConst());
+
+  // if we use the internal pow2 operator, the translation does not
+  // have any ites
+  if (options().smt.bvToIntUsePow2)
+  {
+    Node pow2Node = d_nm->mkNode(kind::POW2, y);
+    if (isLeftShift)
+    {
+      return d_nm->mkNode(kind::INTS_MODULUS_TOTAL,
+                          d_nm->mkNode(kind::MULT, x, pow2Node),
+                          pow2(bvsize));
+    }
+    else
+    {
+      return d_nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2Node);
+    }
+  }
+
+  // if we do not use the internal pow2 operator, we use ites.
   Node ite = d_zero;
   Node body;
   for (uint64_t i = 0; i < bvsize; i++)

diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2
index 1f5df2c3183f4c7f1d08c071b65d86ba8cb9ddb4..0b290fefdc243bc5d88c46ca257fd82b8836a172 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
-; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=sum --bv-to-int-use-pow2 --bvand-integer-granularity=1
 ; 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
index 4dc37a94c89edee3290d156347b8d3fd21eb328d..2d7349c8fed020f4958f47488d53ea2c41b4642f 100644 (file)
--- a/test/regress/regress2/bv_to_int_bitwise.smt2
+++ b/test/regress/regress2/bv_to_int_bitwise.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bv-to-int-use-pow2 --bvand-integer-granularity=1 --no-check-unsat-cores
 ; COMMAND-LINE: --solve-bv-as-int=bitwise --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=bitwise --bvand-integer-granularity=5 --no-check-unsat-cores

diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2
index 173f1a552e928f7cf835fd2a207308d13921cd37..71241cff9146ade93198e22cbb64d818707c5740 100644 (file)
--- a/test/regress/regress2/bv_to_int_shifts.smt2
+++ b/test/regress/regress2/bv_to_int_shifts.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
-; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --bv-to-int-use-pow2
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun s () (_ BitVec 4))

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 5c96417d5dc3d2f1665339b9d96e5504f7255ddb..7fbe5361482e14b74b722f000be4cc12c1e1e3ed 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,4 +1,5 @@
 ; COMMAND-LINE:  --solve-bv-as-int=sum  --no-check-models
+; COMMAND-LINE:  --solve-bv-as-int=sum  --bv-to-int-use-pow2 --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
index 3c50acc1cd94c697eb40b81c3b9225304982380a..2147bf5908b0fbaea6538197c85f6a476e3f40f4 100644 (file)
--- 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
@@ -1,5 +1,6 @@
 ; COMMAND-LINE:  --solve-bv-as-int=bv
 ; COMMAND-LINE:  --solve-bv-as-int=sum
+; COMMAND-LINE:  --solve-bv-as-int=sum --bv-to-int-use-pow2
 ; COMMAND-LINE:  --solve-bv-as-int=iand --iand-mode=sum
 ; COMMAND-LINE:  --solve-bv-as-int=iand --iand-mode=bitwise
 ; COMMAND-LINE:  --solve-bv-as-int=iand --iand-mode=value

diff --git a/test/regress/regress3/bv_to_int_quant1.smt2 b/test/regress/regress3/bv_to_int_quant1.smt2
index 48d0388d2c1b44c51c5f0b9db3f694a4b936ce73..e1f6c8c37bdd272202d361a6bf398879acb2b8d8 100644 (file)
--- a/test/regress/regress3/bv_to_int_quant1.smt2
+++ b/test/regress/regress3/bv_to_int_quant1.smt2
@@ -1,4 +1,5 @@
 ; 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=sum  --bv-to-int-use-pow2
 ; EXPECT: unsat
 (set-logic BV)
 (declare-fun s () (_ BitVec 4))