Demote BETA_REDUCE and ARRAYS_EQ_RANGE_EXPAND to ProofRewriteRules (c…

…vc5#10699)

include/cvc5/cvc5_proof_rule.h

@@ -1142,21 +1142,6 @@ enum ENUM(ProofRule) : uint32_t
    * \endverbatim
    */
   EVALUE(HO_CONG),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Equality -- Beta reduction**
-   *
-   * .. math::
-   *
-   *   \inferrule{\mid \lambda x_1\dots x_n.\> t, t_1,\dots,t_n}
-   *   {((\lambda x_1\dots x_n.\> t) t_1 \ldots t_n)=t\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}}
-   *
-   * The right hand side of the equality in the conclusion is computed using
-   * standard substitution via Node::substitute.
-   * \endverbatim
-   */
-  EVALUE(BETA_REDUCE),
-
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Arrays -- Read over write**
@@ -1204,19 +1189,6 @@ enum ENUM(ProofRule) : uint32_t
    * \endverbatim
    */
   EVALUE(ARRAYS_EXT),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Arrays -- Expansion of array range equality**
-   *
-   * .. math::
-   *
-   *   \inferrule{-\mid \mathit{eqrange}(a,b,i,j)}
-   *   {\mathit{eqrange}(a,b,i,j)=
-   *   \forall x.\> i \leq x \leq j \rightarrow
-   *   \mathit{select}(a,x)=\mathit{select}(b,x)}
-   * \endverbatim
-   */
-  EVALUE(ARRAYS_EQ_RANGE_EXPAND),
 
   /**
    * \verbatim embed:rst:leading-asterisk
@@ -2296,6 +2268,31 @@ enum ENUM(ProofRewriteRule) : uint32_t
    * \endverbatim
    */
   EVALUE(DISTINCT_ELIM),
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Equality -- Beta reduction**
+   *
+   * .. math::
+   *
+   *   ((\lambda x_1\dots x_n.\> t) t_1 \ldots t_n)=t\{x_1\mapsto
+   * t_1,\dots,x_n\mapsto t_n\}
+   *
+   * The right hand side of the equality in the conclusion is computed using
+   * standard substitution via Node::substitute.
+   * \endverbatim
+   */
+  EVALUE(BETA_REDUCE),
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Arrays -- Expansion of array range equality**
+   *
+   * .. math::
+   *   \mathit{eqrange}(a,b,i,j)=
+   *   \forall x.\> i \leq x \leq j \rightarrow
+   *   \mathit{select}(a,x)=\mathit{select}(b,x)
+   * \endverbatim
+   */
+  EVALUE(ARRAYS_EQ_RANGE_EXPAND),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Quantifiers -- Exists elimination**

src/api/cpp/cvc5_proof_rule_template.cpp

@@ -111,14 +111,12 @@ const char* toString(ProofRule rule)
     case ProofRule::FALSE_ELIM: return "FALSE_ELIM";
     case ProofRule::HO_APP_ENCODE: return "HO_APP_ENCODE";
     case ProofRule::HO_CONG: return "HO_CONG";
-    case ProofRule::BETA_REDUCE: return "BETA_REDUCE";
     //================================================= Array rules
     case ProofRule::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE";
     case ProofRule::ARRAYS_READ_OVER_WRITE_CONTRA:
       return "ARRAYS_READ_OVER_WRITE_CONTRA";
     case ProofRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1";
     case ProofRule::ARRAYS_EXT: return "ARRAYS_EXT";
-    case ProofRule::ARRAYS_EQ_RANGE_EXPAND: return "ARRAYS_EQ_RANGE_EXPAND";
     //================================================= Bit-Vector rules
     case ProofRule::MACRO_BV_BITBLAST: return "MACRO_BV_BITBLAST";
     case ProofRule::BV_BITBLAST_STEP: return "BV_BITBLAST_STEP";
@@ -222,6 +220,9 @@ const char* toString(cvc5::ProofRewriteRule rule)
     case ProofRewriteRule::NONE: return "NONE";
     //================================================= ad-hoc rules
     case ProofRewriteRule::DISTINCT_ELIM: return "distinct-elim";
