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, 17 insertions, 44 deletions

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index f3e0d0bd6..60b850a31 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -26,13 +26,23 @@ using namespace std;
 
 namespace CVC4 {
 
-RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u)
-    : d_tfCache(u),
-      d_skolem_cache(u),
-      d_pnm(nullptr),
-      d_tpg(nullptr),
-      d_lp(nullptr)
+RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u,
+                                       ProofNodeManager* pnm)
+    : d_tfCache(u), d_skolem_cache(u), d_pnm(pnm), d_tpg(nullptr), d_lp(nullptr)
 {
+  // enable proofs if necessary
+  if (d_pnm != nullptr)
+  {
+    d_tpg.reset(
+        new TConvProofGenerator(d_pnm,
+                                nullptr,
+                                TConvPolicy::FIXPOINT,
+                                TConvCachePolicy::NEVER,
+                                "RemoveTermFormulas::TConvProofGenerator",
+                                &d_rtfc));
+    d_lp.reset(new LazyCDProof(
+        d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
+  }
 }
 
 RemoveTermFormulas::~RemoveTermFormulas() {}
@@ -40,29 +50,9 @@ RemoveTermFormulas::~RemoveTermFormulas() {}
 theory::TrustNode RemoveTermFormulas::run(
     Node assertion,
     std::vector<theory::TrustNode>& newAsserts,
-    std::vector<Node>& newSkolems,
-    bool reportDeps)
+    std::vector<Node>& newSkolems)
 {
   Node itesRemoved = runInternal(assertion, newAsserts, newSkolems);
-  // In some calling contexts, not necessary to report dependence information.
-  if (reportDeps && options::unsatCores())
-  {
-    // new assertions have a dependence on the node
-    if (options::unsatCores())
-    {
-      ProofManager::currentPM()->addDependence(itesRemoved, assertion);
-    }
-    unsigned n = 0;
-    while (n < newAsserts.size())
-    {
-      if (options::unsatCores())
-      {
-        ProofManager::currentPM()->addDependence(newAsserts[n].getProven(),
-                                                 assertion);
-      }
-      ++n;
-    }
-  }
   // The rewriting of assertion can be justified by the term conversion proof
   // generator d_tpg.
   return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get());
@@ -536,23 +526,6 @@ Node RemoveTermFormulas::getAxiomFor(Node n)
   return Node::null();
 }
 
-void RemoveTermFormulas::setProofNodeManager(ProofNodeManager* pnm)
-{
-  if (d_tpg == nullptr)
-  {
-    d_pnm = pnm;
-    d_tpg.reset(
-        new TConvProofGenerator(d_pnm,
-                                nullptr,
-                                TConvPolicy::FIXPOINT,
-                                TConvCachePolicy::NEVER,
-                                "RemoveTermFormulas::TConvProofGenerator",
-                                &d_rtfc));
-    d_lp.reset(new LazyCDProof(
-        d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
-  }
-}
-
 ProofGenerator* RemoveTermFormulas::getTConvProofGenerator()
 {
   return d_tpg.get();