(proof-new) Make theory preprocessor user-context dependent (#5296)

Previously, theory preprocessing cache was manually cleared whenever the theory preprocess pass was run. However, proofs for theory preprocessing required to be alive for the remainder of the user context. This PR changes theory preprocessing so that both the cache and proofs in theory preprocessing are user-context dependent.

This PR also makes the theory preprocess pass proof producing.

5 files changed, 40 insertions, 63 deletions

diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index a4d7db72e..bf9c3e9fe 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -32,12 +32,11 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
   TheoryEngine* te = d_preprocContext->getTheoryEngine();
-  te->preprocessStart();
   for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
     TNode a = (*assertionsToPreprocess)[i];
     Assert(Rewriter::rewrite(a) == a);
-    assertionsToPreprocess->replace(i, te->preprocess(a));
+    assertionsToPreprocess->replaceTrusted(i, te->preprocess(a));
     a = (*assertionsToPreprocess)[i];
     Assert(Rewriter::rewrite(a) == a);
   }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 924d045da..706149d86 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -251,7 +251,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_propagatedLiterals(context),
       d_propagatedLiteralsIndex(context, 0),
       d_atomRequests(context),
-      d_tpp(*this, iteRemover, d_pnm),
+      d_tpp(*this, iteRemover, userContext, d_pnm),
       d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
       d_true(),
       d_false(),
@@ -824,8 +824,6 @@ void TheoryEngine::shutdown() {
       theoryOf(theoryId)->shutdown();
     }
   }
