From 692838a334b6a0e68ecfe7e9f473a834f99ba5e6 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 8 Sep 2021 02:00:23 -0500
Subject: [PATCH] Use rewriteViaMethod instead of accessing builtin proof
 checker (#7146)

---
 src/proof/method_id.h                |  3 ++-
 src/smt/proof_post_processor.cpp     | 13 ++++---------
 src/theory/builtin/proof_checker.cpp | 11 +++--------
 src/theory/builtin/proof_checker.h   | 10 ----------
 4 files changed, 9 insertions(+), 28 deletions(-)

diff --git a/src/proof/method_id.h b/src/proof/method_id.h
index b353232f4..fe7a9a90d 100644
--- a/src/proof/method_id.h
+++ b/src/proof/method_id.h
@@ -49,7 +49,8 @@ enum class MethodId : uint32_t
   RW_IDENTITY,
   // theory preRewrite, note this is only intended to be used as an argument
   // to THEORY_REWRITE in the final proof. It is not implemented in
-  // applyRewrite below, see documentation in proof_rule.h for THEORY_REWRITE.
+  // Rewriter::rewriteViaMethod, see documentation in proof_rule.h for
+  // THEORY_REWRITE.
   RW_REWRITE_THEORY_PRE,
   // same as above, for theory postRewrite
   RW_REWRITE_THEORY_POST,
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 9db8f1020..f5d0e8ee8 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -477,10 +477,8 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
         rargs.push_back(args[3]);
       }
     }
-    builtin::BuiltinProofRuleChecker* builtinPfC =
-        static_cast<builtin::BuiltinProofRuleChecker*>(
-            d_pnm->getChecker()->getCheckerFor(PfRule::MACRO_SR_EQ_INTRO));
-    Node tr = builtinPfC->applyRewrite(ts, idr);
+    Rewriter* rr = d_env.getRewriter();
+    Node tr = rr->rewriteViaMethod(ts, idr);
     Trace("smt-proof-pp-debug")
         << "...eq intro rewrite equality is " << ts << " == " << tr << ", from "
         << idr << std::endl;
@@ -954,17 +952,14 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     {
       getMethodId(args[1], idr);
     }
-    builtin::BuiltinProofRuleChecker* builtinPfC =
-        static_cast<builtin::BuiltinProofRuleChecker*>(
-            d_pnm->getChecker()->getCheckerFor(PfRule::REWRITE));
-    Node ret = builtinPfC->applyRewrite(args[0], idr);
+    Rewriter* rr = d_env.getRewriter();
+    Node ret = rr->rewriteViaMethod(args[0], idr);
     Node eq = args[0].eqNode(ret);
     if (idr == MethodId::RW_REWRITE || idr == MethodId::RW_REWRITE_EQ_EXT)
     {
       // rewrites from theory::Rewriter
       bool isExtEq = (idr == MethodId::RW_REWRITE_EQ_EXT);
       // use rewrite with proof interface
-      Rewriter* rr = d_env.getRewriter();
       TrustNode trn = rr->rewriteWithProof(args[0], isExtEq);
       std::shared_ptr<ProofNode> pfn = trn.toProofNode();
       if (pfn == nullptr)
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index e51db4ce3..d71b3635b 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -67,12 +67,7 @@ Node BuiltinProofRuleChecker::applySubstitutionRewrite(
     MethodId idr)
 {
   Node nks = applySubstitution(n, exp, ids, ida);
-  return applyRewrite(nks, idr);
-}
-
-Node BuiltinProofRuleChecker::applyRewrite(TNode n, MethodId idr)
-{
-  return d_env.getRewriter()->rewriteViaMethod(n, idr);
+  return d_env.getRewriter()->rewriteViaMethod(nks, idr);
 }
 
 bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp,
@@ -254,7 +249,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     {
       return Node::null();
     }
-    Node res = applyRewrite(args[0], idr);
+    Node res = d_env.getRewriter()->rewriteViaMethod(args[0], idr);
     if (res.isNull())
     {
       return Node::null();
@@ -265,7 +260,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
   {
     Assert(children.empty());
     Assert(args.size() == 1);
-    Node res = applyRewrite(args[0], MethodId::RW_EVALUATE);
+    Node res = d_env.getRewriter()->rewriteViaMethod(args[0], MethodId::RW_EVALUATE);
     if (res.isNull())
     {
       return Node::null();
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index bb746e467..8b3988f27 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -39,16 +39,6 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
   BuiltinProofRuleChecker(Env& env);
   /** Destructor. */
   ~BuiltinProofRuleChecker() {}
-  /**
-   * Apply rewrite on n (in skolem form). This encapsulates the exact behavior
-   * of a REWRITE step in a proof.
-   *
-   * @param n The node to rewrite,
-   * @param idr The method identifier of the rewriter, by default RW_REWRITE
-   * specifying a call to Rewriter::rewrite.
-   * @return The rewritten form of n.
-   */
-  Node applyRewrite(TNode n, MethodId idr = MethodId::RW_REWRITE);
   /**
    * Get substitution for literal exp. Updates vars/subs to the substitution
    * specified by exp for the substitution method ids.
-- 
2.30.2