From 6a383befdf0fd88ff3c76dc001777475b34cf694 Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Thu, 25 Mar 2010 20:25:04 +0000
Subject: Merging let/flet rules in SMT parser

---
 src/parser/smt/smt_parser.g | 22 +++++-----------------
 1 file changed, 5 insertions(+), 17 deletions(-)

(limited to 'src/parser/smt')

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 */
   ;
 
 /**
-- 
cgit v1.2.3