Move ownership of theory preprocessor to TheoryProxy (#5690)

With this PR, TheoryEngine is independent of theory preprocessing. All theory preprocessing is handled at the level of PropEngine.

No significant behavior changes in this PR.

The next step will make theory preprocessing not mandatory in preprocessing, and optionally done instead at the time when literals are asserted to TheoryEngine.

2 files changed, 37 insertions, 12 deletions

diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 3531497e8..d2f053379 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -38,15 +38,13 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
 
   IteSkolemMap& imap = assertions->getIteSkolemMap();
   // Remove all of the ITE occurrences and normalize
-  theory::TheoryPreprocessor* tpp =
-      d_preprocContext->getTheoryEngine()->getTheoryPreprocess();
+  prop::PropEngine* pe = d_preprocContext->getPropEngine();
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
     Node assertion = (*assertions)[i];
     std::vector<theory::TrustNode> newAsserts;
     std::vector<Node> newSkolems;
-    // TODO (project #42): this will call the prop engine
-    TrustNode trn = tpp->preprocess(assertion, newAsserts, newSkolems, false);
+    TrustNode trn = pe->preprocess(assertion, newAsserts, newSkolems, false);
     if (!trn.isNull())
     {
       // process
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index e888e7a2b..6c751f864 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -29,17 +29,44 @@ TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "theory-preprocess"){};
 
 PreprocessingPassResult TheoryPreprocess::applyInternal(
-    AssertionPipeline* assertionsToPreprocess)
+    AssertionPipeline* assertions)
 {
-  TheoryEngine* te = d_preprocContext->getTheoryEngine();
-  for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+
+  IteSkolemMap& imap = assertions->getIteSkolemMap();
+  PropEngine* propEngine = d_preprocContext->getPropEngine();
+  // Remove all of the ITE occurrences and normalize
+  for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
-    TNode a = (*assertionsToPreprocess)[i];
-    Assert(Rewriter::rewrite(a) == a);
-    assertionsToPreprocess->replaceTrusted(i, te->preprocess(a));
-    a = (*assertionsToPreprocess)[i];
-    Assert(Rewriter::rewrite(a) == a);
+    Node assertion = (*assertions)[i];
+    std::vector<theory::TrustNode> newAsserts;
+    std::vector<Node> newSkolems;
+    TrustNode trn =
+        propEngine->preprocess(assertion, newAsserts, newSkolems, true);
+    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);
+      }
+    }
   }
+
   return PreprocessingPassResult::NO_CONFLICT;
 }