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

1 files changed, 24 insertions, 0 deletions

diff --git a/test/regress/regress0/rels/set-strat.cvc b/test/regress/regress0/rels/set-strat.cvc
new file mode 100644
index 000000000..0dee0e84d
--- /dev/null
+++ b/test/regress/regress0/rels/set-strat.cvc
@@ -0,0 +1,24 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [ INT, INT];
+SetIntPair: TYPE = [ SET OF IntPair, SET OF IntPair ];
+x : SET OF IntPair;
+y : SET OF IntPair;
+w : SET OF IntPair;
+z : SET OF SetIntPair;
+
+a : IntPair;
+b : IntPair;
+
+ASSERT NOT a = b;
+
+ASSERT a IS_IN x;
+ASSERT b IS_IN y;
+ASSERT b IS_IN w;
+ASSERT (x,y) IS_IN z;
+ASSERT (w,x) IS_IN z;
+ASSERT NOT ( (x,x) IS_IN (z JOIN z) );
+
+ASSERT (x, { ( 0, 0 ) } ) IS_IN (z JOIN z);
+
+CHECKSAT;