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 de8750d89a2206a2c21097a57e7a090d36e23775..d02069fd8fd50264c93f3b4341a898a27e6c5dca 100644 (file)
--- 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 09f0123bfde1c3a00e900b567d990f26eb2d497e..9ee13d952054693d36deadc034a2f15a8987fb29 100644 (file)
--- 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 6bec3dc8fda1b047ffb4b1901479204ea51125f3..db98b47fa8befbcce44ddedc217b908fd58c6868 100644 (file)
--- 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 e610adcf7e1c3df859a83443f90ff68dbbb82e37..81769254fbd4af332788fc8d5843ee4f0b926094 100644 (file)
--- 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.
    */