diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-07 18:16:40 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-07 18:16:40 -0700 |
commit | 97c7e81a68b31328e5bf40dd6939826e3cc1cf93 (patch) | |
tree | 9daa06998b858d27675bb3a716728e2ede3cb385 /src | |
parent | 3fac8f369bd29f9856e2b61fbb5029d780fde64b (diff) |
[SMT2 Parser] Move code of `rewriterulesCommand` (#3334)
This commit moves the code in `rewriterulesCommand` in the SMT2 parser
to the `Smt2` class. Additionally, it creates a `boundVarList` rule to
reduce code duplication.
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/smt2/Smt2.g | 132 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 45 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 27 |
3 files changed, 111 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 */ diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ec4fd0fa3..ba512ded9 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -627,6 +627,33 @@ void Smt2::resetAssertions() { } } +std::unique_ptr<Command> Smt2::assertRewriteRule( + Kind kind, + Expr bvl, + const std::vector<Expr>& triggers, + const std::vector<Expr>& guards, + const std::vector<Expr>& heads, + Expr body) +{ + assert(kind == kind::RR_REWRITE || kind == kind::RR_REDUCTION + || kind == kind::RR_DEDUCTION); + + ExprManager* em = getExprManager(); + + std::vector<Expr> args; + args.push_back(mkAnd(heads)); + args.push_back(body); + + if (!triggers.empty()) + { + args.push_back(em->mkExpr(kind::INST_PATTERN_LIST, triggers)); + } + + Expr rhs = em->mkExpr(kind, args); + Expr rule = em->mkExpr(kind::REWRITE_RULE, bvl, mkAnd(guards), rhs); + return std::unique_ptr<Command>(new AssertCommand(rule, false)); +} + Smt2::SynthFunFactory::SynthFunFactory( Smt2* smt2, const std::string& fun, @@ -1904,5 +1931,23 @@ Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr) return func; } +Expr Smt2::mkAnd(const std::vector<Expr>& es) +{ + ExprManager* em = getExprManager(); + + if (es.size() == 0) + { + return em->mkConst(true); + } + else if (es.size() == 1) + { + return es[0]; + } + else + { + return em->mkExpr(kind::AND, es); + } +} + } // namespace parser }/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 5caedb934..ec7e2071a 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -198,6 +198,24 @@ class Smt2 : public Parser void resetAssertions(); /** + * Creates a command that asserts a rule. + * + * @param kind The kind of rule (RR_REWRITE, RR_REDUCTION, RR_DEDUCTION) + * @param bvl Bound variable list + * @param triggers List of triggers + * @param guards List of guards + * @param heads List of heads + * @param body The body of the rule + * @return The command that asserts the rewrite rule + */ + std::unique_ptr<Command> assertRewriteRule(Kind kind, + Expr bvl, + const std::vector<Expr>& triggers, + const std::vector<Expr>& guards, + const std::vector<Expr>& heads, + Expr body); + + /** * Class for creating instances of `SynthFunCommand`s. Creating an instance * of this class pushes the scope, destroying it pops the scope. */ @@ -624,6 +642,15 @@ class Smt2 : public Parser void addSepOperators(); InputLanguage getLanguage() const; + + /** + * Utility function to create a conjunction of expressions. + * + * @param es Expressions in the conjunction + * @return True if `es` is empty, `e` if `es` consists of a single element + * `e`, the conjunction of expressions otherwise. + */ + Expr mkAnd(const std::vector<Expr>& es); }; /* class Smt2 */ }/* CVC4::parser namespace */ |