Lexical scoping for let-bound variables (Bug #53)

3 files changed, 12 insertions, 0 deletions

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index cadff04ac..593a89873 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -193,6 +193,14 @@ AntlrParser::defineVar(const std::string& name, const Expr& val) {
   Assert(isDeclared(name));
 }
 
+void
+AntlrParser::undefineVar(const std::string& name) {
+  Assert(isDeclared(name));
+  d_varSymbolTable.unbindName(name);
+  Assert(!isDeclared(name));
+}
+
+
 const Type* 
 AntlrParser::newSort(const std::string& name) {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 5a6beb132..94d919555 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -254,6 +254,8 @@ protected:
 
   /** Create a new variable definition (e.g., from a let binding). */
   void defineVar(const std::string& name, const Expr& val);
+  /** Remove a variable definition (e.g., from a let binding). */
+  void undefineVar(const std::string& name);
 
   /** 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_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 */