(proof-new) Updates to lazy proof chain (#5317)

Support for a default proof generator, which is optionally not called recursively.

This is required for preprocessing.

diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index c9fed5434afb69bc1401473df9c0201ae13af0f4..5c096767bf993ef10d0e93fde1eb879f876b37b8 100644 (file)
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -22,8 +22,15 @@ namespace CVC4 {
 
 LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm,
                                    bool cyclic,
-                                   context::Context* c)
-    : d_manager(pnm), d_cyclic(cyclic), d_context(), d_gens(c ? c : &d_context)
+                                   context::Context* c,
+                                   ProofGenerator* defGen,
+                                   bool defRec)
+    : d_manager(pnm),
+      d_cyclic(cyclic),
+      d_defRec(defRec),
+      d_context(),
+      d_gens(c ? c : &d_context),
+      d_defGen(defGen)
 {
 }
 
@@ -72,8 +79,9 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
     {
       Trace("lazy-cdproofchain")
           << "LazyCDProofChain::getProofFor: check " << cur << "\n";
-      ProofGenerator* pg = getGeneratorFor(cur);
       Assert(toConnect.find(cur) == toConnect.end());
+      bool rec = true;
+      ProofGenerator* pg = getGeneratorForInternal(cur, rec);
       if (!pg)
       {
         Trace("lazy-cdproofchain")
@@ -87,6 +95,21 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
           << "LazyCDProofChain::getProofFor: Call generator " << pg->identify()
           << " for chain link " << cur << "\n";
       std::shared_ptr<ProofNode> curPfn = pg->getProofFor(cur);
+      if (curPfn == nullptr)
+      {
+        Trace("lazy-cdproofchain")
+            << "LazyCDProofChain::getProofFor: No proof found, skip\n";
+        visited[cur] = true;
+        continue;
+      }
+      // map node whose proof node must be expanded to the respective poof node
+      toConnect[cur] = curPfn;
+      if (!rec)
+      {
+        // we don't want to recursively connect this proof
+        visited[cur] = true;
+        continue;
+      }
       Trace("lazy-cdproofchain-debug")
           << "LazyCDProofChain::getProofFor: stored proof: " << *curPfn.get()
           << "\n";
@@ -103,8 +126,6 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
               << "LazyCDProofChain::getProofFor:  - " << fap.first << "\n";
         }
       }
-      // map node whose proof node must be expanded to the respective poof node
-      toConnect[cur] = curPfn;
       // mark for post-traversal if we are controlling cycles
       if (d_cyclic)
       {
@@ -198,6 +219,7 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
       Assert(npfn.first == fact);
       continue;
     }
+    Assert(npfn.second);
     Trace("lazy-cdproofchain")
         << "LazyCDProofChain::getProofFor: expand assumption " << npfn.first
         << "\n";
@@ -269,12 +291,24 @@ bool LazyCDProofChain::hasGenerator(Node fact) const
 }
 
 ProofGenerator* LazyCDProofChain::getGeneratorFor(Node fact)
+{
+  bool rec = true;
+  return getGeneratorForInternal(fact, rec);
+}
+
+ProofGenerator* LazyCDProofChain::getGeneratorForInternal(Node fact, bool& rec)
 {
   auto it = d_gens.find(fact);
   if (it != d_gens.end())
   {
     return (*it).second;
   }
+  // otherwise, if no explicit generators, we use the default one
+  if (d_defGen != nullptr)
+  {
+    rec = d_defRec;
+    return d_defGen;
+  }
   return nullptr;
 }
 

diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
index a58cc5c7d96c9f0bff7905f9d0232a2bef18b3ff..28de3cea0d47b950914972eb4b309f80749ce369 100644 (file)
--- a/src/expr/lazy_proof_chain.h
+++ b/src/expr/lazy_proof_chain.h
@@ -41,13 +41,18 @@ class LazyCDProofChain : public ProofGenerator
   /** Constructor
    *
    * @param pnm The proof node manager for constructing ProofNode objects.
-   * @param cyclic Whether this instance is robust to cycles in the cahin.
+   * @param cyclic Whether this instance is robust to cycles in the chain.
    * @param c The context that this class depends on. If none is provided,
    * this class is context-independent.
+   * @param defGen The default generator to be used if no generator exists
+   * for a step.
+   * @param defRec Whether this instance expands proofs from defGen recursively.
    */
   LazyCDProofChain(ProofNodeManager* pnm,
                    bool cyclic = true,
-                   context::Context* c = nullptr);
+                   context::Context* c = nullptr,
+                   ProofGenerator* defGen = nullptr,
+                   bool defRec = true);
   ~LazyCDProofChain();
   /**
    * Get lazy proof for fact, or nullptr if it does not exist, by connecting the
@@ -124,14 +129,23 @@ class LazyCDProofChain : public ProofGenerator
   const std::map<Node, std::shared_ptr<ProofNode>> getLinks() const;
 
  private:
+  /**
+   * Get generator for fact, or nullptr if it doesnt exist. Updates rec to
+   * true if we should recurse on its proof.
+   */
+  ProofGenerator* getGeneratorForInternal(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. */
   bool d_cyclic;
+  /** Whether we expand recursively (for the default generator) */
+  bool d_defRec;
   /** A dummy context used by this class if none is provided */
   context::Context d_context;
   /** Maps facts that can be proven to generators */
   context::CDHashMap<Node, ProofGenerator*, NodeHashFunction> d_gens;
+  /** The default proof generator (if one exists) */
+  ProofGenerator* d_defGen;
 };
 
 }  // namespace CVC4