diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-05 15:43:47 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-05 16:25:59 -0400 |
| commit | 3544cac0bd08e3cf8b12c742fd7a6f6ab19de068 (patch) | |
| tree | 0d9e98020a0e3437fd079f91fdd119b7e5d141d0 /src/parser/cvc | |
| parent | 7f6ded8353c91996d021c35461a5b3c2224746ae (diff) | |
Fix FLOOR and DISTINCT in CVC language parser.
Diffstat (limited to 'src/parser/cvc')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 9131c220f..51ea87e39 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -150,6 +150,7 @@ tokens { MOD_TOK = 'MOD'; INTDIV_TOK = 'DIV'; FLOOR_TOK = 'FLOOR'; + DISTINCT_TOK = 'DISTINCT'; // Bitvectors @@ -270,8 +271,7 @@ int getOperatorPrecedence(int type) { case LEQ_TOK: case LT_TOK: case GEQ_TOK: - case GT_TOK: - case FLOOR_TOK: return 25; + case GT_TOK: return 25; case EQUAL_TOK: case DISEQUAL_TOK: return 26; case NOT_TOK: return 27; @@ -1583,7 +1583,7 @@ postfixTerm[CVC4::Expr& f] std::string id; Type t; } - : bvTerm[f] + : ( bvTerm[f] ( /* array select / bitvector extract */ LBRACKET ( formula[f2] { extract = false; } @@ -1664,6 +1664,13 @@ postfixTerm[CVC4::Expr& f] } ) )* + | FLOOR_TOK LPAREN formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::TO_INTEGER, f); } + | DISTINCT_TOK LPAREN + formula[f] { args.push_back(f); } + ( COMMA formula[f] { args.push_back(f); } )* RPAREN + { f = (args.size() == 1) ? MK_CONST(bool(true)) : MK_EXPR(CVC4::kind::DISTINCT, args); } + ) ( typeAscription[f, t] { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) { std::vector<CVC4::Expr> v; |