bv_to_int preprocessing pass

Introduces a preprocessing pass that translates bv problems to integer problems.

13 files changed, 208 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 92a6200ee..b909817df 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -204,6 +204,15 @@ set(regress_0_tests
   regress0/bv/bv-options4.smt2
   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_zext.smt2
+  regress0/bv/bv_to_int_bitwise.smt2
+  regress0/bv/bvuf_to_intuf.smt2
+  regress0/bv/bvuf_to_intuf_smtlib.smt2
+  regress0/bv/bvuf_to_intuf_sorts.smt2
   regress0/bv/bv2nat-ground-c.smt2
   regress0/bv/bv2nat-simp-range.smt2
   regress0/bv/bvmul-pow2-only.smt2
@@ -1922,6 +1931,8 @@ set(regress_2_tests
   regress2/bug674.smt2
   regress2/bug765.smt2
   regress2/bug812.smt2
+  regress2/bv_to_int_ashr.smt2
+  regress2/bv_to_int_shifts.smt2
   regress2/error0.smt2
   regress2/error1.smtv1.smt2
   regress2/friedman_n4_i5.smtv1.smt2
@@ -2007,6 +2018,7 @@ set(regress_3_tests
   regress3/bmc-ibm-2.smtv1.smt2
   regress3/bmc-ibm-5.smtv1.smt2
   regress3/bmc-ibm-7.smtv1.smt2
+  regress3/bv_to_int_and_or.smt2
   regress3/eq_diamond14.smtv1.smt2
   regress3/friedman_n6_i4.smtv1.smt2
   regress3/hole9.cvc
diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2
new file mode 100644
index 000000000..1df9ec2d6
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int1.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; COMMAND-LINE: --solve-bv-as-int=2 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=3 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=4 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun x () (_ BitVec 4))
+(declare-fun y () (_ BitVec 4))
+(assert (= x (_ bv3 4)))
+(assert (= y (_ bv3 4)))
+(assert (not (bvsle (bvadd x y) (_ bv6 4))))
+(assert (= (bvadd x y) (_ bv6 4)))
+(check-sat)
diff --git a/test/regress/regress0/bv/bv_to_int2.smt2 b/test/regress/regress0/bv/bv_to_int2.smt2
new file mode 100644
index 000000000..ab1bf10f3
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int2.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=5 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models  --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
new file mode 100644
index 000000000..52eb78830
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_bitwise.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=5 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; 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
new file mode 100644
index 000000000..d0d699b4d
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=4 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models  --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)))
+
+(check-sat)
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
new file mode 100644
index 000000000..541229813
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun T4_180 () (_ BitVec 32))
+(assert (and 
+(= (bvmul T4_180 (_ bv1056 32)) (_ bv0 32)) 
+(not (= (bvmul T4_180 (_ bv1408 32)) (_ bv0 32))) 
+)
+)
+(check-sat)
diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2
new file mode 100644
index 000000000..3525cebb6
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_zext.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun T1_31078 () (_ BitVec 8))
+(assert (let ((?v_0 ((_ zero_extend 8) T1_31078))) (and true (= ?v_0 (_ bv123 16)) (not (= (_ bv123 16) ?v_0)))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bvuf_to_intuf.smt2
new file mode 100644
index 000000000..7176f4012
--- /dev/null
+++ b/test/regress/regress0/bv/bvuf_to_intuf.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; EXPECT: sat
+(set-logic QF_UFBV)
+(declare-fun a () (_ BitVec 4))
+(declare-fun b () (_ BitVec 4))
+(declare-fun f ((_ BitVec 4)) (_ BitVec 4) )
+(assert (distinct (bvadd a b) (f a)))
+(check-sat)
diff --git a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
new file mode 100644
index 000000000..297bb2422
--- /dev/null
+++ b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
@@ -0,0 +1,81 @@
+;COMMAND-LINE: --solve-bv-as-int=1 --no-produce-models --no-produce-unsat-cores --no-check-proofs
+;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/bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2
new file mode 100644
index 000000000..873acd6c4
--- /dev/null
+++ b/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; EXPECT: sat
+(set-logic QF_UFBV)
+(declare-sort S 0)
+(declare-fun s () S)
+(declare-fun a () (_ BitVec 4))
+(declare-fun b () (_ BitVec 4))
+(declare-fun f ((_ BitVec 4)) (_ BitVec 4) )
+(declare-fun g (S) (_ BitVec 4))
+(declare-fun h ((_ BitVec 4)) S)
+(assert (distinct (bvadd a b) (f a)))
+(assert (distinct (f a) (g s)))
+(assert (distinct (h a) s))
+(check-sat)
diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2
new file mode 100644
index 000000000..e3fcb1790
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_ashr.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(assert (bvult (bvashr a b) (bvlshr a b)))
+
+(check-sat)
diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2
new file mode 100644
index 000000000..39dace123
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_shifts.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun s () (_ BitVec 64))
+(declare-fun t () (_ BitVec 64))
+(declare-fun splust () (_ BitVec 64))
+(declare-fun shift1 () (_ BitVec 64))
+(declare-fun shift2 () (_ BitVec 64))
+(declare-fun negshift1 () (_ BitVec 64))
+
+(assert (= shift1 (bvlshr s splust)))
+(assert (= shift2 (bvlshr t splust)))
+(assert (= negshift1 (bvneg shift1)))
+(assert (= splust (bvadd s t)))
+(assert (distinct negshift1 shift2))
+
+(check-sat)
diff --git a/test/regress/regress3/bv_to_int_and_or.smt2 b/test/regress/regress3/bv_to_int_and_or.smt2
new file mode 100644
index 000000000..54a491093
--- /dev/null
+++ b/test/regress/regress3/bv_to_int_and_or.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; COMMAND-LINE: --solve-bv-as-int=2 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(assert (bvult (bvor a b) (bvand a b)))
+(check-sat)