From: yoni206 <yoni206@users.noreply.github.com>
Date: Thu, 16 Dec 2021 16:49:30 +0000 (+0200)
Subject: bv-to-int: use pow2 operator (#7812)
X-Git-Tag: cvc5-1.0.0~655
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=add28ea44dd1c63191c9ca8b4efc114dfb9d95d7;p=cvc5.git

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 1e55f63d0..f829068cd 100644
--- 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 58c12ceff..ec76d82f9 100644
--- 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 1f5df2c31..0b290fefd 100644
--- 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 4dc37a94c..2d7349c8f 100644
--- 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 173f1a552..71241cff9 100644
--- 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 5c96417d5..7fbe53614 100644
--- 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 3c50acc1c..2147bf590 100644
--- 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 48d0388d2..e1f6c8c37 100644
--- 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))