diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-10-09 17:06:30 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-09 17:06:30 -0700 |
| commit | 3b0ce95e7b7d1cbc351df9a7d2acbf3b6e13f9e7 (patch) | |
| tree | f442287bef2e1fcfa070cd03c04650191b9c0d81 /test/regress | |
| parent | 9bc8fe0ea33a280f2a24cca0b2c6f08b962a8f8d (diff) | |
CBQI BV: Add inverse for more operators. (#1213)
This implements side conditions and the instantiation via word-level inversion for operators BITVECTOR_AND, BITVECTOR_OR, BITVECTOR_UREM (Index=1), BITVECTOR_LSHR (index=0).
Diffstat (limited to 'test/regress')
7 files changed, 52 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 new file mode 100644 index 000000000..040bc33c1 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvand x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 new file mode 100644 index 000000000..2fb5d9bec --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvlshr x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 new file mode 100644 index 000000000..c83b0ca73 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvor x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 new file mode 100644 index 000000000..f54abccfd --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (bvult x a) ))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 new file mode 100644 index 000000000..a10f2fbea --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (bvult a x)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 new file mode 100644 index 000000000..6a1987c49 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvurem a x) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 index 235d353ef..84e9fa7ce 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 @@ -4,7 +4,6 @@ (set-info :status sat) (declare-fun a () (_ BitVec 32)) (declare-fun b () (_ BitVec 32)) -(declare-fun c () (_ BitVec 32)) (assert (forall ((x (_ BitVec 32))) (not (= (bvmul x a) b)))) |