(proof-new) Improve interfaces to proof generators (#4803)

This includes configurable naming and a caching policy for term conversion proof generator.

Also corrects a subtle issue in LazyCDProof related to making getProofFor idempotent using the notion of owned proofs.

16 files changed, 323 insertions, 61 deletions

diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index df0258af7..dc984438c 100644
--- a/src/expr/lazy_proof.cpp
+++ b/src/expr/lazy_proof.cpp
@@ -20,8 +20,9 @@ namespace CVC4 {
 
 LazyCDProof::LazyCDProof(ProofNodeManager* pnm,
                          ProofGenerator* dpg,
-                         context::Context* c)
-    : CDProof(pnm, c), d_gens(c ? c : &d_context), d_defaultGen(dpg)
+                         context::Context* c,
+                         std::string name)
+    : CDProof(pnm, c, name), d_gens(c ? c : &d_context), d_defaultGen(dpg)
 {
 }
 
@@ -56,36 +57,47 @@ std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact)
     if (it == visited.end())
     {
       visited.insert(cur);
-      if (cur->getRule() == PfRule::ASSUME)
+      Node cfact = cur->getResult();
+      if (getProof(cfact).get() != cur)
+      {
+        // We don't own this proof, skip it. This is to ensure that this method
+        // is idempotent, since it may be the case that a previous call to
+        // getProofFor connected a proof from a proof generator as a child of
+        // a ProofNode in the range of the map in CDProof. Thus, this ensures
+        // we don't touch such proofs.
+        Trace("lazy-cdproof") << "...skip unowned proof" << std::endl;
+      }
+      else if (cur->getRule() == PfRule::ASSUME)
       {
-        Node afact = cur->getResult();
         bool isSym = false;
-        ProofGenerator* pg = getGeneratorFor(afact, isSym);
+        ProofGenerator* pg = getGeneratorFor(cfact, isSym);
         if (pg != nullptr)
         {
-          Trace("lazy-cdproof") << "LazyCDProof: Call generator for assumption "
-                                << afact << std::endl;
-          Node afactGen = isSym ? CDProof::getSymmFact(afact) : afact;
-          Assert(!afactGen.isNull());
-          // use the addProofTo interface
-          if (!pg->addProofTo(afactGen, this))
+          Trace("lazy-cdproof")
+              << "LazyCDProof: Call generator " << pg->identify()
+              << " for assumption " << cfact << std::endl;
+          Node cfactGen = isSym ? CDProof::getSymmFact(cfact) : cfact;
+          Assert(!cfactGen.isNull());
+          // Do not use the addProofTo interface, instead use the update node
+          // interface, since this ensures that we don't take ownership for
+          // the current proof. Instead, it is only linked, and ignored on
+          // future calls to getProofFor due to the check above.
+          std::shared_ptr<ProofNode> pgc = pg->getProofFor(cfactGen);
+          if (isSym)
           {
-            Trace("lazy-cdproof") << "LazyCDProof: Failed added fact for "
-                                  << afactGen << std::endl;
-            Assert(false) << "Proof generator " << pg->identify()
-                          << " could not add proof for fact " << afactGen
-                          << std::endl;
+            d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {});
           }
           else
           {
-            Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for "
-                                  << afactGen << std::endl;
+            d_manager->updateNode(cur, pgc.get());
           }
+          Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for "
+                                << cfactGen << std::endl;
         }
         else
         {
-          Trace("lazy-cdproof")
-              << "LazyCDProof: No generator for " << afact << std::endl;
+          Trace("lazy-cdproof") << "LazyCDProof: " << identify()
+                                << " : No generator for " << cfact << std::endl;
         }
         // Notice that we do not traverse the proofs that have been generated
         // lazily by the proof generators here.  In other words, we assume that
@@ -104,11 +116,14 @@ std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact)
   } while (!visit.empty());
   // we have now updated the ASSUME leafs of opf, return it
   Trace("lazy-cdproof") << "...finished" << std::endl;
