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).

21 files changed, 92 insertions, 28 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 87b3c7310..bc45a3105 100644
--- 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 970a9fd75..9111ac25c 100644
--- 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_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
index 4bbe5685e..91e0c45fd 100644
--- 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 5879542eb..3e545ef03 100644
--- 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_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
index f43c8c860..0a0ec7b20 100644
--- 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/regress0/bv/bv_to_int2.smt2 b/test/regress/regress2/bv_to_int2.smt2
index d60f4903b..4c1ca0c00 100644
--- a/test/regress/regress0/bv/bv_to_int2.smt2
+++ b/test/regress/regress2/bv_to_int2.smt2
@@ -1,6 +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=5   --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
+; 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))
diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2
index 11952839f..5516f974b 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   --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/regress0/bv/bv_to_int_bitwise.smt2 b/test/regress/regress2/bv_to_int_bitwise.smt2
index 444551776..373f9c323 100644
--- a/test/regress/regress0/bv/bv_to_int_bitwise.smt2
+++ b/test/regress/regress2/bv_to_int_bitwise.smt2
@@ -1,5 +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=5   --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=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))
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 b/test/regress/regress2/bv_to_int_bvmul1.smt2
index e21415244..cfd5c4b9a 100644
--- a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
+++ b/test/regress/regress2/bv_to_int_bvmul1.smt2
@@ -1,6 +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=4   --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
+; 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))
diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
index 6196b2bb9..babf9af32 100644
--- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2
+++ b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
@@ -1,6 +1,5 @@
-;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-models --no-produce-unsat-cores
+;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))
diff --git a/test/regress/regress2/bv_to_int_inc1.smt2 b/test/regress/regress2/bv_to_int_inc1.smt2
index 0d09a7252..4b22c8ed8 100644
--- 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 970f27fb9..b1c8b9509 100644
--- 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 0960b9359..c054f9693 100644
--- 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 329ee715a..37582d9d8 100644
--- 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
index 000000000..aeacda35e
--- /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 a2c964e9a..67f8f69ad 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,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
index 000000000..300883882
--- /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 22656d17f..1db79b1e9 100644
--- 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
index 000000000..22656d17f
--- /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
index 000000000..c2bf6d9d0
--- /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
index 000000000..50cce4511
--- /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)