(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.

diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index a4d7db72e46627dd8b8e48bbd585e84ffaae15f5..bf9c3e9fed4cc2186d5f41373e385981d58bc3f1 100644 (file)
--- 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 924d045daf6612a7e97cb6b27c80981c3a68cf54..706149d86f618caad10e7b32a2ce5af094807162 100644 (file)
--- 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 3626b623ad35c898ad42693f4aa3ac9587a60786..e47dbbc6fabca704f4556f47f5344f3f5348cc46 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -445,17 +445,12 @@ class TheoryEngine {
   bool isProofEnabled() const;
 
  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 b37a459671a1666a7d0797b82abdda4c6b491dee..42ac074ce5d5c51112c3e25c070e92aa15f9ec98 100644 (file)
--- 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 769d548d97e85faa4ab251d140bfa994b2316dbd..e34b10b1dbd01bc6fb018cc6d3c820e019ca5a46 100644 (file)
--- 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;
   /**