+  Assert(opf->getResult() == fact);
   return opf;
 }
 
 void LazyCDProof::addLazyStep(Node expected,
                               ProofGenerator* pg,
+                              bool isClosed,
+                              const char* ctx,
                               bool forceOverwrite,
                               PfRule idNull)
 {
@@ -117,7 +132,8 @@ void LazyCDProof::addLazyStep(Node expected,
     // null generator, should have given a proof rule
     if (idNull == PfRule::ASSUME)
     {
-      Assert(false);
+      Unreachable() << "LazyCDProof::addLazyStep: " << identify()
+                    << ": failed to provide proof generator for " << expected;
       return;
     }
     Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
@@ -138,6 +154,12 @@ void LazyCDProof::addLazyStep(Node expected,
   }
   // just store now
   d_gens.insert(expected, pg);
+  // debug checking
+  if (isClosed)
+  {
+    Trace("lazy-cdproof-debug") << "Checking closed..." << std::endl;
+    pfgEnsureClosed(expected, pg, "lazy-cdproof-debug", ctx);
+  }
 }
 
 ProofGenerator* LazyCDProof::getGeneratorFor(Node fact,
@@ -191,6 +213,4 @@ bool LazyCDProof::hasGenerator(Node fact) const
   return it != d_gens.end();
 }
 
-std::string LazyCDProof::identify() const { return "LazyCDProof"; }
-
 }  // namespace CVC4
diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
index 1f68a3ccb..4368cbb85 100644
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -45,7 +45,8 @@ class LazyCDProof : public CDProof
    */
   LazyCDProof(ProofNodeManager* pnm,
               ProofGenerator* dpg = nullptr,
-              context::Context* c = nullptr);
+              context::Context* c = nullptr,
+              std::string name = "LazyCDProof");
   ~LazyCDProof();
   /**
    * Get lazy proof for fact, or nullptr if it does not exist. This may
@@ -66,6 +67,9 @@ class LazyCDProof : public CDProof
    *
    * @param expected The fact that can be proven.
    * @param pg The generator that can proof expected.
+   * @param isClosed Whether to expect that pg can provide a closed proof for
+   * this fact.
+   * @param ctx The context we are in (for debugging).
    * @param forceOverwrite If this flag is true, then this call overwrites
    * an existing proof generator provided for expected, if one was provided
    * via a previous call to addLazyStep in the current context.
@@ -76,6 +80,8 @@ class LazyCDProof : public CDProof
    */
   void addLazyStep(Node expected,
                    ProofGenerator* pg,
+                   bool isClosed = true,
+                   const char* ctx = "LazyCDProof::addLazyStep",
                    bool forceOverwrite = false,
                    PfRule trustId = PfRule::ASSUME);
   /**
@@ -85,8 +91,6 @@ class LazyCDProof : public CDProof
   bool hasGenerators() const;
   /** Does the given fact have an explicitly provided generator? */
   bool hasGenerator(Node fact) const;
-  /** identify */
-  std::string identify() const override;
 
  protected:
   typedef context::CDHashMap<Node, ProofGenerator*, NodeHashFunction>
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index 20e8e29e2..a9e6d6940 100644
--- a/src/expr/proof.cpp
+++ b/src/expr/proof.cpp
@@ -18,8 +18,8 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
-CDProof::CDProof(ProofNodeManager* pnm, context::Context* c)
-    : d_manager(pnm), d_context(), d_nodes(c ? c : &d_context)
+CDProof::CDProof(ProofNodeManager* pnm, context::Context* c, std::string name)
+    : d_manager(pnm), d_context(), d_nodes(c ? c : &d_context), d_name(name)
 {
 }
 
@@ -111,9 +111,13 @@ bool CDProof::addStep(Node expected,
                       bool ensureChildren,
                       CDPOverwrite opolicy)
 {
-  Trace("cdproof") << "CDProof::addStep: " << id << " " << expected
-                   << ", ensureChildren = " << ensureChildren
+  Trace("cdproof") << "CDProof::addStep: " << identify() << " : " << id << " "
+                   << expected << ", ensureChildren = " << ensureChildren
                    << ", overwrite policy = " << opolicy << std::endl;
+  Trace("cdproof-debug") << "CDProof::addStep: " << identify()
+                         << " : children: " << children << "\n";
+  Trace("cdproof-debug") << "CDProof::addStep: " << identify()
+                         << " : args: " << args << "\n";
   // We must always provide expected to this method
   Assert(!expected.isNull());
 
@@ -424,6 +428,6 @@ Node CDProof::getSymmFact(TNode f)
   return polarity ? symFact : symFact.notNode();
 }
 
