diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-29 23:42:41 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-29 23:42:41 +0000 |
| commit | 349131957e91150c24a9c69f5e1f04e34494b0c6 (patch) | |
| tree | 8012c2475dde1f1177f693643fb1a07e89c29538 /src/parser/smt/Smt.g | |
| parent | ac8b46fe3b5256e387da724b7c3abfb59d25531e (diff) | |
Added the capability to construct expressions by passing the operator instead of the kind, i.e.
Expr op = ..."f"...
em.mkExpr(op, children);
Operator kinds are automatically associated with the enclosing expression kind in the DSL and generated.
Diffstat (limited to 'src/parser/smt/Smt.g')
| -rw-r--r-- | src/parser/smt/Smt.g | 17 |
1 files changed, 12 insertions, 5 deletions
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 */ |