Fix issues in cvc parser (#2901)

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index c79da40a03a8761325a3b42c349b9861019cc7ba..6de746ad7f2e1e05cff7b3586a7c832aa76c49e1 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1552,9 +1552,6 @@ booleanBinop[unsigned& op]
   | OR_TOK
   | XOR_TOK
   | AND_TOK
-  | JOIN_TOK
-  | PRODUCT_TOK
-  | JOIN_IMAGE_TOK  
   ;
 
 comparison[CVC4::Expr& f]
@@ -1705,9 +1702,8 @@ uminusTerm[CVC4::Expr& f]
   unsigned minusCount = 0;
 }
     /* Unary minus */
-  : (MINUS_TOK { ++minusCount; })+ bvBinaryOpTerm[f]
+  : (MINUS_TOK { ++minusCount; })* bvBinaryOpTerm[f]
     { while(minusCount > 0) { --minusCount; f = MK_EXPR(CVC4::kind::UMINUS, f); } }
-  | bvBinaryOpTerm[f]
   ;
 
 /** Parses bitvectors.  Starts with binary operators @, &, and |. */
@@ -1734,28 +1730,27 @@ bvNegTerm[CVC4::Expr& f]
     /* BV neg */
   : BVNEG_TOK bvNegTerm[f]
     { f = f.getType().isSet() ? MK_EXPR(CVC4::kind::COMPLEMENT, f) : MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
-  | relationTerm[f]
+  | relationBinopTerm[f]
   ;
 
-relationTerm[CVC4::Expr& f]
-    /* relation terms */
-  : TRANSPOSE_TOK relationTerm[f]
-    { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } 
-  | TRANSCLOSURE_TOK relationTerm[f]
-    { f = MK_EXPR(CVC4::kind::TCLOSURE, f); }
-  | TUPLE_TOK LPAREN relationTerm[f] RPAREN
-    { std::vector<Type> types;
-      std::vector<Expr> args;
-      args.push_back(f);
-           types.push_back(f.getType());
-      DatatypeType t = EXPR_MANAGER->mkTupleType(types);
-      const Datatype& dt = t.getDatatype();
-      args.insert( args.begin(), dt[0].getConstructor() );
-      f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args);
-    }
-  | IDEN_TOK relationTerm[f]
-    { f = MK_EXPR(CVC4::kind::IDEN, f); }                 
-  | postfixTerm[f]
+relationBinop[unsigned& op]
+@init {
+  op = LT(1)->getType(LT(1));
+}
+  : JOIN_TOK
+  | PRODUCT_TOK
+  | JOIN_IMAGE_TOK
+  ;
+
+relationBinopTerm[CVC4::Expr& f]
+@init {
+  std::vector<CVC4::Expr> expressions;
+  std::vector<unsigned> operators;
+  unsigned op;
+}
+  : postfixTerm[f] { expressions.push_back(f); }
+    ( relationBinop[op] postfixTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
+    { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); }
   ;
 
 /**
@@ -1775,7 +1770,7 @@ postfixTerm[CVC4::Expr& f]
   std::string id;
   Type t;
 }
-  : ( bvTerm[f]
+  : ( relationTerm[f]
     ( /* array select / bitvector extract */
       LBRACKET
         ( formula[f2] { extract = false; }
@@ -1883,7 +1878,28 @@ postfixTerm[CVC4::Expr& f]
       }
     )?
   ;
