Implement smtlib2 format "let" properly. Fixes #388

include/stp/Parser/LetMgr.h

@@ -32,78 +32,58 @@ namespace stp
 using std::string;
 
 // LET Management
-class LETMgr
+class LetMgr
 {
 private:
   const ASTNode ASTUndefined;
 
   typedef std::unordered_map<string, ASTNode> MapType;
 
-  // MAP: This map is from bound IDs that occur in LETs to
-  // expression. The map is useful in checking replacing the IDs
-  // with the corresponding expressions. As soon as the brackets
-  // that close a let expression is reached, it is emptied by
-  // a call to CleanupLetIDMap().
-  MapType* _letid_expr_map;
-
-  // Need to pop/push the let nodes, they can be nested.
-  std::stack<vector<string>> stack;
-
-  // Allocate LetID map
-  void InitializeLetIDMap(void);
+  // This maps from bound IDs that occur in LETs to
+  // expressions. It's used to replace the IDs
+  // with the corresponding expressions.
+  // It's complicated because bindings can be shadowed by later bindings.
+  // As soon as the brackets that close a let expression is reached it should be popped.
+
+  // Initally empty because we expect push() to be called before any bindings are added.
+  std::vector<MapType> stack;
+  MapType interim;
 
 public:
-  // I think this keeps a reference to symbols so they don't get garbage
-  // collected. Used only by the CVC parser.
-  ASTNodeSet _parser_symbol_table;
+
+  bool frameMode = true;
 
-  // A let with this name has already been declared.
-  bool isLetDeclared(string s)
+  LetMgr(ASTNode undefined) : ASTUndefined(undefined)
   {
-    return _letid_expr_map->find(s) != _letid_expr_map->end();
+    assert(!undefined.IsNull());
+    push(); // CVC format has a global let scope.
   }
 
-  void cleanupParserSymbolTable() { _parser_symbol_table.clear(); }
-
-  LETMgr(ASTNode undefined) : ASTUndefined(undefined)
-  {
-    assert(!undefined.IsNull());
-    InitializeLetIDMap();
+  ~LetMgr() 
+  {  
   }
 
-  ~LETMgr() { delete _letid_expr_map; }
+  // I think this keeps a reference to symbols so they don't get garbage
+  // collected. Used only by the CVC parser.
+  ASTNodeSet _parser_symbol_table;
+  void cleanupParserSymbolTable();
 
-  // We know for sure that it's a let.
-  ASTNode resolveLet(const string s)
-  {
-    assert(isLetDeclared(s));
-    return _letid_expr_map->find(s)->second;
-  }
+  void CleanupLetIDMap(void);
 
+  // Has a let with this name has already been declared.
+  bool isLetDeclared(string s);
+
+  ASTNode resolveLet(const string s);
   ASTNode ResolveID(const ASTNode& var);
 
-  // Functions that are used to manage LET expressions
+  // Functions that are used to create LET expressions
   void LetExprMgr(const ASTNode& var, const ASTNode& letExpr);
   void LetExprMgr(string name, const ASTNode& letExpr);
 
-  // Delete Letid Map. Called when we move onto the expression after (let ... )
-  void CleanupLetIDMap(void);
-
-  void push()
-  {
-    // new frame.
-    stack.push(vector<string>());
-  }
-
-  void pop()
-  {
-    vector<string> v = stack.top();
-    for (string s : v)
-    {
-      _letid_expr_map->erase(s);
-    }
-    stack.pop();
-  }
+  void commit();
+  void push();
+  void pop();
+
 };
 } // end of namespace
 

include/stp/cpp_interface.h

@@ -40,7 +40,7 @@ namespace stp
 // Foward declarations
 struct UserDefinedFlags;
 class STPMgr;
