diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-10-10 18:08:56 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-10-10 18:08:56 -0400 |
commit | 4e91f51cb0e58a9d2d8c1f12e387ca2455d307e4 (patch) | |
tree | 98c74cefa8faa2cbf7aced5c21c2d85e6d8fe665 /test/regress/regress0 | |
parent | 089d232454e89dc44a6ca2136f9b408c9335d8f1 (diff) | |
parent | 5527b0c00639f24b11d5e1d4c69050d908b82400 (diff) |
Merge remote-tracking branch 'origin/1.4.x'
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/trim.cvc | 36 |
2 files changed, 38 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 89b620655..e7b8e3b73 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -106,7 +106,8 @@ CVC_TESTS = \ wiki.20.cvc \ wiki.21.cvc \ queries0.cvc \ - print_lambda.cvc + print_lambda.cvc \ + trim.cvc # Regression tests for TPTP inputs TPTP_TESTS = diff --git a/test/regress/regress0/trim.cvc b/test/regress/regress0/trim.cvc new file mode 100644 index 000000000..8bdbde79a --- /dev/null +++ b/test/regress/regress0/trim.cvc @@ -0,0 +1,36 @@ +% COMMAND-LINE: --finite-model-find +% EXPECT: sat +DATATYPE + myType = A | B +END; +%%% structured datatypes +myTypeSet: TYPE = SET OF myType; +myTypeGammaSet: TYPE = [# pos: myTypeSet, neg: myTypeSet #]; +delta: TYPE = ARRAY myType OF myTypeGammaSet; +labels: TYPE = ARRAY myType OF SET OF STRING; + +%%% the empty myTypes set +emptymyTypeSet : SET OF myType; +ASSERT emptymyTypeSet = {} :: SET OF myType; + +d: delta; +l: labels; + +ASSERT (l[A] = {"L","H"}); +ASSERT (l[B] = {"L"}); + +ic0_i : myTypeSet; +ic0_c : myTypeSet; +ASSERT FORALL (r:myType): + (r IS_IN ic0_i) => FORALL (r2: myType): (r2 IS_IN d[r].neg) => r2 IS_IN ic0_c; +ASSERT {A} <= ic0_i; +ASSERT ((EXISTS (e0 : myType): (e0 IS_IN ic0_i) => (l[A] <= l[e0]))) OR ((ic0_i & ic0_c) <= emptymyTypeSet); + +ic1_i : myTypeSet; +ic1_c : myTypeSet; +ASSERT FORALL (r:myType): + (r IS_IN d[B].pos) => r IS_IN ic1_i; +ASSERT ((EXISTS (e1 : myType): (e1 IS_IN ic1_i) => (l[B] <= l[e1]))) OR ((ic1_i & ic1_c) <= emptymyTypeSet); + +CHECKSAT; +%COUNTEREXAMPLE; |