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

10 files changed, 82 insertions, 6 deletions

diff --git a/.project b/.project
index 9f40fa245..cd7732047 100644
--- a/.project
+++ b/.project
@@ -6,6 +6,11 @@
 	</projects>
 	<buildSpec>
 		<buildCommand>
+			<name>org.eclipse.dltk.core.scriptbuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+		<buildCommand>
 			<name>org.eclipse.cdt.managedbuilder.core.genmakebuilder</name>
 			<triggers>clean,full,incremental,</triggers>
 			<arguments>
@@ -82,5 +87,6 @@
 		<nature>org.eclipse.cdt.core.ccnature</nature>
 		<nature>org.eclipse.cdt.managedbuilder.core.managedBuildNature</nature>
 		<nature>org.eclipse.cdt.managedbuilder.core.ScannerConfigNature</nature>
+		<nature>net.certiv.antlrdt.core.nature</nature>
 	</natures>
 </projectDescription>
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); }
   ;
 
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index a8786b4ff..29141d633 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -2,7 +2,12 @@ SUBDIRS = precedence uf
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
 TESTS =	bug32.cvc \
+    distinct.smt \
+    flet.smt \
+    flet2.smt \
 	hole6.cvc \
+	let.smt \
+	let2.smt \
 	logops.01.cvc \
 	logops.02.cvc \
 	logops.03.cvc \
diff --git a/test/regress/regress0/flet.smt b/test/regress/regress0/flet.smt
new file mode 100644
index 000000000..95742de77
--- /dev/null
+++ b/test/regress/regress0/flet.smt
@@ -0,0 +1,5 @@
+(benchmark flet_test
+  :logic QF_UF
+  :status unsat
+  :extrapreds ((a) (b)) 
+  :formula (flet ($x (and a b)) (and $x (or (not a) (not b)))))
\ No newline at end of file
diff --git a/test/regress/regress0/flet2.smt b/test/regress/regress0/flet2.smt
new file mode 100644
index 000000000..4d71ebf30
--- /dev/null
+++ b/test/regress/regress0/flet2.smt
@@ -0,0 +1,5 @@
+(benchmark flet_test
+  :logic QF_UF
+  :status sat
+  :extrapreds ((a) (b)) 
+  :formula (flet ($x (and a b)) (and $x (or a b))))
\ No newline at end of file
diff --git a/test/regress/regress0/let.smt b/test/regress/regress0/let.smt
new file mode 100644
index 000000000..45d0eaecb
--- /dev/null
+++ b/test/regress/regress0/let.smt
@@ -0,0 +1,5 @@
+(benchmark let_test
+  :logic QF_UF
+  :status unsat
+  :extrafuns ((a U) (b U) (f U U)) 
+  :formula (let (?x a) (not (= ?x a))))
\ No newline at end of file
diff --git a/test/regress/regress0/let2.smt b/test/regress/regress0/let2.smt
new file mode 100644
index 000000000..aa3d20b8c
--- /dev/null
+++ b/test/regress/regress0/let2.smt
@@ -0,0 +1,5 @@
+(benchmark let_test
+  :logic QF_UF
+  :status sat
+  :extrafuns ((a U) (b U) (f U U)) 
+  :formula (let (?x (f a)) (= ?x (f b))))
\ No newline at end of file