summaryrefslogtreecommitdiff
path: root/test/regress/regress0/rels/rel_complex_1.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/rels/rel_complex_1.cvc')
-rw-r--r--test/regress/regress0/rels/rel_complex_1.cvc34
1 files changed, 34 insertions, 0 deletions
diff --git a/test/regress/regress0/rels/rel_complex_1.cvc b/test/regress/regress0/rels/rel_complex_1.cvc
new file mode 100644
index 000000000..969d0d71c
--- /dev/null
+++ b/test/regress/regress0/rels/rel_complex_1.cvc
@@ -0,0 +1,34 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+w : SET OF IntTup;
+z : SET OF IntTup;
+r2 : SET OF IntPair;
+
+a : IntPair;
+ASSERT a = (3,1);
+ASSERT a IS_IN x;
+
+d : IntPair;
+ASSERT d = (1,3);
+ASSERT d IS_IN y;
+
+e : IntPair;
+ASSERT e = (4,3);
+ASSERT r = (x JOIN y);
+
+ASSERT TUPLE(1) IS_IN w;
+ASSERT TUPLE(2) IS_IN z;
+ASSERT r2 = (w PRODUCT z);
+
+ASSERT NOT (e IS_IN r);
+%ASSERT e IS_IN r2;
+ASSERT (r <= r2);
+ASSERT NOT ((3,3) IS_IN r2);
+
+CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback