Eliminate recursion from the internals of term formula removal (#5701)

This makes all recursion (applying term formula removal on lemmas introduced by term formula removal) optionally happen at the top level call.

This is in preparation for making term formula removal lazier, in which case we will only apply one step of term formula removal at a time.

One QF_UFNIA regression times out due to changing the search, an option is changed for this benchmark.

3 files changed, 103 insertions, 53 deletions

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 4b519f06a..ae3039ffa 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -50,14 +50,77 @@ RemoveTermFormulas::~RemoveTermFormulas() {}
 theory::TrustNode RemoveTermFormulas::run(
     Node assertion,
     std::vector<theory::TrustNode>& newAsserts,
-    std::vector<Node>& newSkolems)
+    std::vector<Node>& newSkolems,
+    bool fixedPoint)
 {
   Node itesRemoved = runInternal(assertion, newAsserts, newSkolems);
+  Assert(newAsserts.size() == newSkolems.size());
+  if (itesRemoved == assertion)
+  {
+    return theory::TrustNode::null();
+  }
+  // if running to fixed point, we run each new assertion through the
+  // run lemma method
+  if (fixedPoint)
+  {
+    size_t i = 0;
+    std::unordered_set<Node, NodeHashFunction> processed;
+    while (i < newAsserts.size())
+    {
+      theory::TrustNode trn = newAsserts[i];
+      AlwaysAssert(processed.find(trn.getProven()) == processed.end());
+      processed.insert(trn.getProven());
+      // do not run to fixed point on subcall, since we are processing all
+      // lemmas in this loop
+      newAsserts[i] = runLemma(trn, newAsserts, newSkolems, false);
+      i++;
+    }
+  }
   // The rewriting of assertion can be justified by the term conversion proof
   // generator d_tpg.
   return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get());
 }
 
+theory::TrustNode RemoveTermFormulas::runLemma(
+    theory::TrustNode lem,
+    std::vector<theory::TrustNode>& newAsserts,
+    std::vector<Node>& newSkolems,
+    bool fixedPoint)
+{
+  theory::TrustNode trn =
+      run(lem.getProven(), newAsserts, newSkolems, fixedPoint);
+  if (trn.isNull())
+  {
+    // no change
+    return lem;
+  }
+  Assert(trn.getKind() == theory::TrustNodeKind::REWRITE);
+  Node newAssertion = trn.getNode();
+  if (!isProofEnabled())
+  {
+    // proofs not enabled, just take result
+    return theory::TrustNode::mkTrustLemma(newAssertion, nullptr);
+  }
+  Trace("rtf-proof-debug")
+      << "RemoveTermFormulas::run: setup proof for processed new lemma"
+      << std::endl;
+  Node assertionPre = lem.getProven();
+  Node naEq = trn.getProven();
+  // this method is applying this method to TrustNode whose generator is
+  // already d_lp (from the run method above), in which case this link is
+  // not necessary.
+  if (trn.getGenerator() != d_lp.get())
+  {
+    d_lp->addLazyStep(naEq, trn.getGenerator());
+  }
+  // ---------------- from input  ------------------------------- from trn
+  // assertionPre                 assertionPre = newAssertion
+  // ------------------------------------------------------- EQ_RESOLVE
+  // newAssertion
+  d_lp->addStep(newAssertion, PfRule::EQ_RESOLVE, {assertionPre, naEq}, {});
+  return theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
+}
+
 Node RemoveTermFormulas::runInternal(Node assertion,
                                      std::vector<theory::TrustNode>& output,
                                      std::vector<Node>& newSkolems)
