(proof-new) Proof production for term formula removal (#4687)

This adds proof support in the term formula removal pass.

It also refactors this class heavily so that its interface is more intuitive and does not depend on AssertionPipeline.

1 files changed, 28 insertions, 17 deletions

diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index b12916b7d..328c65fcb 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -36,41 +36,52 @@ TheoryPreprocessor::~TheoryPreprocessor() {}
 
 void TheoryPreprocessor::clearCache() { d_ppCache.clear(); }
 
-void TheoryPreprocessor::preprocess(TNode node,
-                                    preprocessing::AssertionPipeline& lemmas,
-                                    bool doTheoryPreprocess)
+TrustNode TheoryPreprocessor::preprocess(TNode node,
+                                         std::vector<TrustNode>& newLemmas,
+                                         std::vector<Node>& newSkolems,
+                                         bool doTheoryPreprocess)
 {
   // Run theory preprocessing, maybe
   Node ppNode = doTheoryPreprocess ? theoryPreprocess(node) : Node(node);
 
   // Remove the ITEs
   Trace("te-tform-rm") << "Remove term formulas from " << ppNode << std::endl;
-  lemmas.push_back(ppNode);
-  lemmas.updateRealAssertionsEnd();
-  d_tfr.run(lemmas.ref(), lemmas.getIteSkolemMap());
-  Trace("te-tform-rm") << "..done " << lemmas[0] << std::endl;
+  TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, false);
+  Trace("te-tform-rm") << "..done " << ttfr.getNode() << std::endl;
+  Node retNode = ttfr.getNode();
 
   if (Debug.isOn("lemma-ites"))
   {
-    Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl;
-    Debug("lemma-ites") << " + now have the following " << lemmas.size()
+    Debug("lemma-ites") << "removed ITEs from lemma: " << ttfr.getNode()
+                        << endl;
+    Debug("lemma-ites") << " + now have the following " << newLemmas.size()
                         << " lemma(s):" << endl;
-    for (std::vector<Node>::const_iterator i = lemmas.begin();
-         i != lemmas.end();
-         ++i)
+    for (size_t i = 0, lsize = newLemmas.size(); i <= lsize; ++i)
     {
-      Debug("lemma-ites") << " + " << *i << endl;
+      Debug("lemma-ites") << " + " << newLemmas[i].getNode() << endl;
     }
     Debug("lemma-ites") << endl;
   }
 
+  retNode = Rewriter::rewrite(retNode);
+
   // now, rewrite the lemmas
-  Node retLemma;
-  for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i)
+  for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
   {
-    Node rewritten = Rewriter::rewrite(lemmas[i]);
-    lemmas.replace(i, rewritten);
+    // get the trust node to process
+    TrustNode trn = newLemmas[i];
+    Assert(trn.getKind() == TrustNodeKind::LEMMA);
+    Node assertion = trn.getNode();
+    // rewrite, which is independent of d_tpg, since additional lemmas
+    // are justified separately.
+    Node rewritten = Rewriter::rewrite(assertion);
+    if (assertion != rewritten)
+    {
+      // not tracking proofs, just make new
+      newLemmas[i] = TrustNode::mkTrustLemma(rewritten, nullptr);
+    }
   }
+  return TrustNode::mkTrustRewrite(node, retNode, nullptr);
 }
 
 struct preprocess_stack_element