diff options
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/parser.h | 2 | ||||
| -rw-r--r-- | src/parser/smt/Smt.g | 17 |
2 files changed, 13 insertions, 6 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index a84021c10..f56ec03ac 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -13,7 +13,7 @@ ** A collection of state for use by parser implementations. **/ -#include "cvc4parser_private.h" +#include "cvc4parser_public.h" #ifndef __CVC4__PARSER__PARSER_STATE_H #define __CVC4__PARSER__PARSER_STATE_H diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 2dd680f09..5cd94ec0d 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -178,6 +178,7 @@ annotatedFormula[CVC4::Expr& expr] Kind kind; std::string name; std::vector<Expr> args; /* = getExprVector(); */ + Expr op; /* Operator expression FIXME: move away kill it */ } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK @@ -195,14 +196,12 @@ annotatedFormula[CVC4::Expr& expr] // Semantic predicate not necessary if parenthesized subexpressions // are disallowed - // { isFunction(LT(2)->getText()) }? - + // { isFunction(LT(2)->getText()) }? LPAREN_TOK - functionSymbol[expr] - { args.push_back(expr); } + parameterizedOperator[op] annotatedFormulas[args,expr] RPAREN_TOK // TODO: check arity - { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); } + { expr = MK_EXPR(op,args); } | /* An ite expression */ LPAREN_TOK ITE_TOK @@ -283,11 +282,19 @@ builtinOp[CVC4::Kind& kind] | STAR_TOK { $kind = CVC4::kind::MULT; } | TILDE_TOK { $kind = CVC4::kind::UMINUS; } | MINUS_TOK { $kind = CVC4::kind::MINUS; } + // Bit-vectors // NOTE: Theory operators go here /* TODO: lt, gt, plus, minus, etc. */ ; /** + * Matches an operator. + */ +parameterizedOperator[CVC4::Expr& op] + : functionSymbol[op] + ; + +/** * Matches a (possibly undeclared) predicate identifier (returning the string). * @param check what kind of check to do with the symbol */ |