-std::string CDProof::identify() const { return "CDProof"; }
+std::string CDProof::identify() const { return d_name; }
 
 }  // namespace CVC4
diff --git a/src/expr/proof.h b/src/expr/proof.h
index ff6b8bbf1..5fbcc4ec8 100644
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -134,7 +134,9 @@ namespace CVC4 {
 class CDProof : public ProofGenerator
 {
  public:
-  CDProof(ProofNodeManager* pnm, context::Context* c = nullptr);
+  CDProof(ProofNodeManager* pnm,
+          context::Context* c = nullptr,
+          std::string name = "CDProof");
   virtual ~CDProof();
   /**
    * Make proof for fact.
@@ -224,6 +226,8 @@ class CDProof : public ProofGenerator
    * f suffices as a proof for g according to this class.
    */
   static bool isSame(TNode f, TNode g);
+  /** Get proof for fact, or nullptr if it does not exist. */
+  std::shared_ptr<ProofNode> getProof(Node fact) const;
   /**
    * Get symmetric fact (a g such that isSame returns true for isSame(f,g)), or
    * null if none exist.
@@ -241,8 +245,8 @@ class CDProof : public ProofGenerator
   context::Context d_context;
   /** The nodes of the proof */
   NodeProofNodeMap d_nodes;
-  /** Get proof for fact, or nullptr if it does not exist. */
-  std::shared_ptr<ProofNode> getProof(Node fact) const;
+  /** Name identifier */
+  std::string d_name;
   /** Ensure fact sym */
   std::shared_ptr<ProofNode> getProofSymm(Node fact);
   /**
diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index be2c22c1e..7a480fa97 100644
--- a/src/expr/proof_generator.cpp
+++ b/src/expr/proof_generator.cpp
@@ -15,6 +15,8 @@
 #include "expr/proof_generator.h"
 
 #include "expr/proof.h"
+#include "expr/proof_node_algorithm.h"
+#include "options/smt_options.h"
 
 namespace CVC4 {
 
@@ -66,4 +68,93 @@ bool ProofGenerator::addProofTo(Node f, CDProof* pf, CDPOverwrite opolicy)
   return false;
 }
 
+void pfgEnsureClosed(Node proven,
+                     ProofGenerator* pg,
+                     const char* c,
+                     const char* ctx,
+                     bool reqGen)
+{
+  std::vector<Node> assumps;
+  pfgEnsureClosedWrt(proven, pg, assumps, c, ctx, reqGen);
+}
+
+void pfgEnsureClosedWrt(Node proven,
+                        ProofGenerator* pg,
+                        const std::vector<Node>& assumps,
+                        const char* c,
+                        const char* ctx,
+                        bool reqGen)
+{
+  if (!options::proofNew())
+  {
+    // proofs not enabled, do not do check
+    return;
+  }
+  bool isTraceDebug = Trace.isOn(c);
+  if (!options::proofNewEagerChecking() && !isTraceDebug)
+  {
+    // trace is off and proof new eager checking is off, do not do check
+    return;
+  }
+  std::stringstream ss;
+  ss << "ProofGenerator: " << (pg == nullptr ? "null" : pg->identify())
+     << " in context " << ctx;
+  std::stringstream sdiag;
+  bool isTraceOn = Trace.isOn(c);
+  if (!isTraceOn)
+  {
+    sdiag << ", use -t " << c << " for details";
+  }
+  Trace(c) << "=== pfgEnsureClosed: " << ss.str() << std::endl;
+  Trace(c) << "Proven: " << proven << std::endl;
+  if (pg == nullptr)
+  {
+    // only failure if flag is true
+    if (reqGen)
+    {
+      Unreachable() << "...pfgEnsureClosed: no generator in context " << ctx
+                    << sdiag.str();
+    }
+    Trace(c) << "...pfgEnsureClosed: no generator in context " << ctx
+             << std::endl;
+    return;
+  }
+  std::shared_ptr<ProofNode> pn = pg->getProofFor(proven);
+  Trace(c) << " Proof: " << *pn.get() << std::endl;
+  if (pn == nullptr)
+  {
+    AlwaysAssert(false) << "...pfgEnsureClosed: null proof from " << ss.str()
+                        << sdiag.str();
+  }
+  std::vector<Node> fassumps;
+  expr::getFreeAssumptions(pn.get(), fassumps);
+  bool isClosed = true;
+  std::stringstream ssf;
+  for (const Node& fa : fassumps)
+  {
+    if (std::find(assumps.begin(), assumps.end(), fa) == assumps.end())
+    {
+      isClosed = false;
+      ssf << "- " << fa << std::endl;
+    }
+  }
+  if (!isClosed)
+  {
+    Trace(c) << "Free assumptions:" << std::endl;
+    Trace(c) << ssf.str();
+    if (!assumps.empty())
+    {
+      Trace(c) << "Expected assumptions:" << std::endl;
+      for (const Node& a : assumps)
+      {
+        Trace(c) << "- " << a << std::endl;
+      }
+    }
+  }
+  AlwaysAssert(isClosed) << "...pfgEnsureClosed: open proof from " << ss.str()
+                         << sdiag.str();
+  Trace(c) << "...pfgEnsureClosed: success" << std::endl;
+  Trace(c) << "====" << std::endl;
+}
+
 }  // namespace CVC4
diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h
index 35f94194f..298f9b4c6 100644
--- a/src/expr/proof_generator.h
+++ b/src/expr/proof_generator.h
@@ -105,6 +105,33 @@ class ProofGenerator
   virtual std::string identify() const = 0;
 };
 
+/**
+ * Debug check closed on Trace c. Context ctx is string for debugging.
+ * This method throws an assertion failure if pg cannot provide a closed
+ * proof for fact proven. This is checked only if --proof-new-eager-checking
+ * is enabled or the Trace c is enabled.
+ *
+ * @param reqGen Whether we consider a null generator to be a failure.
+ */
+void pfgEnsureClosed(Node proven,
+                     ProofGenerator* pg,
+                     const char* c,
+                     const char* ctx,
+                     bool reqGen = true);
+
+/**
+ * Debug check closed with Trace c. Context ctx is string for debugging and
+ * assumps is the set of allowed open assertions.
+ *
+ * @param reqGen Whether we consider a null generator to be a failure.
+ */
+void pfgEnsureClosedWrt(Node proven,
+                        ProofGenerator* pg,
+                        const std::vector<Node>& assumps,
+                        const char* c,
+                        const char* ctx,
+                        bool reqGen = true);
+
 }  // namespace CVC4
 
 #endif /* CVC4__EXPR__PROOF_GENERATOR_H */
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 9713adbec..c4b72208e 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -134,4 +134,9 @@ std::ostream& operator<<(std::ostream& out, PfRule id)
   return out;
 }
 
