From add28ea44dd1c63191c9ca8b4efc114dfb9d95d7 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 16 Dec 2021 18:49:30 +0200 Subject: [PATCH] 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. --- src/options/smt_options.toml | 8 ++++++++ src/theory/bv/int_blaster.cpp | 19 +++++++++++++++++++ test/regress/regress2/bv_to_int_ashr.smt2 | 2 +- test/regress/regress2/bv_to_int_bitwise.smt2 | 1 + test/regress/regress2/bv_to_int_shifts.smt2 | 2 +- ...eck_bvsge_bvashr0_4bit.smt2.minimized.smt2 | 1 + ...eck_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 | 1 + test/regress/regress3/bv_to_int_quant1.smt2 | 1 + 8 files changed, 33 insertions(+), 2 deletions(-) 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 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)) -- 2.30.2