Fix issues in cvc parser (#2901)

27 files changed, 39 insertions, 39 deletions

diff --git a/test/regress/regress0/rels/rel_join_5.cvc b/test/regress/regress0/rels/rel_join_5.cvc
index 5209d8131..590e581a7 100644
--- a/test/regress/regress0/rels/rel_join_5.cvc
+++ b/test/regress/regress0/rels/rel_join_5.cvc
@@ -14,6 +14,6 @@ ASSERT (3, 4) IS_IN z;
 
 a : IntPair;
 ASSERT a = (1,4);
-ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z);
+ASSERT r = ((TRANSPOSE(x) JOIN y) JOIN z);
 ASSERT NOT (a IS_IN r);
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_11.cvc b/test/regress/regress0/rels/rel_tc_11.cvc
index 7edeb0efb..813b8235b 100644
--- a/test/regress/regress0/rels/rel_tc_11.cvc
+++ b/test/regress/regress0/rels/rel_tc_11.cvc
@@ -12,7 +12,7 @@ ASSERT z = (x PRODUCT y);
 ASSERT (1, 2, 3, 4) IS_IN z;
 ASSERT NOT ((5, 9) IS_IN x);
 ASSERT (3, 8) IS_IN y;
-ASSERT y = (TCLOSURE x);
+ASSERT y = TCLOSURE(x);
 ASSERT NOT ((1, 2) IS_IN y);
 
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_3.cvc b/test/regress/regress0/rels/rel_tc_3.cvc
index 39564c4cf..dc2138357 100644
--- a/test/regress/regress0/rels/rel_tc_3.cvc
+++ b/test/regress/regress0/rels/rel_tc_3.cvc
@@ -15,8 +15,8 @@ ASSERT (b = d);
 ASSERT (b > (d -1));
 ASSERT (b < (d+1));
 %ASSERT (2,3) IS_IN ((x JOIN x) JOIN x);
-%ASSERT NOT (2, 3) IS_IN (TCLOSURE x);
-ASSERT y = (TCLOSURE x);
+%ASSERT NOT (2, 3) IS_IN TCLOSURE(x);
+ASSERT y = TCLOSURE(x);
 ASSERT NOT ((1, 1) IS_IN y);
 
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_3_1.cvc b/test/regress/regress0/rels/rel_tc_3_1.cvc
index 7f5535656..a9b2e8b98 100644
--- a/test/regress/regress0/rels/rel_tc_3_1.cvc
+++ b/test/regress/regress0/rels/rel_tc_3_1.cvc
@@ -13,6 +13,6 @@ ASSERT (1, d) IS_IN x;
 ASSERT (b, 1) IS_IN x;
 ASSERT (b = d);
 
-ASSERT y = (TCLOSURE x);
+ASSERT y = TCLOSURE(x);
 
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_7.cvc b/test/regress/regress0/rels/rel_tc_7.cvc
index 15c0510a6..1958c0eee 100644
--- a/test/regress/regress0/rels/rel_tc_7.cvc
+++ b/test/regress/regress0/rels/rel_tc_7.cvc
@@ -3,8 +3,8 @@ OPTION "logic" "ALL_SUPPORTED";
 IntPair: TYPE = [INT, INT];
 x : SET OF IntPair;
 y : SET OF IntPair;
-ASSERT y = ((TCLOSURE x) JOIN x);
+ASSERT y = (TCLOSURE(x) JOIN x);
 ASSERT (1,2) IS_IN ((x JOIN x) JOIN x);
-ASSERT NOT (y <= TCLOSURE x);
+ASSERT NOT (y <= TCLOSURE(x));
 
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tc_8.cvc b/test/regress/regress0/rels/rel_tc_8.cvc
index 9f5879c6d..ecf938c23 100644
--- a/test/regress/regress0/rels/rel_tc_8.cvc
+++ b/test/regress/regress0/rels/rel_tc_8.cvc
@@ -4,7 +4,7 @@ IntPair: TYPE = [INT, INT];
 x : SET OF IntPair;
 y : SET OF IntPair;
 
