diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-12-20 18:27:39 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-20 18:27:39 -0800 |
commit | f9149d3b3e785950a846fb195bf9fa9cb1a2d94a (patch) | |
tree | c69c90377a6c24abbc9c608a767507740abfd3b6 /test | |
parent | 13cc0e94ac8892fa1cefa53ff1c884d154894b58 (diff) |
Add explicit disequality handling when generating side condition for CBQI BV. (#1447)
This refactors solveBvLit to support explicit handling of disequalities (and, in the next step, inequalities) when generating side conditions.
Diffstat (limited to 'test')
44 files changed, 445 insertions, 188 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index c59570651..bb43d6c1c 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -90,25 +90,38 @@ TESTS = \ qbv-simp.smt2 \ psyco-001-bv.smt2 \ bug822.smt2 \ - qbv-test-invert-mul.smt2 \ + qbv-disequality3.smt2 \ + qbv-inequality2.smt2 \ + qbv-simple-2vars-vo.smt2 \ + qbv-test-invert-bvadd-neq.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-bvand-neq.smt2 \ qbv-test-invert-bvashr-0.smt2 \ + qbv-test-invert-bvashr-0-neq.smt2 \ + qbv-test-invert-bvashr-1.smt2 \ + qbv-test-invert-bvashr-1-neq.smt2 \ + qbv-test-invert-bvlshr-0.smt2 \ + qbv-test-invert-bvlshr-0-neq.smt2 \ + qbv-test-invert-bvlshr-1.smt2 \ + qbv-test-invert-bvlshr-1-neq.smt2 \ + qbv-test-invert-bvmul.smt2 \ + qbv-test-invert-bvmul-neq.smt2 \ + qbv-test-invert-bvor.smt2 \ + qbv-test-invert-bvor-neq.smt2 \ + qbv-test-invert-bvshl-0.smt2 \ + qbv-test-invert-bvudiv-0.smt2 \ + qbv-test-invert-bvudiv-0-neq.smt2 \ + qbv-test-invert-bvudiv-1.smt2 \ + qbv-test-invert-bvudiv-1-neq.smt2 \ + qbv-test-invert-bvult-1.smt2 \ qbv-test-invert-bvurem-1.smt2 \ + qbv-test-invert-bvurem-1-neq.smt2 \ + qbv-test-invert-bvxor.smt2 \ + qbv-test-invert-bvxor-neq.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 \ - qbv-test-invert-bvult-1.smt2 \ intersection-example-onelane.proof-node22337.smt2 \ nested9_true-unreach-call.i_575.smt2 \ small-pipeline-fixpoint-3.smt2 \ @@ -127,6 +140,8 @@ TESTS = \ # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 +# disabled since bvcomp handling is currently disabled +# qbv-test-invert-bvcomp.smt2 # removed because they take more than 20s # javafe.ast.ArrayInit.35.smt2 diff --git a/test/regress/regress0/quantifiers/qbv-disequality3.smt2 b/test/regress/regress0/quantifiers/qbv-disequality3.smt2 new file mode 100644 index 000000000..d16157509 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-disequality3.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvmul (bvadd x b) a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-inequality2.smt2 b/test/regress/regress0/quantifiers/qbv-inequality2.smt2 index d53715a2d..1486e176d 100644 --- a/test/regress/regress0/quantifiers/qbv-inequality2.smt2 +++ b/test/regress/regress0/quantifiers/qbv-inequality2.smt2 @@ -1,11 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) - -(assert (forall ((x (_ BitVec 32))) (or (bvuge x (bvadd a b)) (bvule x b)))) +(assert (forall ((x (_ BitVec 8))) (or (bvuge x (bvadd a b)) (bvule x b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 index d74a6cfea..3c4f93243 100644 --- a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 +++ b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-simp.smt2 b/test/regress/regress0/quantifiers/qbv-simp.smt2 index 1f72d44e4..ec4626f52 100644 --- a/test/regress/regress0/quantifiers/qbv-simp.smt2 +++ b/test/regress/regress0/quantifiers/qbv-simp.smt2 @@ -1,9 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --no-cbqi-full +; EXPECT: unsat (set-logic BV) (set-info :status unsat) (assert (forall - ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32))) + ((A (_ BitVec 8)) (B (_ BitVec 8)) (C (_ BitVec 8)) (D (_ BitVec 8))) (or (and (= A B) (= C D)) (and (= A C) (= B D))))) - + (check-sat) - + diff --git a/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 b/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 index b6ae95fec..c36322aac 100644 --- a/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 +++ b/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 @@ -1,16 +1,16 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) -(declare-fun c () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) +(declare-fun c () (_ BitVec 8)) -(assert (not (= a #x00000000))) +(assert (not (= a #x00))) -(assert (forall ((x (_ BitVec 32)) (y (_ BitVec 32))) (or -(not (= (bvmul x y) #x0000000A)) -(not (= (bvadd y a) #x00000010)) +(assert (forall ((x (_ BitVec 8)) (y (_ BitVec 8))) (or +(not (= (bvmul x y) #x0A)) +(not (= (bvadd y a) #x10)) ))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 new file mode 100644 index 000000000..216a98531 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvadd x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 new file mode 100644 index 000000000..ad3b9a9e5 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvand x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 index d611fcd68..8dd50b1be 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvand x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvand x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 new file mode 100644 index 000000000..e05c3446d --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvashr x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 index db7725896..30e7c2f8b 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvashr x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvashr x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 new file mode 100644 index 000000000..2835e5956 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvashr a x) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2 new file mode 100644 index 000000000..c3de64c4c --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvashr a x) 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 index e8f7c25db..3b55c0b9a 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 @@ -1,11 +1,11 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: unsat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) (declare-fun c () (_ BitVec 1)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvcomp x a) (bvcomp x b))))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvcomp x a) ((_ extract 7 7) (bvmul a b)))))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 new file mode 100644 index 000000000..e05c3446d --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvashr 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 index db7725896..1018ce72c 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvashr x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvlshr x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 new file mode 100644 index 000000000..503bc9852 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvlshr a x) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2 new file mode 100644 index 000000000..08479d90e --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvlshr a x) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2 new file mode 100644 index 000000000..9dc9f98ac --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvmul x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2 new file mode 100644 index 000000000..f3dad679b --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvmul x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 new file mode 100644 index 000000000..74c2891cf --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvor 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 index 287da08c7..4145c68b1 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvor x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvor x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 new file mode 100644 index 000000000..e85ecc7de --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvshl x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 new file mode 100644 index 000000000..abef84da2 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvshl x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 new file mode 100644 index 000000000..3748eca24 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (distinct a b (_ bv0 8))) +(assert (forall ((x (_ BitVec 8))) (= (bvudiv x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2 new file mode 100644 index 000000000..2cabb502e --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (distinct a b (_ bv0 8))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvudiv x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 new file mode 100644 index 000000000..a0e1b62c2 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (distinct a b (_ bv0 8))) +(assert (forall ((x (_ BitVec 8))) (= (bvudiv a x) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1.smt2 index bf69a8b4a..2690a0ac9 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --bv-div-zero-const +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const ; EXPECT: sat (set-logic BV) (set-info :status 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 index 13c1bf10a..a1dca469a 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 @@ -1,9 +1,9 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (bvult a x)))) +(assert (forall ((x (_ BitVec 8))) (not (bvult a x)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 new file mode 100644 index 000000000..871df4827 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvurem a x) b))) + +(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 index f7fe54e3e..22bd306ee 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv --bv-div-zero-const +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvurem a x) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvurem a x) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 new file mode 100644 index 000000000..4f9c6edc3 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvxor x a) (bvmul a a))))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 index eec40a425..ef41eecdd 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 @@ -1,9 +1,9 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: unsat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvxor x a) (bvmul a a))))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvxor x a) (bvmul a a))))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 new file mode 100644 index 000000000..769854f6f --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) + +(assert (forall ((x (_ BitVec 8))) (= (concat x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 index f4e19fc52..7b66bd859 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 64)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) -(assert (forall ((x (_ BitVec 32))) (not (= (concat x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (concat x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 new file mode 100644 index 000000000..7dab5637e --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) + +(assert (forall ((x (_ BitVec 8))) (= (concat a x) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 index 827e74605..13fb3e1c2 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 64)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) -(assert (forall ((x (_ BitVec 32))) (not (= (concat a x) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (concat a x) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 deleted file mode 100644 index 6ba782597..000000000 --- a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep -; EXPECT: sat -(set-logic BV) -(set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) - -(assert (forall ((x (_ BitVec 32))) (= (bvand x a) 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 deleted file mode 100644 index 84e9fa7ce..000000000 --- a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -; 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 (= (bvmul x a) b)))) - -(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 deleted file mode 100644 index 97a0662eb..000000000 --- a/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -; 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 (= (bvshl x a) b)))) - -(check-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 index 21aa519ad..43019c4cb 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 64)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) -(assert (forall ((x (_ BitVec 32))) (not (= ((_ sign_extend 32) x) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= ((_ sign_extend 8) x) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 deleted file mode 100644 index becfc5315..000000000 --- a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 +++ /dev/null @@ -1,11 +0,0 @@ -; COMMAND-LINE: --cbqi-bv --bv-div-zero-const -; EXPECT: sat -(set-logic BV) -(set-info :status sat) -(declare-fun a () (_ BitVec 16)) -(declare-fun b () (_ BitVec 16)) - -(assert (distinct a b (_ bv0 16))) -(assert (forall ((x (_ BitVec 16))) (not (= (bvudiv x a) b)))) - -(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 b/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 index 6df69d80b..e57352b8f 100644 --- a/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --bv-div-zero-const +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h index ce01c17e4..5e1d404dc 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h @@ -23,6 +23,7 @@ #include "util/result.h" using namespace CVC4; +using namespace CVC4::kind; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::smt; @@ -45,58 +46,63 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite unsigned idx, Node (*getsc)(bool, Kind, unsigned, Node, Node)) { - Assert(k == kind::BITVECTOR_ULT - || k == kind::BITVECTOR_SLT - || k == kind::EQUAL); - Assert(k != kind::EQUAL || pol == false); + Assert(k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == EQUAL); + Assert(k != EQUAL || pol == false); Node sc = getsc(pol, k, idx, d_sk, d_t); Kind ksc = sc.getKind(); - TS_ASSERT((k == kind::BITVECTOR_ULT && pol == false) - || (k == kind::BITVECTOR_SLT && pol == false) - || ksc == kind::IMPLIES); - Node scl = ksc == kind::IMPLIES ? sc[0] : bv::utils::mkTrue(); + TS_ASSERT((k == BITVECTOR_ULT && pol == false) + || (k == BITVECTOR_SLT && pol == false) + || ksc == IMPLIES); + Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue(); if (!pol) { - k = k == kind::BITVECTOR_ULT - ? kind::BITVECTOR_UGE - : (k == kind::BITVECTOR_SLT ? kind::BITVECTOR_SGE : kind::DISTINCT); + k = k == BITVECTOR_ULT + ? BITVECTOR_UGE + : (k == BITVECTOR_SLT ? BITVECTOR_SGE : DISTINCT); } Node body = idx == 0 ? d_nm->mkNode(k, d_x, d_t) : d_nm->mkNode(k, d_t, d_x); - Node scr = d_nm->mkNode(kind::EXISTS, d_bvarlist, body); - Expr a = d_nm->mkNode(kind::DISTINCT, scl, scr).toExpr(); + Node scr = d_nm->mkNode(EXISTS, d_bvarlist, body); + Expr a = d_nm->mkNode(DISTINCT, scl, scr).toExpr(); Result res = d_smt->checkSat(a); TS_ASSERT(res.d_sat == Result::UNSAT); } - void runTest(Kind k, + void runTest(bool pol, + Kind litk, + Kind k, unsigned idx, - Node (*getsc)(Kind, unsigned, Node, Node, Node)) - { - Assert(k == kind::BITVECTOR_MULT - || k == kind::BITVECTOR_UREM_TOTAL - || k == kind::BITVECTOR_UDIV_TOTAL - || k == kind::BITVECTOR_AND - || k == kind::BITVECTOR_OR - || k == kind::BITVECTOR_LSHR - || k == kind::BITVECTOR_ASHR - || k == kind::BITVECTOR_SHL); - Assert(k != kind::BITVECTOR_UREM_TOTAL || idx == 1); - - Node sc = getsc(k, idx, d_sk, d_s, d_t); + Node (*getsc)(bool, Kind, Kind, unsigned, Node, Node, Node)) + { + Assert(k == BITVECTOR_MULT + || k == BITVECTOR_UREM_TOTAL + || k == BITVECTOR_UDIV_TOTAL + || k == BITVECTOR_AND + || k == BITVECTOR_OR + || k == BITVECTOR_LSHR + || k == BITVECTOR_ASHR + || k == BITVECTOR_SHL); + Assert(k != BITVECTOR_UREM_TOTAL || pol == false || idx == 1); + + Node sc = getsc(pol, litk, k, idx, d_sk, d_s, d_t); + TS_ASSERT (litk != EQUAL || sc != Node::null()); Kind ksc = sc.getKind(); - TS_ASSERT(ksc == kind::IMPLIES); + TS_ASSERT((k == BITVECTOR_UDIV_TOTAL && idx == 1 && pol == false) + || (k == BITVECTOR_ASHR && idx == 0 && pol == false) + || ksc == IMPLIES); + Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue(); Node body = idx == 0 - ? d_nm->mkNode(k, d_x, d_s).eqNode(d_t) - : d_nm->mkNode(k, d_s, d_x).eqNode(d_t); - Node scr = d_nm->mkNode(kind::EXISTS, d_bvarlist, body); - Expr a = d_nm->mkNode(kind::DISTINCT, sc[0], scr).toExpr(); + ? d_nm->mkNode(pol ? EQUAL : DISTINCT, d_nm->mkNode(k, d_x, d_s), d_t) + : d_nm->mkNode(pol ? EQUAL : DISTINCT, d_nm->mkNode(k, d_s, d_x), d_t); + Node scr = d_nm->mkNode(EXISTS, d_bvarlist, body); + Expr a = d_nm->mkNode(DISTINCT, scl, scr).toExpr(); Result res = d_smt->checkSat(a); if (res.d_sat == Result::SAT) { - std::cout << std::endl << "s " << d_smt->getValue(d_s.toExpr()) << std::endl; + std::cout << std::endl; + std::cout << "s " << d_smt->getValue(d_s.toExpr()) << std::endl; std::cout << "t " << d_smt->getValue(d_t.toExpr()) << std::endl; std::cout << "x " << d_smt->getValue(d_x.toExpr()) << std::endl; } @@ -119,7 +125,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite d_t = d_nm->mkVar("t", d_nm->mkBitVectorType(4)); d_sk = d_nm->mkSkolem("sk", d_t.getType()); d_x = d_nm->mkBoundVar(d_t.getType()); - d_bvarlist = d_nm->mkNode(kind::BOUND_VAR_LIST, { d_x }); + d_bvarlist = d_nm->mkNode(BOUND_VAR_LIST, { d_x }); } void tearDown() @@ -174,99 +180,163 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite runTestPred(false, BITVECTOR_SLT, 1, getScBvSlt); } - void testGetScBvEq0() + void testGetScBvMultEqTrue0() { - runTestPred(false, EQUAL, 0, getScBvEq); - TS_ASSERT_THROWS(runTestPred(true, EQUAL, 0, getScBvEq), - AssertionException); + runTest(true, EQUAL, BITVECTOR_MULT, 0, getScBvMult); } - void testGetScBvEq1() + void testGetScBvMultEqTrue1() { - runTestPred(false, EQUAL, 1, getScBvEq); - TS_ASSERT_THROWS(runTestPred(true, EQUAL, 1, getScBvEq), - AssertionException); + runTest(true, EQUAL, BITVECTOR_MULT, 1, getScBvMult); } - void testGetScBvMult0() + void testGetScBvMultEqFalse0() { - runTest(BITVECTOR_MULT, 0, getScBvMult); + runTest(false, EQUAL, BITVECTOR_MULT, 0, getScBvMult); } - void testGetScBvMult1() + void testGetScBvMultEqFalse1() { - runTest(BITVECTOR_MULT, 1, getScBvMult); + runTest(false, EQUAL, BITVECTOR_MULT, 1, getScBvMult); } - void testGetScBvUrem0() + void testGetScBvUremEqTrue0() { - TS_ASSERT_THROWS(runTest(BITVECTOR_UREM_TOTAL, 0, getScBvUrem), + TS_ASSERT_THROWS(runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 0, getScBvUrem), AssertionException); } - void testGetScBvUrem1() + void testGetScBvUremEqTrue1() + { + runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 1, getScBvUrem); + } + + void testGetScBvUremEqFalse0() + { + runTest(false, EQUAL, BITVECTOR_UREM_TOTAL, 0, getScBvUrem); + } + + void testGetScBvUremEqFalse1() + { + runTest(false, EQUAL, BITVECTOR_UREM_TOTAL, 1, getScBvUrem); + } + void testGetScBvUdivEqTrue0() + { + runTest(true, EQUAL, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv); + } + + void testGetScBvUdivEqTrue1() + { + runTest(true, EQUAL, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv); + } + + void testGetScBvUdivFalse0() { - runTest(BITVECTOR_UREM_TOTAL, 1, getScBvUrem); + runTest(false, EQUAL, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv); } - void testGetScBvUdiv0() + void testGetScBvUdivFalse1() { - runTest(BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv); + runTest(false, EQUAL, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv); } - void testGetScBvUdiv1() + void testGetScBvAndEqTrue0() { - runTest(BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv); + runTest(true, EQUAL, BITVECTOR_AND, 0, getScBvAndOr); } - void testGetScBvAnd0() + void testGetScBvAndEqTrue1() { - runTest(BITVECTOR_AND, 0, getScBvAndOr); + runTest(true, EQUAL, BITVECTOR_AND, 1, getScBvAndOr); } - void testGetScBvAnd1() + void testGetScBvAndEqFalse0() { - runTest(BITVECTOR_AND, 1, getScBvAndOr); + runTest(false, EQUAL, BITVECTOR_AND, 0, getScBvAndOr); } - void testGetScBvOr0() + void testGetScBvAndEqFalse1() { - runTest(BITVECTOR_OR, 0, getScBvAndOr); + runTest(false, EQUAL, BITVECTOR_AND, 1, getScBvAndOr); } - void testGetScBvOr1() + void testGetScBvOrEqTrue0() { - runTest(BITVECTOR_OR, 1, getScBvAndOr); + runTest(true, EQUAL, BITVECTOR_OR, 0, getScBvAndOr); } - void testGetScBvLshr0() + void testGetScBvOrEqTrue1() { - runTest(BITVECTOR_LSHR, 0, getScBvLshr); + runTest(true, EQUAL, BITVECTOR_OR, 1, getScBvAndOr); } - void testGetScBvLshr1() + void testGetScBvOrEqFalse0() { - runTest(BITVECTOR_LSHR, 1, getScBvLshr); + runTest(false, EQUAL, BITVECTOR_OR, 0, getScBvAndOr); } - void testGetScBvAshr0() + void testGetScBvOrEqFalse1() { - runTest(BITVECTOR_ASHR, 0, getScBvAshr); + runTest(false, EQUAL, BITVECTOR_OR, 1, getScBvAndOr); } - void testGetScBvAshr1() + void testGetScBvLshrEqTrue0() { - runTest(BITVECTOR_ASHR, 1, getScBvAshr); + runTest(true, EQUAL, BITVECTOR_LSHR, 0, getScBvLshr); } - void testGetScBvShl0() + void testGetScBvLshrEqTrue1() { - runTest(BITVECTOR_SHL, 0, getScBvShl); + runTest(true, EQUAL, BITVECTOR_LSHR, 1, getScBvLshr); } - void testGetScBvShl1() + void testGetScBvLshrEqFalse0() { - runTest(BITVECTOR_SHL, 1, getScBvShl); + runTest(false, EQUAL, BITVECTOR_LSHR, 0, getScBvLshr); } + void testGetScBvLshrEqFalse1() + { + runTest(false, EQUAL, BITVECTOR_LSHR, 1, getScBvLshr); + } + + void testGetScBvAshrEqTrue0() + { + runTest(true, EQUAL, BITVECTOR_ASHR, 0, getScBvAshr); + } + + void testGetScBvAshrEqTrue1() + { + runTest(true, EQUAL, BITVECTOR_ASHR, 1, getScBvAshr); + } + + void testGetScBvAshrEqFalse0() + { + runTest(false, EQUAL, BITVECTOR_ASHR, 0, getScBvAshr); + } + + void testGetScBvAshrEqFalse1() + { + runTest(false, EQUAL, BITVECTOR_ASHR, 1, getScBvAshr); + } + + void testGetScBvShlEqTrue0() + { + runTest(true, EQUAL, BITVECTOR_SHL, 0, getScBvShl); + } + + void testGetScBvShlEqTrue1() + { + runTest(true, EQUAL, BITVECTOR_SHL, 1, getScBvShl); + } + + void testGetScBvShlEqFalse0() + { + runTest(false, EQUAL, BITVECTOR_SHL, 0, getScBvShl); + } + + void testGetScBvShlEqFalse1() + { + runTest(false, EQUAL, BITVECTOR_SHL, 1, getScBvShl); + } }; |