(proof-new) Proof production for term formula removal (#4687)

This adds proof support in the term formula removal pass.

It also refactors this class heavily so that its interface is more intuitive and does not depend on AssertionPipeline.

1 files changed, 16 insertions, 2 deletions

diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index f021fff28..2cc244a34 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -34,9 +34,23 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
 {
   d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
 
+  IteSkolemMap& imap = assertions->getIteSkolemMap();
   // Remove all of the ITE occurrences and normalize
-  d_preprocContext->getIteRemover()->run(
-      assertions->ref(), assertions->getIteSkolemMap(), true);
+  for (unsigned i = 0, size = assertions->size(); i < size; ++i)
+  {
+    std::vector<theory::TrustNode> newAsserts;
+    std::vector<Node> newSkolems;
+    TrustNode trn = d_preprocContext->getIteRemover()->run(
+        (*assertions)[i], newAsserts, newSkolems, true);
+    // process
+    assertions->replace(i, trn.getNode());
+    Assert(newSkolems.size() == newAsserts.size());
+    for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
+    {
+      imap[newSkolems[j]] = assertions->size();
+      assertions->ref().push_back(newAsserts[j].getNode());
+    }
+  }
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
     assertions->replace(i, Rewriter::rewrite((*assertions)[i]));