diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-26 16:23:58 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-26 16:23:58 -0500 |
commit | 031722bee8682005bd4c8700ef78b5f893fc48fe (patch) | |
tree | 46a936a1bd20ea2cc588df0d3205cf7eb0fd4177 /test/regress/regress0/rels/prod-mod-eq2.cvc | |
parent | e79e64329ce7d6df0003cab28dadb9b8bcc6f9ca (diff) |
New implementation of sets+cardinality. Merge Paul Meng's relation solver as extension of sets solver, add regressions.
Diffstat (limited to 'test/regress/regress0/rels/prod-mod-eq2.cvc')
-rw-r--r-- | test/regress/regress0/rels/prod-mod-eq2.cvc | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test/regress/regress0/rels/prod-mod-eq2.cvc b/test/regress/regress0/rels/prod-mod-eq2.cvc new file mode 100644 index 000000000..b9341a216 --- /dev/null +++ b/test/regress/regress0/rels/prod-mod-eq2.cvc @@ -0,0 +1,26 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntPairPair: TYPE = [INT, INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPairPair; +z1 : SET OF IntPair; +w1 : SET OF IntPair; +z2 : SET OF IntPair; +w2 : SET OF IntPair; +P : SET OF IntPairPair -> BOOLEAN; + +ASSERT z = (x PRODUCT y); + +ASSERT P( z ); +ASSERT NOT P( {(0,1,2,3)} ); + +ASSERT (0,1) IS_IN z1; +ASSERT (0,1) IS_IN z2; +ASSERT (2,3) IS_IN w1; +ASSERT (2,3) IS_IN w2; + +ASSERT ( x = z1 AND y = w1 ) OR ( x = z2 AND y = w2 ); + +CHECKSAT; |