From 6094c2e2e43d2e6716f35689654d4915a6a1f4fc Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 12 Oct 2021 11:24:40 -0500
Subject: [PATCH] Provide a non-traversal interface to term formula removal
 (#7328)

Towards making theory preprocessing a single pass.
---
 src/smt/term_formula_removal.cpp | 31 +++++++++++++++++++++----------
 src/smt/term_formula_removal.h   | 24 ++++++++++++++++++------
 2 files changed, 39 insertions(+), 16 deletions(-)

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 470c035a9..07100576d 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -153,7 +153,12 @@ Node RemoveTermFormulas::runInternal(TNode assertion,
     {
       // check if we should replace the current node
       TrustNode newLem;
-      Node currt = runCurrent(curr, newLem);
+      bool inQuant, inTerm;
+      RtfTermContext::getFlags(nodeVal, inQuant, inTerm);
+      Debug("ite") << "removeITEs(" << node << ")"
+                   << " " << inQuant << " " << inTerm << std::endl;
+      Assert(!inQuant);
+      Node currt = runCurrentInternal(node, inTerm, newLem);
       // if we replaced by a skolem, we do not recurse
       if (!currt.isNull())
       {
@@ -237,17 +242,22 @@ Node RemoveTermFormulas::runInternal(TNode assertion,
   return (*itc).second;
 }
 
-Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
-                                    TrustNode& newLem)
+TrustNode RemoveTermFormulas::runCurrent(TNode node,
+                                         bool inTerm,
+                                         TrustNode& newLem)
 {
-  TNode node = curr.first;
-  uint32_t cval = curr.second;
-  bool inQuant, inTerm;
-  RtfTermContext::getFlags(curr.second, inQuant, inTerm);
-  Debug("ite") << "removeITEs(" << node << ")"
-               << " " << inQuant << " " << inTerm << std::endl;
-  Assert(!inQuant);
+  Node k = runCurrentInternal(node, inTerm, newLem);
+  if (!k.isNull())
+  {
+    return TrustNode::mkTrustRewrite(node, k, d_tpg.get());
+  }
+  return TrustNode::null();
+}
 
+Node RemoveTermFormulas::runCurrentInternal(TNode node,
+                                            bool inTerm,
+                                            TrustNode& newLem)
+{
   NodeManager *nodeManager = NodeManager::currentNM();
 
   TypeNode nodeType = node.getType();
@@ -447,6 +457,7 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
     // since a formula-term may rewrite to the same skolem in multiple contexts.
     if (isProofEnabled())
     {
+      uint32_t cval = RtfTermContext::getValue(false, inTerm);
       // justify the introduction of the skolem
       // ------------------- MACRO_SR_PRED_INTRO
       // t = witness x. x=t
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 80cbc3b03..1942b0fdc 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -117,6 +117,18 @@ class RemoveTermFormulas : protected EnvObj
    */
   static Node getAxiomFor(Node n);
 
+  /**
+   * This is called on a term node that occurs in a term context (see
+   * RtfTermContext) if inTerm is true. If node should be replaced by a skolem,
+   * this method returns this skolem k. If this was the first time that node
+   * was encountered, we set newLem to the lemma for the skolem that
+   * axiomatizes k.
+   *
+   * Otherwise, if t should not be replaced in the term context, this method
+   * returns the null node.
+   */
+  TrustNode runCurrent(TNode node, bool inTerm, TrustNode& newLem);
+
  private:
   typedef context::CDInsertHashMap<
       std::pair<Node, uint32_t>,
@@ -184,16 +196,16 @@ class RemoveTermFormulas : protected EnvObj
   Node runInternal(TNode assertion,
                    std::vector<theory::SkolemLemma>& newAsserts);
   /**
-   * This is called on curr of the form (t, val) where t is a term and val is
-   * a term context identifier computed by RtfTermContext. If curr should be
-   * replaced by a skolem, this method returns this skolem k. If this was the
-   * first time that t was encountered, we set newLem to the lemma for the
-   * skolem that axiomatizes k.
+   * This is called on a term node that occurs in a term context (see
+   * RtfTermContext) if inTerm is true. If node should be replaced by a skolem,
+   * this method returns this skolem k. If this was the first time that node
+   * was encountered, we set newLem to the lemma for the skolem that
+   * axiomatizes k.
    *
    * Otherwise, if t should not be replaced in the term context, this method
    * returns the null node.
    */
-  Node runCurrent(std::pair<Node, uint32_t>& curr, TrustNode& newLem);
+  Node runCurrentInternal(TNode node, bool inTerm, TrustNode& newLem);
   /** Is proof enabled? True if proofs are enabled in any mode. */
   bool isProofEnabled() const;
 }; /* class RemoveTTE */
-- 
2.30.2