Add ProofNode data structure (#4311)

This is the core data structure for proofs in the new proofs infrastructure. PfRule is a global enumeration of ids of proof nodes (analogous to Kind for Nodes).

5 files changed, 306 insertions, 0 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index a308e536c..aa928fdb7 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -33,6 +33,10 @@ libcvc4_add_sources(
   node_value.cpp
   node_value.h
   node_visitor.h
+  proof_node.cpp
+  proof_node.h
+  proof_rule.cpp
+  proof_rule.h
   symbol_table.cpp
   symbol_table.h
   term_canonize.cpp
diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp
new file mode 100644
index 000000000..94c175025
--- /dev/null
+++ b/src/expr/proof_node.cpp
@@ -0,0 +1,92 @@
+/*********************                                                        */
+/*! \file proof_node.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 utility
+ **/
+
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+
+ProofNode::ProofNode(PfRule id,
+                     const std::vector<std::shared_ptr<ProofNode>>& children,
+                     const std::vector<Node>& args)
+{
+  setValue(id, children, args);
+}
+
+PfRule ProofNode::getId() const { return d_id; }
+
+const std::vector<std::shared_ptr<ProofNode>>& ProofNode::getChildren() const
+{
+  return d_children;
+}
+
+const std::vector<Node>& ProofNode::getArguments() const { return d_args; }
+
+Node ProofNode::getResult() const { return d_proven; }
+
+void ProofNode::getAssumptions(std::vector<Node>& assump) const
+{
+  std::unordered_set<const ProofNode*> visited;
+  std::unordered_set<const ProofNode*>::iterator it;
+  std::vector<const ProofNode*> visit;
+  const ProofNode* cur;
+  visit.push_back(this);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+    if (it == visited.end())
+    {
+      visited.insert(cur);
+      if (cur->getId() == PfRule::ASSUME)
+      {
+        assump.push_back(cur->d_proven);
+      }
+      else
+      {
+        for (const std::shared_ptr<ProofNode>& cp : cur->d_children)
+        {
+          visit.push_back(cp.get());
+        }
+      }
+    }
+  } while (!visit.empty());
+}
+
+void ProofNode::setValue(
+    PfRule id,
+    const std::vector<std::shared_ptr<ProofNode>>& children,
+    const std::vector<Node>& args)
+{
+  d_id = id;
+  d_children = children;
+  d_args = args;
+}
+
+void ProofNode::printDebug(std::ostream& os) const
+{
+  os << "(" << d_id;
+  for (const std::shared_ptr<ProofNode>& c : d_children)
+  {
+    os << " ";
+    c->printDebug(os);
+  }
+  if (!d_args.empty())
+  {
+    os << " :args " << d_args;
+  }
+  os << ")";
+}
+
+}  // namespace CVC4
diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
new file mode 100644
index 000000000..7bf7cb0b4
--- /dev/null
+++ b/src/expr/proof_node.h
@@ -0,0 +1,93 @@
+/*********************                                                        */
+/*! \file proof_node.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 utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__PROOF_NODE_H
+#define CVC4__EXPR__PROOF_NODE_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/proof_rule.h"
+
+namespace CVC4 {
+
+/** A node in a proof
+ *
+ * A ProofNode represents a single step in a proof. It contains:
+ * (1) d_id, an identifier indicating the kind of inference,
+ * (2) d_children, the child ProofNode objects indicating its premises,
+ * (3) d_args, additional arguments used to determine the conclusion,
+ * (4) d_proven, cache of the formula that this ProofNode proves.
+ *
+ * Overall, a ProofNode and its children form a directed acyclic graph.
+ *
+ * A ProofNode is partially mutable in that (1), (2) and (3) can be
+ * modified. A motivating example of when this is useful is when a ProofNode
+ * is established to be a "hole" for something to be proven later. On the other
+ * hand, (4) is intended to be immutable.
+ *
+ * The method setValue is private and can be called by objects that manage
+ * 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.
+ */
+class ProofNode
+{
+ public:
+  ProofNode(PfRule id,
+            const std::vector<std::shared_ptr<ProofNode>>& children,
+            const std::vector<Node>& args);
+  ~ProofNode() {}
+  /** get the id of this proof node */
+  PfRule getId() const;
+  /** Get children */
+  const std::vector<std::shared_ptr<ProofNode>>& getChildren() const;
+  /** Get arguments */
+  const std::vector<Node>& getArguments() const;
+  /** get what this node proves, or the null node if this is an invalid proof */
+  Node getResult() const;
+  /** Get assumptions
+   *
+   * This adds to the vector assump all formulas that are "assumptions" of the
+   * proof whose root is this ProofNode. An assumption is a formula that is an
+   * argument (in d_args) of a ProofNode whose kind is ASSUME. This traverses
+   * the structure of the dag represented by this ProofNode.
+   */
+  void getAssumptions(std::vector<Node>& assump) const;
+  /** Print debug on output strem os */
+  void printDebug(std::ostream& os) const;
+
+ private:
+  /**
+   * Set value, called to overwrite the contents of this ProofNode with the
+   * given arguments.
+   */
+  void setValue(PfRule id,
+                const std::vector<std::shared_ptr<ProofNode>>& children,
+                const std::vector<Node>& args);
+  /** The proof step */
+  PfRule d_id;
+  /** The children of this proof node */
+  std::vector<std::shared_ptr<ProofNode>> d_children;
+  /** arguments of this node */
+  std::vector<Node> d_args;
+  /** The cache of the fact that has been proven, modifiable by ProofChecker */
+  Node d_proven;
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__PROOF_NODE_H */
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
new file mode 100644
index 000000000..2c10e09e6
--- /dev/null
+++ b/src/expr/proof_rule.cpp
@@ -0,0 +1,39 @@
+/*********************                                                        */
+/*! \file proof_rule.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 rule
+ **/
+
+#include "expr/proof_rule.h"
+
+#include <iostream>
+
+namespace CVC4 {
+
+const char* toString(PfRule id)
+{
+  switch (id)
+  {
+    //================================================= Core rules
+    case PfRule::ASSUME: return "ASSUME";
+    //================================================= Unknown rule
+    case PfRule::UNKNOWN: return "UNKNOWN";
+    default: return "?";
+  }
+}
+
+std::ostream& operator<<(std::ostream& out, PfRule id)
+{
+  out << toString(id);
+  return out;
+}
+
+}  // namespace CVC4
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
new file mode 100644
index 000000000..16f4ca971
--- /dev/null
+++ b/src/expr/proof_rule.h
@@ -0,0 +1,78 @@
+/*********************                                                        */
+/*! \file proof_rule.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 rule enumeration
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__PROOF_RULE_H
+#define CVC4__EXPR__PROOF_RULE_H
+
+#include <iosfwd>
+
+namespace CVC4 {
+
+/**
+ * An enumeration for proof rules. This enumeration is analogous to Kind for
+ * Node objects. In the documentation below, P:F denotes a ProofNode that
+ * proves formula F.
+ *
+ * Conceptually, the following proof rules form a calculus whose target
+ * user is the Node-level theory solvers. This means that the rules below
+ * are designed to reason about, among other things, common operations on Node
+ * objects like Rewriter::rewrite or Node::substitute. It is intended to be
+ * translated or printed in other formats.
+ *
+ * The following PfRule values include core rules and those categorized by
+ * theory, including the theory of equality.
+ *
+ * The "core rules" include ASSUME, which represents an open leaf in a proof.
+ * The core rules additionally correspond to generic operations that are done
+ * internally on nodes, e.g. calling Rewriter::rewrite.
+ */
+enum class PfRule : uint32_t
+{
+  //================================================= Core rules
+  // ======== Assumption (a leaf)
+  // Children: none
+  // Arguments: (F)
+  // --------------
+  // Conclusion F
+  ASSUME,
+
+  //================================================= Unknown rule
+  UNKNOWN,
+};
+
+/**
+ * Converts a proof rule to a string. Note: This function is also used in
+ * `safe_print()`. Changing this function name or signature will result in
+ * `safe_print()` printing "<unsupported>" instead of the proper strings for
+ * the enum values.
+ *
+ * @param id The proof rule
+ * @return The name of the proof rule
+ */
+const char* toString(PfRule id);
+
+/**
+ * Writes a proof rule name to a stream.
+ *
+ * @param out The stream to write to
+ * @param id The proof rule to write to the stream
+ * @return The stream
+ */
+std::ostream& operator<<(std::ostream& out, PfRule id);
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__PROOF_RULE_H */