From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Fri, 10 Dec 2021 15:39:43 +0000 (-0300)
Subject: [proofs] Make LazyCDProofChain extend CDProof (#7726)
X-Git-Tag: cvc5-1.0.0~689
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cf5e9c06eb649e77996a0da20ca0b492a6f64e4d;p=cvc5.git

[proofs] Make LazyCDProofChain extend CDProof (#7726)

This commit makes LazyCDProofChain behave more similarly to LazyCDProof, in that it is an object that not only builds a proof to a fact based on lazy steps but also on regular steps that may already have for it.

The motivation for this commit is the upcoming handling of context-dependent proofs in incremental mode, which benefits from a more uniform behavior between CDProof, LazyCDProof and LazyCDProofChain (with the latter two both extending CDProof).
---

diff --git a/src/proof/lazy_proof_chain.cpp b/src/proof/lazy_proof_chain.cpp
index 0de5673ab..3280626ad 100644
--- a/src/proof/lazy_proof_chain.cpp
+++ b/src/proof/lazy_proof_chain.cpp
@@ -30,7 +30,8 @@ LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm,
                                    ProofGenerator* defGen,
                                    bool defRec,
                                    const std::string& name)
-    : d_manager(pnm),
+    : CDProof(pnm, c, name, false),
+      d_manager(pnm),
       d_cyclic(cyclic),
       d_defRec(defRec),
       d_context(),
@@ -85,21 +86,10 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
       Trace("lazy-cdproofchain")
           << "LazyCDProofChain::getProofFor: check " << cur << "\n";
       Assert(toConnect.find(cur) == toConnect.end());
+      // The current fact may be justified by concrete steps added to this
+      // proof, in which case we do not use the generators.
       bool rec = true;
-      ProofGenerator* pg = getGeneratorForInternal(cur, rec);
-      if (!pg)
-      {
-        Trace("lazy-cdproofchain")
-            << "LazyCDProofChain::getProofFor: nothing to do\n";
-        // nothing to do for this fact, it'll be a leaf in the final proof
-        // node, don't post-traverse.
-        visited[cur] = true;
-        continue;
-      }
-      Trace("lazy-cdproofchain")
-          << "LazyCDProofChain::getProofFor: Call generator " << pg->identify()
-          << " for chain link " << cur << "\n";
-      std::shared_ptr<ProofNode> curPfn = pg->getProofFor(cur);
+      std::shared_ptr<ProofNode> curPfn = getProofForInternal(cur, rec);
       if (curPfn == nullptr)
       {
         Trace("lazy-cdproofchain")
@@ -107,7 +97,8 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
         visited[cur] = true;
         continue;
       }
-      // map node whose proof node must be expanded to the respective poof node
+      // map node whose proof node must be expanded to the respective poof
+      // node
       toConnect[cur] = curPfn;
       // We may not want to recursively connect this proof so we skip.
       if (!rec)
@@ -368,6 +359,27 @@ ProofGenerator* LazyCDProofChain::getGeneratorForInternal(Node fact, bool& rec)
   return nullptr;
 }
 
+std::shared_ptr<ProofNode> LazyCDProofChain::getProofForInternal(Node fact,
+                                                                 bool& rec)
+{
+  std::shared_ptr<ProofNode> pfn = CDProof::getProofFor(fact);
+  Assert(pfn != nullptr);
+  // If concrete proof, save it, otherwise try generators.
+  if (pfn->getRule() != PfRule::ASSUME)
+  {
+    return pfn;
+  }
+  ProofGenerator* pg = getGeneratorForInternal(fact, rec);
+  if (!pg)
+  {
+    return nullptr;
+  }
+  Trace("lazy-cdproofchain")
+      << "LazyCDProofChain::getProofFor: Call generator " << pg->identify()
+      << " for chain link " << fact << "\n";
+  return pg->getProofFor(fact);
+}
+
 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 d15b8f9e2..114e2310e 100644
--- a/src/proof/lazy_proof_chain.h
+++ b/src/proof/lazy_proof_chain.h
@@ -20,8 +20,7 @@
 
 #include <vector>
 
-#include "context/cdhashmap.h"
-#include "proof/proof_generator.h"
+#include "proof/proof.h"
 
 namespace cvc5 {
 
@@ -36,7 +35,7 @@ class ProofNodeManager;
  * connecting, for the proof generated to one fact, assumptions to the proofs
  * generated for those assumptinos that are registered in the chain.
  */
-class LazyCDProofChain : public ProofGenerator
+class LazyCDProofChain : public CDProof
 {
  public:
   /** Constructor
@@ -92,6 +91,11 @@ class LazyCDProofChain : public ProofGenerator
    * it is required to do so. This mapping is maintained in the remainder of
    * the current context (according to the context c provided to this class).
    *
+   * It is important to note that pg is asked to provide a proof for expected
+   * only when no other call for the fact expected is provided via the addStep
+   * method of this class. In particular, pg is asked to prove expected when it
+   * appears as the conclusion of an ASSUME leaf within CDProof::getProofFor.
+   *
    * Moreover the lazy steps of this class are expected to fulfill the
    * requirement that pg.getProofFor(expected) generates a proof node closed
    * with relation to
@@ -136,6 +140,14 @@ class LazyCDProofChain : public ProofGenerator
    * true if we should recurse on its proof.
    */
   ProofGenerator* getGeneratorForInternal(Node fact, bool& rec);
+  /**
+   * Get internal proof for fact from the underlying CDProof, if any, otherwise
+   * via a call to the above method.
+   *
+   * Returns a nullptr when no internal proof stored.
+   */
+  std::shared_ptr<ProofNode> getProofForInternal(Node fact, bool& rec);
+
   /** The proof manager, used for allocating new ProofNode objects */
   ProofNodeManager* d_manager;
   /** Whether this instance is robust to cycles in the chain. */