+size_t PfRuleHashFunction::operator()(PfRule id) const
+{
+  return static_cast<size_t>(id);
+}
+
 }  // namespace CVC4
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 3d468d08e..beff92bd4 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -851,6 +851,12 @@ const char* toString(PfRule id);
  */
 std::ostream& operator<<(std::ostream& out, PfRule id);
 
+/** Hash function for proof rules */
+struct PfRuleHashFunction
+{
+  size_t operator()(PfRule id) const;
+}; /* struct PfRuleHashFunction */
+
 }  // namespace CVC4
 
 #endif /* CVC4__EXPR__PROOF_RULE_H */
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
index bad163375..1c4baeed7 100644
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -29,10 +29,28 @@ std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol)
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol)
+{
+  switch (tcpol)
+  {
+    case TConvCachePolicy::STATIC: out << "STATIC"; break;
+    case TConvCachePolicy::DYNAMIC: out << "DYNAMIC"; break;
+    case TConvCachePolicy::NEVER: out << "NEVER"; break;
+    default: out << "TConvCachePolicy:unknown"; break;
+  }
+  return out;
+}
+
 TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
                                          context::Context* c,
-                                         TConvPolicy tpol)
-    : d_proof(pnm, nullptr, c), d_rewriteMap(c ? c : &d_context), d_policy(tpol)
+                                         TConvPolicy pol,
+                                         TConvCachePolicy cpol,
+                                         std::string name)
+    : d_proof(pnm, nullptr, c, name + "::LazyCDProof"),
+      d_rewriteMap(c ? c : &d_context),
+      d_policy(pol),
+      d_cpolicy(cpol),
+      d_name(name)
 {
 }
 
