1 files changed, 42 insertions, 27 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 88709c29a..c7156635d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -117,6 +117,7 @@ namespace CVC4 {
 #include <set>
 #include <sstream>
 #include <string>
+#include <unordered_set>
 #include <vector>
 
 #include "base/output.h"
@@ -150,7 +151,7 @@ using namespace CVC4::parser;
 #define MK_CONST EXPR_MANAGER->mkConst
 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
 
-static bool isClosed(const Expr& e, std::set<Expr>& free, std::hash_set<Expr, ExprHashFunction>& closedCache) {
+static bool isClosed(const Expr& e, std::set<Expr>& free, std::unordered_set<Expr, ExprHashFunction>& closedCache) {
   if(closedCache.find(e) != closedCache.end()) {
     return true;
   }
@@ -181,7 +182,7 @@ static bool isClosed(const Expr& e, std::set<Expr>& free, std::hash_set<Expr, Ex
 }
 
 static inline bool isClosed(const Expr& e, std::set<Expr>& free) {
-  std::hash_set<Expr, ExprHashFunction> cache;
+  std::unordered_set<Expr, ExprHashFunction> cache;
   return isClosed(e, free, cache);
 }  
   
@@ -898,7 +899,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
         sgt.d_gterm_type = SygusGTerm::gterm_op;
         sgt.d_expr = EXPR_MANAGER->operatorOf(k);
       }
-     | LET_TOK LPAREN_TOK { 
+     | SYGUS_LET_TOK LPAREN_TOK { 
          sgt.d_name = std::string("let");
          sgt.d_gterm_type = SygusGTerm::gterm_let;
          PARSER_STATE->pushScope(true);
@@ -1798,12 +1799,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   Expr attexpr;
   std::vector<Expr> patexprs;
   std::vector<Expr> patconds;
-  std::hash_set<std::string, StringHashFunction> names;
+  std::unordered_set<std::string> names;
   std::vector< std::pair<std::string, Expr> > binders;
   Type type;
   std::string s;
   bool isBuiltinOperator = false;
-  bool readLetSort = false;
   int match_vindex = -1;
   std::vector<Type> match_ptypes;
 }
@@ -2005,27 +2005,41 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = MK_CONST( ::CVC4::ArrayStoreAll(type, f) );
       }
     )
-  | /* a let binding */
-    LPAREN_TOK LET_TOK LPAREN_TOK
-    { PARSER_STATE->pushScope(true); }
-    ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
-      (term[expr, f2] | sortSymbol[type,CHECK_DECLARED]
-       { readLetSort = true; } term[expr, f2]
-      )
-      RPAREN_TOK
-      // this is a parallel let, so we have to save up all the contributions
-      // of the let and define them only later on
-      { if( !PARSER_STATE->sygus() && readLetSort ){
-          PARSER_STATE->parseError("Bad syntax for let term.");
-        }else if(names.count(name) == 1) {
-          std::stringstream ss;
-          ss << "warning: symbol `" << name << "' bound multiple times by let;"
-             << " the last binding will be used, shadowing earlier ones";
-          PARSER_STATE->warning(ss.str());
-        } else {
-          names.insert(name);
-        }
-        binders.push_back(std::make_pair(name, expr)); } )+
+  | /* a let or sygus let binding */
+    LPAREN_TOK ( 
+      LET_TOK LPAREN_TOK
+      { PARSER_STATE->pushScope(true); }
+      ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
+        term[expr, f2]
+        RPAREN_TOK
+        // this is a parallel let, so we have to save up all the contributions
+        // of the let and define them only later on
+        { if(names.count(name) == 1) {
+            std::stringstream ss;
+            ss << "warning: symbol `" << name << "' bound multiple times by let;"
+               << " the last binding will be used, shadowing earlier ones";
+            PARSER_STATE->warning(ss.str());
+          } else {
+            names.insert(name);
+          }
+          binders.push_back(std::make_pair(name, expr)); } )+ |
+      SYGUS_LET_TOK LPAREN_TOK
+      { PARSER_STATE->pushScope(true); }
+      ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
+        sortSymbol[type,CHECK_DECLARED]
+        term[expr, f2]
+        RPAREN_TOK
+        // this is a parallel let, so we have to save up all the contributions
+        // of the let and define them only later on
+        { if(names.count(name) == 1) {
+            std::stringstream ss;
+            ss << "warning: symbol `" << name << "' bound multiple times by let;"
+               << " the last binding will be used, shadowing earlier ones";
+            PARSER_STATE->warning(ss.str());
+          } else {
+            names.insert(name);
+          }
+          binders.push_back(std::make_pair(name, expr)); } )+ )
     { // now implement these bindings
       for(std::vector< std::pair<std::string, Expr> >::iterator
             i = binders.begin(); i != binders.end(); ++i) {
@@ -3004,7 +3018,8 @@ EXIT_TOK : 'exit';
 RESET_TOK : { PARSER_STATE->v2_5(false) }? 'reset';
 RESET_ASSERTIONS_TOK : 'reset-assertions';
 ITE_TOK : 'ite';
-LET_TOK : 'let';
+LET_TOK : { !PARSER_STATE->sygus() }? 'let';
+SYGUS_LET_TOK : { PARSER_STATE->sygus() }? 'let';
 ATTRIBUTE_TOK : '!';
 LPAREN_TOK : '(';
 RPAREN_TOK : ')';