[proof-new] Adds Lazy CDProof chain data-structure (#5060)

A proof generator to facilitate connection of locally independent but globally dependent proofs. In particular this will be used to model the resolution chains done in Minisat.

6 files changed, 401 insertions, 19 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 3e3b569af..7fa8b12e7 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -17,6 +17,8 @@ libcvc4_add_sources(
   kind_map.h
   lazy_proof.cpp
   lazy_proof.h
+  lazy_proof_chain.cpp
+  lazy_proof_chain.h
   match_trie.cpp
   match_trie.h
   node.cpp
diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
new file mode 100644
index 000000000..a01d541eb
--- /dev/null
+++ b/src/expr/lazy_proof_chain.cpp
@@ -0,0 +1,239 @@
+/*********************                                                        */
+/*! \file lazy_proof_chain.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of lazy proof utility
+ **/
+
+#include "expr/lazy_proof_chain.h"
+
+#include "expr/proof.h"
+#include "expr/proof_node_algorithm.h"
+#include "options/smt_options.h"
+
+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)
+{
+}
+
+LazyCDProofChain::~LazyCDProofChain() {}
+
+std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
+{
+  Trace("lazy-cdproofchain")
+      << "LazyCDProofChain::getProofFor " << fact << "\n";
+  // which facts have had proofs retrieved for. This is maintained to avoid
+  // cycles. It also saves the proof node of the fact
+  std::unordered_map<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
+      toConnect;
+  // leaves of proof node links in the chain, i.e. assumptions, yet to be
+  // expanded
+  std::unordered_map<Node,
+                     std::vector<std::shared_ptr<ProofNode>>,
+                     NodeHashFunction>
+      assumptionsToExpand;
+  // invariant of the loop below, the first iteration notwhistanding:
+  //   visit = domain(assumptionsToExpand) \ domain(toConnect)
+  std::vector<Node> visit{fact};
+  std::unordered_map<Node, bool, NodeHashFunction> visited;
+  Node cur;
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    auto itVisited = visited.find(cur);
+    // pre-traversal
+    if (itVisited == visited.end())
+    {
+      Trace("lazy-cdproofchain")
+          << "LazyCDProofChain::getProofFor: check " << cur << "\n";
+      ProofGenerator* pg = getGeneratorFor(cur);
+      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);
+      Trace("lazy-cdproofchain-debug")
+          << "LazyCDProofChain::getProofFor: stored proof: " << *curPfn.get()
+          << "\n";
+      // retrieve free assumptions and their respective proof nodes
+      std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
+      expr::getFreeAssumptionsMap(curPfn, famap);
+      if (Trace.isOn("lazy-cdproofchain"))
+      {
+        Trace("lazy-cdproofchain")
+            << "LazyCDProofChain::getProofFor: free assumptions:\n";
+        for (auto fap : famap)
+        {
+          Trace("lazy-cdproofchain")
+              << "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)
+      {
+        visit.push_back(cur);
+        visited[cur] = false;
+        Trace("lazy-cdproofchain") << push;
+        Trace("lazy-cdproofchain-debug") << push;
+      }
+      else
+      {
+        visited[cur] = true;
+      }
+      // enqueue free assumptions to process
+      for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
+               fap : famap)
+      {
+        // check cycles, which are cases in which the assumption has already
+        // been marked to be connected but we have not finished processing the
+        // nodes it depends on
+        if (d_cyclic && toConnect.find(fap.first) != toConnect.end()
+            && std::find(visit.begin(), visit.end(), fap.first) != visit.end())
+        {
+          // Since we have a cycle with an assumption, this fact will be an
+          // assumption in the final proof node produced by this method. This we
+          // mark the proof node it results on, i.e. its value in the toConnect
+          // map, as an assumption proof node. Note that we don't assign
+          // visited[fap.first] to true so that we properly pop the traces
+          // previously pushed.
+          Trace("lazy-cdproofchain")
+              << "LazyCDProofChain::getProofFor: removing cyclic assumption "
+              << fap.first << " from expansion\n";
+          toConnect[fap.first] = fap.second[0];
+          continue;
+        }
+        // only process further the assumptions not already in the map
+        auto it = assumptionsToExpand.find(fap.first);
+        if (it == assumptionsToExpand.end())
+        {
+          visit.push_back(fap.first);
+        }
+        // add assumption proof nodes to be updated
+        assumptionsToExpand[fap.first].insert(
+            assumptionsToExpand[fap.first].end(),
+            fap.second.begin(),
+            fap.second.end());
+      }
+    }
+    else if (!itVisited->second)
+    {
+      visited[cur] = true;
+      Trace("lazy-cdproofchain") << pop;
+      Trace("lazy-cdproofchain-debug") << pop;
+    }
+  } while (!visit.empty());
+  // expand all assumptions marked to be connected
+  for (const std::pair<const Node, std::shared_ptr<ProofNode>>& npfn :
+       toConnect)
+  {
+    auto it = assumptionsToExpand.find(npfn.first);
+    if (it == assumptionsToExpand.end())
+    {
+      Assert(npfn.first == fact);
+      continue;
+    }
+    Trace("lazy-cdproofchain")
+        << "LazyCDProofChain::getProofFor: expand assumption " << npfn.first
+        << "\n";
+    Trace("lazy-cdproofchain-debug")
+        << "LazyCDProofChain::getProofFor: ...expand to " << *npfn.second.get()
+        << "\n";
+    // update each assumption proof node
+    for (std::shared_ptr<ProofNode> pfn : it->second)
+    {
+      d_manager->updateNode(pfn.get(), npfn.second.get());
+    }
+  }
+  // final proof of fact
+  auto it = toConnect.find(fact);
+  if (it == toConnect.end())
+  {
+    return nullptr;
+  }
+  return it->second;
+}
+
+void LazyCDProofChain::addLazyStep(Node expected, ProofGenerator* pg)
+{
+  Assert(pg != nullptr);
+  Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
+                             << " set to generator " << pg->identify() << "\n";
+  // note this will replace the generator for expected, if any
+  d_gens.insert(expected, pg);
+}
+
+void LazyCDProofChain::addLazyStep(Node expected,
+                                   ProofGenerator* pg,
+                                   const std::vector<Node>& assumptions,
+                                   const char* ctx)
+{
+  Assert(pg != nullptr);
+  Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
+                             << " set to generator " << pg->identify() << "\n";
+  // note this will rewrite the generator for expected, if any
+  d_gens.insert(expected, pg);
+  // check if chain is closed if options::proofNewEagerChecking() is on
+  if (options::proofNewEagerChecking())
+  {
+    Trace("lazy-cdproofchain")
+        << "LazyCDProofChain::addLazyStep: Checking closed proof...\n";
+    std::shared_ptr<ProofNode> pfn = pg->getProofFor(expected);
+    std::vector<Node> allowedLeaves{assumptions.begin(), assumptions.end()};
+    // add all current links in the chain
+    for (const std::pair<const Node, ProofGenerator*>& link : d_gens)
+    {
+      allowedLeaves.push_back(link.first);
+    }
+    if (Trace.isOn("lazy-cdproofchain"))
+    {
+      Trace("lazy-cdproofchain") << "Checking relative to leaves...\n";
+      for (const Node& n : allowedLeaves)
+      {
+        Trace("lazy-cdproofchain") << "  - " << n << "\n";
+      }
+      Trace("lazy-cdproofchain") << "\n";
+    }
+    pfnEnsureClosedWrt(pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx);
+  }
+}
+
+bool LazyCDProofChain::hasGenerator(Node fact) const
+{
+  return d_gens.find(fact) != d_gens.end();
+}
+
+ProofGenerator* LazyCDProofChain::getGeneratorFor(Node fact)
+{
+  auto it = d_gens.find(fact);
+  if (it != d_gens.end())
+  {
+    return (*it).second;
+  }
+  return nullptr;
+}
+
+std::string LazyCDProofChain::identify() const { return "LazyCDProofChain"; }
+
+}  // namespace CVC4
diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
new file mode 100644
index 000000000..7fa49bccc
--- /dev/null
+++ b/src/expr/lazy_proof_chain.h
@@ -0,0 +1,135 @@
+/*********************                                                        */
+/*! \file lazy_proof_chain.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Lazy proof chain utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__LAZY_PROOF_CHAIN_H
+#define CVC4__EXPR__LAZY_PROOF_CHAIN_H
+
+#include <unordered_map>
+#include <vector>
+
+#include "context/cdhashmap.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+
+namespace CVC4 {
+
+/**
+ * A (context-dependent) lazy generator for proof chains. This class is an
+ * extension of ProofGenerator that additionally that maps facts to proof
+ * generators in a context-dependent manner. The map is built with the addition
+ * of lazy steps mapping facts to proof generators. More importantly, its
+ * getProofFor method expands the proof generators registered to this class by
+ * 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
+{
+ public:
+  /** Constructor
+   *
+   * @param pnm The proof node manager for constructing ProofNode objects.
+   * @param cyclic Whether this instance is robust to cycles in the cahin.
+   * @param c The context that this class depends on. If none is provided,
+   * this class is context-independent.
+   */
+  LazyCDProofChain(ProofNodeManager* pnm,
+                   bool cyclic = true,
+                   context::Context* c = nullptr);
+  ~LazyCDProofChain();
+  /**
+   * Get lazy proof for fact, or nullptr if it does not exist, by connecting the
+   * proof nodes generated for each intermediate relevant fact registered in the
+   * chain (i.e., in the domain of d_gens).
+   *
+   * For example, if d_gens consists of the following pairs
+   *
+   * --- (A, PG1)
+   * --- (B, PG2)
+   * --- (C, PG3)
+   *
+   * and getProofFor(A) is called, with PG1 generating a proof with assumptions
+   * B and D, then B is expanded, with its assumption proof node being updated
+   * to the expanded proof node, while D is not. Assuming PG2 provides a proof
+   * with assumptions C and E, then C is expanded and E is not. Suppose PG3
+   * gives a closed proof, thus the call getProofFor(A) produces a proof node
+   *
+   *  A : ( ... B : ( ... C : (...), ... ASSUME( E ) ), ... ASSUME( D ) )
+   *
+   * Note that the expansions are done directly on the proof nodes produced by
+   * the generators.
+   *
+   * If this instance has been set to be robust to cyclic proofs (i.e., d_cyclic
+   * is true), then the construction of the proof chain checks that there are no
+   * cycles, i.e., a given fact would have itself as an assumption when
+   * connecting the chain links. If such a cycle were to be detected then the
+   * fact will be marked as an assumption and not expanded in the final proof
+   * node. The method does not fail.
+   */
+  std::shared_ptr<ProofNode> getProofFor(Node fact) override;
+  /** Add step by generator
+   *
+   * This method stores that expected can be proven by proof generator pg if
+   * 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).
+   *
+   * 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
+   *  (1) a fixed set F1, ..., Fn,
+   *  (2) formulas in the current domain of d_gens.
+   *
+   * This is so that we only add links to the chain that depend on a fixed set
+   * of assumptions or in other links.
+   *
+   * @param expected The fact that can be proven.
+   * @param pg The generator that can proof expected.
+   * @param assumptions The fixed set of assumptions with relation to which the
+   * chain, now augmented with expect, must be closed.
+   * @param ctx The context we are in (for debugging).
+   */
+  void addLazyStep(Node expected,
+                   ProofGenerator* pg,
+                   const std::vector<Node>& assumptions,
+                   const char* ctx = "LazyCDProofChain::addLazyStep");
+
+  /** As above but does not do the closedness check. */
+  void addLazyStep(Node expected, ProofGenerator* pg);
+
+  /** Does the given fact have an explicitly provided generator? */
+  bool hasGenerator(Node fact) const;
+
+  /**
+   * Get generator for fact, or nullptr if it doesnt exist.
+   */
+  ProofGenerator* getGeneratorFor(Node fact);
+
+  /** identify */
+  std::string identify() const override;
+
+ private:
+  /** 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;
+  /** 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;
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__LAZY_PROOF_CHAIN_H */
diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp
index 9e1018024..984379d54 100644
--- a/src/expr/proof_node_algorithm.cpp
+++ b/src/expr/proof_node_algorithm.cpp
@@ -19,22 +19,26 @@ namespace expr {
 
 void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump)
 {
-  std::map<Node, std::vector<ProofNode*>> amap;
-  getFreeAssumptionsMap(pn, amap);
-  for (const std::pair<const Node, std::vector<ProofNode*>>& p : amap)
+  std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap;
+  std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>(
+      pn->getRule(), pn->getChildren(), pn->getArguments());
+  getFreeAssumptionsMap(spn, amap);
+  for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p :
+       amap)
   {
     assump.push_back(p.first);
   }
 }
 
