Move ownership of term formula removal to theory preprocessor (#5670)

This is work towards refactoring ITE removal (more generally, term formula removal) so that it happens at a configurable time, preferably post-CNF conversion.

This moves the TermFormulaRemover to the TheoryPreprocessor and changes several interfaces as a consequence of this move.

The next step will move the TheoryPreprocessor inside prop::TheoryProxy.

There are no behavior changes to solving in this PR. One aspect of CheckModels is simplified.

1 files changed, 23 insertions, 4 deletions

diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index a75b6f5ad..3531497e8 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -18,6 +18,7 @@
 #include "preprocessing/passes/ite_removal.h"
 
 #include "theory/rewriter.h"
+#include "theory/theory_preprocessor.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -25,6 +26,7 @@ namespace passes {
 
 using namespace CVC4::theory;
 
+// TODO (project #42): note this preprocessing pass is deprecated
 IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "ite-removal")
 {
@@ -36,19 +38,36 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
 
   IteSkolemMap& imap = assertions->getIteSkolemMap();
   // Remove all of the ITE occurrences and normalize
+  theory::TheoryPreprocessor* tpp =
+      d_preprocContext->getTheoryEngine()->getTheoryPreprocess();
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
+    Node assertion = (*assertions)[i];
     std::vector<theory::TrustNode> newAsserts;
     std::vector<Node> newSkolems;
-    TrustNode trn = d_preprocContext->getIteRemover()->run(
-        (*assertions)[i], newAsserts, newSkolems, true);
-    // process
-    assertions->replaceTrusted(i, trn);
+    // TODO (project #42): this will call the prop engine
+    TrustNode trn = tpp->preprocess(assertion, newAsserts, newSkolems, false);
+    if (!trn.isNull())
+    {
+      // process
+      assertions->replaceTrusted(i, trn);
+      // rewritten assertion has a dependence on the node (old pf architecture)
+      if (options::unsatCores())
+      {
+        ProofManager::currentPM()->addDependence(trn.getNode(), assertion);
+      }
+    }
     Assert(newSkolems.size() == newAsserts.size());
     for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
     {
       imap[newSkolems[j]] = assertions->size();
       assertions->pushBackTrusted(newAsserts[j]);
+      // new assertions have a dependence on the node (old pf architecture)
+      if (options::unsatCores())
+      {
+        ProofManager::currentPM()->addDependence(newAsserts[j].getProven(),
+                                                 assertion);
+      }
     }
   }
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)