diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-20 10:35:38 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-20 10:35:43 +0200 |
commit | 6d82ee2d1f84065ff4a86f688a3b671b85728f80 (patch) | |
tree | aad38c08dc4cef60132a1734776c5c9d252e7806 /src/parser | |
parent | d70a63324c95210f1d78c2efc46395d2369d2e2b (diff) |
Fix a few bugs related to sygus.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 62 |
1 files changed, 38 insertions, 24 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 88709c29a..a2c859055 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -898,7 +898,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); @@ -1803,7 +1803,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] Type type; std::string s; bool isBuiltinOperator = false; - bool readLetSort = false; int match_vindex = -1; std::vector<Type> match_ptypes; } @@ -2005,27 +2004,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 +3017,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 : ')'; |