@@ -87,6 +105,11 @@ Node TConvProofGenerator::registerRewriteStep(Node t, Node s)
     return Node::null();
   }
   d_rewriteMap[t] = s;
+  if (d_cpolicy == TConvCachePolicy::DYNAMIC)
+  {
+    // clear the cache
+    d_cache.clear();
+  }
   return t.eqNode(s);
 }
 
@@ -101,7 +124,8 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
     return nullptr;
   }
   // we use the existing proofs
-  LazyCDProof lpf(d_proof.getManager(), &d_proof);
+  LazyCDProof lpf(
+      d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProof");
   Node conc = getProofForRewriting(f[0], lpf);
   if (conc != f)
   {
@@ -125,6 +149,7 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf)
   std::unordered_map<TNode, Node, TNodeHashFunction> rewritten;
   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator itr;
+  std::map<Node, std::shared_ptr<ProofNode> >::iterator itc;
   std::vector<TNode> visit;
   TNode cur;
   visit.push_back(t);
@@ -132,8 +157,17 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf)
   {
     cur = visit.back();
     visit.pop_back();
+    // has the proof for cur been cached?
+    itc = d_cache.find(cur);
+    if (itc != d_cache.end())
+    {
+      Node res = itc->second->getResult();
+      Assert(res.getKind() == EQUAL);
+      visited[cur] = res[1];
+      pf.addProof(itc->second);
+      continue;
+    }
     it = visited.find(cur);
-
     if (it == visited.end())
     {
       visited[cur] = Node::null();
@@ -157,6 +191,7 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf)
           Assert(d_policy == TConvPolicy::ONCE);
           // not rewriting again, rcur is final
           visited[cur] = rcur;
+          doCache(cur, rcur, pf);
         }
       }
       else
@@ -189,6 +224,7 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf)
           pf.addStep(result, PfRule::TRANS, pfChildren, {});
         }
         visited[cur] = rcurFinal;
+        doCache(cur, rcurFinal, pf);
       }
       else
       {
@@ -259,6 +295,7 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf)
         {
           // it is final
           visited[cur] = ret;
+          doCache(cur, ret, pf);
         }
       }
     }
@@ -269,6 +306,15 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf)
   return t.eqNode(visited[t]);
 }
 
+void TConvProofGenerator::doCache(Node cur, Node r, LazyCDProof& pf)
+{
+  if (d_cpolicy != TConvCachePolicy::NEVER)
+  {
+    Node eq = cur.eqNode(r);
+    d_cache[cur] = pf.getProofFor(eq);
+  }
+}
+
 Node TConvProofGenerator::getRewriteStep(Node t) const
 {
   NodeNodeMap::const_iterator it = d_rewriteMap.find(t);
@@ -278,9 +324,6 @@ Node TConvProofGenerator::getRewriteStep(Node t) const
   }
   return (*it).second;
 }
-std::string TConvProofGenerator::identify() const
-{
-  return "TConvProofGenerator";
-}
+std::string TConvProofGenerator::identify() const { return d_name; }
 
 }  // namespace CVC4
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
index d7ff6e8f6..e634b8a83 100644
--- a/src/expr/term_conversion_proof_generator.h
+++ b/src/expr/term_conversion_proof_generator.h
@@ -35,6 +35,19 @@ enum class TConvPolicy : uint32_t
 /** Writes a term conversion policy name to a stream. */
 std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol);
 
