diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 132 |
1 files changed, 39 insertions, 93 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index c63bc4a95..dc57be11e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1547,94 +1547,33 @@ datatypesDef[bool isCo, rewriterulesCommand[std::unique_ptr<CVC4::Command>* cmd] @declarations { - std::vector<std::pair<std::string, Type> > sortedVarNames; - std::vector<Expr> args, guards, heads, triggers; - Expr head, body, expr, expr2, bvl; + std::vector<Expr> guards, heads, triggers; + Expr head, body, bvl, expr, expr2; Kind kind; } : /* rewrite rules */ - REWRITE_RULE_TOK - LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - { - kind = CVC4::kind::RR_REWRITE; - PARSER_STATE->pushScope(true); - args = PARSER_STATE->mkBoundVars(sortedVarNames); - bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); - } + REWRITE_RULE_TOK { kind = CVC4::kind::RR_REWRITE; } + { PARSER_STATE->pushScope(true); } + boundVarList[bvl] LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK LPAREN_TOK (termList[guards,expr])? RPAREN_TOK - term[head, expr2] term[body, expr2] + term[head, expr2] + term[body, expr2] { - args.clear(); - args.push_back(head); - args.push_back(body); - /* triggers */ - if( !triggers.empty() ){ - expr2 = MK_EXPR(kind::INST_PATTERN_LIST, triggers); - args.push_back(expr2); - }; - expr = MK_EXPR(kind, args); - args.clear(); - args.push_back(bvl); - /* guards */ - switch( guards.size() ){ - case 0: - args.push_back(MK_CONST(bool(true))); break; - case 1: - args.push_back(guards[0]); break; - default: - expr2 = MK_EXPR(kind::AND, guards); - args.push_back(expr2); break; - }; - args.push_back(expr); - expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args); - cmd->reset(new AssertCommand(expr, false)); } + *cmd = PARSER_STATE->assertRewriteRule( + kind, bvl, triggers, guards, {head}, body); + } /* propagation rule */ | rewritePropaKind[kind] - LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - { - PARSER_STATE->pushScope(true); - args = PARSER_STATE->mkBoundVars(sortedVarNames); - bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); - } + { PARSER_STATE->pushScope(true); } + boundVarList[bvl] LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK LPAREN_TOK (termList[guards,expr])? RPAREN_TOK LPAREN_TOK (termList[heads,expr])? RPAREN_TOK term[body, expr2] { - args.clear(); - /* heads */ - switch( heads.size() ){ - case 0: - args.push_back(MK_CONST(bool(true))); break; - case 1: - args.push_back(heads[0]); break; - default: - expr2 = MK_EXPR(kind::AND, heads); - args.push_back(expr2); break; - }; - args.push_back(body); - /* triggers */ - if( !triggers.empty() ){ - expr2 = MK_EXPR(kind::INST_PATTERN_LIST, triggers); - args.push_back(expr2); - }; - expr = MK_EXPR(kind, args); - args.clear(); - args.push_back(bvl); - /* guards */ - switch( guards.size() ){ - case 0: - args.push_back(MK_CONST(bool(true))); break; - case 1: - args.push_back(guards[0]); break; - default: - expr2 = MK_EXPR(kind::AND, guards); - args.push_back(expr2); break; - }; - args.push_back(expr); - expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args); - cmd->reset(new AssertCommand(expr, false)); + *cmd = PARSER_STATE->assertRewriteRule( + kind, bvl, triggers, guards, heads, body); } ; @@ -1752,6 +1691,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] std::string name; std::vector<Expr> args; std::vector< std::pair<std::string, Type> > sortedVarNames; + Expr bvl; Expr f, f2, f3; std::string attr; Expr attexpr; @@ -1766,16 +1706,12 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] std::vector<Type> argTypes; } : LPAREN_TOK quantOp[kind] - LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - { - PARSER_STATE->pushScope(true); - args = PARSER_STATE->mkBoundVars(sortedVarNames); - Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); - args.clear(); - args.push_back(bvl); - } + { PARSER_STATE->pushScope(true); } + boundVarList[bvl] term[f, f2] RPAREN_TOK { + args.push_back(bvl); + PARSER_STATE->popScope(); switch(f.getKind()) { case CVC4::kind::RR_REWRITE: @@ -2000,19 +1936,14 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] } | /* lambda */ LPAREN_TOK HO_LAMBDA_TOK - LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - { - PARSER_STATE->pushScope(true); - args = PARSER_STATE->mkBoundVars(sortedVarNames); - Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); - args.clear(); - args.push_back(bvl); - } + { PARSER_STATE->pushScope(true); } + boundVarList[bvl] term[f, f2] RPAREN_TOK { - args.push_back( f ); + args.push_back(bvl); + args.push_back(f); PARSER_STATE->popScope(); - expr = MK_EXPR( CVC4::kind::LAMBDA, args ); + expr = MK_EXPR(CVC4::kind::LAMBDA, args); } | LPAREN_TOK TUPLE_CONST_TOK termList[args,expr] RPAREN_TOK { @@ -2459,6 +2390,21 @@ sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars] ; /** + * Matches a sequence of (variable, sort) symbol pairs, registers them as bound + * variables, and returns a term corresponding to the list of pairs. + */ +boundVarList[CVC4::Expr& expr] +@declarations { + std::vector<std::pair<std::string, CVC4::Type>> sortedVarNames; +} + : LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK + { + std::vector<CVC4::Expr> args = PARSER_STATE->mkBoundVars(sortedVarNames); + expr = MK_EXPR(kind::BOUND_VAR_LIST, args); + } + ; + +/** * Matches the sort symbol, which can be an arbitrary symbol. * @param check the check to perform on the name */ |