diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 69 |
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 : ')'; |