+    case ProofRewriteRule::BETA_REDUCE: return "beta-reduce";
+    case ProofRewriteRule::ARRAYS_EQ_RANGE_EXPAND:
+      return "arrays-eq-range-expand";
     case ProofRewriteRule::EXISTS_ELIM: return "exists-elim";
     case ProofRewriteRule::DT_COLLAPSE_SELECTOR: return "dt-collapse-selector";
     case ProofRewriteRule::DT_COLLAPSE_TESTER: return "dt-collapse-tester";

src/proof/eager_proof_generator.cpp

@@ -18,6 +18,7 @@
 #include "proof/proof.h"
 #include "proof/proof_node.h"
 #include "proof/proof_node_manager.h"
+#include "rewriter/rewrites.h"
 #include "smt/env.h"
 
 namespace cvc5::internal {
@@ -125,6 +126,16 @@ TrustNode EagerProofGenerator::mkTrustNode(Node conc,
   return mkTrustNode(pfs->getResult(), pfs, isConflict);
 }
 
+TrustNode EagerProofGenerator::mkTrustNodeRewrite(const Node& a,
+                                                  const Node& b,
+                                                  ProofRewriteRule id)
+{
+  std::vector<Node> args;
+  args.push_back(rewriter::mkRewriteRuleNode(id));
+  args.push_back(a);
+  return mkTrustedRewrite(a, b, ProofRule::THEORY_REWRITE, args);
+}
+
 TrustNode EagerProofGenerator::mkTrustedRewrite(Node a,
                                                 Node b,
                                                 std::shared_ptr<ProofNode> pf)

src/proof/eager_proof_generator.h

@@ -137,6 +137,21 @@ class EagerProofGenerator : protected EnvObj, public ProofGenerator
                         const std::vector<Node>& exp,
                         const std::vector<Node>& args,
                         bool isConflict = false);
