diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-25 20:25:04 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-25 20:25:04 +0000 |
| commit | 6a383befdf0fd88ff3c76dc001777475b34cf694 (patch) | |
| tree | 04a07e9f3aac9485a04d26a0c49350e9537b6ae7 /src/parser/smt | |
| parent | 56837b30117fda75298138cdd052e0c5ba201b86 (diff) | |
Merging let/flet rules in SMT parser
Diffstat (limited to 'src/parser/smt')
| -rw-r--r-- | src/parser/smt/smt_parser.g | 22 |
1 files changed, 5 insertions, 17 deletions
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index f9758dc5c..4f93caa87 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -149,28 +149,16 @@ annotatedFormula returns [CVC4::Expr formula] RPAREN { formula = mkExpr(CVC4::kind::ITE, test, trueExpr, falseExpr); } - | /* A let binding */ - /* TODO: Create an Expr of LET kind? */ - LPAREN LET LPAREN name=variable[CHECK_UNDECLARED] expr1=annotatedFormula RPAREN - { defineVar(name,expr1); } - formula=annotatedFormula - { undefineVar(name); } - RPAREN - - | /* An flet binding */ - /* TODO: Create an Expr of LET kind? */ - LPAREN FLET LPAREN name=function_var[CHECK_UNDECLARED] expr1=annotatedFormula RPAREN + | /* A let/flet binding */ + LPAREN (LET LPAREN name=variable[CHECK_UNDECLARED] + | FLET LPAREN name=function_var[CHECK_UNDECLARED] ) + expr1=annotatedFormula RPAREN { defineVar(name,expr1); } formula=annotatedFormula { undefineVar(name); } RPAREN | /* A non-built-in function application */ - - // Semantic predicate not necessary if parenthesized subexpressions - // are disallowed - // { isFunction(LT(2)->getText()) }? - { Expr f; } LPAREN f = functionSymbol { args.push_back(f); } @@ -188,7 +176,7 @@ annotatedFormula returns [CVC4::Expr formula] /* constants */ | TRUE { formula = getTrueExpr(); } | FALSE { formula = getFalseExpr(); } - /* TODO: let, flet, quantifiers, arithmetic constants */ + /* TODO: quantifiers, arithmetic constants */ ; /** |