refactored the code

- send out facts as lemmas
- fixed the non-termination problem caused by sending facts as lemmas
- unfolded symbolic tuples by adding equality lemmas

7 files changed, 110 insertions, 6 deletions

diff --git a/test/regress/regress0/sets/rels/rel_join_0_1.cvc b/test/regress/regress0/sets/rels/rel_join_0_1.cvc
index 70e35164a..a7fa7efb9 100644
--- a/test/regress/regress0/sets/rels/rel_join_0_1.cvc
+++ b/test/regress/regress0/sets/rels/rel_join_0_1.cvc
@@ -15,6 +15,7 @@ a : IntPair;
 ASSERT a = (1,5);
 
 ASSERT (1, 7) IS_IN x;
+ASSERT (4, 3) IS_IN x;
 ASSERT (7, 5) IS_IN y;
 
 ASSERT z IS_IN x;
diff --git a/test/regress/regress0/sets/rels/rel_symbolic_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_1.cvc
new file mode 100644
index 000000000..08ed32411
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_symbolic_1.cvc
@@ -0,0 +1,21 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+f : INT;
+d : IntPair;
+ASSERT d = (f,3);
+ASSERT d IS_IN y;
+e : IntPair;
+ASSERT e = (4, f);
+ASSERT e IS_IN x;
+
+a : IntPair;
+ASSERT a = (4,3);
+
+ASSERT r = (x JOIN y);
+
+ASSERT NOT (a IS_IN r);
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc
new file mode 100644
index 000000000..df2d7f412
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc
@@ -0,0 +1,20 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+d : IntPair;
+ASSERT d IS_IN y;
+
+a : IntPair;
+ASSERT a IS_IN x;
+
+e : IntPair;
+ASSERT e = (4,3);
+
+ASSERT r = (x JOIN y);
+
+ASSERT NOT (e IS_IN r);
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_tp_join_1.cvc b/test/regress/regress0/sets/rels/rel_tp_join_1.cvc
index dca0a3bfa..60b6edf58 100644
--- a/test/regress/regress0/sets/rels/rel_tp_join_1.cvc
+++ b/test/regress/regress0/sets/rels/rel_tp_join_1.cvc
@@ -6,12 +6,20 @@ y : SET OF IntPair;
 z : SET OF IntPair;
 r : SET OF IntPair;
 
-ASSERT (1, 7) IS_IN x;
-ASSERT (2, 3) IS_IN x;
+b : IntPair;
+ASSERT b = (1,7);
+c : IntPair;
+ASSERT c = (2,3);
+ASSERT b IS_IN x;
+ASSERT c IS_IN x;
 
+d : IntPair;
+ASSERT d = (7,3);
+e : IntPair;
+ASSERT e = (4,7);
 
-ASSERT (7, 3) IS_IN y;
-ASSERT (4, 7) IS_IN y;
+ASSERT d IS_IN y;
+ASSERT e IS_IN y;
 
 ASSERT (3, 4) IS_IN z;
 
diff --git a/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc
new file mode 100644
index 000000000..54e16dd51
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc
@@ -0,0 +1,28 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+
+
+ASSERT x = {(1,7), (2,3)};
+
+d : IntPair;
+ASSERT d = (7,3);
+e : IntPair;
+ASSERT e = (4,7);
+
+ASSERT d IS_IN y;
+ASSERT e IS_IN y;
+
+ASSERT (3, 4) IS_IN z;
+
+a : IntPair;
+ASSERT a = (4,1);
+
+ASSERT r = ((x JOIN y) JOIN z);
+
+ASSERT NOT (a IS_IN (TRANSPOSE r));
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_tp_join_int.cvc b/test/regress/regress0/sets/rels/rel_tp_join_int.cvc
new file mode 100644
index 000000000..8d149a48d
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_int.cvc
@@ -0,0 +1,26 @@
+% EXPECT: unsat
+% crash on this
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+w : SET OF IntPair;
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+
+t : INT;
+u : INT;
+
+ASSERT 4 < t AND t < 6;
+ASSERT 4 < u AND u < 6;
+
+ASSERT (1, u) IS_IN x;
+ASSERT (t, 3) IS_IN y;
+
+a : IntPair;
+ASSERT a = (1,3);
+
+ASSERT NOT (a IS_IN  (x JOIN y));
+
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_tp_join_var.cvc b/test/regress/regress0/sets/rels/rel_tp_join_var.cvc
index c7757bd3e..aacf6c054 100644
--- a/test/regress/regress0/sets/rels/rel_tp_join_var.cvc
+++ b/test/regress/regress0/sets/rels/rel_tp_join_var.cvc
@@ -13,8 +13,8 @@ u : INT;
 ASSERT 4 < t AND t < 6;
 ASSERT 4 < u AND u < 6;
 
-ASSERT (1, u) IS_IN x;
-ASSERT (t, 3) IS_IN y;
+ASSERT (1, t) IS_IN x;
+ASSERT (u, 3) IS_IN y;
 
 a : IntPair;
 ASSERT a = (1,3);