+  /**
+   * Make trust node from a single step proof of a rewrite. This is a
+   * convenience function that avoids the need to explictly construct ProofNode
+   * by the caller.
+   *
+   * @param a the original
+   * @param b what is rewrites to
+   * @param id The rewrite rule of the proof concluding conc based on rewriting
+   * the term a.
+   * @return The trust node corresponding to the fact that this generator has
+   * a proof of a=b.
+   */
+  TrustNode mkTrustNodeRewrite(const Node& a,
+                               const Node& b,
+                               ProofRewriteRule id);
   /**
    * Make trust node: wrap `exp => n` in a trust node with this generator, and
    * have it store the proof `pf` too.

src/proof/lfsc/lfsc_post_processor.cpp

@@ -22,6 +22,7 @@
 #include "proof/proof_node_algorithm.h"
 #include "proof/proof_node_manager.h"
 #include "proof/proof_node_updater.h"
+#include "rewriter/rewrites.h"
 #include "smt/env.h"
 #include "theory/strings/theory_strings_utils.h"
 
@@ -430,11 +431,20 @@ bool LfscProofPostprocessCallback::update(Node res,
       }
     }
     break;
-    case ProofRule::BETA_REDUCE:
+    case ProofRule::THEORY_REWRITE:
     {
-      // get the term to beta-reduce
-      Node termToReduce = nm->mkNode(Kind::APPLY_UF, args);
-      addLfscRule(cdp, res, {}, LfscRule::BETA_REDUCE, {termToReduce});
+      Assert(args.size() >= 2);
+      ProofRewriteRule idr;
+      if (!rewriter::getRewriteRule(args[0], idr))
+      {
+        return false;
+      }
+      if (idr == ProofRewriteRule::BETA_REDUCE)
+      {
+        // get the term to beta-reduce
+        Node termToReduce = nm->mkNode(Kind::APPLY_UF, args[1]);
+        addLfscRule(cdp, res, {}, LfscRule::BETA_REDUCE, {termToReduce});
+      }
     }
     break;
     default: return false; break;

src/rewriter/basic_rewrite_rcons.cpp

@@ -64,19 +64,6 @@ bool BasicRewriteRCons::prove(
       return true;
     }
   }
-
-  if (eq[0].getKind() == Kind::APPLY_UF
-      && eq[0].getOperator().getKind() == Kind::LAMBDA)
-  {
-    std::vector<Node> args;
-    args.push_back(eq[0].getOperator());
-    args.insert(args.end(), eq[0].begin(), eq[0].end());
-    if (tryRule(cdp, eq, ProofRule::BETA_REDUCE, args))
-    {
-      Trace("trewrite-rcons") << "...BETA_REDUCE" << std::endl;
-      return true;
-    }
-  }
   Trace("trewrite-rcons") << "...(fail)" << std::endl;
   return false;
 }

src/theory/arrays/proof_checker.cpp

@@ -34,7 +34,6 @@ void ArraysProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(ProofRule::ARRAYS_READ_OVER_WRITE_CONTRA, this);
   pc->registerChecker(ProofRule::ARRAYS_READ_OVER_WRITE_1, this);
   pc->registerChecker(ProofRule::ARRAYS_EXT, this);
-  pc->registerChecker(ProofRule::ARRAYS_EQ_RANGE_EXPAND, this);
 }
 
 Node ArraysProofRuleChecker::checkInternal(ProofRule id,
@@ -108,11 +107,6 @@ Node ArraysProofRuleChecker::checkInternal(ProofRule id,
     Node bs = nm->mkNode(Kind::SELECT, b, k);
     return as.eqNode(bs).notNode();
   }
-  if (id == ProofRule::ARRAYS_EQ_RANGE_EXPAND)
-  {
-    Node expandedEqRange = TheoryArraysRewriter::expandEqRange(args[0]);
-    return args[0].eqNode(expandedEqRange);
-  }
   // no rule
   return Node::null();
 }

src/theory/arrays/theory_arrays_rewriter.cpp

@@ -64,6 +64,25 @@ TheoryArraysRewriter::TheoryArraysRewriter(NodeManager* nm,
                                            EagerProofGenerator* epg)
     : TheoryRewriter(nm), d_rewriter(r), d_epg(epg)
 {
+  registerProofRewriteRule(ProofRewriteRule::ARRAYS_EQ_RANGE_EXPAND,
+                           TheoryRewriteCtx::PRE_DSL);
+}
+
+Node TheoryArraysRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
+{
+  switch (id)
+  {
+    case ProofRewriteRule::ARRAYS_EQ_RANGE_EXPAND:
+    {
+      if (n.getKind() == Kind::EQ_RANGE)
+      {
+        return expandEqRange(n);
+      }
+    break;
+    }
+    default: break;
+  }
+  return Node::null();
 }
 
 Node TheoryArraysRewriter::normalizeConstant(TNode node)
@@ -692,11 +711,8 @@ TrustNode TheoryArraysRewriter::expandDefinition(Node node)
     Node expandedEqRange = expandEqRange(node);
     if (d_epg)
     {
-      TrustNode tn = d_epg->mkTrustNode(node.eqNode(expandedEqRange),
-                                        ProofRule::ARRAYS_EQ_RANGE_EXPAND,
-                                        {},
-                                        {node});
-      return TrustNode::mkTrustRewrite(node, expandedEqRange, d_epg);
+      return d_epg->mkTrustNodeRewrite(
+          node, expandedEqRange, ProofRewriteRule::ARRAYS_EQ_RANGE_EXPAND);
     }
     return TrustNode::mkTrustRewrite(node, expandedEqRange, nullptr);
   }

src/theory/arrays/theory_arrays_rewriter.h

@@ -63,6 +63,15 @@ class TheoryArraysRewriter : public TheoryRewriter
 
   RewriteResponse preRewrite(TNode node) override;
 
+  /**
+   * Rewrite n based on the proof rewrite rule id.
+   * @param id The rewrite rule.
+   * @param n The node to rewrite.
+   * @return The rewritten version of n based on id, or Node::null() if n
+   * cannot be rewritten.
+   */
+  Node rewriteViaRule(ProofRewriteRule id, const Node& n) override;
+
   TrustNode expandDefinition(Node node) override;
 
   /**

src/theory/uf/proof_checker.cpp

@@ -37,7 +37,6 @@ void UfProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(ProofRule::FALSE_ELIM, this);
   pc->registerChecker(ProofRule::HO_CONG, this);
   pc->registerChecker(ProofRule::HO_APP_ENCODE, this);
-  pc->registerChecker(ProofRule::BETA_REDUCE, this);
 }
 
 Node UfProofRuleChecker::checkInternal(ProofRule id,
@@ -205,29 +204,6 @@ Node UfProofRuleChecker::checkInternal(ProofRule id,
     Node ret = TheoryUfRewriter::getHoApplyForApplyUf(args[0]);
     return args[0].eqNode(ret);
   }
-  else if (id == ProofRule::BETA_REDUCE)
-  {
-    Assert(args.size() >= 2);
-    Node lambda = args[0];
-    if (lambda.getKind() != Kind::LAMBDA)
-    {
-      return Node::null();
-    }
-    std::vector<TNode> vars(lambda[0].begin(), lambda[0].end());
-    std::vector<TNode> subs(args.begin() + 1, args.end());
-    if (vars.size() != subs.size())
-    {
-      return Node::null();
-    }
-    NodeManager* nm = nodeManager();
-    std::vector<Node> appArgs;
-    appArgs.push_back(lambda);
-    appArgs.insert(appArgs.end(), subs.begin(), subs.end());
-    Node app = nm->mkNode(Kind::APPLY_UF, appArgs);
-    Node ret = lambda[1].substitute(
-        vars.begin(), vars.end(), subs.begin(), subs.end());
-    return app.eqNode(ret);
-  }
   // no rule
   return Node::null();
 }

src/theory/uf/theory_uf_rewriter.cpp

@@ -29,7 +29,11 @@ namespace cvc5::internal {
 namespace theory {
 namespace uf {
 
-TheoryUfRewriter::TheoryUfRewriter(NodeManager* nm) : TheoryRewriter(nm) {}
+TheoryUfRewriter::TheoryUfRewriter(NodeManager* nm) : TheoryRewriter(nm)
+{
+  registerProofRewriteRule(ProofRewriteRule::BETA_REDUCE,
+                           TheoryRewriteCtx::PRE_DSL);
+}
 
 RewriteResponse TheoryUfRewriter::postRewrite(TNode node)
 {
@@ -153,6 +157,34 @@ RewriteResponse TheoryUfRewriter::preRewrite(TNode node)
   return RewriteResponse(REWRITE_DONE, node);
 }
 
+Node TheoryUfRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
+{
+  switch (id)
+  {
+    case ProofRewriteRule::BETA_REDUCE:
+    {
+      if (n.getKind() != Kind::APPLY_UF
+          || n.getOperator().getKind() != Kind::LAMBDA)
+      {
+        return Node::null();
+      }
+      Node lambda = n.getOperator();
+      std::vector<TNode> vars(lambda[0].begin(), lambda[0].end());
+      std::vector<TNode> subs(n.begin(), n.end());
+      if (vars.size() != subs.size())
+      {
+        return Node::null();
+      }
+      Node ret = lambda[1].substitute(
+          vars.begin(), vars.end(), subs.begin(), subs.end());
+      return ret;
+    }
+    break;
+    default: break;
+  }
+  return Node::null();
+}
+
 Node TheoryUfRewriter::getHoApplyForApplyUf(TNode n)
 {
   Assert(n.getKind() == Kind::APPLY_UF);

src/theory/uf/theory_uf_rewriter.h

@@ -39,6 +39,14 @@ class TheoryUfRewriter : public TheoryRewriter
   RewriteResponse postRewrite(TNode node) override;
   /** pre-rewrite */
   RewriteResponse preRewrite(TNode node) override;
+  /**
+   * Rewrite n based on the proof rewrite rule id.
+   * @param id The rewrite rule.
+   * @param n The node to rewrite.
+   * @return The rewritten version of n based on id, or Node::null() if n
+   * cannot be rewritten.
+   */
+  Node rewriteViaRule(ProofRewriteRule id, const Node& n) override;
   // conversion between HO_APPLY AND APPLY_UF
   /**
    * converts an APPLY_UF to a curried HO_APPLY e.g.