-
+  
+relationTerm[CVC4::Expr& f]
+    /* relation terms */
+  : TRANSPOSE_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } 
+  | TRANSCLOSURE_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::TCLOSURE, f); }
+  | TUPLE_TOK LPAREN formula[f] RPAREN
+    { std::vector<Type> types;
+      std::vector<Expr> args;
+      args.push_back(f);
+      types.push_back(f.getType());
+      DatatypeType t = EXPR_MANAGER->mkTupleType(types);
+      const Datatype& dt = t.getDatatype();
+      args.insert( args.begin(), dt[0].getConstructor() );
+      f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args);
+    }
+  | IDEN_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::IDEN, f); }                 
+  | bvTerm[f]
+  ;
+  
 bvTerm[CVC4::Expr& f]
 @init {
   Expr f2;

diff --git a/test/regress/regress0/rels/rel_join_5.cvc b/test/regress/regress0/rels/rel_join_5.cvc
index 5209d81313c7e45a66c5949f2bf68b264f34c3c3..590e581a788e806b5f03c7552c4019d0a84b2877 100644 (file)
--- 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 7edeb0efb3d4c71e099f4b1a0abbebeee6ec9e17..813b8235bcbcc5ecc23266c0a1f187c40b9cda4a 100644 (file)
--- 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 39564c4cfae7cd122f8a8fb1714ad8e97317b137..dc213835768bb58395fa44e75fcbf5b5916eb17e 100644 (file)
--- 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 7f5535656892f50d2b2a3e5172e840442171ced3..a9b2e8b98651e6a3a28f6ca04be20e70b07966f9 100644 (file)
--- 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 15c0510a6e24a7d6535851f6e4382fc17ad6b0a9..1958c0eeefe7ce84ab96c24c3ccbd67b74f467a8 100644 (file)
--- 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 9f5879c6d3f1341c64c99299451b47d41c713af6..ecf938c239b379d7f78912904cf2e80c86bf959e 100644 (file)
--- 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 46806b43237bc1dd254f1ae8711abe5264102a18..00c83e2d2f15dd19564a363b6cd669d9545e9e1e 100644 (file)
--- 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 a03f0e3fd86b8315ee464782a3beee9c59181d21..9aaf6d9b1afe4c9d4ce527a471fb07eee8a996ae 100644 (file)
--- 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 60b6edf5876ffbd58eda0104976fd8f0e2110237..5d9b5447f599ca05e9de93dbf7e39b74c8e9c417 100644 (file)
--- 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 cc851f6223e5e1104bded34abff7cfab4fa3c0b5..40471c1f9205519f696463bc3f3d0946ba97203d 100644 (file)
--- 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 25277f43a64001299781d6cb98c028f1aa85ff89..008b2aa1e9d93c0f90cd0f75933c9326eab37b7f 100644 (file)
--- 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 54e16dd51b8fad91e2a1dc78007725c445bf9b3a..c5a90ff293964e772b9e920cafada9917e38bea0 100644 (file)
--- 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 b05026bc9cd9533dd9d33efe9ed414f915b6fcae..77de6b82917d9f5dad9fa02ed882173bbbc8732c 100644 (file)
--- 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 49fb87569e3629d2d5eaa36814965934f1afe901..d46caceade79577990a8f0b851441049369b89a4 100644 (file)
--- 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 bdcf31bb841387cb39c00a81fd1f8633febe9fc9..bbd6e57434b75e9702c9f37859b757309e37bdbe 100644 (file)
--- 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 fa6ee5069f488488e032a266a14475a8861199a1..627e20fbf164ee431d37330fd8a91580908f5fe9 100644 (file)
--- 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 5dfe3b031b7074c60aaa7517c3a7e4f5a812b48b..06cc82c45e938781a506a9a39c683ded0e467f67 100644 (file)
--- 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 b260147c83dca2f6955403548499fc08bdda466a..882148013e44eb0cb684ea4ba028b0efde280977 100644 (file)
--- 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 a2e8bcf10db04490dde9d44226bcb1cd49d19d81..3923e26b6e86819e3c0e340263b607677dd6a1a7 100644 (file)
--- 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 6cdf0360094726b4308be4f7befe6aecff64ab54..0e9646f95b3b15ff95a8928eb79ab2f7a3bd4c08 100644 (file)
--- 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 67c444070f226993d05fb4efd9825fb2bf04ddec..65686ef080a590c074d4216f31e9b8fc6e06d6da 100644 (file)
--- 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 decd38fe14140b63a59af18ea30abb3a239037cc..a32e8b66d916e845979c91aa056e949fdaa69893 100644 (file)
--- 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 8ee75f7e9a49a1d41cbef505e0ca8f577bbd1ca6..484d09ec39901b6d987b47991e120e412648a6c2 100644 (file)
--- 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 fd9caeade71ad27111f80f6806463019bc2e2720..a4b2fe1dbfd193b9585e8906ab54f072976eb221 100644 (file)
--- 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 4570c5a8d505b95e413c3debcc373851023a8ba5..2bc552170779552f436c9019f2d2adc4de1423ac 100644 (file)
--- 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 f884349b19e54a0db139445ce537ada519482d77..8a9e8eecae938885dba3ac54ed62da2fb90fe27a 100644 (file)
--- 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 acf3dbccf40a0b45d8226e5ca1219f17a679c0ce..9a79582b707d5a226514526b5a2720fe1aac6368 100644 (file)
--- 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;