From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 1 Sep 2021 14:24:02 +0000 (-0700)
Subject: rewriter: Make registerTheoryRewriter non-static. (#7101)
X-Git-Tag: cvc5-1.0.0~1305
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=24c4e9d5612fd7549a8ff7acaf76ce95acaca0d9;p=cvc5.git

rewriter: Make registerTheoryRewriter non-static. (#7101)

More work towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.
---

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index de8750d89..d02069fd8 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -148,7 +148,7 @@ Node Rewriter::rewriteEqualityExt(TNode node)
 void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
                                       TheoryRewriter* trew)
 {
-  getInstance()->d_theoryRewriters[tid] = trew;
+  d_theoryRewriters[tid] = trew;
 }
 
 void Rewriter::registerPreRewrite(
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 09f0123bf..9ee13d952 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -103,8 +103,7 @@ class Rewriter {
    * @param tid The theory that the theory rewriter should be associated with.
    * @param trew The theory rewriter to register.
    */
-  static void registerTheoryRewriter(theory::TheoryId tid,
-                                     TheoryRewriter* trew);
+  void registerTheoryRewriter(theory::TheoryId tid, TheoryRewriter* trew);
 
   /**
    * Register a prerewrite for a given kind.
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 6bec3dc8f..db98b47fa 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1965,4 +1965,6 @@ void TheoryEngine::initializeProofChecker(ProofChecker* pc)
   }
 }
 
+theory::Rewriter* TheoryEngine::getRewriter() { return d_env.getRewriter(); }
+
 }  // namespace cvc5
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index e610adcf7..81769254f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -78,11 +78,13 @@ struct NodeTheoryPairHashFunction {
 
 /* Forward declarations */
 namespace theory {
-class TheoryModel;
+
 class CombinationEngine;
-class SharedSolver;
 class DecisionManager;
 class RelevanceManager;
+class Rewriter;
+class SharedSolver;
+class TheoryModel;
 
 }  // namespace theory
 
@@ -316,7 +318,7 @@ class TheoryEngine {
     d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId);
     d_theoryTable[theoryId] =
         new TheoryClass(d_env, *d_theoryOut[theoryId], theory::Valuation(this));
-    theory::Rewriter::registerTheoryRewriter(
+    getRewriter()->registerTheoryRewriter(
         theoryId, d_theoryTable[theoryId]->getTheoryRewriter());
   }
 
@@ -372,6 +374,11 @@ class TheoryEngine {
   }
 
  private:
+  /**
+   * Get a pointer to the rewriter owned by the associated Env.
+   */
+  theory::Rewriter* getRewriter();
+
   /**
    * Queue of nodes for pre-registration.
    */