diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 21 |
1 files changed, 1 insertions, 20 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 6a0bf2188..21e09317d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -886,28 +886,12 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] Type t; std::string sname; std::vector< Expr > let_vars; - bool readingLet = false; std::string s; CVC4::api::Term atomTerm; } : LPAREN_TOK //read operator - ( SYGUS_LET_TOK LPAREN_TOK { - sgt.d_name = std::string("let"); - sgt.d_gterm_type = SygusGTerm::gterm_let; - PARSER_STATE->pushScope(true); - readingLet = true; - } - ( LPAREN_TOK - symbol[sname,CHECK_NONE,SYM_VARIABLE] - sortSymbol[t,CHECK_DECLARED] { - Expr v = PARSER_STATE->mkBoundVar(sname,t); - sgt.d_let_vars.push_back( v ); - sgt.addChild(); - } - sygusGTerm[sgt.d_children.back(), fun] - RPAREN_TOK )+ RPAREN_TOK - | SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED] + ( SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED] { sgt.d_gterm_type = SygusGTerm::gterm_constant; sgt.d_type = t; Debug("parser-sygus") << "Sygus grammar constant." << std::endl; @@ -971,9 +955,6 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] RPAREN_TOK { //pop last child index sgt.d_children.pop_back(); - if( readingLet ){ - PARSER_STATE->popScope(); - } } | termAtomic[atomTerm] { |