Merge branch 'master' into splitEqRew

10 files changed, 11 insertions, 61 deletions

diff --git a/test/regress/regress1/rels/join-eq-structure_0_1.cvc b/test/regress/regress1/rels/join-eq-structure_0_1.cvc
deleted file mode 100644
index e27d3811c..000000000
--- a/test/regress/regress1/rels/join-eq-structure_0_1.cvc
+++ /dev/null
@@ -1,26 +0,0 @@
-% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
-IntPair: TYPE = [INT, INT];
-x : SET OF IntPair;
-y : SET OF IntPair;
-DATATYPE unit = u END;
-IntUPair: TYPE = [INT, unit];
-UIntPair: TYPE = [unit, INT];
-w : SET OF IntUPair;
-z : SET OF UIntPair;
-
-ASSERT  (x JOIN y) = (w JOIN z) OR (x JOIN y ) = TRANSPOSE(w JOIN z);
-
-ASSERT (0,1) IS_IN (x JOIN y);
-
-t : INT;
-ASSERT t >= 0 AND t <=1;
-s : INT;
-ASSERT s >= 0 AND s <=1;
-
-ASSERT s+t = 1;
-
-ASSERT ( s ,u ) IS_IN w;
-ASSERT NOT ( u, t ) IS_IN z;
-
-CHECKSAT;
diff --git a/test/regress/regress1/rels/rel_pressure_0.cvc b/test/regress/regress1/rels/rel_pressure_0.cvc
index 6cdf03600..0e9646f95 100644
--- a/test/regress/regress1/rels/rel_pressure_0.cvc
+++ b/test/regress/regress1/rels/rel_pressure_0.cvc
@@ -611,7 +611,7 @@ ASSERT (1, 9) IS_IN z;
 
 a : IntPair;
 ASSERT a = (9,1);
-ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z);
-ASSERT NOT (a IS_IN (TRANSPOSE r));
+ASSERT r = ((TRANSPOSE(x) JOIN y) JOIN z);
+ASSERT NOT (a IS_IN TRANSPOSE(r));
 
 CHECKSAT;
diff --git a/test/regress/regress1/rels/rel_tc_10_1.cvc b/test/regress/regress1/rels/rel_tc_10_1.cvc
index 67c444070..65686ef08 100644
--- a/test/regress/regress1/rels/rel_tc_10_1.cvc
+++ b/test/regress/regress1/rels/rel_tc_10_1.cvc
@@ -12,7 +12,7 @@ ASSERT a = d;
 ASSERT (1, c) IS_IN x;
 ASSERT (2, d) IS_IN x;
 ASSERT (a, 5) IS_IN y;
-ASSERT y = (TCLOSURE x);
+ASSERT y = TCLOSURE(x);
 ASSERT ((2, 5) IS_IN y);
 
 CHECKSAT;
diff --git a/test/regress/regress1/rels/rel_tc_4.cvc b/test/regress/regress1/rels/rel_tc_4.cvc
index decd38fe1..a32e8b66d 100644
--- a/test/regress/regress1/rels/rel_tc_4.cvc
+++ b/test/regress/regress1/rels/rel_tc_4.cvc
@@ -13,7 +13,7 @@ ASSERT (1, d) IS_IN x;
 ASSERT (b, 1) IS_IN x;
 ASSERT (b = d);
 ASSERT (2,b) IS_IN ((x JOIN x) JOIN x);
-ASSERT NOT (2, 1) IS_IN (TCLOSURE x);
+ASSERT NOT (2, 1) IS_IN TCLOSURE(x);
 
 
 CHECKSAT;
diff --git a/test/regress/regress1/rels/rel_tc_4_1.cvc b/test/regress/regress1/rels/rel_tc_4_1.cvc
index 8ee75f7e9..484d09ec3 100644
--- a/test/regress/regress1/rels/rel_tc_4_1.cvc
+++ b/test/regress/regress1/rels/rel_tc_4_1.cvc
@@ -4,7 +4,7 @@ IntPair: TYPE = [INT, INT];
 x : SET OF IntPair;
 y : SET OF IntPair;
 z : SET OF IntPair;
