Move ownership of theory preprocessor to TheoryProxy (#5690)

With this PR, TheoryEngine is independent of theory preprocessing. All theory preprocessing is handled at the level of PropEngine.

No significant behavior changes in this PR.

The next step will make theory preprocessing not mandatory in preprocessing, and optionally done instead at the time when literals are asserted to TheoryEngine.

1 files changed, 0 insertions, 11 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index bdc79931f..bade5a206 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -290,9 +290,6 @@ class TheoryEngine {
   /** sort inference module */
   SortInference d_sortInfer;
 
-  /** The theory preprocessor */
-  theory::TheoryPreprocessor d_tpp;
-
   /** Time spent in theory combination */
   TimerStat d_combineTheoriesTime;
 
@@ -442,14 +439,6 @@ class TheoryEngine {
   bool isProofEnabled() const;
 
  public:
-  /**
-   * Runs theory specific preprocessing on the non-Boolean parts of
-   * the formula.  This is only called on input assertions, after ITEs
-   * have been removed.
-   */
-  theory::TrustNode preprocess(TNode node);
-  /** Get the theory preprocessor TODO (project #42) remove this */
-  theory::TheoryPreprocessor* getTheoryPreprocess() { return &d_tpp; }
 
   /** Notify (preprocessed) assertions. */
   void notifyPreprocessedAssertions(const std::vector<Node>& assertions);