-class LETMgr;
+class LetMgr;
 
 class Cpp_interface
 {
@@ -119,7 +119,7 @@ class Cpp_interface
   bool changed_model_status;
 
 public:
-  std::unique_ptr<LETMgr> letMgr;
+  std::unique_ptr<LetMgr> letMgr;
   NodeFactory* nf;
 
   ~Cpp_interface()

lib/Interface/c_interface.cpp

@@ -1844,6 +1844,7 @@ Expr vc_parseExpr(VC vc, const char* infile)
   {
     stp::GlobalSTP = stp_i;
     stp::GlobalParserBM = b;
+    stp::GlobalParserInterface->letMgr->frameMode = false;
     cvcparse((void*)AssertsQuery);
     stp::GlobalSTP = NULL;
     stp::GlobalParserBM = NULL;

lib/Interface/cpp_interface.cpp

@@ -82,7 +82,7 @@ void Cpp_interface::removeFrame()
 }
 
 Cpp_interface::Cpp_interface(STPMgr& bm_, NodeFactory* factory)
-    : bm(bm_), letMgr(new LETMgr(bm.ASTUndefined)), nf(factory)
+    : bm(bm_), letMgr(new LetMgr(bm.ASTUndefined)), nf(factory)
 {
   init();
 }
@@ -528,7 +528,7 @@ void Cpp_interface::checkSat(const ASTVec& assertionsSMT2)
 
 // This method sets up some of the globally required data.
 Cpp_interface::Cpp_interface(STPMgr& bm_)
-    : bm(bm_), letMgr(new LETMgr(bm.ASTUndefined)), nf(bm_.defaultNodeFactory)
+    : bm(bm_), letMgr(new LetMgr(bm.ASTUndefined)), nf(bm_.defaultNodeFactory)
 {
   nf = bm.defaultNodeFactory;
   startup();

lib/Parser/LetMgr.cpp

@@ -27,89 +27,120 @@ THE SOFTWARE.
 
 namespace stp
 {
-// FUNC: This function builds the map between LET-var names and
-// LET-expressions
-//
-// 1. if the Let-var is already defined in the LET scope, then the
-// 1. function returns an error.
-//
-// 2. if the Let-var is already declared variable in the input, then
-// 2. the function returns an error
-//
-// 3. otherwise add the <var,letExpr> pair to the _letid_expr table.
-void LETMgr::LetExprMgr(const ASTNode& var, const ASTNode& letExpr)
+
+//Creates a new binding.  
+void LetMgr::LetExprMgr(const ASTNode& var, const ASTNode& letExpr)
 {
-  string name = var.GetName();
-  MapType::iterator it;
-  if (((it = _letid_expr_map->find(name)) != _letid_expr_map->end()))
+  if (var.GetKind() != SYMBOL)
   {
-    FatalError("LetExprMgr:The LET-var v has already been defined"
-               "in this LET scope: v =",
-               var);
+    std::cerr << var;
+    FatalError("Should be a symbol.");
   }
+  LetExprMgr(var.GetName(), letExpr);
+}
+
+//Creates a new binding.  
+void LetMgr::LetExprMgr(string name, const ASTNode& letExpr)
+{
+  assert(stack.size() > 0);
 
-  if (_parser_symbol_table.find(var) != _parser_symbol_table.end())
+  // In CVC lets are available immediately. In SMTLIB2 it's only when the list of them has all been done.
+  if (frameMode)
   {
-    FatalError("LetExprMgr:This var is already declared. "
-               "cannot redeclare as a letvar: v =",
-               var);
+    if (interim.find(name) != interim.end())
+      {
+        string msg = "Let already created:" + name;
+        FatalError(msg.c_str());
+      }
+    interim.insert(make_pair(name,letExpr));
   }
+  else
+  {
+    if (stack.back().find(name) != stack.back().end())
+      {
+        string msg = "Let already created:" + name;
+        FatalError(msg.c_str());
+      }
 
-  LetExprMgr(var.GetName(), letExpr);
+    stack.back().insert(make_pair(name,letExpr));
+  }
+}
+
+// We're ready for these bindings to participate. 
+void LetMgr::commit()
+{
+  if (interim.size() == 0)
+    return;
+
+  for (const auto& k : interim)
+    stack.back().insert(k);
+  interim.clear();
+}
+
+
+void LetMgr::push()
+{
+  commit();
+  stack.push_back(MapType());
 }
 
-void LETMgr::LetExprMgr(string name, const ASTNode& letExpr)
+void LetMgr::pop()
 {
-  assert(_letid_expr_map->find(name) == _letid_expr_map->end());
-  (*_letid_expr_map)[name] = letExpr;
+  if (stack.size() == 0)
+    FatalError("Popping from empty let stack");
 
-  if (stack.size() > 0) // only smtlib2 maintains the stack.
-    stack.top().push_back(name);
+  stack.erase(stack.end() - 1);
 }
 
-// this function looks up the "var to letexpr map" and returns the
+// this function looks up the symbols let-binding and returns the
 // corresponding letexpr. if there is no letexpr, then it simply
 // returns the var.
-ASTNode LETMgr::ResolveID(const ASTNode& v)
+ASTNode LetMgr::ResolveID(const ASTNode& v)
 {
   if (v.GetKind() != SYMBOL)
   {
     return v;
   }
 
-  if (_parser_symbol_table.find(v) != _parser_symbol_table.end())
-  {
-    return v;
-  }
+  //Lets shadow other symbols, so check them first.
+  if (isLetDeclared(v.GetName()))
+    return resolveLet(v.GetName());
+
+  return v;
+}
 
-  MapType::iterator it;
-  if ((it = _letid_expr_map->find(v.GetName())) != _letid_expr_map->end())
-  {
-    return it->second;
-  }
+ASTNode LetMgr::resolveLet(const string s)
+{
+  assert(isLetDeclared(s));
 
-  return v;
+  // Searches backwards because they could be shadowed.
+  for (auto i = stack.rbegin(); i != stack.rend(); ++i ) 
+      if ((*i).find(s) != (*i).end())
+        return (*i).find(s)->second;
+  FatalError("never here...");
 }
 
-// This function simply cleans up the LetID -> LetExpr Map.
-void LETMgr::CleanupLetIDMap(void)
+bool LetMgr::isLetDeclared(const string s)
 {
-  while (!stack.empty())
-  {
-    stack.pop();
-  }
+  for (auto frame : stack )
+    if (frame.find(s) != frame.end())
+      return true;
 
-  // std::unordered_map::clear() is very expensive on big empty maps. shortcut.
-  if (_letid_expr_map->size() == 0)
-    return;
+  return false;
 
-  // May contain lots of buckets, so reset.
-  delete _letid_expr_map;
-  InitializeLetIDMap();
 }
 
-void LETMgr::InitializeLetIDMap(void)
+void LetMgr::cleanupParserSymbolTable() 
 {
-  _letid_expr_map = new std::unordered_map<string, ASTNode>();
+  _parser_symbol_table.clear(); 
 }
+
+// Used only by the SMT1 & CVC parsers.
+void LetMgr::CleanupLetIDMap(void)
+{
+  interim.clear();
+  stack.clear();
+  push();
+}
+
 }

lib/Parser/cvc.y

@@ -1127,6 +1127,7 @@ LetDecl         :       STRING_TOK '=' Expr
 
 namespace stp {
   int CVCParse(void* AssertsQuery) {
+    GlobalParserInterface->letMgr->frameMode = false;
     return cvcparse(AssertsQuery);
   }
 }

lib/Parser/smt.y

@@ -643,14 +643,16 @@ LPAREN_TOK LET_TOK LPAREN_TOK QUESTION_TOK STRING_TOK an_term RPAREN_TOK
   //2. Ensure that LET variables are not
   //2. defined more than once
   GlobalParserInterface->letMgr->LetExprMgr(*$5,*$6);
-
+  GlobalParserInterface->letMgr->commit();
+
   delete $5;
   delete $6;      
 }
 | LPAREN_TOK FLET_TOK LPAREN_TOK DOLLAR_TOK STRING_TOK an_formula RPAREN_TOK 
 {
   //Do LET-expr management
   GlobalParserInterface->letMgr->LetExprMgr(*$5,*$6);
+  GlobalParserInterface->letMgr->commit();
   delete $5;
   delete $6;     
 }

lib/Parser/smt2.lex

@@ -43,6 +43,7 @@
 
   extern char *smt2text;
   extern int smt2error (const char *msg);
+  bool stringOnly = false;
 
 #ifdef _MSC_VER
   #include <io.h>
@@ -71,16 +72,24 @@
       }
     }
 
+    if (stringOnly)
+    {
+      smt2lval.str = new std::string(s);
+      if (cleaned)
+        free (cleaned);
+      return STRING_TOK;
+    }
+
     stp::ASTNode nptr;
     bool found = false;
 
-    if (stp::GlobalParserInterface->LookupSymbol(s,nptr)) // it's a symbol.
+    if (stp::GlobalParserInterface->letMgr->isLetDeclared(s)) // Lets shadow everything else.
     {
+      nptr = stp::GlobalParserInterface->letMgr->resolveLet(s);
       found = true;
     }
-    else if (stp::GlobalParserInterface->letMgr->isLetDeclared(s)) // a let.
+    else if (stp::GlobalParserInterface->LookupSymbol(s,nptr)) // it's a symbol.
     {
-      nptr = stp::GlobalParserInterface->letMgr->resolveLet(s);
       found = true;
     }
     else if (stp::GlobalParserInterface->isBitVectorFunction(s))