From 97c7e81a68b31328e5bf40dd6939826e3cc1cf93 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 7 Oct 2019 18:16:40 -0700 Subject: [PATCH] [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. --- src/parser/smt2/Smt2.g | 132 ++++++++++++--------------------------- src/parser/smt2/smt2.cpp | 45 +++++++++++++ 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* cmd] @declarations { - std::vector > sortedVarNames; - std::vector args, guards, heads, triggers; - Expr head, body, expr, expr2, bvl; + std::vector 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 args; std::vector< std::pair > 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 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 { @@ -2458,6 +2389,21 @@ sortedVarList[std::vector >& 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> sortedVarNames; +} + : LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK + { + std::vector 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 Smt2::assertRewriteRule( + Kind kind, + Expr bvl, + const std::vector& triggers, + const std::vector& guards, + const std::vector& heads, + Expr body) +{ + assert(kind == kind::RR_REWRITE || kind == kind::RR_REDUCTION + || kind == kind::RR_DEDUCTION); + + ExprManager* em = getExprManager(); + + std::vector 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(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& 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 @@ -197,6 +197,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 assertRewriteRule(Kind kind, + Expr bvl, + const std::vector& triggers, + const std::vector& guards, + const std::vector& 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& es); }; /* class Smt2 */ }/* CVC4::parser namespace */ -- 2.30.2