-void getFreeAssumptionsMap(ProofNode* pn,
-                           std::map<Node, std::vector<ProofNode*>>& amap)
+void getFreeAssumptionsMap(
+    std::shared_ptr<ProofNode> pn,
+    std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap)
 {
   // proof should not be cyclic
   // visited set false after preorder traversal, true after postorder traversal
   std::unordered_map<ProofNode*, bool> visited;
   std::unordered_map<ProofNode*, bool>::iterator it;
-  std::vector<ProofNode*> visit;
+  std::vector<std::shared_ptr<ProofNode>> visit;
   // Maps a bound assumption to the number of bindings it is under
   // e.g. in (SCOPE (SCOPE (ASSUME x) (x y)) (y)), y would be mapped to 2 at
   // (ASSUME x), and x would be mapped to 1.
@@ -54,17 +58,17 @@ void getFreeAssumptionsMap(ProofNode* pn,
   //   after postvisiting SCOPE2: {}
   //
   std::unordered_map<Node, uint32_t, NodeHashFunction> scopeDepth;
-  ProofNode* cur;
+  std::shared_ptr<ProofNode> cur;
   visit.push_back(pn);
   do
   {
     cur = visit.back();
     visit.pop_back();
-    it = visited.find(cur);
+    it = visited.find(cur.get());
     const std::vector<Node>& cargs = cur->getArguments();
     if (it == visited.end())
     {
-      visited[cur] = true;
+      visited[cur.get()] = true;
       PfRule id = cur->getRule();
       if (id == PfRule::ASSUME)
       {
@@ -85,7 +89,7 @@ void getFreeAssumptionsMap(ProofNode* pn,
             scopeDepth[a] += 1;
           }
           // will need to unbind the variables below
-          visited[cur] = false;
+          visited[cur.get()] = false;
           visit.push_back(cur);
         }
         // The following loop cannot be merged with the loop above because the
@@ -93,13 +97,13 @@ void getFreeAssumptionsMap(ProofNode* pn,
         const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
         for (const std::shared_ptr<ProofNode>& cp : cs)
         {
-          visit.push_back(cp.get());
+          visit.push_back(cp);
         }
       }
     }
     else if (!it->second)
     {
-      visited[cur] = true;
+      visited[cur.get()] = true;
       Assert(cur->getRule() == PfRule::SCOPE);
       // unbind its assumptions
       for (const Node& a : cargs)
diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h
index bc44d7314..aec098e17 100644
--- a/src/expr/proof_node_algorithm.h
+++ b/src/expr/proof_node_algorithm.h
@@ -49,8 +49,9 @@ void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump);
  * @param amap The mapping to add the free asumptions of pn and their
  * corresponding proof nodes to.
  */
-void getFreeAssumptionsMap(ProofNode* pn,
-                           std::map<Node, std::vector<ProofNode*>>& amap);
+void getFreeAssumptionsMap(
+    std::shared_ptr<ProofNode> pn,
+    std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap);
 
 }  // namespace expr
 }  // namespace CVC4
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index 0d13531a5..54315ee05 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -75,10 +75,11 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
   bool computedAcr = false;
 
   // The free assumptions of the proof
-  std::map<Node, std::vector<ProofNode*>> famap;
-  expr::getFreeAssumptionsMap(pf.get(), famap);
+  std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
+  expr::getFreeAssumptionsMap(pf, famap);
   std::unordered_set<Node, NodeHashFunction> acu;
-  for (const std::pair<const Node, std::vector<ProofNode*>>& fa : famap)
+  for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
+           fa : famap)
   {
     Node a = fa.first;
     if (ac.find(a) != ac.end())
@@ -135,10 +136,10 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
       children.push_back(pfaa);
       std::vector<Node> args;
       args.push_back(a);
-      for (ProofNode* pfs : fa.second)
+      for (std::shared_ptr<ProofNode> pfs : fa.second)
       {
         Assert(pfs->getResult() == a);
-        updateNode(pfs, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+        updateNode(pfs.get(), PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
       }
       Trace("pnm-scope") << "...finished" << std::endl;
       acu.insert(aMatch);