summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2017-12-20 18:27:39 -0800
committerGitHub <noreply@github.com>2017-12-20 18:27:39 -0800
commitf9149d3b3e785950a846fb195bf9fa9cb1a2d94a (patch)
treec69c90377a6c24abbc9c608a767507740abfd3b6 /test
parent13cc0e94ac8892fa1cefa53ff1c884d154894b58 (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')
-rw-r--r--test/regress/regress0/quantifiers/Makefile.am39
-rw-r--r--test/regress/regress0/quantifiers/qbv-disequality3.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-inequality2.smt29
-rw-r--r--test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt22
-rw-r--r--test/regress/regress0/quantifiers/qbv-simp.smt28
-rw-r--r--test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt216
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt28
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt28
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt28
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt28
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt28
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt211
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt211
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt211
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1.smt2 (renamed from test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2)2
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt26
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt28
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt29
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt26
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt28
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt28
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-mul.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-shl.smt210
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt28
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt211
-rw-r--r--test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt22
-rw-r--r--test/unit/theory/theory_quantifiers_bv_inverter_white.h218
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);
+ }
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback