(proof-new) Update proof node, add proof node algorithm utility file. (#4600)

Moves get free assumptions to a proof_node_algorithm.h/cpp file, analogous to node_algorithm.h/cpp. Adds a more general form of it, getFreeAssumptionsMap, which is required for future method ProofNodeManager::mkScope.

5 files changed, 229 insertions, 84 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 00eeaecea..5173c076d 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -47,6 +47,8 @@ libcvc4_add_sources(
   proof_generator.h
   proof_node.cpp
   proof_node.h
+  proof_node_algorithm.cpp
+  proof_node_algorithm.h
   proof_node_to_sexpr.cpp
   proof_node_to_sexpr.h
   proof_node_manager.cpp
diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp
index b5e391049..6ef31b903 100644
--- a/src/expr/proof_node.cpp
+++ b/src/expr/proof_node.cpp
@@ -14,6 +14,9 @@
 
 #include "expr/proof_node.h"
 
+#include "expr/proof_node_algorithm.h"
+#include "expr/proof_node_to_sexpr.h"
+
 namespace CVC4 {
 
 ProofNode::ProofNode(PfRule id,
@@ -34,71 +37,24 @@ const std::vector<Node>& ProofNode::getArguments() const { return d_args; }
 
 Node ProofNode::getResult() const { return d_proven; }
 
-void ProofNode::getFreeAssumptions(std::vector<Node>& assump) const
+bool ProofNode::isClosed()
 {
-  // visited set false after preorder traversal, true after postorder traversal
-  std::unordered_map<const ProofNode*, bool> visited;
-  std::unordered_map<const ProofNode*, bool>::iterator it;
-  std::vector<const ProofNode*> visit;
-  // the current set of formulas bound by SCOPE
-  std::unordered_set<Node, NodeHashFunction> currentScope;
-  const ProofNode* cur;
-  visit.push_back(this);
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    it = visited.find(cur);
-    if (it == visited.end())
-    {
-      visited[cur] = true;
-      PfRule id = cur->getRule();
-      if (id == PfRule::ASSUME)
-      {
-        Assert(cur->d_args.size() == 1);
-        Node f = cur->d_args[0];
-        if (currentScope.find(f) == currentScope.end())
-        {
-          assump.push_back(f);
-        }
-      }
-      else
-      {
-        if (id == PfRule::SCOPE)
-        {
-          // mark that its arguments are bound in the current scope
-          for (const Node& a : cur->d_args)
-          {
-            // should not have assumption shadowing
-            Assert(currentScope.find(a) != currentScope.end());
-            currentScope.insert(a);
-          }
-          // will need to unbind the variables below
-          visited[cur] = false;
-        }
-        for (const std::shared_ptr<ProofNode>& cp : cur->d_children)
-        {
-          visit.push_back(cp.get());
-        }
-      }
-    }
-    else if (!it->second)
-    {
-      Assert(cur->getRule() == PfRule::SCOPE);
-      // unbind its assumptions
-      for (const Node& a : cur->d_args)
-      {
-        currentScope.erase(a);
-      }
-    }
-  } while (!visit.empty());
+  std::vector<Node> assumps;
+  expr::getFreeAssumptions(this, assumps);
+  return assumps.empty();
 }
 
-bool ProofNode::isClosed() const
+std::shared_ptr<ProofNode> ProofNode::clone() const
 {
-  std::vector<Node> assumps;
-  getFreeAssumptions(assumps);
-  return assumps.empty();
+  std::vector<std::shared_ptr<ProofNode>> cchildren;
+  for (const std::shared_ptr<ProofNode>& cp : d_children)
+  {
+    cchildren.push_back(cp->clone());
+  }
+  std::shared_ptr<ProofNode> thisc =
+      std::make_shared<ProofNode>(d_rule, cchildren, d_args);
+  thisc->d_proven = d_proven;
+  return thisc;
 }
 
 void ProofNode::setValue(
@@ -113,17 +69,10 @@ void ProofNode::setValue(
 
 void ProofNode::printDebug(std::ostream& os) const
 {
-  os << "(" << d_rule;
-  for (const std::shared_ptr<ProofNode>& c : d_children)
-  {
-    os << " ";
-    c->printDebug(os);
-  }
-  if (!d_args.empty())
-  {
-    os << " :args " << d_args;
-  }
-  os << ")";
+  // convert to sexpr and print
+  ProofNodeToSExpr pnts;
+  Node ps = pnts.convertToSExpr(this);
+  os << ps;
 }
 
 }  // namespace CVC4
diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
index c3f1719e7..41575200f 100644
--- a/src/expr/proof_node.h
+++ b/src/expr/proof_node.h
@@ -45,6 +45,33 @@ class ProofNodeManager;
  * ProofNode objects in trusted ways that ensure that the node maintains
  * the invariant above. Furthermore, notice that this class is not responsible
  * for setting d_proven; this is done externally by a ProofNodeManager class.
+ *
+ * Notice that all fields of ProofNode are stored in ***Skolem form***. Their
+ * correctness is checked in ***witness form*** (for details on this
+ * terminology, see expr/skolem_manager.h). As a simple example, say a
+ * theory solver has a term t, and wants to introduce a unit lemma (= k t)
+ * where k is a fresh Skolem variable. It creates this variable via:
+ *   k = SkolemManager::mkPurifySkolem(t,"k");
+ * A checked ProofNode for the fact (= k t) then may have fields:
+ *   d_rule := MACRO_SR_PRED_INTRO,
+ *   d_children := {},
+ *   d_args := {(= k t)}
+ *   d_proven := (= k t).
+ * Its justification via the rule MACRO_SR_PRED_INTRO (see documentation
+ * in theory/builtin/proof_kinds) is in terms of the witness form of the
+ * argument:
+ *   (= (witness ((z T)) (= z t)) t)
+ * which, by that rule's side condition, is such that:
+ *   Rewriter::rewrite((= (witness ((z T)) (= z t)) t)) = true.
+ * Notice that the correctness of the rule is justified here by rewriting
+ * the witness form of (= k t). The conversion to/from witness form is
+ * managed by ProofRuleChecker::check.
+ *
+ * An external proof checker is expected to formalize the ProofNode only in
+ * terms of *witness* forms.
+ *
+ * However, the rest of CVC4 sees only the *Skolem* form of arguments and
+ * conclusions in ProofNode, since this is what is used throughout CVC4.
  */
 class ProofNode
 {
@@ -64,22 +91,13 @@ class ProofNode
   /** get what this node proves, or the null node if this is an invalid proof */
   Node getResult() const;
   /**
-   * This adds to the vector assump all formulas that are "free assumptions" of
-   * the proof whose root is this ProofNode. A free assumption is a formula F
-   * that is an argument (in d_args) of a ProofNode whose kind is ASSUME, and
-   * that proof node is not beneath an application of SCOPE containing F as an
-   * argument.
-   *
-   * This traverses the structure of the dag represented by this ProofNode.
-   * Its implementation is analogous to expr::getFreeVariables.
-   */
-  void getFreeAssumptions(std::vector<Node>& assump) const;
-  /**
    * Returns true if this is a closed proof (i.e. it has no free assumptions).
    */
-  bool isClosed() const;
+  bool isClosed();
   /** Print debug on output strem os */
   void printDebug(std::ostream& os) const;
+  /** Clone, create a deep copy of this */
+  std::shared_ptr<ProofNode> clone() const;
 
  private:
   /**
diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp
new file mode 100644
index 000000000..1929088dc
--- /dev/null
+++ b/src/expr/proof_node_algorithm.cpp
@@ -0,0 +1,118 @@
+/*********************                                                        */
+/*! \file proof_node_algorithm.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 proof node algorithm utilities
+ **/
+
+#include "expr/proof_node_algorithm.h"
+
+namespace CVC4 {
+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)
+  {
+    assump.push_back(p.first);
+  }
+}
+
+void getFreeAssumptionsMap(ProofNode* pn,
+                           std::map<Node, std::vector<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;
+  // 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.
+  //
+  // This map is used to track which nodes are in scope while traversing the
+  // DAG. The in-scope assumptions are keys in the map. They're removed when
+  // their binding count drops to zero. Let's annotate the above example to
+  // serve as an illustration:
+  //
+  //   (SCOPE0 (SCOPE1 (ASSUME x) (x y)) (y))
+  //
+  // This is how the map changes during the traversal:
+  //   after  previsiting SCOPE0: { y: 1 }
+  //   after  previsiting SCOPE1: { y: 2, x: 1 }
+  //   at                 ASSUME: { y: 2, x: 1 } (so x is in scope!)
+  //   after postvisiting SCOPE1: { y: 1 }
+  //   after postvisiting SCOPE2: {}
+  //
+  std::unordered_map<Node, uint32_t, NodeHashFunction> scopeDepth;
+  ProofNode* cur;
+  visit.push_back(pn);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+    const std::vector<Node>& cargs = cur->getArguments();
+    if (it == visited.end())
+    {
+      visited[cur] = true;
+      PfRule id = cur->getRule();
+      if (id == PfRule::ASSUME)
+      {
+        Assert(cargs.size() == 1);
+        Node f = cargs[0];
+        if (!scopeDepth.count(f))
+        {
+          amap[f].push_back(cur);
+        }
+      }
+      else
+      {
+        if (id == PfRule::SCOPE)
+        {
+          // mark that its arguments are bound in the current scope
+          for (const Node& a : cargs)
+          {
+            scopeDepth[a] += 1;
+          }
+          // will need to unbind the variables below
+          visited[cur] = false;
+        }
+        // The following loop cannot be merged with the loop above because the
+        // same subproof
+        const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
+        for (const std::shared_ptr<ProofNode>& cp : cs)
+        {
+          visit.push_back(cp.get());
+        }
+      }
+    }
+    else if (!it->second)
+    {
+      Assert(cur->getRule() == PfRule::SCOPE);
+      // unbind its assumptions
+      for (const Node& a : cargs)
+      {
+        auto scopeCt = scopeDepth.find(a);
+        Assert(scopeCt != scopeDepth.end());
+        scopeCt->second -= 1;
+        if (scopeCt->second == 0)
+        {
+          scopeDepth.erase(scopeCt);
+        }
+      }
+    }
+  } while (!visit.empty());
+}
+
+}  // namespace expr
+}  // namespace CVC4
diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h
new file mode 100644
index 000000000..a82f52539
--- /dev/null
+++ b/src/expr/proof_node_algorithm.h
@@ -0,0 +1,58 @@
+/*********************                                                        */
+/*! \file proof_node_algorithm.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Proof node algorithm utilities.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__PROOF_NODE_ALGORITHM_H
+#define CVC4__EXPR__PROOF_NODE_ALGORITHM_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace expr {
+
+/**
+ * This adds to the vector assump all formulas that are "free assumptions" of
+ * the proof whose root is ProofNode pn. A free assumption is a formula F
+ * that is an argument (in d_args) of a ProofNode whose kind is ASSUME, and
+ * that proof node is not beneath an application of SCOPE containing F as an
+ * argument.
+ *
+ * This traverses the structure of the dag represented by this ProofNode.
+ * Its implementation is analogous to expr::getFreeVariables.
+ *
+ * @param pn The proof node.
+ * @param assump The vector to add the free asumptions of pn to.
+ */
+void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump);
+/**
+ * Same as above, but maps assumptions to the proof pointer(s) for that
+ * assumption. Notice that depending on how pn is constructed, there may be
+ * multiple ProofNode that are ASSUME proofs of the same assumption, which
+ * are each added to the range of the assumption.
+ *
+ * @param pn The proof node.
+ * @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);
+
+}  // namespace expr
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__PROOF_NODE_ALGORITHM_H */