bv_to_int preprocessing pass

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

9 files changed, 162 insertions, 0 deletions

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)