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.

3 files changed, 23 insertions, 11 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)
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index ff4a0e6ca..707d1314c 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -23,12 +23,10 @@ namespace preprocessing {
 
 PreprocessingPassContext::PreprocessingPassContext(
     SmtEngine* smt,
-    RemoveTermFormulas* iteRemover,
     theory::booleans::CircuitPropagator* circuitPropagator,
     ProofNodeManager* pnm)
     : d_smt(smt),
       d_resourceManager(smt->getResourceManager()),
-      d_iteRemover(iteRemover),
       d_topLevelSubstitutions(smt->getUserContext(), pnm),
       d_circuitPropagator(circuitPropagator),
       d_pnm(pnm),
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 824197bc5..c22a69255 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -40,7 +40,6 @@ class PreprocessingPassContext
  public:
   PreprocessingPassContext(
       SmtEngine* smt,
-      RemoveTermFormulas* iteRemover,
       theory::booleans::CircuitPropagator* circuitPropagator,
       ProofNodeManager* pnm);
 
@@ -49,7 +48,6 @@ class PreprocessingPassContext
   prop::PropEngine* getPropEngine() { return d_smt->getPropEngine(); }
   context::Context* getUserContext() { return d_smt->getUserContext(); }
   context::Context* getDecisionContext() { return d_smt->getContext(); }
-  RemoveTermFormulas* getIteRemover() { return d_iteRemover; }
 
   theory::booleans::CircuitPropagator* getCircuitPropagator()
   {
@@ -95,9 +93,6 @@ class PreprocessingPassContext
   /** Pointer to the ResourceManager for this context. */
   ResourceManager* d_resourceManager;
 
-  /** Instance of the ITE remover */
-  RemoveTermFormulas* d_iteRemover;
-
   /* The top level substitutions */
   theory::TrustSubstitutionMap d_topLevelSubstitutions;