-ASSERT y = ((TCLOSURE x) JOIN x);
-ASSERT NOT (y = TCLOSURE x);
+ASSERT y = (TCLOSURE(x) JOIN x);
+ASSERT NOT (y = TCLOSURE(x));
 
 CHECKSAT;
diff --git a/test/regress/regress1/rels/rel_tc_5_1.cvc b/test/regress/regress1/rels/rel_tc_5_1.cvc
index fd9caeade..a4b2fe1db 100644
--- a/test/regress/regress1/rels/rel_tc_5_1.cvc
+++ b/test/regress/regress1/rels/rel_tc_5_1.cvc
@@ -3,7 +3,7 @@ OPTION "logic" "ALL_SUPPORTED";
 IntPair: TYPE = [INT, INT];
 x : SET OF IntPair;
 y : SET OF IntPair;
-ASSERT y = (TCLOSURE x);
+ASSERT y = TCLOSURE(x);
 ASSERT NOT ( y = ((x JOIN x) JOIN x));
 
 CHECKSAT;
diff --git a/test/regress/regress1/rels/rel_tc_6.cvc b/test/regress/regress1/rels/rel_tc_6.cvc
index 4570c5a8d..2bc552170 100644
--- a/test/regress/regress1/rels/rel_tc_6.cvc
+++ b/test/regress/regress1/rels/rel_tc_6.cvc
@@ -3,7 +3,7 @@ OPTION "logic" "ALL_SUPPORTED";
 IntPair: TYPE = [INT, INT];
 x : SET OF IntPair;
 y : SET OF IntPair;
-ASSERT y = (TCLOSURE x);
+ASSERT y = TCLOSURE(x);
 ASSERT NOT (((x JOIN x) JOIN x) <= y);
 
 CHECKSAT;
diff --git a/test/regress/regress1/rels/rel_tc_9_1.cvc b/test/regress/regress1/rels/rel_tc_9_1.cvc
index f884349b1..8a9e8eeca 100644
--- a/test/regress/regress1/rels/rel_tc_9_1.cvc
+++ b/test/regress/regress1/rels/rel_tc_9_1.cvc
@@ -6,7 +6,7 @@ y : SET OF IntPair;
 z : SET OF IntPair;
 w : SET OF IntPair;
 
-ASSERT z = (TCLOSURE x);
+ASSERT z = TCLOSURE(x);
 ASSERT w = (x JOIN y);
 ASSERT (2, 2) IS_IN z;
 ASSERT (0,3) IS_IN y;
diff --git a/test/regress/regress1/rels/rel_tp_join_2_1.cvc b/test/regress/regress1/rels/rel_tp_join_2_1.cvc
index acf3dbccf..9a79582b7 100644
--- a/test/regress/regress1/rels/rel_tp_join_2_1.cvc
+++ b/test/regress/regress1/rels/rel_tp_join_2_1.cvc
@@ -14,6 +14,6 @@ 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);
+ASSERT r = ((TRANSPOSE(x) JOIN y) JOIN z);
+ASSERT a IS_IN TRANSPOSE(r);
 CHECKSAT;
diff --git a/test/regress/regress1/rels/strat_0_1.cvc b/test/regress/regress1/rels/strat_0_1.cvc
deleted file mode 100644
index b91ddbbe8..000000000
--- a/test/regress/regress1/rels/strat_0_1.cvc
+++ /dev/null
@@ -1,24 +0,0 @@
-% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
-IntPair: TYPE = [ INT, INT];
-IntIntPair: TYPE = [ IntPair, IntPair];
-x : SET OF IntIntPair;
-y : SET OF IntIntPair;
-z : SET OF IntPair;
-w : SET OF IntPair;
-
-a : IntPair;
-b : IntPair;
-c : IntIntPair;
-
-ASSERT NOT a = b;
-
-ASSERT a IS_IN z;
-ASSERT b IS_IN z;
-ASSERT (a,b) IS_IN x;
-ASSERT (b,a) IS_IN x;
-ASSERT c IS_IN x;
-ASSERT NOT ( c = (a,b) ) AND NOT ( c = (b,a) );
-
-
-CHECKSAT;