-ASSERT (2, 2) IS_IN (TCLOSURE x);
+ASSERT (2, 2) IS_IN TCLOSURE(x);
 ASSERT x = {}::SET OF IntPair;
 
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tp_3_1.cvc b/test/regress/regress0/rels/rel_tp_3_1.cvc
index 46806b432..00c83e2d2 100644
--- a/test/regress/regress0/rels/rel_tp_3_1.cvc
+++ b/test/regress/regress0/rels/rel_tp_3_1.cvc
@@ -7,8 +7,8 @@ z: SET OF IntPair;
 
 ASSERT (1, 3) IS_IN x;
 ASSERT ((2,3) IS_IN z OR (2,1) IS_IN z);
-ASSERT y = (TRANSPOSE x);
+ASSERT y = TRANSPOSE(x);
 ASSERT NOT (1,2) IS_IN y;
 
 ASSERT x = z;
-CHECKSAT;
\ No newline at end of file
+CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tp_join_0.cvc b/test/regress/regress0/rels/rel_tp_join_0.cvc
index a03f0e3fd..9aaf6d9b1 100644
--- a/test/regress/regress0/rels/rel_tp_join_0.cvc
+++ b/test/regress/regress0/rels/rel_tp_join_0.cvc
@@ -28,5 +28,5 @@ 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));
+ASSERT NOT (a IS_IN TRANSPOSE(r));
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tp_join_1.cvc b/test/regress/regress0/rels/rel_tp_join_1.cvc
index 60b6edf58..5d9b5447f 100644
--- a/test/regress/regress0/rels/rel_tp_join_1.cvc
+++ b/test/regress/regress0/rels/rel_tp_join_1.cvc
@@ -28,5 +28,5 @@ ASSERT a = (4,1);
 
 ASSERT r = ((x JOIN y) JOIN z);
 
-ASSERT NOT (a IS_IN (TRANSPOSE r));
+ASSERT NOT (a IS_IN TRANSPOSE(r));
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tp_join_2.cvc b/test/regress/regress0/rels/rel_tp_join_2.cvc
index cc851f622..40471c1f9 100644
--- a/test/regress/regress0/rels/rel_tp_join_2.cvc
+++ b/test/regress/regress0/rels/rel_tp_join_2.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 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/regress0/rels/rel_tp_join_3.cvc b/test/regress/regress0/rels/rel_tp_join_3.cvc
index 25277f43a..008b2aa1e 100644
--- a/test/regress/regress0/rels/rel_tp_join_3.cvc
+++ b/test/regress/regress0/rels/rel_tp_join_3.cvc
@@ -17,11 +17,11 @@ 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));
+%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 zz = (TRANSPOSE(x) JOIN y);
 ASSERT NOT ((1,3) IS_IN w);
 ASSERT NOT ((1,3) IS_IN (w | zz) );
 
diff --git a/test/regress/regress0/rels/rel_tp_join_eq_0.cvc b/test/regress/regress0/rels/rel_tp_join_eq_0.cvc
index 54e16dd51..c5a90ff29 100644
--- a/test/regress/regress0/rels/rel_tp_join_eq_0.cvc
+++ b/test/regress/regress0/rels/rel_tp_join_eq_0.cvc
@@ -24,5 +24,5 @@ ASSERT a = (4,1);
 
 ASSERT r = ((x JOIN y) JOIN z);
 
-ASSERT NOT (a IS_IN (TRANSPOSE r));
+ASSERT NOT (a IS_IN TRANSPOSE(r));
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_tp_join_pro_0.cvc b/test/regress/regress0/rels/rel_tp_join_pro_0.cvc
index b05026bc9..77de6b829 100644
--- a/test/regress/regress0/rels/rel_tp_join_pro_0.cvc
+++ b/test/regress/regress0/rels/rel_tp_join_pro_0.cvc
@@ -16,6 +16,6 @@ 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));
+ASSERT r = ((TRANSPOSE(x) JOIN y) PRODUCT z);
+ASSERT NOT (v IS_IN TRANSPOSE(r));
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_transpose_0.cvc b/test/regress/regress0/rels/rel_transpose_0.cvc
index 49fb87569..d46cacead 100644
--- a/test/regress/regress0/rels/rel_transpose_0.cvc
+++ b/test/regress/regress0/rels/rel_transpose_0.cvc
@@ -11,8 +11,8 @@ zt : IntPair;
 ASSERT zt = (2,1);
 
 ASSERT z IS_IN x;
