(proof-new) Theory preprocessor proof producing (#4807)

This makes the theory preprocessor proof producing in the new infrastructure, which involves updating its interfaces to TrustNode in a few places.

1 files changed, 178 insertions, 28 deletions

diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 328c65fcb..6e569508b 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/theory_preprocessor.h"
 
+#include "expr/lazy_proof.h"
+#include "expr/skolem_manager.h"
 #include "theory/logic_info.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
@@ -24,31 +26,90 @@ namespace CVC4 {
 namespace theory {
 
 TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
-                                       RemoveTermFormulas& tfr)
+                                       RemoveTermFormulas& tfr,
+                                       ProofNodeManager* pnm)
     : d_engine(engine),
       d_logicInfo(engine.getLogicInfo()),
       d_ppCache(),
-      d_tfr(tfr)
+      d_tfr(tfr),
+      d_pfContext(),
+      d_tpg(pnm ? new TConvProofGenerator(
+                      pnm,
+                      &d_pfContext,
+                      TConvPolicy::FIXPOINT,
+                      TConvCachePolicy::NEVER,
+                      "TheoryPreprocessor::TConvProofGenerator")
+                : nullptr),
+      d_lp(pnm ? new LazyCDProof(pnm,
+                                 nullptr,
+                                 &d_pfContext,
+                                 "TheoryPreprocessor::LazyCDProof")
+               : nullptr)
 {
+  if (isProofEnabled())
+  {
+    // enable proofs in the term formula remover
+    d_tfr.setProofNodeManager(pnm);
+    // push the proof context, since proof steps may be cleared on calls to
+    // clearCache() below.
+    d_pfContext.push();
+  }
 }
 
 TheoryPreprocessor::~TheoryPreprocessor() {}
 
-void TheoryPreprocessor::clearCache() { d_ppCache.clear(); }
+void TheoryPreprocessor::clearCache()
+{
+  d_ppCache.clear();
+  // clear proofs from d_tpg and d_lp using internal push/pop context
+  if (isProofEnabled())
+  {
+    d_pfContext.pop();
+    d_pfContext.push();
+  }
+}
 
 TrustNode TheoryPreprocessor::preprocess(TNode node,
                                          std::vector<TrustNode>& newLemmas,
                                          std::vector<Node>& newSkolems,
                                          bool doTheoryPreprocess)
 {
+  // In this method, all rewriting steps of node are stored in d_tpg.
+
+  Trace("tpp-proof-debug") << "TheoryPreprocessor::preprocess: start " << node
+                           << std::endl;
   // Run theory preprocessing, maybe
-  Node ppNode = doTheoryPreprocess ? theoryPreprocess(node) : Node(node);
+  Node ppNode = node;
+  if (doTheoryPreprocess)
+  {
+    // run theory preprocessing
+    TrustNode tpp = theoryPreprocess(node);
+    ppNode = tpp.getNode();
+  }
+  Trace("tpp-proof-debug")
+      << "TheoryPreprocessor::preprocess: after preprocessing " << ppNode
+      << std::endl;
 
   // Remove the ITEs
   Trace("te-tform-rm") << "Remove term formulas from " << ppNode << 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 (isProofEnabled())
+  {
+    // if we rewrote
+    if (retNode != ppNode)
+    {
+      // should always have provided a proof generator, or else term formula
+      // removal and this class do not agree on whether proofs are enabled.
+      Assert(ttfr.getGenerator() != nullptr);
+      Trace("tpp-proof-debug")
+          << "TheoryPreprocessor: addRewriteStep (term formula removal) "
+          << ppNode << " -> " << retNode << std::endl;
+      // store as a rewrite in d_tpg
+      d_tpg->addRewriteStep(ppNode, retNode, ttfr.getGenerator());
+    }
+  }
 
   if (Debug.isOn("lemma-ites"))
   {
@@ -62,14 +123,25 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
     }
     Debug("lemma-ites") << endl;
   }
-
-  retNode = Rewriter::rewrite(retNode);
+  // Rewrite the main node, we rewrite and store the proof step, if necessary,
+  // in d_tpg, which maintains the fact that d_tpg can prove the rewrite.
+  Trace("tpp-proof-debug")
+      << "TheoryPreprocessor::preprocess: rewrite returned node " << retNode
+      << std::endl;
+  retNode = rewriteWithProof(retNode);
+  Trace("tpp-proof-debug")
+      << "TheoryPreprocessor::preprocess: after rewriting is " << retNode
+      << std::endl;
 
   // now, rewrite the lemmas
+  Trace("tpp-proof-debug") << "TheoryPreprocessor::preprocess: process lemmas"
+                           << std::endl;
   for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
   {
     // get the trust node to process
     TrustNode trn = newLemmas[i];
+    trn.debugCheckClosed(
+        "tpp-proof-debug", "TheoryPreprocessor::lemma_new_initial", false);
     Assert(trn.getKind() == TrustNodeKind::LEMMA);
     Node assertion = trn.getNode();
     // rewrite, which is independent of d_tpg, since additional lemmas
@@ -77,11 +149,37 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
     Node rewritten = Rewriter::rewrite(assertion);
     if (assertion != rewritten)
     {
-      // not tracking proofs, just make new
-      newLemmas[i] = TrustNode::mkTrustLemma(rewritten, nullptr);
+      if (isProofEnabled())
+      {
+        Assert(d_lp != nullptr);
+        // store in the lazy proof
+        d_lp->addLazyStep(assertion,
+                          trn.getGenerator(),
+                          true,
+                          "TheoryPreprocessor::rewrite_lemma_new",
+                          false,
+                          PfRule::THEORY_PREPROCESS_LEMMA);
+        d_lp->addStep(rewritten,
+                      PfRule::MACRO_SR_PRED_TRANSFORM,
+                      {assertion},
+                      {rewritten});
+      }
+      newLemmas[i] = TrustNode::mkTrustLemma(rewritten, d_lp.get());
     }
+    Assert(!isProofEnabled() || newLemmas[i].getGenerator() != nullptr);
+    newLemmas[i].debugCheckClosed("tpp-proof-debug",
+                                  "TheoryPreprocessor::lemma_new");
   }
-  return TrustNode::mkTrustRewrite(node, retNode, nullptr);
+  if (node == retNode)
+  {
+    // no change
+    return TrustNode::null();
+  }
+  Trace("tpp-proof-debug") << "Preprocessed: " << node << " " << retNode
+                           << std::endl;
+  TrustNode tret = TrustNode::mkTrustRewrite(node, retNode, d_tpg.get());
+  tret.debugCheckClosed("tpp-proof-debug", "TheoryPreprocessor::lemma_ret");
+  return tret;
 }
 
 struct preprocess_stack_element
