(proof-new) Lazy proof chain debug names (#6680)

diff --git a/src/proof/lazy_proof.cpp b/src/proof/lazy_proof.cpp
index d7b62a8dce4c3366a7d4a3879f9467988af93d63..b16a8d758f493d9df933a1c9a70fc3b089bb8ecb 100644 (file)
--- 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 b566e408ee04dd4d1ce5eb2f199a91f87580a3b2..bf5bc229cc629aed7e8aad1ca9b4ef2db87eb144 100644 (file)
--- 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 4c1b19ffe27b50f579edf7a4486c09f6df385ed2..c835ca03d2b8c94d813b96a736534d2ccfdc7d6b 100644 (file)
--- 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 4315ee87a374d0345001b8ac2d1ef5cc244b2b23..d15b8f9e2a1db947d9b1209a9aa9f6e1aeb34ba4 100644 (file)
--- 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 a100be9900f813cac02d758539542dd5db5e2123..79f84135d83191cfc237b2d05cb60ffd2dc3d864 100644 (file)
--- 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 2c57e0a2ede6b99aad4ef6a5daf58948db7d0dba..7d8fa4155086eb7cf2f9dfe71c450b2c165c601b 100644 (file)
--- 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 2fa2890c2b34abdd0edd3f7cf36aad80e0b99fe8..9e53e24dd3f988fbd9ba06d6d3fd60a2ba3abf6c 100644 (file)
--- 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"));
   }
 }