(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, 7 insertions, 6 deletions

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