@@ -91,7 +189,7 @@ struct preprocess_stack_element
   preprocess_stack_element(TNode n) : node(n), children_added(false) {}
 };
 
-Node TheoryPreprocessor::theoryPreprocess(TNode assertion)
+TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
 {
   Trace("theory::preprocess")
       << "TheoryPreprocessor::theoryPreprocess(" << assertion << ")" << endl;
@@ -158,7 +256,7 @@ Node TheoryPreprocessor::theoryPreprocess(TNode assertion)
       Node result = builder;
       if (result != current)
       {
-        result = Rewriter::rewrite(result);
+        result = rewriteWithProof(result);
       }
       Debug("theory::internal")
           << "TheoryPreprocessor::theoryPreprocess(" << assertion
@@ -196,9 +294,9 @@ Node TheoryPreprocessor::theoryPreprocess(TNode assertion)
       }
     }
   }
-
   // Return the substituted version
-  return d_ppCache[assertion];
+  Node res = d_ppCache[assertion];
+  return TrustNode::mkTrustRewrite(assertion, res, d_tpg.get());
 }
 
 // Recursively traverse a term and call the theory rewriter on its sub-terms
@@ -212,18 +310,13 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term)
   unsigned nc = term.getNumChildren();
   if (nc == 0)
   {
-    TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term);
-    return trn.isNull() ? Node(term) : trn.getNode();
+    return preprocessWithProof(term);
   }
   Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
 
-  Node newTerm;
+  Node newTerm = term;
   // do not rewrite inside quantifiers
-  if (term.isClosure())
-  {
-    newTerm = Rewriter::rewrite(term);
-  }
-  else
+  if (!term.isClosure())
   {
     NodeBuilder<> newNode(term.getKind());
     if (term.getMetaKind() == kind::metakind::PARAMETERIZED)
@@ -235,18 +328,75 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term)
     {
       newNode << ppTheoryRewrite(term[i]);
     }
-    newTerm = Rewriter::rewrite(Node(newNode));
-  }
-  TrustNode trn = d_engine.theoryOf(newTerm)->ppRewrite(newTerm);
-  Node newTerm2 = trn.isNull() ? newTerm : trn.getNode();
-  if (newTerm != newTerm2)
-  {
-    newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2));
+    newTerm = Node(newNode);
   }
+  newTerm = rewriteWithProof(newTerm);
+  newTerm = preprocessWithProof(newTerm);
   d_ppCache[term] = newTerm;
   Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl;
   return newTerm;
 }
 
+Node TheoryPreprocessor::rewriteWithProof(Node term)
+{
+  Node termr = Rewriter::rewrite(term);
+  // store rewrite step if tracking proofs and it rewrites
+  if (isProofEnabled())
+  {
+    // may rewrite the same term more than once, thus check hasRewriteStep
+    if (termr != term)
+    {
+      Trace("tpp-proof-debug")
+          << "TheoryPreprocessor: addRewriteStep (rewriting) " << term << " -> "
+          << termr << std::endl;
+      d_tpg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term});
+    }
+  }
+  return termr;
+}
+
+Node TheoryPreprocessor::preprocessWithProof(Node term)
+{
+  // Important that it is in rewritten form, to ensure that the rewrite steps
+  // recorded in d_tpg are functional. In other words, there should not
+  // be steps from the same term to multiple rewritten forms, which would be
+  // the case if we registered a preprocessing step for a non-rewritten term.
+  Assert(term == Rewriter::rewrite(term));
+  // call ppRewrite for the given theory
+  TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term);
+  if (trn.isNull())
+  {
+    // no change, return original term
+    return term;
+  }
+  Node termr = trn.getNode();
+  Assert(term != termr);
+  if (isProofEnabled())
+  {
+    if (trn.getGenerator() != nullptr)
+    {
+      Trace("tpp-proof-debug")
+          << "TheoryPreprocessor: addRewriteStep (generator) " << term << " -> "
+          << termr << std::endl;
+      trn.debugCheckClosed("tpp-proof-debug",
+                           "TheoryPreprocessor::preprocessWithProof");
+      d_tpg->addRewriteStep(term, termr, trn.getGenerator());
+    }
+    else
+    {
+      Trace("tpp-proof-debug")
+          << "TheoryPreprocessor: addRewriteStep (trusted) " << term << " -> "
+          << termr << std::endl;
+      // small step trust
+      d_tpg->addRewriteStep(
+          term, termr, PfRule::THEORY_PREPROCESS, {}, {term.eqNode(termr)});
+    }
+  }
+  termr = rewriteWithProof(termr);
+  return ppTheoryRewrite(termr);
+}
+
+bool TheoryPreprocessor::isProofEnabled() const { return d_tpg != nullptr; }
+
 }  // namespace theory
 }  // namespace CVC4