-ASSERT NOT (zt IS_IN (TRANSPOSE x));
+ASSERT NOT (zt IS_IN TRANSPOSE(x));
 
-ASSERT y = (TRANSPOSE x);
+ASSERT y = TRANSPOSE(x);
 
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_transpose_1.cvc b/test/regress/regress0/rels/rel_transpose_1.cvc
index bdcf31bb8..bbd6e5743 100644
--- a/test/regress/regress0/rels/rel_transpose_1.cvc
+++ b/test/regress/regress0/rels/rel_transpose_1.cvc
@@ -8,5 +8,5 @@ ASSERT z = (1,2,3);
 zt : IntTup;
 ASSERT zt = (3,2,1);
 ASSERT z IS_IN x;
-ASSERT NOT (zt IS_IN (TRANSPOSE x));
+ASSERT NOT (zt IS_IN TRANSPOSE(x));
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_transpose_1_1.cvc b/test/regress/regress0/rels/rel_transpose_1_1.cvc
index fa6ee5069..627e20fbf 100644
--- a/test/regress/regress0/rels/rel_transpose_1_1.cvc
+++ b/test/regress/regress0/rels/rel_transpose_1_1.cvc
@@ -9,6 +9,6 @@ ASSERT z = (1,2,a);
 zt : IntTup;
 ASSERT zt = (3,2,2);
 ASSERT z IS_IN x;
-ASSERT zt IS_IN (TRANSPOSE x);
-ASSERT y = (TRANSPOSE x);
+ASSERT zt IS_IN TRANSPOSE(x);
+ASSERT y = TRANSPOSE(x);
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_transpose_3.cvc b/test/regress/regress0/rels/rel_transpose_3.cvc
index 5dfe3b031..06cc82c45 100644
--- a/test/regress/regress0/rels/rel_transpose_3.cvc
+++ b/test/regress/regress0/rels/rel_transpose_3.cvc
@@ -10,6 +10,6 @@ zt : IntPair;
 ASSERT zt = (2,1);
 ASSERT (x = y);
 ASSERT z IS_IN x;
-ASSERT NOT (zt IS_IN (TRANSPOSE y));
+ASSERT NOT (zt IS_IN TRANSPOSE(y));
 
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_transpose_4.cvc b/test/regress/regress0/rels/rel_transpose_4.cvc
index b260147c8..882148013 100644
--- a/test/regress/regress0/rels/rel_transpose_4.cvc
+++ b/test/regress/regress0/rels/rel_transpose_4.cvc
@@ -8,6 +8,6 @@ z : IntPair;
 ASSERT z = (1,2);
 
 ASSERT z IS_IN x;
-ASSERT NOT ((2, 1) IS_IN (TRANSPOSE x));
+ASSERT NOT ((2, 1) IS_IN TRANSPOSE(x));
 
 CHECKSAT;
diff --git a/test/regress/regress0/rels/rel_transpose_6.cvc b/test/regress/regress0/rels/rel_transpose_6.cvc
index a2e8bcf10..3923e26b6 100644
--- a/test/regress/regress0/rels/rel_transpose_6.cvc
+++ b/test/regress/regress0/rels/rel_transpose_6.cvc
@@ -19,6 +19,6 @@ ASSERT x = TRANSPOSE(y);
 ASSERT NOT (zt IS_IN y);
 
 ASSERT z IS_IN y;
-ASSERT NOT (zt IS_IN (TRANSPOSE y));
+ASSERT NOT (zt IS_IN TRANSPOSE(y));
 
 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;