diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2020-02-24 19:58:01 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-24 19:58:01 -0800 |
commit | 6e17dd6d5e3ec043e5edd097ac6a736f6a41c753 (patch) | |
tree | 5faac828524e121bcba8cd2d4f1c09bb46cadcfe /test/regress/regress0/bv | |
parent | a3b9a99404ee00bde5db42aab63ab08df3712ba3 (diff) |
bv_to_int preprocessing pass
Introduces a preprocessing pass that translates bv problems to integer problems.
Diffstat (limited to 'test/regress/regress0/bv')
-rw-r--r-- | test/regress/regress0/bv/bv_to_int1.smt2 | 13 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int2.smt2 | 10 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int_bitwise.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int_bvmul1.smt2 | 10 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int_bvmul2.smt2 | 10 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv_to_int_zext.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/bv/bvuf_to_intuf.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 | 81 | ||||
-rw-r--r-- | test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 | 14 |
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) |