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

1 files changed, 29 insertions, 2 deletions

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