diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-10-25 13:04:05 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-25 13:04:05 -0700 |
| commit | c49ef48588c708bfef3c7a0f9db8219415301a94 (patch) | |
| tree | 1664042f6a64daeaf3cee0dbbe0ebf7caa3544be /test/regress/regress0/quantifiers | |
| parent | e03d56b6de112cae8e9234fff16b985f0765740e (diff) | |
CBQI BV: Add handling for missing operators. (#1274)
This adds inverse handling for BITVECTOR_XOR, BITVECTOR_SIGN_EXTENDS, BITVECTOR_COMP, BITVECTOR_ASHR. Function isInvertible() now corresponds to exactly the operators (plus index) for which we can determine an inverse, which avoids traversing along non-invertible paths.
This further enables a test case that I missed to enable in PR #1268.
Diffstat (limited to 'test/regress/regress0/quantifiers')
7 files changed, 47 insertions, 2 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index a2f5c18b5..4cfdec90e 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -92,14 +92,19 @@ TESTS = \ bug822.smt2 \ qbv-test-invert-mul.smt2 \ qbv-test-invert-bvand.smt2 \ + qbv-test-invert-bvcomp.smt2 \ qbv-test-invert-bvor.smt2 \ qbv-test-invert-bvlshr-0.smt2 \ + qbv-test-invert-bvashr-0.smt2 \ qbv-test-invert-bvurem-1.smt2 \ qbv-test-invert-concat-0.smt2 \ qbv-test-invert-concat-1.smt2 \ + qbv-test-invert-disequality.smt2 \ qbv-test-invert-shl.smt2 \ qbv-test-invert-udiv-0.smt2 \ qbv-test-invert-udiv-1.smt2 \ + qbv-test-invert-sign-extend.smt2 \ + qbv-test-invert-bvxor.smt2 \ qbv-simple-2vars-vo.smt2 \ qbv-test-urem-rewrite.smt2 \ qbv-inequality2.smt2 \ diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 new file mode 100644 index 000000000..db7725896 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvashr x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 new file mode 100644 index 000000000..e8f7c25db --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: unsat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) +(declare-fun c () (_ BitVec 1)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvcomp x a) (bvcomp x 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 index d40e88248..db7725896 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 @@ -5,6 +5,6 @@ (declare-fun a () (_ BitVec 32)) (declare-fun b () (_ BitVec 32)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvlshr x a) b)))) +(assert (forall ((x (_ BitVec 32))) (not (= (bvashr x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 new file mode 100644 index 000000000..eec40a425 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: unsat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvxor x a) (bvmul a a))))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 index 814b0d90b..6ba782597 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-inv-in-dis-eq +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 new file mode 100644 index 000000000..21aa519ad --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 64)) + +(assert (forall ((x (_ BitVec 32))) (not (= ((_ sign_extend 32) x) b)))) + +(check-sat) |