diff options
author | François Bobot <francois@bobot.eu> | 2012-07-27 13:36:32 +0000 |
---|---|---|
committer | François Bobot <francois@bobot.eu> | 2012-07-27 13:36:32 +0000 |
commit | 4bfa927dac67bbcadf219f70e61f1d123e33944b (patch) | |
tree | f295343430799748de8b9a823f1a3c641c096905 /src/parser | |
parent | 988c97d92fa617c5dccaeb1ef33121bfa6459afc (diff) |
Merge quantifiers2-trunk:
- new syntax for rewrite rules
- better rewrite rules theory
- remove the rewriting with rewrite rules during ppRewrite temporarily
- theory can define their own candidate generator
- define a general candidate generator (inefficient ask to every theory)
- split inst_match between the pattern matching used for quantifiers (inst_match.*) and
the one used for rewrite rules (rr_inst_match.*):
- the pattern matching is less exhaustive for quantifiers,
- the one for rewrite rules can use efficient-e-matching.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 123 |
1 files changed, 123 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index be5a797bf..56fa93a94 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -398,6 +398,126 @@ extendedCommand[CVC4::Command*& cmd] } | { cmd = new EchoCommand(); } ) + | rewriterulesCommand[cmd] + ; + +rewriterulesCommand[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; + Kind kind; +} + : /* rewrite rules */ + REWRITE_RULE_TOK + LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK + { + kind = CVC4::kind::RR_REWRITE; + PARSER_STATE->pushScope(); + for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = + sortedVarNames.begin(), iend = sortedVarNames.end(); + i != iend; + ++i) { + args.push_back(PARSER_STATE->mkVar((*i).first, (*i).second)); + } + bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); + } + LPAREN_TOK (termList[guards,expr])? RPAREN_TOK + term[head, expr2] term[body, expr2] + LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK + { + 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 = new AssertCommand(expr); } + /* propagation rule */ + | rewritePropaKind[kind] + LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK + { + PARSER_STATE->pushScope(); + for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = + sortedVarNames.begin(), iend = sortedVarNames.end(); + i != iend; + ++i) { + args.push_back(PARSER_STATE->mkVar((*i).first, (*i).second)); + } + bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); + } + LPAREN_TOK (termList[guards,expr])? RPAREN_TOK + LPAREN_TOK (termList[heads,expr])? RPAREN_TOK + term[body, expr2] + LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK + { + 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 = new AssertCommand(expr); } + ; + +rewritePropaKind[CVC4::Kind& kind] + : + REDUCTION_RULE_TOK { $kind = CVC4::kind::RR_REDUCTION; } + | PROPAGATION_RULE_TOK { $kind = CVC4::kind::RR_DEDUCTION; } + ; + +pattern[CVC4::Expr& expr] +@declarations { + std::vector<Expr> patexpr; +} + : LPAREN_TOK termList[patexpr,expr] RPAREN_TOK + { + expr = MK_EXPR(kind::INST_PATTERN, patexpr); + //std::cout << "parsed pattern expr " << retExpr << std::endl; + } ; simpleSymbolicExpr[CVC4::SExpr& sexpr] @@ -1076,6 +1196,9 @@ POP_TOK : 'pop'; DECLARE_DATATYPES_TOK : 'declare-datatypes'; GET_MODEL_TOK : 'get-model'; ECHO_TOK : 'echo'; +REWRITE_RULE_TOK : 'assert-rewrite'; +REDUCTION_RULE_TOK : 'assert-reduction'; +PROPAGATION_RULE_TOK : 'assert-propagation'; // attributes ATTRIBUTE_PATTERN_TOK : ':pattern'; |