diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-10 13:11:36 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-10 19:30:43 -0400 |
| commit | fb51c4e5494ad1dd71d6b343e20df3a5806ffc01 (patch) | |
| tree | cd52c105ed0729eceeec9bcab344b90c6c83c3e4 /src/parser/cvc | |
| parent | 5ddaecbf5288bc7ecb551627ab11083264a63b31 (diff) | |
membership cvc token changed to `IS_IN' to avoid conflict with IN used for let
Diffstat (limited to 'src/parser/cvc')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 12a3fa6f2..0a440f299 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -91,6 +91,7 @@ tokens { IN_TOK = 'IN'; INT_TOK = 'INT'; LET_TOK = 'LET'; + MEMBER_TOK = 'IS_IN'; NOT_TOK = 'NOT'; OR_TOK = 'OR'; REAL_TOK = 'REAL'; @@ -288,7 +289,8 @@ int getOperatorPrecedence(int type) { case LEQ_TOK: case LT_TOK: case GEQ_TOK: - case GT_TOK: return 25; + case GT_TOK: + case MEMBER_TOK: return 25; case EQUAL_TOK: case DISEQUAL_TOK: return 26; case NOT_TOK: return 27; @@ -327,7 +329,7 @@ Kind getOperatorKind(int type, bool& negate) { case GEQ_TOK: return kind::GEQ; case LT_TOK: return kind::LT; case LEQ_TOK: return kind::LEQ; - case IN_TOK: return kind::MEMBER; + case MEMBER_TOK: return kind::MEMBER; // arithmeticBinop case PLUS_TOK: return kind::PLUS; @@ -1442,7 +1444,7 @@ comparisonBinop[unsigned& op] | GEQ_TOK | LT_TOK | LEQ_TOK - | IN_TOK + | MEMBER_TOK ; term[CVC4::Expr& f] |