[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.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c63bc4a95d1cec58b6eceef521ac29818fa27d02..dc57be11e446d727e83209c259e5e55e5c06180a 100644 (file)
--- 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
   {
@@ -2458,6 +2389,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 ec4fd0fa3048304c4411760d3e0916ca6e6cae81..ba512ded9aa4607d282c6a4b968b7485488b7f63 100644 (file)
--- 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 5caedb934bb0a5986c18aca36ab5857632854b50..ec7e2071a705a16ea83d8db9a146ec496f073833 100644 (file)
--- 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<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 */