diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 13:35:07 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-01 13:35:07 -0500 |
commit | 13e452be03bef09e2f54f42e2bc42383505ffcea (patch) | |
tree | 39695fe22d387bc84bc49d20831a19648d55011f /test/regress | |
parent | be11fae39055f213586058ec9129d1276f724b0e (diff) |
CBQI BV choice expressions (#1296)
* Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently.
* Minor
* Make unique bound variables for choice functions in BvInstantor, clean up.
* Incorporate missing optimizations
* Clang format
* Unused field.
* Minor
* Fix, add regression.
* Fix regression.
* Fix bug that led to incorrect cleanup of instantiations.
* Add missing regression
* Improve handling of choice rewriting.
* Fix
* Clang format
* Use canonical variables for choice functions in cbqi bv.
* Add regression
* Clang format.
* Address review.
* Clang format
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 5 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/NUM878.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/ari118-bv-2occ-x.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/psyco-107-bv.smt2 | 162 |
4 files changed, 181 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 4cfdec90e..014f06aad 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -111,7 +111,10 @@ TESTS = \ qbv-test-invert-bvult-1.smt2 \ intersection-example-onelane.proof-node22337.smt2 \ nested9_true-unreach-call.i_575.smt2 \ - small-pipeline-fixpoint-3.smt2 + small-pipeline-fixpoint-3.smt2 \ + NUM878.smt2 \ + psyco-107-bv.smt2 \ + ari118-bv-2occ-x.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/NUM878.smt2 b/test/regress/regress0/quantifiers/NUM878.smt2 new file mode 100644 index 000000000..8d78bf861 --- /dev/null +++ b/test/regress/regress0/quantifiers/NUM878.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(assert (not (exists ((?X (_ BitVec 32))) (= (bvmul ?X ?X) ?X)))) +(check-sat) +(exit) diff --git a/test/regress/regress0/quantifiers/ari118-bv-2occ-x.smt2 b/test/regress/regress0/quantifiers/ari118-bv-2occ-x.smt2 new file mode 100644 index 000000000..2d70dfb8e --- /dev/null +++ b/test/regress/regress0/quantifiers/ari118-bv-2occ-x.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +; two occurrences of x +(assert (not (exists ((?X (_ BitVec 32)) (?Y (_ BitVec 32))) (= (bvmul ?X ?Y) ?X)))) +(check-sat) +(exit) diff --git a/test/regress/regress0/quantifiers/psyco-107-bv.smt2 b/test/regress/regress0/quantifiers/psyco-107-bv.smt2 new file mode 100644 index 000000000..82b54a231 --- /dev/null +++ b/test/regress/regress0/quantifiers/psyco-107-bv.smt2 @@ -0,0 +1,162 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=eq-boundary +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun W_S1_V6 () Bool) +(declare-fun W_S1_V4 () Bool) +(declare-fun W_S1_V2 () Bool) +(declare-fun W_S1_V3 () Bool) +(declare-fun W_S1_V1 () Bool) +(declare-fun R_E2_V1 () Bool) +(declare-fun R_E2_V3 () Bool) +(declare-fun R_E1_V3 () Bool) +(declare-fun R_E1_V1 () Bool) +(declare-fun R_E1_V6 () Bool) +(declare-fun R_E1_V4 () Bool) +(declare-fun R_E1_V5 () Bool) +(declare-fun R_E1_V2 () Bool) +(declare-fun DISJ_W_S1_R_E1 () Bool) +(declare-fun R_S1_V6 () Bool) +(declare-fun R_S1_V4 () Bool) +(declare-fun R_S1_V5 () Bool) +(declare-fun R_S1_V2 () Bool) +(declare-fun R_S1_V3 () Bool) +(declare-fun R_S1_V1 () Bool) +(declare-fun DISJ_W_S1_R_S1 () Bool) +(declare-fun R_E2_V6 () Bool) +(declare-fun R_E2_V4 () Bool) +(declare-fun R_E2_V5 () Bool) +(declare-fun R_E2_V2 () Bool) +(declare-fun DISJ_W_S1_R_E2 () Bool) +(declare-fun W_S1_V5 () Bool) +(assert + (let + (($x59848 + (forall + ((V1_0 (_ BitVec 32)) (V3_0 (_ BitVec 32)) + (V2_0 (_ BitVec 32)) (V5_0 (_ BitVec 32)) + (V4_0 (_ BitVec 32)) (V6_0 (_ BitVec 32)) + (MW_S1_V1 Bool) (MW_S1_V3 Bool) + (MW_S1_V2 Bool) (MW_S1_V5 Bool) + (MW_S1_V4 Bool) (MW_S1_V6 Bool) + (S1_V1_!5000 (_ BitVec 32)) (S1_V3_!5001 (_ BitVec 32)) + (S1_V2_!5002 (_ BitVec 32)) (E1_!4994 (_ BitVec 32)) + (E1_!4997 (_ BitVec 32)) (E1_!4999 (_ BitVec 32)) + (S1_V5_!5003 (_ BitVec 32)) (E2_!4995 (_ BitVec 32)) + (E2_!4996 (_ BitVec 32)) (E2_!4998 (_ BitVec 32)) + (S1_V4_!5004 (_ BitVec 32)) (S1_V6_!5005 (_ BitVec 32))) + (let ((?x62719 (ite MW_S1_V6 S1_V6_!5005 V6_0))) + (let (($x60064 (= V6_0 ?x62719))) + (let ((?x61425 (ite MW_S1_V4 S1_V4_!5004 V4_0))) + (let (($x59873 (= V4_0 ?x61425))) + (let ((?x59861 (ite MW_S1_V5 S1_V5_!5003 V5_0))) + (let (($x62312 (= V5_0 ?x59861))) + (let ((?x60966 (ite MW_S1_V2 S1_V2_!5002 V2_0))) + (let (($x61331 (= V2_0 ?x60966))) + (let ((?x62280 (ite MW_S1_V3 S1_V3_!5001 E2_!4998))) + (let ((?x60903 (bvadd (_ bv1 32) ?x62280))) + (let (($x61268 (= E2_!4996 ?x60903))) + (let ((?x60065 (ite MW_S1_V1 S1_V1_!5000 E1_!4999))) + (let (($x60169 (= E1_!4994 ?x60065))) + (let (($x62661 (and $x60169 $x61268 $x61331 $x62312 $x59873 $x60064))) + (let ((?x62301 (bvadd (bvneg (_ bv1 32)) ?x61425))) + (let (($x61124 (bvsge ?x62280 ?x62301))) + (let ((?x61096 (bvadd (bvneg (_ bv1 32)) ?x60966))) + (let (($x60960 (bvsge ?x60065 ?x61096))) + (let (($x62453 (bvsle V2_0 E1_!4999))) + (let (($x61140 (not $x62453))) + (let (($x60239 (bvsle V4_0 E2_!4998))) + (let (($x61367 (not $x60239))) + (let (($x59857 (bvsle V2_0 E1_!4997))) + (let (($x62570 (not $x59857))) + (let ((?x62418 (bvadd (bvneg (_ bv1 32)) V2_0))) + (let (($x60189 (bvsge E1_!4994 ?x62418))) + (let (($x62421 (bvsge E2_!4996 V4_0))) + (let (($x60898 (bvsle V2_0 E1_!4994))) + (let (($x59938 (not $x60898))) + (let (($x62400 (bvsle V4_0 E2_!4995))) + (let (($x60971 (not $x62400))) + (let + (($x62394 + (and $x60971 $x59938 $x62421 $x60189 $x62570 $x61367 $x61140 $x60960 + $x61124))) + (let (($x62485 (not $x62394))) + (let (($x60905 (not MW_S1_V6))) + (let (($x61285 (or $x60905 W_S1_V6))) + (let (($x61317 (not MW_S1_V4))) + (let (($x60137 (or $x61317 W_S1_V4))) + (let (($x62306 (not MW_S1_V2))) + (let (($x62708 (or $x62306 W_S1_V2))) + (let (($x62310 (not MW_S1_V3))) + (let (($x60291 (or $x62310 W_S1_V3))) + (let (($x62641 (not MW_S1_V1))) + (let (($x61174 (or $x62641 W_S1_V1))) + (let (($x62627 (= E2_!4998 E2_!4995))) + (let (($x60904 (= E1_!4997 E1_!4994))) + (let (($x128 (not R_E2_V1))) + (let (($x60161 (or $x128 $x60904))) + (let (($x62415 (not $x60161))) + (let (($x62645 (or $x62415 $x62627))) + (let (($x60924 (= E2_!4996 E2_!4998))) + (let (($x62711 (= E2_!4995 V3_0))) + (let (($x130 (not R_E2_V3))) + (let (($x62623 (or $x130 $x62711))) + (let (($x60954 (= E1_!4994 E1_!4997))) + (let (($x59868 (or $x128 $x60954))) + (let (($x62319 (and $x59868 $x62623))) + (let (($x62554 (not $x62319))) + (let (($x60985 (or $x62554 $x60924))) + (let (($x62256 (= E2_!4996 E2_!4995))) + (let (($x62540 (not $x62623))) + (let (($x60968 (or $x62540 $x62256))) + (let (($x62486 (= E1_!4999 E1_!4997))) + (let (($x60109 (= E2_!4998 V3_0))) + (let (($x115 (not R_E1_V3))) + (let (($x60129 (or $x115 $x60109))) + (let (($x60976 (= E1_!4997 V1_0))) + (let (($x113 (not R_E1_V1))) + (let (($x62568 (or $x113 $x60976))) + (let (($x60942 (and $x62568 $x60129))) + (let (($x60209 (not $x60942))) + (let (($x62263 (or $x60209 $x62486))) + (let (($x60965 (= E1_!4999 E1_!4994))) + (let (($x62348 (or $x60209 $x60965))) + (let + (($x60285 + (and $x60954 $x62348 $x62263 $x60968 $x60985 $x62645 $x61174 $x60291 + $x62708 $x60137 $x61285))) + (let (($x62430 (not $x60285))) (or $x62430 $x62485 $x62661))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + (let (($x56 (and W_S1_V6 R_E1_V6))) + (let (($x54 (and W_S1_V4 R_E1_V4))) + (let (($x50 (and W_S1_V2 R_E1_V2))) + (let (($x48 (and W_S1_V3 R_E1_V3))) + (let (($x46 (and W_S1_V1 R_E1_V1))) + (let (($x69 (or $x46 $x48 $x50 R_E1_V5 $x54 $x56))) + (let (($x70 (not $x69))) + (let (($x71 (= DISJ_W_S1_R_E1 $x70))) + (let (($x40 (and W_S1_V6 R_S1_V6))) + (let (($x38 (and W_S1_V4 R_S1_V4))) + (let (($x34 (and W_S1_V2 R_S1_V2))) + (let (($x32 (and W_S1_V3 R_S1_V3))) + (let (($x30 (and W_S1_V1 R_S1_V1))) + (let (($x66 (or $x30 $x32 $x34 R_S1_V5 $x38 $x40))) + (let (($x67 (not $x66))) + (let (($x68 (= DISJ_W_S1_R_S1 $x67))) + (let (($x24 (and W_S1_V6 R_E2_V6))) + (let (($x21 (and W_S1_V4 R_E2_V4))) + (let (($x16 (and W_S1_V2 R_E2_V2))) + (let (($x13 (and W_S1_V3 R_E2_V3))) + (let (($x10 (and W_S1_V1 R_E2_V1))) + (let (($x63 (or $x10 $x13 $x16 R_E2_V5 $x21 $x24))) + (let (($x64 (not $x63))) + (let (($x65 (= DISJ_W_S1_R_E2 $x64))) + (let (($x130 (not R_E2_V3))) + (let (($x115 (not R_E1_V3))) + (let (($x113 (not R_E1_V1))) + (let (($x60916 (and $x113 $x115))) + (let (($x62291 (or $x60916 $x130))) + (and $x62291 W_S1_V5 $x65 $x68 $x71 $x59848)))))))))))))))))))))))))))))))) +(assert R_E2_V3) +(check-sat) +(exit) + |