From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Thu, 25 Mar 2010 20:25:04 +0000 (+0000)
Subject: Merging let/flet rules in SMT parser
X-Git-Tag: cvc5-1.0.0~9170
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a383befdf0fd88ff3c76dc001777475b34cf694;p=cvc5.git

Merging let/flet rules in SMT parser
---

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 */
   ;
 
 /**