From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 17 Dec 2020 15:19:20 +0000 (-0600)
Subject: Simplify term formula removal interface (#5695)
X-Git-Tag: cvc5-1.0.0~2429
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bdcb62974f553acd47fdb04f8d95725489328139;p=cvc5.git

Simplify term formula removal interface (#5695)

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

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 60b850a31..4b519f06a 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -467,54 +467,6 @@ Node RemoveTermFormulas::getSkolemForNode(Node node) const
   return Node::null();
 }
 
-Node RemoveTermFormulas::replace(TNode node) const
-{
-  TCtxStack ctx(&d_rtfc);
-  ctx.pushInitial(node);
-  return replaceInternal(ctx);
-}
-
-Node RemoveTermFormulas::replaceInternal(TCtxStack& ctx) const
-{
-  // get the current node, tagged with a term context identifier
-  Assert(!ctx.empty());
-  std::pair<Node, uint32_t> curr = ctx.getCurrent();
-  ctx.pop();
-  TNode node = curr.first;
-
-  if( node.getKind()==kind::INST_PATTERN_LIST ){
-    return Node(node);
-  }
-
-  // Check the cache
-  TermFormulaCache::const_iterator itc = d_tfCache.find(curr);
-  if (itc != d_tfCache.end())
-  {
-    return (*itc).second;
-  }
-
-  vector<Node> newChildren;
-  bool somethingChanged = false;
-  if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    newChildren.push_back(node.getOperator());
-  }
-  // Replace in children
-  uint32_t cval = curr.second;
-  for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++)
-  {
-    ctx.pushChild(node, cval, i);
-    Node newChild = replaceInternal(ctx);
-    somethingChanged |= (newChild != node[i]);
-    newChildren.push_back(newChild);
-  }
-
-  // If changes, we rewrite
-  if(somethingChanged) {
-    return NodeManager::currentNM()->mkNode(node.getKind(), newChildren);
-  }
-  return node;
-}
-
 Node RemoveTermFormulas::getAxiomFor(Node n)
 {
   NodeManager* nm = NodeManager::currentNM();
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
@@ -91,18 +91,6 @@ class RemoveTermFormulas {
                         std::vector<theory::TrustNode>& newAsserts,
                         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
@@ -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;