From fb4a3021359059c82f9a01ad4a9d78d1c126a64c Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 1 Sep 2021 19:57:21 -0700
Subject: [PATCH] rewriter: Make rewriteEqualityExt non-static. (#7110)

More work towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.
---
 src/theory/builtin/proof_checker.cpp      |  5 +++-
 src/theory/builtin/proof_checker.h        | 11 ++++++++-
 src/theory/builtin/theory_builtin.cpp     |  1 +
 src/theory/quantifiers/extended_rewrite.h | 29 ++++++++++++-----------
 src/theory/rewriter.cpp                   |  3 +--
 src/theory/rewriter.h                     |  2 +-
 6 files changed, 32 insertions(+), 19 deletions(-)

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 54d1779ec..bb0f9a413 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -16,6 +16,7 @@
 #include "theory/builtin/proof_checker.h"
 
 #include "expr/skolem_manager.h"
+#include "smt/env.h"
 #include "smt/term_formula_removal.h"
 #include "theory/evaluator.h"
 #include "theory/rewriter.h"
@@ -28,6 +29,8 @@ namespace cvc5 {
 namespace theory {
 namespace builtin {
 
+BuiltinProofRuleChecker::BuiltinProofRuleChecker(Env& env) : d_env(env) {}
+
 void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
 {
   pc->registerChecker(PfRule::ASSUME, this);
@@ -81,7 +84,7 @@ Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr)
   }
   if (idr == MethodId::RW_REWRITE_EQ_EXT)
   {
-    return Rewriter::rewriteEqualityExt(n);
+    return d_env.getRewriter()->rewriteEqualityExt(n);
   }
   if (idr == MethodId::RW_EVALUATE)
   {
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index 1e671a7b3..d7edd2c53 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -25,6 +25,9 @@
 #include "theory/quantifiers/extended_rewrite.h"
 
 namespace cvc5 {
+
+class Env;
+
 namespace theory {
 namespace builtin {
 
@@ -32,7 +35,9 @@ namespace builtin {
 class BuiltinProofRuleChecker : public ProofRuleChecker
 {
  public:
-  BuiltinProofRuleChecker() {}
+  /** Constructor. */
+  BuiltinProofRuleChecker(Env& env);
+  /** Destructor. */
   ~BuiltinProofRuleChecker() {}
   /**
    * Apply rewrite on n (in skolem form). This encapsulates the exact behavior
@@ -121,6 +126,10 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
 
   /** extended rewriter object */
   quantifiers::ExtendedRewriter d_ext_rewriter;
+
+ private:
+  /** Reference to the environment. */
+  Env& d_env;
 };
 
 }  // namespace builtin
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 092bcc9ab..ff718bff3 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -27,6 +27,7 @@ namespace builtin {
 
 TheoryBuiltin::TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_BUILTIN, env, out, valuation),
+      d_checker(env),
       d_state(env, valuation),
       d_im(*this, d_state, d_pnm, "theory::builtin::")
 {
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index 8996fc441..b1b08657d 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -54,20 +54,6 @@ class ExtendedRewriter
   Node extendedRewrite(Node n) const;
 
  private:
-  /**
-   * Whether this extended rewriter applies aggressive rewriting techniques,
-   * which are more expensive. Examples of aggressive rewriting include:
-   * - conditional rewriting,
-   * - condition merging,
-   * - sorting childing of commutative operators with more than 5 children.
-   *
-   * Aggressive rewriting is applied for SyGuS, whereas non-aggressive rewriting
-   * may be applied as a preprocessing step.
-   */
-  bool d_aggr;
-  /** true/false nodes */
-  Node d_true;
-  Node d_false;
   /** cache that the extended rewritten form of n is ret */
   void setCache(Node n, Node ret) const;
   /** get the cache for n */
@@ -256,6 +242,21 @@ class ExtendedRewriter
    */
   Node extendedRewriteStrings(Node ret) const;
   //--------------------------------------end theory-specific top-level calls
+
+  /**
+   * Whether this extended rewriter applies aggressive rewriting techniques,
+   * which are more expensive. Examples of aggressive rewriting include:
+   * - conditional rewriting,
+   * - condition merging,
+   * - sorting childing of commutative operators with more than 5 children.
+   *
+   * Aggressive rewriting is applied for SyGuS, whereas non-aggressive rewriting
+   * may be applied as a preprocessing step.
+   */
+  bool d_aggr;
+  /** true/false nodes */
+  Node d_true;
+  Node d_false;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index d02069fd8..bcd095265 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -141,8 +141,7 @@ Node Rewriter::rewriteEqualityExt(TNode node)
 {
   Assert(node.getKind() == kind::EQUAL);
   // note we don't force caching of this method currently
-  return getInstance()->d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt(
-      node);
+  return d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt(node);
 }
 
 void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 9ee13d952..23a9914bd 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -74,7 +74,7 @@ class Rewriter {
    * combination, which needs to guarantee that equalities between terms
    * can be communicated for all pairs of terms.
    */
-  static Node rewriteEqualityExt(TNode node);
+  Node rewriteEqualityExt(TNode node);
 
   /**
    * Rewrite with proof production, which is managed by the term conversion
-- 
2.30.2