diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-10 03:58:23 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-10 03:58:23 +0000 |
| commit | f50d6702ad0ffc5a10308abc2a43f86a9b623a8c (patch) | |
| tree | 6f1ce4e5d07b94ab1d9fbfcd5cf6603b0017078b /src/parser/smt | |
| parent | 0cd57d89001a73ea1ebe0d43b2cb720d68cca82a (diff) | |
Lexical scoping for let-bound variables (Bug #53)
Diffstat (limited to 'src/parser/smt')
| -rw-r--r-- | src/parser/smt/smt_parser.g | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index c12aa5f7a..d1ac50651 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -154,6 +154,7 @@ annotatedFormula returns [CVC4::Expr formula] LPAREN LET LPAREN name=variable[CHECK_UNDECLARED] expr1=annotatedFormula RPAREN { defineVar(name,expr1); } formula=annotatedFormula + { undefineVar(name); } RPAREN | /* An flet binding */ @@ -161,6 +162,7 @@ annotatedFormula returns [CVC4::Expr formula] LPAREN FLET LPAREN name=function_var[CHECK_UNDECLARED] expr1=annotatedFormula RPAREN { defineVar(name,expr1); } formula=annotatedFormula + { undefineVar(name); } RPAREN | /* A non-built-in function application */ |