-
-  d_tpp.clearCache();
 }
 
 theory::Theory::PPAssertStatus TheoryEngine::solve(
@@ -855,18 +853,9 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(
   return solveStatus;
 }
 
-void TheoryEngine::preprocessStart() { d_tpp.clearCache(); }
-
-Node TheoryEngine::preprocess(TNode assertion)
+TrustNode TheoryEngine::preprocess(TNode assertion)
 {
-  TrustNode trn = d_tpp.theoryPreprocess(assertion);
-  if (trn.isNull())
-  {
-    // no change
-    return assertion;
-  }
-  // notice that we could alternatively return the trust node here.
-  return trn.getNode();
+  return d_tpp.theoryPreprocess(assertion);
 }
 
 void TheoryEngine::notifyPreprocessedAssertions(
@@ -1147,7 +1136,8 @@ Node TheoryEngine::ensureLiteral(TNode n) {
   Debug("ensureLiteral") << "rewriting: " << n << std::endl;
   Node rewritten = Rewriter::rewrite(n);
   Debug("ensureLiteral") << "      got: " << rewritten << std::endl;
-  Node preprocessed = preprocess(rewritten);
+  TrustNode tp = preprocess(rewritten);
+  Node preprocessed = tp.isNull() ? rewritten : tp.getNode();
   Debug("ensureLiteral") << "preprocessed: " << preprocessed << std::endl;
   d_propEngine->ensureLiteral(preprocessed);
   return preprocessed;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 3626b623a..e47dbbc6f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -446,16 +446,11 @@ class TheoryEngine {
 
  public:
   /**
-   * Signal the start of a new round of assertion preprocessing
-   */
-  void preprocessStart();
-
-  /**
    * Runs theory specific preprocessing on the non-Boolean parts of
    * the formula.  This is only called on input assertions, after ITEs
    * have been removed.
    */
-  Node preprocess(TNode node);
+  theory::TrustNode preprocess(TNode node);
 
   /** Notify (preprocessed) assertions. */
   void notifyPreprocessedAssertions(const std::vector<Node>& assertions);
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index b37a45967..42ac074ce 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -27,15 +27,15 @@ namespace theory {
 
 TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
                                        RemoveTermFormulas& tfr,
+                                       context::UserContext* userContext,
                                        ProofNodeManager* pnm)
     : d_engine(engine),
       d_logicInfo(engine.getLogicInfo()),
-      d_ppCache(),
+      d_ppCache(userContext),
       d_tfr(tfr),
-      d_pfContext(),
       d_tpg(pnm ? new TConvProofGenerator(
                       pnm,
-                      &d_pfContext,
+                      userContext,
                       TConvPolicy::FIXPOINT,
                       TConvCachePolicy::NEVER,
                       "TheoryPreprocessor::preprocess_rewrite",
@@ -43,7 +43,7 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
                 : nullptr),
       d_tspg(nullptr),
       d_tpgRew(pnm ? new TConvProofGenerator(pnm,
-                                             &d_pfContext,
+                                             userContext,
                                              TConvPolicy::FIXPOINT,
                                              TConvCachePolicy::NEVER,
                                              "TheoryPreprocessor::rewrite")
@@ -51,15 +51,12 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
       d_tspgNoPp(nullptr),
       d_lp(pnm ? new LazyCDProof(pnm,
                                  nullptr,
-                                 &d_pfContext,
+                                 userContext,
                                  "TheoryPreprocessor::LazyCDProof")
                : nullptr)
 {
   if (isProofEnabled())
   {
-    // push the proof context, since proof steps may be cleared on calls to
-    // clearCache() below.
-    d_pfContext.push();
     // Make the main term conversion sequence generator, which tracks up to
     // three conversions made in succession:
     // (1) theory preprocessing+rewriting
@@ -71,7 +68,7 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
     ts.push_back(d_tfr.getTConvProofGenerator());
     ts.push_back(d_tpg.get());
     d_tspg.reset(new TConvSeqProofGenerator(
-        pnm, ts, &d_pfContext, "TheoryPreprocessor::sequence"));
+        pnm, ts, userContext, "TheoryPreprocessor::sequence"));
     // Make the "no preprocess" term conversion sequence generator, which
     // applies only steps (2) and (3), where notice (3) must use the
     // "pure rewrite" term conversion (d_tpgRew).
@@ -79,24 +76,12 @@ TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
     tsNoPp.push_back(d_tfr.getTConvProofGenerator());
     tsNoPp.push_back(d_tpgRew.get());
     d_tspgNoPp.reset(new TConvSeqProofGenerator(
-        pnm, tsNoPp, &d_pfContext, "TheoryPreprocessor::sequence_no_pp"));
+        pnm, tsNoPp, userContext, "TheoryPreprocessor::sequence_no_pp"));
   }
 }
 
 TheoryPreprocessor::~TheoryPreprocessor() {}
 
-void TheoryPreprocessor::clearCache()
-{
-  Trace("tpp-proof-debug") << "TheoryPreprocessor::clearCache" << std::endl;
-  d_ppCache.clear();
-  // clear proofs from d_tpg, d_tspg 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,
@@ -115,18 +100,10 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
     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 rtfNode = ttfr.getNode();
-  Trace("tpp-proof-debug")
-      << "TheoryPreprocessor::preprocess: rtf returned node " << rtfNode
-      << std::endl;
 
   if (Debug.isOn("lemma-ites"))
   {
@@ -143,9 +120,25 @@ TrustNode TheoryPreprocessor::preprocess(TNode node,
   // 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.
   Node retNode = rewriteWithProof(rtfNode);
-  Trace("tpp-proof-debug")
-      << "TheoryPreprocessor::preprocess: after rewriting is " << retNode
-      << std::endl;
+
+  if (Trace.isOn("tpp-proof-debug"))
+  {
+    if (node != ppNode)
+    {
+      Trace("tpp-proof-debug")
+          << "after preprocessing : " << ppNode << std::endl;
+    }
+    if (rtfNode != ppNode)
+    {
+      Trace("tpp-proof-debug") << "after rtf : " << rtfNode << std::endl;
+    }
+    if (retNode != rtfNode)
+    {
+      Trace("tpp-proof-debug") << "after rewriting : " << retNode << std::endl;
+    }
+    Trace("tpp-proof-debug")
+        << "TheoryPreprocessor::preprocess: finish" << std::endl;
+  }
   if (node == retNode)
   {
     // no change
@@ -284,7 +277,8 @@ TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
     {
       Node ppRewritten = ppTheoryRewrite(current);
       d_ppCache[current] = ppRewritten;
-      Assert(Rewriter::rewrite(d_ppCache[current]) == d_ppCache[current]);
+      Assert(Rewriter::rewrite(d_ppCache[current].get())
+             == d_ppCache[current].get());
       continue;
     }
 
@@ -300,7 +294,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess(TNode assertion)
       for (unsigned i = 0; i < current.getNumChildren(); ++i)
       {
         Assert(d_ppCache.find(current[i]) != d_ppCache.end());
-        builder << d_ppCache[current[i]];
+        builder << d_ppCache[current[i]].get();
       }
       // Mark the substitution and continue
       Node result = builder;
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index 769d548d9..e34b10b1d 100644
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -19,6 +19,8 @@
 
 #include <unordered_map>
 
+#include "context/cdhashmap.h"
+#include "context/context.h"
 #include "expr/lazy_proof.h"
 #include "expr/node.h"
 #include "expr/tconv_seq_proof_generator.h"
@@ -38,17 +40,16 @@ namespace theory {
  */
 class TheoryPreprocessor
 {
-  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
 
  public:
   /** Constructs a theory preprocessor */
   TheoryPreprocessor(TheoryEngine& engine,
                      RemoveTermFormulas& tfr,
+                     context::UserContext* userContext,
                      ProofNodeManager* pnm = nullptr);
   /** Destroys a theory preprocessor */
   ~TheoryPreprocessor();
-  /** Clear the cache of this class */
-  void clearCache();
   /**
    * Preprocesses the given assertion node. It returns a TrustNode of kind
    * TrustNodeKind::REWRITE indicating the preprocessed form of node. It stores
@@ -84,8 +85,6 @@ class TheoryPreprocessor
   NodeMap d_ppCache;
   /** The term formula remover */
   RemoveTermFormulas& d_tfr;
-  /** The context for the proof generator below */
-  context::Context d_pfContext;
   /** The term context, which computes hash values for term contexts. */
   InQuantTermContext d_iqtc;
   /**