Add new interfaces to term formula removal and theory preprocess (#5717)

This is in preparation for lazy lemmas for term formula removal.

1 files changed, 29 insertions, 4 deletions

diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index c56554b53..9a425fc1c 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -84,7 +84,8 @@ TheoryPreprocessor::~TheoryPreprocessor() {}
 TrustNode TheoryPreprocessor::preprocess(TNode node,
                                          std::vector<TrustNode>& newLemmas,
                                          std::vector<Node>& newSkolems,
-                                         bool doTheoryPreprocess)
+                                         bool doTheoryPreprocess,
+                                         bool fixedPoint)
 {
   // In this method, all rewriting steps of node are stored in d_tpg.
 
@@ -101,7 +102,7 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   }
 
   // Remove the ITEs, fixed point
-  TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, true);
+  TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, fixedPoint);
   Node rtfNode = ttfr.isNull() ? ppNode : ttfr.getNode();
 
   if (Debug.isOn("lemma-ites"))
@@ -222,15 +223,24 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   return tret;
 }
 
+TrustNode TheoryPreprocessor::preprocess(TNode node, bool doTheoryPreprocess)
+{
+  // ignore lemmas, no fixed point
+  std::vector<TrustNode> newLemmas;
+  std::vector<Node> newSkolems;
+  return preprocess(node, newLemmas, newSkolems, doTheoryPreprocess, false);
+}
+
 TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
                                               std::vector<TrustNode>& newLemmas,
                                               std::vector<Node>& newSkolems,
-                                              bool doTheoryPreprocess)
+                                              bool doTheoryPreprocess,
+                                              bool fixedPoint)
 {
   // what was originally proven
   Node lemma = node.getProven();
   TrustNode tplemma =
-      preprocess(lemma, newLemmas, newSkolems, doTheoryPreprocess);
+      preprocess(lemma, newLemmas, newSkolems, doTheoryPreprocess, fixedPoint);
   if (tplemma.isNull())
   {
     // no change needed
@@ -267,6 +277,21 @@ TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
   return TrustNode::mkTrustLemma(lemmap, d_lp.get());
 }
 
+TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
+                                              bool doTheoryPreprocess)
+{
+  // ignore lemmas, no fixed point
+  std::vector<TrustNode> newLemmas;
+  std::vector<Node> newSkolems;
+  return preprocessLemma(
+      node, newLemmas, newSkolems, doTheoryPreprocess, false);
+}
+
+RemoveTermFormulas& TheoryPreprocessor::getRemoveTermFormulas()
+{
+  return d_tfr;
+}
+
 struct preprocess_stack_element
 {
   TNode node;