Simplify term formula removal interface (#5695)

This no longer needs some methods that were previously used specifically for ITE preprocessing and check-model.

1 files changed, 0 insertions, 14 deletions

diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index fc10e19c9..4a5d4648e 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -92,18 +92,6 @@ class RemoveTermFormulas {
                         std::vector<Node>& newSkolems);
 
   /**
-   * Substitute under node using pre-existing cache.  Do not remove
-   * any ITEs not seen during previous runs.
-   */
-  Node replace(TNode node) const;
-
-  /** Returns true if e contains a term ite. */
-  bool containsTermITE(TNode e) const;
-
-  /** Garbage collects non-context dependent data-structures. */
-  void garbageCollect();
-
-  /**
    * Get proof generator that is responsible for all proofs for removing term
    * formulas from nodes. When proofs are enabled, the returned trust node
    * of the run method use this proof generator (the trust nodes in newAsserts
@@ -199,8 +187,6 @@ class RemoveTermFormulas {
   Node runCurrent(std::pair<Node, uint32_t>& curr,
                   std::vector<theory::TrustNode>& newAsserts,
                   std::vector<Node>& newSkolems);
-  /** Replace internal */
-  Node replaceInternal(TCtxStack& ctx) const;
 
   /** Whether proofs are enabled */
   bool isProofEnabled() const;