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

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index cadff04ac81a9e382df16254f949504f5fe97412..593a89873c3a02cfb995ac642959d3660b6cede4 100644 (file)
--- 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 5a6beb1320871d62b1a20482767cf9cf81b3cb29..94d919555bd9d9146046fc778f5870ee0f00f191 100644 (file)
--- 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 c12aa5f7a588dfecd968c6bc202fa9e121c66aa4..d1ac506518894ec1030de8c9675de56aa8bd6680 100644 (file)
--- 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 */