diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-24 17:01:38 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-24 17:01:38 -0500 |
| commit | 22916321f5c26fdc632df24f3c1fef45beaeb918 (patch) | |
| tree | a8a43b5aea9b8a4efbe5069eacb720e5506fc423 /test | |
| parent | 25d3eea9614a0882a5c18c455e5a14d118a78dce (diff) | |
Improvements to sets + cardinality + quantifiers (#2200)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 2 | ||||
| -rw-r--r-- | test/regress/regress1/fmf/radu-quant-set.smt2 | 18 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/set-choice-koikonomou.cvc | 10 |
3 files changed, 30 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index cef27bc72..48b290bfe 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1104,6 +1104,7 @@ REG1_TESTS = \ regress1/fmf/nlp042+1.smt2 \ regress1/fmf/nun-0208-to.smt2 \ regress1/fmf/pow2-bool.smt2 \ + regress1/fmf/radu-quant-set.smt2 \ regress1/fmf/refcount24.cvc.smt2 \ regress1/fmf/sc-crash-052316.smt2 \ regress1/fmf/with-ind-104-core.smt2 \ @@ -1309,6 +1310,7 @@ REG1_TESTS = \ regress1/quantifiers/rew-to-0211-dd.smt2 \ regress1/quantifiers/ricart-agrawala6.smt2 \ regress1/quantifiers/set8.smt2 \ + regress1/quantifiers/set-choice-koikonomou.cvc \ regress1/quantifiers/small-pipeline-fixpoint-3.smt2 \ regress1/quantifiers/smtcomp-qbv-053118.smt2 \ regress1/quantifiers/smtlib384a03.smt2 \ diff --git a/test/regress/regress1/fmf/radu-quant-set.smt2 b/test/regress/regress1/fmf/radu-quant-set.smt2 new file mode 100644 index 000000000..09d5cc706 --- /dev/null +++ b/test/regress/regress1/fmf/radu-quant-set.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --fmf-bound +; EXPECT: unsat +(set-logic ALL_SUPPORTED) + +(declare-const A (Set Int)) +(declare-const B (Set Int)) + +(define-fun F () Bool + (exists ((i Int) (j Int)) (and (distinct i j) (member i A) (member j B))) +) + +(define-fun G () Bool + (and (>= (card (union A B)) 2) (>= (card A) 1) (>= (card B) 1)) +) + +(assert (and G (not F))) + +(check-sat) diff --git a/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc b/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc new file mode 100644 index 000000000..f7407a2a5 --- /dev/null +++ b/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc @@ -0,0 +1,10 @@ +% EXPECT: valid +OPTION "finite-model-find"; +OPTION "fmf-bound-int"; + +X : SET OF INT; + +ASSERT CARD(X) = 3; +ASSERT FORALL(z: INT): z IS_IN X => (z > 0 AND z < 2); % 1 + +QUERY FORALL(z: INT): z IS_IN X => z > 0; |