added rules for join and transpose operators

added more benchmarks

13 files changed, 230 insertions, 22 deletions

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index d694d553b..5069d061e 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -39,7 +39,6 @@ TESTS =	\
 	mar2014/smaller.smt2 \
 	mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 \
 	mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 \
-	rels/rel.cvc \
 	copy_check_heap_access_33_4.smt2 \
 	cvc-sample.cvc \
 	emptyset.smt2 \
@@ -84,4 +83,4 @@ regress regress0 test: check
 
 # do nothing in this subdir
 .PHONY: regress1 regress2 regress3
-regress1 regress2 regress3:
+regress1 regress2 regress3:
\ No newline at end of file
diff --git a/test/regress/regress0/sets/rels/rel.cvc b/test/regress/regress0/sets/rels/rel.cvc
deleted file mode 100644
index 27eb43b9f..000000000
--- a/test/regress/regress0/sets/rels/rel.cvc
+++ /dev/null
@@ -1,20 +0,0 @@
-% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
-IntPair: TYPE = [INT, INT];
-x : SET OF IntPair;
-y : SET OF IntPair;
-z : SET OF IntPair;
-m: SET OF INT;
-a: IntPair;
-b: INT;
-
-ASSERT a IS_IN (y JOIN z);
-ASSERT (y PRODUCT x) = (y PRODUCT z);
-ASSERT x = ((y JOIN z) JOIN x);
-
-ASSERT x = y | z;
-ASSERT x = y & z;
-ASSERT y = y - z;
-ASSERT z = (TRANSPOSE z);
-ASSERT z = x | y;
-CHECKSAT TRUE;
diff --git a/test/regress/regress0/sets/rels/rel_join.cvc b/test/regress/regress0/sets/rels/rel_join.cvc
new file mode 100644
index 000000000..7cce736f5
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join.cvc
@@ -0,0 +1,26 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+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 (7, 5) IS_IN y;
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+%ASSERT a IS_IN (x JOIN y);
+%ASSERT NOT (v IS_IN (x JOIN y));
+ASSERT NOT (a IS_IN (x JOIN y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_join_0.cvc b/test/regress/regress0/sets/rels/rel_join_0.cvc
new file mode 100644
index 000000000..a251218c6
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join_0.cvc
@@ -0,0 +1,25 @@
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+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 (7, 5) IS_IN y;
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+%ASSERT a IS_IN (x JOIN y);
+%ASSERT NOT (v IS_IN (x JOIN y));
+ASSERT NOT (a IS_IN (x JOIN y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_join_0_1.cvc b/test/regress/regress0/sets/rels/rel_join_0_1.cvc
new file mode 100644
index 000000000..70e35164a
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join_0_1.cvc
@@ -0,0 +1,26 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+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 (7, 5) IS_IN y;
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+%ASSERT a IS_IN (x JOIN y);
+%ASSERT NOT (v IS_IN (x JOIN y));
+ASSERT a IS_IN (x JOIN y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_join_1.cvc b/test/regress/regress0/sets/rels/rel_join_1.cvc
new file mode 100644
index 000000000..c8921afb9
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join_1.cvc
@@ -0,0 +1,31 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+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 (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN x;
+
+ASSERT (7, 5) IS_IN y;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+
+%ASSERT (a IS_IN (r JOIN(x JOIN y)));
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (a IS_IN (x JOIN y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_join_1_1.cvc b/test/regress/regress0/sets/rels/rel_join_1_1.cvc
new file mode 100644
index 000000000..3436bd707
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join_1_1.cvc
@@ -0,0 +1,31 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+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 (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN x;
+
+ASSERT (7, 5) IS_IN y;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+
+%ASSERT (a IS_IN (r JOIN(x JOIN y)));
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT a IS_IN (x JOIN y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_join_2.cvc b/test/regress/regress0/sets/rels/rel_join_2.cvc
new file mode 100644
index 000000000..cac7ce84d
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join_2.cvc
@@ -0,0 +1,20 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT, INT, INT];
+x : SET OF IntPair;
+y : SET OF IntTup;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntTup;
+ASSERT zt = (2,1,3);
+a : IntTup;
+ASSERT a = (1,1,3);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+
+ASSERT NOT (a IS_IN (x JOIN y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_join_2_1.cvc b/test/regress/regress0/sets/rels/rel_join_2_1.cvc
new file mode 100644
index 000000000..3e27b9cc5
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join_2_1.cvc
@@ -0,0 +1,20 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT, INT, INT];
+x : SET OF IntPair;
+y : SET OF IntTup;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntTup;
+ASSERT zt = (2,1,3);
+a : IntTup;
+ASSERT a = (1,1,3);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+
+ASSERT a IS_IN (x JOIN y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_transpose.cvc b/test/regress/regress0/sets/rels/rel_transpose.cvc
new file mode 100644
index 000000000..10644d794
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_transpose.cvc
@@ -0,0 +1,12 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+ASSERT z IS_IN x;
+ASSERT NOT (zt IS_IN (TRANSPOSE x));
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_transpose_0.cvc b/test/regress/regress0/sets/rels/rel_transpose_0.cvc
new file mode 100644
index 000000000..d06528fd2
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_transpose_0.cvc
@@ -0,0 +1,14 @@
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+zt : IntPair;
+ASSERT zt = (2,1);
+
+ASSERT z IS_IN x;
+ASSERT NOT (zt IS_IN (TRANSPOSE x));
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_transpose_1.cvc b/test/regress/regress0/sets/rels/rel_transpose_1.cvc
new file mode 100644
index 000000000..bdcf31bb8
--- /dev/null
+++ b/test/regress/regress0/sets/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;
diff --git a/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc b/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc
new file mode 100644
index 000000000..11653de04
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+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 zt IS_IN (TRANSPOSE x);
+CHECKSAT;