+/** A policy for how proofs are cached in TConvProofGenerator */
+enum class TConvCachePolicy : uint32_t
+{
+  // proofs are statically cached
+  STATIC,
+  // proofs are dynamically cached, cleared when a new rewrite is added
+  DYNAMIC,
+  // proofs are never cached
+  NEVER,
+};
+/** Writes a term conversion cache policy name to a stream. */
+std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol);
+
 /**
  * The term conversion proof generator.
  *
@@ -75,17 +88,23 @@ std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol);
 class TConvProofGenerator : public ProofGenerator
 {
  public:
-  /** Constructor
+  /**
+   * Constructor, which notice does fixpoint rewriting (since this is the
+   * most common use case) and never caches.
    *
    * @param pnm The proof node manager for constructing ProofNode objects.
    * @param c The context that this class depends on. If none is provided,
    * this class is context-independent.
    * @param tpol The policy for applying rewrite steps of this class. For
    * details, see d_policy.
+   * @param cpol The caching policy for this generator.
+   * @param name The name of this generator (for debugging).
    */
   TConvProofGenerator(ProofNodeManager* pnm,
                       context::Context* c = nullptr,
-                      TConvPolicy pol = TConvPolicy::FIXPOINT);
+                      TConvPolicy pol = TConvPolicy::FIXPOINT,
+                      TConvCachePolicy cpol = TConvCachePolicy::NEVER,
+                      std::string name = "TConvProofGenerator");
   ~TConvProofGenerator();
   /**
    * Add rewrite step t --> s based on proof generator.
@@ -136,6 +155,12 @@ class TConvProofGenerator : public ProofGenerator
    *   f(a,c) = f(f(c),d) if d_policy is ONCE.
    */
   TConvPolicy d_policy;
+  /** The cache policy */
+  TConvCachePolicy d_cpolicy;
+  /** Name identifier */
+  std::string d_name;
+  /** The cache for terms */
+  std::map<Node, std::shared_ptr<ProofNode> > d_cache;
   /**
    * Adds a proof of t = t' to the proof pf where t' is the result of rewriting
    * t based on the rewrite steps registered to this class. This method then
@@ -147,6 +172,8 @@ class TConvProofGenerator : public ProofGenerator
    * and a rewrite step has not already been registered for t.
    */
   Node registerRewriteStep(Node t, Node s);
+  /** cache that r is the rewritten form of cur, pf can provide a proof */
+  void doCache(Node cur, Node r, LazyCDProof& pf);
 };
 
 }  // namespace CVC4
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index d14a8e1cf..6b5bee6bb 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -183,6 +183,15 @@ header = "options/smt_options.h"
   help       = "check pedantic levels eagerly (during proof rule construction) instead of during final proof construction"
 
 [[option]]
+  name       = "proofNewEagerChecking"
+  category   = "regular"
+  long       = "proof-new-eager-checking"
+  type       = "bool"
+  default    = "false"
+  read_only  = true
+  help       = "check proofs eagerly with proof-new for local debugging"
+
+[[option]]
   name       = "dumpInstantiations"
   category   = "regular"
   long       = "dump-instantiations"
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 3f44e592e..5da190a3d 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -422,13 +422,19 @@ Node RemoveTermFormulas::getAxiomFor(Node n)
   return Node::null();
 }
 
