Support for relational operators identity and join image

11 files changed, 282 insertions, 1 deletions

diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am
index bb9c49298..d1c035371 100644
--- a/test/regress/regress0/rels/Makefile.am
+++ b/test/regress/regress0/rels/Makefile.am
@@ -102,7 +102,17 @@ TESTS =	\
   set-strat.cvc \
   rel_tc_8.cvc \
   atom_univ2.cvc \
-  rels-sharing-simp.cvc
+  rels-sharing-simp.cvc \
+  iden_0.cvc \
+  iden_1_1.cvc \
+  iden_1.cvc \
+  joinImg_0_1.cvc \
+  joinImg_0_2.cvc \
+  joinImg_0.cvc \
+  joinImg_1_1.cvc \
+  joinImg_1.cvc \
+  joinImg_2_1.cvc \
+  joinImg_2.cvc  
 
 # unsolved : garbage_collect.cvc
 
diff --git a/test/regress/regress0/rels/iden_0.cvc b/test/regress/regress0/rels/iden_0.cvc
new file mode 100644
index 000000000..4c2693084
--- /dev/null
+++ b/test/regress/regress0/rels/iden_0.cvc
@@ -0,0 +1,28 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+id : SET OF IntPair;
+
+t : SET OF [INT];
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+
+ASSERT TUPLE(1) IS_IN t;
+ASSERT TUPLE(2) IS_IN t;
+ASSERT z IS_IN x;
+ASSERT zt IS_IN x;
+ASSERT v IS_IN x;
+ASSERT a IS_IN x;
+ASSERT id = IDEN(t);
+ASSERT NOT ((1, 1) IS_IN (id & x));
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/iden_1.cvc b/test/regress/regress0/rels/iden_1.cvc
new file mode 100644
index 000000000..f73700e88
--- /dev/null
+++ b/test/regress/regress0/rels/iden_1.cvc
@@ -0,0 +1,18 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom:TYPE;
+AtomPair: TYPE = [Atom, Atom];
+x : SET OF AtomPair;
+t : SET OF [Atom];
+univ : SET OF [Atom];
+
+a : Atom;
+b : Atom;
+c : Atom;
+d : Atom;
+ASSERT univ = UNIVERSE::SET OF [Atom];
+ASSERT (a, b) IS_IN x;
+ASSERT (c, d) IS_IN x;
+ASSERT NOT(a = b);
+ASSERT IDEN(x JOIN univ) = x;
+CHECKSAT;
diff --git a/test/regress/regress0/rels/iden_1_1.cvc b/test/regress/regress0/rels/iden_1_1.cvc
new file mode 100644
index 000000000..d118f15dd
--- /dev/null
+++ b/test/regress/regress0/rels/iden_1_1.cvc
@@ -0,0 +1,21 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+Atom:TYPE;
+AtomPair: TYPE = [Atom, Atom];
+x : SET OF AtomPair;
+t : SET OF [Atom];
+univ : SET OF [Atom];
+univ2 : SET OF [Atom,Atom];
+
+a : Atom;
+b : Atom;
+c : Atom;
+d : Atom;
+ASSERT univ = UNIVERSE::SET OF [Atom];
+ASSERT univ2 = UNIVERSE::SET OF [Atom, Atom];
+ASSERT univ2 = (univ PRODUCT univ);
+ASSERT (a, b) IS_IN x;
+ASSERT (c, d) IS_IN x;
+ASSERT NOT(a = b);
+ASSERT IDEN(univ) <= x;
+CHECKSAT;
diff --git a/test/regress/regress0/rels/joinImg_0.cvc b/test/regress/regress0/rels/joinImg_0.cvc
new file mode 100644
index 000000000..e36c6a647
--- /dev/null
+++ b/test/regress/regress0/rels/joinImg_0.cvc
@@ -0,0 +1,33 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+t : SET OF [INT];
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT z IS_IN x;
+
+ASSERT (7, 5) IS_IN y;
+
+ASSERT t = (x JOIN_IMAGE 2);
+
+ASSERT TUPLE(3) IS_IN (x JOIN_IMAGE 2);
+
+ASSERT NOT(TUPLE(1) IS_IN (x JOIN_IMAGE 2));
+
+ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2);
+
+ASSERT TUPLE(1) IS_IN (x JOIN_IMAGE 1);
+CHECKSAT;
diff --git a/test/regress/regress0/rels/joinImg_0_1.cvc b/test/regress/regress0/rels/joinImg_0_1.cvc
new file mode 100644
index 000000000..602c4fe3f
--- /dev/null
+++ b/test/regress/regress0/rels/joinImg_0_1.cvc
@@ -0,0 +1,35 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+t : SET OF [INT];
+u : SET OF [INT];
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+v : IntPair;
+ASSERT v = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+b: INT;
+
+ASSERT (1, 7) IS_IN x;
+ASSERT z IS_IN x;
+
+ASSERT (7, 5) IS_IN y;
+
+ASSERT t = (x JOIN_IMAGE 2);
+
+ASSERT TUPLE(3) IS_IN (x JOIN_IMAGE 2);
+
+ASSERT u = (x JOIN_IMAGE 1);
+
+ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2);
+
+ASSERT TUPLE(b) IS_IN (x JOIN_IMAGE 1);
+CHECKSAT;
diff --git a/test/regress/regress0/rels/joinImg_0_2.cvc b/test/regress/regress0/rels/joinImg_0_2.cvc
new file mode 100644
index 000000000..f71069217
--- /dev/null
+++ b/test/regress/regress0/rels/joinImg_0_2.cvc
@@ -0,0 +1,38 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+t : SET OF [INT];
+u : SET OF [INT];
+univ : SET OF [INT];
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+s : IntPair;
+ASSERT s = (1,1);
+a : IntPair;
+ASSERT a = (1,5);
+b: INT;
+
+ASSERT (1, 7) IS_IN x;
+ASSERT z IS_IN x;
+
+ASSERT (7, 5) IS_IN y;
+
+ASSERT t = (x JOIN_IMAGE 2);
+ASSERT univ = (x JOIN_IMAGE 0);
+ASSERT TUPLE(100) IS_IN t;
+
+ASSERT NOT (TUPLE(3) IS_IN univ);
+
+ASSERT u = (x JOIN_IMAGE 1);
+
+ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2);
+
+ASSERT TUPLE(b) IS_IN (x JOIN_IMAGE 1);
+CHECKSAT;
diff --git a/test/regress/regress0/rels/joinImg_1.cvc b/test/regress/regress0/rels/joinImg_1.cvc
new file mode 100644
index 000000000..47e57c1fb
--- /dev/null
+++ b/test/regress/regress0/rels/joinImg_1.cvc
@@ -0,0 +1,20 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+x : SET OF [Atom, Atom];
+y : SET OF [Atom, Atom];
+r : SET OF [Atom, Atom];
+
+t : SET OF [Atom];
+
+a : Atom;
+b : Atom;
+c : Atom;
+d : Atom;
+e : Atom;
+
+ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
+ASSERT x = {(b, c), (d, e), (c, e)};
+ASSERT NOT(a = b);
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/joinImg_1_1.cvc b/test/regress/regress0/rels/joinImg_1_1.cvc
new file mode 100644
index 000000000..a7927f7e2
--- /dev/null
+++ b/test/regress/regress0/rels/joinImg_1_1.cvc
@@ -0,0 +1,21 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+x : SET OF [Atom, Atom];
+y : SET OF [Atom, Atom];
+r : SET OF [Atom, Atom];
+
+t : SET OF [Atom];
+
+a : Atom;
+b : Atom;
+c : Atom;
+d : Atom;
+e : Atom;
+
+ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
+ASSERT t = (x JOIN_IMAGE 2); 
+ASSERT x = {(b, c), (d, e), (c, e)};
+ASSERT TUPLE(c) IS_IN t;
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/joinImg_2.cvc b/test/regress/regress0/rels/joinImg_2.cvc
new file mode 100644
index 000000000..bbf57629b
--- /dev/null
+++ b/test/regress/regress0/rels/joinImg_2.cvc
@@ -0,0 +1,33 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+x : SET OF [Atom, Atom];
+y : SET OF [Atom, Atom];
+r : SET OF [Atom, Atom];
+
+t : SET OF [Atom];
+
+a : Atom;
+b : Atom;
+c : Atom;
+d : Atom;
+e : Atom;
+f : Atom;
+g : Atom;
+
+ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
+ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 3);
+%ASSERT y = {(f, g), (b, c), (d, e), (c, e)};
+ASSERT x = {(f, g), (b, c), (d, e), (c, e), (f, b)};
+ASSERT (a, f) IS_IN x;
+ASSERT (a, f) IS_IN y;
+ASSERT x = y;
+
+
+
+ASSERT NOT(a = b);
+
+ASSERT NOT (TUPLE(d) IS_IN (x JOIN_IMAGE 2));
+ASSERT f = d;
+
+CHECKSAT;
diff --git a/test/regress/regress0/rels/joinImg_2_1.cvc b/test/regress/regress0/rels/joinImg_2_1.cvc
new file mode 100644
index 000000000..b38bfab06
--- /dev/null
+++ b/test/regress/regress0/rels/joinImg_2_1.cvc
@@ -0,0 +1,24 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+x : SET OF [Atom, Atom];
+y : SET OF [Atom, Atom];
+r : SET OF [Atom, Atom];
+
+t : SET OF [Atom];
+
+a : Atom;
+b : Atom;
+c : Atom;
+d : Atom;
+e : Atom;
+f : Atom;
+g : Atom;
+
+ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
+ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 1);
+ASSERT y = {(f, g), (b, c), (d, e), (c, e)};
+ASSERT x = {(f, g), (b, c), (d, e), (c, e)};
+ASSERT (NOT(a = b)) OR (NOT(a = f));
+
+CHECKSAT;
\ No newline at end of file