diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-28 22:21:34 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-28 22:21:34 -0500 |
commit | 952ee3698e7760ccbd90fac5691d455d807af3a6 (patch) | |
tree | 38b5efeb62d039373ff58a0b802661a816c9d9e8 /test/regress/regress1 | |
parent | 361a1798d66266679abdb8c9033089db8de74320 (diff) |
Fix issues in cvc parser (#2901)
Diffstat (limited to 'test/regress/regress1')
-rw-r--r-- | test/regress/regress1/rels/rel_pressure_0.cvc | 4 | ||||
-rw-r--r-- | test/regress/regress1/rels/rel_tc_10_1.cvc | 2 | ||||
-rw-r--r-- | test/regress/regress1/rels/rel_tc_4.cvc | 2 | ||||
-rw-r--r-- | test/regress/regress1/rels/rel_tc_4_1.cvc | 4 | ||||
-rw-r--r-- | test/regress/regress1/rels/rel_tc_5_1.cvc | 2 | ||||
-rw-r--r-- | test/regress/regress1/rels/rel_tc_6.cvc | 2 | ||||
-rw-r--r-- | test/regress/regress1/rels/rel_tc_9_1.cvc | 2 | ||||
-rw-r--r-- | test/regress/regress1/rels/rel_tp_join_2_1.cvc | 4 |
8 files changed, 11 insertions, 11 deletions
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; |