From 029e5378cef6a0432c25ebaab044a69440d398cc Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 7 Jun 2021 09:09:59 -0500
Subject: [PATCH] (proof-new) Lazy proof chain debug names (#6680)

---
 src/proof/lazy_proof.cpp                   | 2 +-
 src/proof/lazy_proof.h                     | 2 +-
 src/proof/lazy_proof_chain.cpp             | 8 +++++---
 src/proof/lazy_proof_chain.h               | 5 ++++-
 src/proof/proof.cpp                        | 2 +-
 src/proof/proof.h                          | 2 +-
 src/theory/booleans/circuit_propagator.cpp | 8 ++++----
 7 files changed, 17 insertions(+), 12 deletions(-)

diff --git a/src/proof/lazy_proof.cpp b/src/proof/lazy_proof.cpp
index d7b62a8dc..b16a8d758 100644
--- a/src/proof/lazy_proof.cpp
+++ b/src/proof/lazy_proof.cpp
@@ -26,7 +26,7 @@ namespace cvc5 {
 LazyCDProof::LazyCDProof(ProofNodeManager* pnm,
                          ProofGenerator* dpg,
                          context::Context* c,
-                         std::string name)
+                         const std::string& name)
     : CDProof(pnm, c, name), d_gens(c ? c : &d_context), d_defaultGen(dpg)
 {
 }
diff --git a/src/proof/lazy_proof.h b/src/proof/lazy_proof.h
index b566e408e..bf5bc229c 100644
--- a/src/proof/lazy_proof.h
+++ b/src/proof/lazy_proof.h
@@ -45,7 +45,7 @@ class LazyCDProof : public CDProof
   LazyCDProof(ProofNodeManager* pnm,
               ProofGenerator* dpg = nullptr,
               context::Context* c = nullptr,
-              std::string name = "LazyCDProof");
+              const std::string& name = "LazyCDProof");
   ~LazyCDProof();
   /**
    * Get lazy proof for fact, or nullptr if it does not exist. This may
diff --git a/src/proof/lazy_proof_chain.cpp b/src/proof/lazy_proof_chain.cpp
index 4c1b19ffe..c835ca03d 100644
--- a/src/proof/lazy_proof_chain.cpp
+++ b/src/proof/lazy_proof_chain.cpp
@@ -28,13 +28,15 @@ LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm,
                                    bool cyclic,
                                    context::Context* c,
                                    ProofGenerator* defGen,
-                                   bool defRec)
+                                   bool defRec,
+                                   const std::string& name)
     : d_manager(pnm),
       d_cyclic(cyclic),
       d_defRec(defRec),
       d_context(),
       d_gens(c ? c : &d_context),
-      d_defGen(defGen)
+      d_defGen(defGen),
+      d_name(name)
 {
 }
 
@@ -322,6 +324,6 @@ ProofGenerator* LazyCDProofChain::getGeneratorForInternal(Node fact, bool& rec)
   return nullptr;
 }
 
-std::string LazyCDProofChain::identify() const { return "LazyCDProofChain"; }
+std::string LazyCDProofChain::identify() const { return d_name; }
 
 }  // namespace cvc5
diff --git a/src/proof/lazy_proof_chain.h b/src/proof/lazy_proof_chain.h
index 4315ee87a..d15b8f9e2 100644
--- a/src/proof/lazy_proof_chain.h
+++ b/src/proof/lazy_proof_chain.h
@@ -53,7 +53,8 @@ class LazyCDProofChain : public ProofGenerator
                    bool cyclic = true,
                    context::Context* c = nullptr,
                    ProofGenerator* defGen = nullptr,
-                   bool defRec = true);
+                   bool defRec = true,
+                   const std::string& name = "LazyCDProofChain");
   ~LazyCDProofChain();
   /**
    * Get lazy proof for fact, or nullptr if it does not exist, by connecting the
@@ -147,6 +148,8 @@ class LazyCDProofChain : public ProofGenerator
   context::CDHashMap<Node, ProofGenerator*> d_gens;
   /** The default proof generator (if one exists) */
   ProofGenerator* d_defGen;
+  /** Name (for debugging) */
+  std::string d_name;
 };
 
 }  // namespace cvc5
diff --git a/src/proof/proof.cpp b/src/proof/proof.cpp
index a100be990..79f84135d 100644
--- a/src/proof/proof.cpp
+++ b/src/proof/proof.cpp
@@ -25,7 +25,7 @@ namespace cvc5 {
 
 CDProof::CDProof(ProofNodeManager* pnm,
                  context::Context* c,
-                 std::string name,
+                 const std::string& name,
                  bool autoSymm)
     : d_manager(pnm),
       d_context(),
diff --git a/src/proof/proof.h b/src/proof/proof.h
index 2c57e0a2e..7d8fa4155 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -144,7 +144,7 @@ class CDProof : public ProofGenerator
    */
   CDProof(ProofNodeManager* pnm,
           context::Context* c = nullptr,
-          std::string name = "CDProof",
+          const std::string& name = "CDProof",
           bool autoSymm = true);
   virtual ~CDProof();
   /**
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 2fa2890c2..9e53e24dd 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -777,15 +777,15 @@ void CircuitPropagator::setProof(ProofNodeManager* pnm,
 {
   d_pnm = pnm;
   d_epg.reset(new EagerProofGenerator(pnm, ctx));
-  d_proofInternal.reset(
-      new LazyCDProofChain(pnm, true, ctx, d_epg.get(), true));
+  d_proofInternal.reset(new LazyCDProofChain(
+      pnm, true, ctx, d_epg.get(), true, "CircuitPropInternalLazyChain"));
   if (defParent != nullptr)
   {
     // If we provide a parent proof generator (defParent), we want the ASSUME
     // leafs of proofs provided by this class to call the getProofFor method on
     // the parent. To do this, we use a LazyCDProofChain.
-    d_proofExternal.reset(
-        new LazyCDProofChain(pnm, true, ctx, defParent, false));
+    d_proofExternal.reset(new LazyCDProofChain(
+        pnm, true, ctx, defParent, false, "CircuitPropExternalLazyChain"));
   }
 }
 
-- 
2.30.2