@@ -91,10 +154,18 @@ Node RemoveTermFormulas::runInternal(Node assertion,
     if (!processedChildren.back())
     {
       // check if we should replace the current node
-      Node currt = runCurrent(curr, output, newSkolems);
-      // if null, we need to recurse
+      theory::TrustNode newLem;
+      Node currt = runCurrent(curr, newLem);
+      // if we replaced by a skolem, we do not recurse
       if (!currt.isNull())
       {
+        // if this is the first time we've seen this term, we have a new lemma
+        // which we add to our vectors
+        if (!newLem.isNull())
+        {
+          output.push_back(newLem);
+          newSkolems.push_back(currt);
+        }
         Trace("rtf-debug") << "...replace by skolem" << std::endl;
         d_tfCache.insert(curr, currt);
         ctx.pop();
@@ -165,14 +236,9 @@ Node RemoveTermFormulas::runInternal(Node assertion,
 }
 
 Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
-                                    std::vector<theory::TrustNode>& output,
-                                    std::vector<Node>& newSkolems)
+                                    theory::TrustNode& newLem)
 {
   TNode node = curr.first;
-  if (node.getKind() == kind::INST_PATTERN_LIST)
-  {
-    return Node(node);
-  }
   uint32_t cval = curr.second;
   bool inQuant, inTerm;
   RtfTermContext::getFlags(curr.second, inQuant, inTerm);
@@ -413,39 +479,11 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
       Trace("rtf-debug") << "*** term formula removal introduced " << skolem
                          << " for " << node << std::endl;
 
-      // Remove ITEs from the new assertion, rewrite it and push it to the
-      // output
-      Node newAssertionPre = newAssertion;
-      newAssertion = runInternal(newAssertion, output, newSkolems);
-
-      if (isProofEnabled())
-      {
-        if (newAssertionPre != newAssertion)
-        {
-          Trace("rtf-proof-debug")
-              << "RemoveTermFormulas::run: setup proof for processed new lemma"
-              << std::endl;
-          // for new assertions that rewrite recursively
-          Node naEq = newAssertionPre.eqNode(newAssertion);
-          d_lp->addLazyStep(naEq, d_tpg.get());
-          // ---------------- from lp  ------------------------------- from tpg
-          // newAssertionPre            newAssertionPre = newAssertion
-          // ------------------------------------------------------- EQ_RESOLVE
-          // newAssertion
-          d_lp->addStep(
-              newAssertion, PfRule::EQ_RESOLVE, {newAssertionPre, naEq}, {});
-        }
-      }
-
-      theory::TrustNode trna =
-          theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
+      newLem = theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get());
 
       Trace("rtf-proof-debug") << "Checking closed..." << std::endl;
-      trna.debugCheckClosed("rtf-proof-debug",
-                            "RemoveTermFormulas::run:new_assert");
-
-      output.push_back(trna);
-      newSkolems.push_back(skolem);
+      newLem.debugCheckClosed("rtf-proof-debug",
+                              "RemoveTermFormulas::run:new_assert");
     }
 
     // The representation is now the skolem
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 4a5d4648e..e5453254c 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -83,13 +83,26 @@ class RemoveTermFormulas {
    * @param newAsserts The new assertions corresponding to axioms for newly
    * introduced skolems.
    * @param newSkolems The skolems corresponding to each of the newAsserts.
+   * @param fixedPoint Whether to run term formula removal on the lemmas in
+   * newAsserts. This adds new assertions to this vector until a fixed
+   * point is reached. When this option is true, all lemmas in newAsserts
+   * have all term formulas removed.
    * @return a trust node of kind TrustNodeKind::REWRITE whose
    * right hand side is assertion after removing term formulas, and the proof
    * generator (if provided) that can prove the equivalence.
    */
   theory::TrustNode run(Node assertion,
                         std::vector<theory::TrustNode>& newAsserts,
-                        std::vector<Node>& newSkolems);
+                        std::vector<Node>& newSkolems,
+                        bool fixedPoint = false);
+  /**
+   * Same as above, but transforms a lemma, returning a LEMMA trust node that
+   * proves the same formula as lem with term formulas removed.
+   */
+  theory::TrustNode runLemma(theory::TrustNode lem,
+                             std::vector<theory::TrustNode>& newAsserts,
+                             std::vector<Node>& newSkolems,
+                             bool fixedPoint = false);
 
   /**
    * Get proof generator that is responsible for all proofs for removing term
@@ -179,14 +192,14 @@ class RemoveTermFormulas {
   /**
    * 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, adds k to
-   * newSkolems and adds the axiom defining that skolem to newAsserts, where
-   * runInternal is called on that axiom. Otherwise, this method returns the
-   * null node.
+   * 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.
+   *
+   * 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,
-                  std::vector<theory::TrustNode>& newAsserts,
-                  std::vector<Node>& newSkolems);
+  Node runCurrent(std::pair<Node, uint32_t>& curr, theory::TrustNode& newLem);
 
   /** Whether proofs are enabled */
   bool isProofEnabled() const;
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 179ecc130..7c917dff5 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -100,14 +100,13 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
     ppNode = tpp.getNode();
   }
 
-  // Remove the ITEs
-  TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems);
-  Node rtfNode = ttfr.getNode();
+  // Remove the ITEs, fixed point
+  TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, true);
+  Node rtfNode = ttfr.isNull() ? ppNode : ttfr.getNode();
 
   if (Debug.isOn("lemma-ites"))
   {
-    Debug("lemma-ites") << "removed ITEs from lemma: " << ttfr.getNode()
-                        << endl;
+    Debug("lemma-ites") << "removed ITEs from lemma: " << rtfNode << endl;
     Debug("lemma-ites") << " + now have the following " << newLemmas.size()
                         << " lemma(s):" << endl;
     for (size_t i = 0, lsize = newLemmas.size(); i <= lsize; ++i)