Added more benchmarks

Fixed the problem that duplicates and split facts were sent as lemmas
causing nontermination
Fixed the computation of join and product relations without simplication

18 files changed, 399 insertions, 0 deletions

diff --git a/test/regress/regress0/sets/rels/rel_join_3.cvc b/test/regress/regress0/sets/rels/rel_join_3.cvc
new file mode 100644
index 000000000..6e190cecf
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join_3.cvc
@@ -0,0 +1,29 @@
+% 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 r = (x JOIN y);
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (a IS_IN r);
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_join_3_1.cvc b/test/regress/regress0/sets/rels/rel_join_3_1.cvc
new file mode 100644
index 000000000..d4e666c6e
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join_3_1.cvc
@@ -0,0 +1,29 @@
+% 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 r = (x JOIN y);
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT a IS_IN r;
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_join_4.cvc b/test/regress/regress0/sets/rels/rel_join_4.cvc
new file mode 100644
index 000000000..030810f3d
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join_4.cvc
@@ -0,0 +1,32 @@
+% 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);
+
+b : IntPair;
+ASSERT b = (7, 5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN x;
+
+ASSERT b IS_IN y;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT r = (x JOIN y);
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (a IS_IN r);
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_join_5.cvc b/test/regress/regress0/sets/rels/rel_join_5.cvc
new file mode 100644
index 000000000..5209d8131
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_join_5.cvc
@@ -0,0 +1,19 @@
+% 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 (7, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+
+a : IntPair;
+ASSERT a = (1,4);
+ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z);
+ASSERT NOT (a IS_IN r);
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_product_0.cvc b/test/regress/regress0/sets/rels/rel_product_0.cvc
new file mode 100644
index 000000000..09981be0b
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_product_0.cvc
@@ -0,0 +1,20 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT, INT, 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 : IntTup;
+ASSERT v = (1,2,2,1);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (v IS_IN (x PRODUCT y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_product_0_1.cvc b/test/regress/regress0/sets/rels/rel_product_0_1.cvc
new file mode 100644
index 000000000..f141c7bd4
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_product_0_1.cvc
@@ -0,0 +1,20 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT, INT, 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 : IntTup;
+ASSERT v = (1,2,2,1);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT v IS_IN (x PRODUCT y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_product_1.cvc b/test/regress/regress0/sets/rels/rel_product_1.cvc
new file mode 100644
index 000000000..1826e5a75
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_product_1.cvc
@@ -0,0 +1,20 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT, INT];
+IntTup: TYPE = [INT, INT, INT, INT,INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2,3);
+zt : IntPair;
+ASSERT zt = (3,2,1);
+v : IntTup;
+ASSERT v = (1,2,3,3,2,1);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (v IS_IN (x PRODUCT y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_product_1_1.cvc b/test/regress/regress0/sets/rels/rel_product_1_1.cvc
new file mode 100644
index 000000000..3e5280c19
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_product_1_1.cvc
@@ -0,0 +1,20 @@
+% EXPECT: SAT
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT, INT];
+IntTup: TYPE = [INT, INT, INT, INT,INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+r : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2,3);
+zt : IntPair;
+ASSERT zt = (3,2,1);
+v : IntTup;
+ASSERT v = (1,2,3,3,2,1);
+
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT v IS_IN (x PRODUCT y);
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_tp_join_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_0.cvc
new file mode 100644
index 000000000..a03f0e3fd
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_0.cvc
@@ -0,0 +1,32 @@
+% 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 = (5,1);
+
+b : IntPair;
+ASSERT b = (7, 5);
+
+ASSERT (1, 7) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (3, 4) IS_IN x;
+
+ASSERT b IS_IN y;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT r = (x JOIN y);
+ASSERT z IS_IN x;
+ASSERT zt IS_IN y;
+ASSERT NOT (a IS_IN (TRANSPOSE 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
new file mode 100644
index 000000000..dca0a3bfa
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_1.cvc
@@ -0,0 +1,24 @@
+% 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 (1, 7) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+
+
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) 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_2.cvc b/test/regress/regress0/sets/rels/rel_tp_join_2.cvc
new file mode 100644
index 000000000..cc851f622
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_2.cvc
@@ -0,0 +1,19 @@
+% 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 (7, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+
+a : IntPair;
+ASSERT a = (4,1);
+ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z);
+ASSERT NOT (a IS_IN (TRANSPOSE r));
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc b/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc
new file mode 100644
index 000000000..04856d825
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc
@@ -0,0 +1,19 @@
+% 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 (7, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+a : IntPair;
+ASSERT a = (4,1);
+
+ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z);
+ASSERT a IS_IN (TRANSPOSE r);
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_tp_join_3.cvc b/test/regress/regress0/sets/rels/rel_tp_join_3.cvc
new file mode 100644
index 000000000..25277f43a
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_3.cvc
@@ -0,0 +1,28 @@
+% 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;
+
+ASSERT (7, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (7, 3) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+ASSERT (3, 3) IS_IN w;
+
+a : IntPair;
+ASSERT a = (4,1);
+%ASSERT r = (((TRANSPOSE x) JOIN y) JOIN (w JOIN z));
+ASSERT NOT (a IS_IN (TRANSPOSE r));
+
+zz : SET OF IntPair;
+ASSERT zz = ((TRANSPOSE x) JOIN y);
+ASSERT NOT ((1,3) IS_IN w);
+ASSERT NOT ((1,3) IS_IN (w | zz) );
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc
new file mode 100644
index 000000000..b05026bc9
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc
@@ -0,0 +1,21 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntTup: TYPE = [INT, INT, INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntTup;
+
+ASSERT (2, 1) IS_IN x;
+ASSERT (2, 3) IS_IN x;
+ASSERT (2, 2) IS_IN y;
+ASSERT (4, 7) IS_IN y;
+ASSERT (3, 4) IS_IN z;
+
+v : IntTup;
+ASSERT v = (4,3,2,1);
+
+ASSERT r = (((TRANSPOSE x) JOIN y) PRODUCT z);
+ASSERT NOT (v IS_IN (TRANSPOSE r));
+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
new file mode 100644
index 000000000..c7757bd3e
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_tp_join_var.cvc
@@ -0,0 +1,28 @@
+% EXPECT: unsat
+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));
+
+st : SET OF INT;
+su : SET OF INT;
+ASSERT t IS_IN st;
+ASSERT u IS_IN su;
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_transpose_2.cvc b/test/regress/regress0/sets/rels/rel_transpose_2.cvc
new file mode 100644
index 000000000..15a035b58
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_transpose_2.cvc
@@ -0,0 +1,12 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntTup: TYPE = [INT];
+x : SET OF IntTup;
+y : SET OF IntTup;
+z : IntTup;
+ASSERT z = (1);
+zt : IntTup;
+ASSERT zt = (1);
+ASSERT z IS_IN x;
+ASSERT NOT (zt IS_IN (TRANSPOSE x));
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_transpose_3.cvc b/test/regress/regress0/sets/rels/rel_transpose_3.cvc
new file mode 100644
index 000000000..225f3491c
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_transpose_3.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 (x = y);
+ASSERT z IS_IN x;
+ASSERT NOT (zt IS_IN (TRANSPOSE y));
+
+CHECKSAT;
diff --git a/test/regress/regress0/sets/rels/rel_transpose_4.cvc b/test/regress/regress0/sets/rels/rel_transpose_4.cvc
new file mode 100644
index 000000000..b260147c8
--- /dev/null
+++ b/test/regress/regress0/sets/rels/rel_transpose_4.cvc
@@ -0,0 +1,13 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+z : IntPair;
+ASSERT z = (1,2);
+
+ASSERT z IS_IN x;
+ASSERT NOT ((2, 1) IS_IN (TRANSPOSE x));
+
+CHECKSAT;