-void RemoveTermFormulas::setProofChecker(ProofChecker* pc)
+void RemoveTermFormulas::setProofNodeManager(ProofNodeManager* pnm)
 {
   if (d_tpg == nullptr)
   {
-    d_pnm.reset(new ProofNodeManager(pc));
-    d_tpg.reset(new TConvProofGenerator(d_pnm.get()));
-    d_lp.reset(new LazyCDProof(d_pnm.get()));
+    d_pnm = pnm;
+    d_tpg.reset(
+        new TConvProofGenerator(d_pnm,
+                                nullptr,
+                                TConvPolicy::FIXPOINT,
+                                TConvCachePolicy::NEVER,
+                                "RemoveTermFormulas::TConvProofGenerator"));
+    d_lp.reset(new LazyCDProof(
+        d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
   }
 }
 
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index d4c22b78b..78d5899d0 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -106,10 +106,10 @@ class RemoveTermFormulas {
   void garbageCollect();
 
   /**
-   * Set proof checker, which signals this class to enable proofs using the
+   * Set proof node manager, which signals this class to enable proofs using the
    * given checker.
    */
-  void setProofChecker(ProofChecker* pc);
+  void setProofNodeManager(ProofNodeManager* pnm);
 
   /**
    * Get axiom for term n. This returns the axiom that this class uses to
@@ -166,7 +166,7 @@ class RemoveTermFormulas {
   static bool hasNestedTermChildren( TNode node );
 
   /** A proof node manager */
-  std::unique_ptr<ProofNodeManager> d_pnm;
+  ProofNodeManager* d_pnm;
   /**
    * A proof generator for the term conversion.
    */
diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp
index 891c0f731..19795119d 100644
--- a/src/smt/witness_form.cpp
+++ b/src/smt/witness_form.cpp
@@ -21,7 +21,12 @@ namespace CVC4 {
 namespace smt {
 
 WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm)
-    : d_tcpg(pnm), d_wintroPf(pnm)
+    : d_tcpg(pnm,
+             nullptr,
+             TConvPolicy::FIXPOINT,
+             TConvCachePolicy::NEVER,
+             "WfGenerator::TConvProofGenerator"),
+      d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof")
 {
 }
 
@@ -89,7 +94,13 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t)
           // (exists ((x T)) (P x))
           // --------------------------- WITNESS_INTRO
           // k = (witness ((x T)) (P x))
-          d_wintroPf.addLazyStep(exists, pg, false, PfRule::WITNESS_AXIOM);
+          d_wintroPf.addLazyStep(
+              exists,
+              pg,
+              true,
+              "WitnessFormGenerator::convertToWitnessForm:witness_axiom",
+              false,
+              PfRule::WITNESS_AXIOM);
           d_wintroPf.addStep(eq, PfRule::WITNESS_INTRO, {exists}, {});
           d_tcpg.addRewriteStep(cur, curw, &d_wintroPf);
         }
diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp
index 9c25fb3e4..09f02708b 100644
--- a/src/theory/eager_proof_generator.cpp
+++ b/src/theory/eager_proof_generator.cpp
@@ -20,8 +20,9 @@ namespace CVC4 {
 namespace theory {
 
 EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm,
-                                         context::Context* c)
-    : d_pnm(pnm), d_proofs(c == nullptr ? &d_context : c)
+                                         context::Context* c,
+                                         std::string name)
+    : d_pnm(pnm), d_name(name), d_proofs(c == nullptr ? &d_context : c)
 {
 }
 
@@ -97,8 +98,7 @@ TrustNode EagerProofGenerator::mkTrustNode(Node n,
                                            const std::vector<Node>& args,
                                            bool isConflict)
 {
-  std::vector<std::shared_ptr<ProofNode>> children;
-  std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, children, args, n);
+  std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, n);
   return mkTrustNode(n, pf, isConflict);
 }
 
@@ -117,9 +117,10 @@ TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f)
 {
   // make the lemma
   Node lem = f.orNode(f.notNode());
-  std::vector<Node> args;
-  return mkTrustNode(lem, PfRule::SPLIT, args, false);
+  return mkTrustNode(lem, PfRule::SPLIT, {f}, false);
 }
 
+std::string EagerProofGenerator::identify() const { return d_name; }
+
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h
index 9a00f3612..226750a91 100644
--- a/src/theory/eager_proof_generator.h
+++ b/src/theory/eager_proof_generator.h
@@ -86,7 +86,9 @@ class EagerProofGenerator : public ProofGenerator
       NodeProofNodeMap;
 
  public:
-  EagerProofGenerator(ProofNodeManager* pnm, context::Context* c = nullptr);
+  EagerProofGenerator(ProofNodeManager* pnm,
+                      context::Context* c = nullptr,
+                      std::string name = "EagerProofGenerator");
   ~EagerProofGenerator() {}
   /** Get the proof for formula f. */
   std::shared_ptr<ProofNode> getProofFor(Node f) override;
@@ -152,7 +154,7 @@ class EagerProofGenerator : public ProofGenerator
   TrustNode mkTrustNodeSplit(Node f);
   //--------------------------------------- end common proofs
   /** identify */
-  std::string identify() const override { return "EagerProofGenerator"; }
+  std::string identify() const override;
 
  protected:
   /** Set that pf is the proof for conflict conf */
@@ -163,6 +165,8 @@ class EagerProofGenerator : public ProofGenerator
   void setProofForPropExp(TNode lit, Node exp, std::shared_ptr<ProofNode> pf);
   /** The proof node manager */
   ProofNodeManager* d_pnm;
+  /** Name identifier */
+  std::string d_name;
   /** A dummy context used by this class if none is provided */
   context::Context d_context;
   /**