Adding preliminary let/flet support to SMT parser (Bug #51)

4 files changed, 51 insertions, 6 deletions

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 9b18eeb5a..cadff04ac 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -171,10 +171,8 @@ const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) {
 Expr 
 AntlrParser::mkVar(const std::string& name, const Type* type) {
   Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
-  Assert( !isDeclared(name) );
   Expr expr = d_exprManager->mkVar(type, name);
-  d_varSymbolTable.bindName(name, expr);
-  Assert( isDeclared(name) );
+  defineVar(name,expr);
   return expr;
 }
 
@@ -188,6 +186,12 @@ AntlrParser::mkVars(const std::vector<std::string> names,
   return vars;
 }
 
+void
+AntlrParser::defineVar(const std::string& name, const Expr& val) {
+  Assert(!isDeclared(name));
+  d_varSymbolTable.bindName(name,val);
+  Assert(isDeclared(name));
+}
 
 const Type* 
 AntlrParser::newSort(const std::string& name) {
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index e68405eb9..5a6beb132 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -252,6 +252,8 @@ protected:
   mkVars(const std::vector<std::string> names, 
          const Type* type);
 
+  /** Create a new variable definition (e.g., from a let binding). */
+  void defineVar(const std::string& name, const Expr& val);
 
   /** Returns a function type over the given domain and range types. */
   const Type* functionType(const Type* domain, const Type* range);
diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g
index 695b7b787..e3985818c 100644
--- a/src/parser/smt/smt_lexer.g
+++ b/src/parser/smt/smt_lexer.g
@@ -110,10 +110,19 @@ IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; }
  * Matches an identifier starting with a colon. An identifier is a sequence of letters,
  * digits and "_", "'", "." symbols, starting with a colon.
  */
-C_IDENTIFIER options { paraphrase = "an identifier starting with a colon"; testLiterals = true; }
+C_IDENTIFIER options { paraphrase = "an attribute (e.g., ':x')"; testLiterals = true; }
   :  ':' ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*
   ;
 
+VAR_IDENTIFIER options { paraphrase = "a variable (e.g., '?x')"; testLiterals = false; }
+  :  '?' IDENTIFIER 
+  ;
+
+FUN_IDENTIFIER options { paraphrase = "a function variable (e.g, '$x')"; testLiterals = false; }
+  :  '$' IDENTIFIER 
+  ;
+
+
 /**
  * Matches the value of user-defined annotations or attributes. The only constraint imposed on a user-defined value is that it start with
  * an open brace and end with closed brace.
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index 7759cf965..c12aa5f7a 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -120,6 +120,8 @@ annotatedFormula returns [CVC4::Expr formula]
   Debug("parser") << "annotated formula: " << LT(1)->getText() << endl;
   Kind kind = CVC4::kind::UNDEFINED_KIND;
   vector<Expr> args; 
+  std::string name;
+  Expr expr1, expr2, expr3;
 }
   : /* a built-in operator application */
     LPAREN kind = builtinOp annotatedFormulas[args] RPAREN 
@@ -127,6 +129,7 @@ annotatedFormula returns [CVC4::Expr formula]
       formula = mkExpr(kind,args); }
 
   | /* a "distinct" expr */
+    /* TODO: Should there be a DISTINCT kind in the Expr package? */
     LPAREN DISTINCT annotatedFormulas[args] RPAREN
     { std::vector<Expr> diseqs;
       for(unsigned i = 0; i < args.size(); ++i) {
@@ -146,7 +149,20 @@ 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
+    RPAREN
 
+  | /* An flet binding */
+    /* TODO: Create an Expr of LET kind? */
+    LPAREN FLET LPAREN name=function_var[CHECK_UNDECLARED] expr1=annotatedFormula RPAREN
+    { defineVar(name,expr1); }
+    formula=annotatedFormula
+    RPAREN
+    
   | /* A non-built-in function application */
 
     // Semantic predicate not necessary if parenthesized subexpressions
@@ -162,7 +178,9 @@ annotatedFormula returns [CVC4::Expr formula]
 
   | /* a variable */
     { std::string name; }
-    name = identifier[CHECK_DECLARED]
+    ( name = identifier[CHECK_DECLARED] 
+      | name = variable[CHECK_DECLARED]
+      | name = function_var[CHECK_DECLARED] )
     { formula = getVariable(name); }
 
     /* constants */
@@ -236,6 +254,18 @@ attribute
   :  C_IDENTIFIER
   ;
 
+variable[DeclarationCheck check = CHECK_NONE] returns [std::string name]
+  : x:VAR_IDENTIFIER
+    { name = x->getText();
+      checkDeclaration(name, check, SYM_VARIABLE); }
+  ;
+
+function_var[DeclarationCheck check = CHECK_NONE] returns [std::string name]
+  : x:FUN_IDENTIFIER
+    { name = x->getText();
+      checkDeclaration(name, check, SYM_FUNCTION); }
+  ;
+
 /**
  * Matches the sort symbol, which can be an arbitrary identifier.
  * @param check the check to perform on the name
@@ -328,6 +358,6 @@ returns [std::string id]
 }
   : x:IDENTIFIER
     { id = x->getText();
-      checkDeclaration(id, check,type); }
+      checkDeclaration(id, check, type); }
   ;