Unify top-level substitutions and model substitutions (#6499)

This unifies top-level substitutions and theory model substitutions. Env is now passed to the TheoryModel, which has access to top-level substitutions.

The former was used for simplfying assertions in the preprocessor, the latter was used for evaluating terms in the model.

There is no reason to have these two things be separate.

1 files changed, 2 insertions, 9 deletions

diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index a4ca166d8..a14fafb47 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -78,15 +78,8 @@ class PreprocessingPassContext
   void recordSymbolsInAssertions(const std::vector<Node>& assertions);
 
   /**
-   * Add substitution to theory model. This method should only be called if
-   * we have already added the substitution to the top-level substitutions
-   * class. Otherwise, addSubstitution should be called instead.
-   * @param lhs The node replaced by node 'rhs'
-   * @param rhs The node to substitute node 'lhs'
-   */
-  void addModelSubstitution(const Node& lhs, const Node& rhs);
-  /**
-   * Add substitution to the top-level substitutions and to the theory model.
+   * Add substitution to the top-level substitutions, which also as a
+   * consequence is used by the theory model.
    * @param lhs The node replaced by node 'rhs'
    * @param rhs The node to substitute node 'lhs'
    * @param pg The proof generator that can provide a proof of lhs == rhs.