New implementation of sets+cardinality. Merge Paul Meng's relation solver as extension of sets solver, add regressions.

1 files changed, 12 insertions, 0 deletions

diff --git a/test/regress/regress0/rels/rel_transpose_1.cvc b/test/regress/regress0/rels/rel_transpose_1.cvc
new file mode 100644
index 000000000..bdcf31bb8
--- /dev/null
+++ b/test/regress/regress0/rels/rel_transpose_1.cvc
@@ -0,0 +1,12 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntTup: TYPE = [INT, INT, INT];
+x : SET OF IntTup;
+y : SET OF IntTup;
+z : IntTup;
+ASSERT z = (1,2,3);
+zt : IntTup;
+ASSERT zt = (3,2,1);
+ASSERT z IS_IN x;
+ASSERT NOT (zt IS_IN (TRANSPOSE x));
+CHECKSAT;