Add ProofNodeManager and ProofChecker (#4317)

Further work on adding core utilities for ProofNode objects, in support of the new proof infrastructure.

ProofNodeManager is analogous to NodeManager. It is a trusted way of generating only "well-formed" ProofNode pointers (according to a checker).

ProofChecker is analogous to TypeChecker. It is intended to be infrastructure for our internal proof checker.

This PR (and 1 more) is required to get to a place where Haniel and I can collaborate on further development for proofs.

6 files changed, 390 insertions, 0 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index aa928fdb7..f21241ef5 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -33,8 +33,12 @@ libcvc4_add_sources(
   node_value.cpp
   node_value.h
   node_visitor.h
+  proof_checker.cpp
+  proof_checker.h
   proof_node.cpp
   proof_node.h
+  proof_node_manager.cpp
+  proof_node_manager.h
   proof_rule.cpp
   proof_rule.h
   symbol_table.cpp
diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
new file mode 100644
index 000000000..f4c275c47
--- /dev/null
+++ b/src/expr/proof_checker.cpp
@@ -0,0 +1,82 @@
+/*********************                                                        */
+/*! \file proof_checker.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 checker
+ **/
+
+#include "expr/proof_checker.h"
+
+namespace CVC4 {
+
+Node ProofChecker::check(ProofNode* pn, Node expected)
+{
+  return check(pn->getId(), pn->getChildren(), pn->getArguments(), expected);
+}
+
+Node ProofChecker::check(
+    PfRule id,
+    const std::vector<std::shared_ptr<ProofNode>>& children,
+    const std::vector<Node>& args,
+    Node expected)
+{
+  std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
+  if (it == d_checker.end())
+  {
+    // no checker for the rule
+    Trace("pfcheck") << "ProofChecker::check: no checker for rule " << id
+                     << std::endl;
+    return Node::null();
+  }
+  // check it with the corresponding checker
+  std::vector<Node> cchildren;
+  for (const std::shared_ptr<ProofNode>& pc : children)
+  {
+    Assert(pc != nullptr);
+    Node cres = pc->getResult();
+    if (cres.isNull())
+    {
+      Trace("pfcheck")
+          << "ProofChecker::check: child proof was invalid (null conclusion)"
+          << std::endl;
+      // should not have been able to create such a proof node
+      Assert(false);
+      return Node::null();
+    }
+    cchildren.push_back(cres);
+  }
+  Node res = it->second->check(id, cchildren, args);
+  if (!expected.isNull() && res != expected)
+  {
+    Trace("pfcheck")
+        << "ProofChecker::check: result does not match expected value."
+        << std::endl;
+    Trace("pfcheck") << "    result: " << res << std::endl;
+    Trace("pfcheck") << "  expected: " << expected << std::endl;
+    // it did not match the given expectation, fail
+    return Node::null();
+  }
+  return res;
+}
+
+void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc)
+{
+  std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
+  if (it != d_checker.end())
+  {
+    // checker is already provided
+    Notice() << "ProofChecker::registerChecker: checker already exists for "
+             << id << std::endl;
+    return;
+  }
+  d_checker[id] = psc;
+}
+
+}  // namespace CVC4
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
new file mode 100644
index 000000000..48b41453f
--- /dev/null
+++ b/src/expr/proof_checker.h
@@ -0,0 +1,94 @@
+/*********************                                                        */
+/*! \file proof_checker.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 checker utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__PROOF_CHECKER_H
+#define CVC4__EXPR__PROOF_CHECKER_H
+
+#include <map>
+
+#include "expr/node.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+
+/** A virtual base class for checking a proof rule */
+class ProofRuleChecker
+{
+ public:
+  ProofRuleChecker() {}
+  virtual ~ProofRuleChecker() {}
+  /**
+   * This checks a single step in a proof.
+   *
+   * Return the formula that is proven by a proof node with the given id,
+   * premises and arguments, or null if such a proof node is not well-formed.
+   *
+   * @param id The id of the proof node to check
+   * @param children The premises of the proof node to check. These are nodes
+   * corresponding to the conclusion (ProofNode::getResult) of the children
+   * of the proof node we are checking.
+   * @param args The arguments of the proof node to check
+   * @return The conclusion of the proof node if successful or null if such a
+   * proof node is malformed.
+   */
+  virtual Node check(PfRule id,
+                     const std::vector<Node>& children,
+                     const std::vector<Node>& args) = 0;
+};
+
+/** A class for checking proofs */
+class ProofChecker
+{
+ public:
+  ProofChecker() {}
+  ~ProofChecker() {}
+  /**
+   * Return the formula that is proven by proof node pn, or null if pn is not
+   * well-formed. If expected is non-null, then we return null if pn does not
+   * prove expected.
+   *
+   * @param pn The proof node to check
+   * @param expected The (optional) formula that is the expected conclusion of
+   * the proof node.
+   * @return The conclusion of the proof node if successful or null if the
+   * proof is malformed, or if no checker is available for id.
+   */
+  Node check(ProofNode* pn, Node expected = Node::null());
+  /** Same as above, with explicit arguments
+   *
+   * @param id The id of the proof node to check
+   * @param children The children of the proof node to check
+   * @param args The arguments of the proof node to check
+   * @param expected The (optional) formula that is the expected conclusion of
+   * the proof node.
+   * @return The conclusion of the proof node if successful or null if the
+   * proof is malformed, or if no checker is available for id.
+   */
+  Node check(PfRule id,
+             const std::vector<std::shared_ptr<ProofNode>>& children,
+             const std::vector<Node>& args,
+             Node expected = Node::null());
+  /** Indicate that psc is the checker for proof rule id */
+  void registerChecker(PfRule id, ProofRuleChecker* psc);
+
+ private:
+  /** Maps proof steps to their checker */
+  std::map<PfRule, ProofRuleChecker*> d_checker;
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__PROOF_CHECKER_H */
diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
index 7bf7cb0b4..9a460c59b 100644
--- a/src/expr/proof_node.h
+++ b/src/expr/proof_node.h
@@ -24,6 +24,8 @@
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /** A node in a proof
  *
  * A ProofNode represents a single step in a proof. It contains:
@@ -46,6 +48,8 @@ namespace CVC4 {
  */
 class ProofNode
 {
+  friend class ProofNodeManager;
+
  public:
   ProofNode(PfRule id,
             const std::vector<std::shared_ptr<ProofNode>>& children,
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
new file mode 100644
index 000000000..e2f5ca2dc
--- /dev/null
+++ b/src/expr/proof_node_manager.cpp
@@ -0,0 +1,89 @@
+/*********************                                                        */
+/*! \file proof_node_manager.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 manager
+ **/
+
+#include "expr/proof_node_manager.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) {}
+
+std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
+    PfRule id,
+    const std::vector<std::shared_ptr<ProofNode>>& children,
+    const std::vector<Node>& args,
+    Node expected)
+{
+  Node res = checkInternal(id, children, args, expected);
+  if (res.isNull())
+  {
+    // if it was invalid, then we return the null node
+    return nullptr;
+  }
+  // otherwise construct the proof node and set its proven field
+  std::shared_ptr<ProofNode> pn =
+      std::make_shared<ProofNode>(id, children, args);
+  pn->d_proven = res;
+  return pn;
+}
+
+bool ProofNodeManager::updateNode(
+    ProofNode* pn,
+    PfRule id,
+    const std::vector<std::shared_ptr<ProofNode>>& children,
+    const std::vector<Node>& args)
+{
+  // should have already computed what is proven
+  Assert(!pn->d_proven.isNull())
+      << "ProofNodeManager::updateProofNode: invalid proof provided";
+  // We expect to prove the same thing as before
+  Node res = checkInternal(id, children, args, pn->d_proven);
+  if (res.isNull())
+  {
+    // if it was invalid, then we do not update
+    return false;
+  }
+  // we update its value
+  pn->setValue(id, children, args);
+  // proven field should already be the same as the result
+  Assert(res == pn->d_proven);
+  return true;
+}
+
+Node ProofNodeManager::checkInternal(
+    PfRule id,
+    const std::vector<std::shared_ptr<ProofNode>>& children,
+    const std::vector<Node>& args,
+    Node expected)
+{
+  Node res;
+  if (d_checker)
+  {
+    // check with the checker, which takes expected as argument
+    res = d_checker->check(id, children, args, expected);
+    Assert(!res.isNull())
+        << "ProofNodeManager::checkInternal: failed to check proof";
+  }
+  else
+  {
+    // otherwise we trust the expected value, if it exists
+    Assert(!expected.isNull()) << "ProofNodeManager::checkInternal: no checker "
+                                  "or expected value provided";
+    res = expected;
+  }
+  return res;
+}
+
+}  // namespace CVC4
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
new file mode 100644
index 000000000..17c5580bf
--- /dev/null
+++ b/src/expr/proof_node_manager.h
@@ -0,0 +1,117 @@
+/*********************                                                        */
+/*! \file proof_node_manager.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 manager utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__PROOF_NODE_MANAGER_H
+#define CVC4__EXPR__PROOF_NODE_MANAGER_H
+
+#include <vector>
+
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+
+/**
+ * A manager for proof node objects. This is a trusted interface for creating
+ * and updating ProofNode objects.
+ *
+ * In more detail, we say a ProofNode is "well-formed (with respect to checker
+ * X)" if its d_proven field is non-null, and corresponds to the formula that
+ * the ProofNode proves according to X. The ProofNodeManager class constructs
+ * and update nodes that are well-formed with respect to its underlying checker.
+ *
+ * If no checker is provided, then the ProofNodeManager assigns the d_proven
+ * field of ProofNode based on the provided "expected" argument in mkNode below,
+ * which must be provided in this case.
+ *
+ * The ProofNodeManager is used as a trusted way of updating ProofNode objects
+ * via updateNode below. In particular, this method leaves the d_proven field
+ * unchanged and updates (if possible) the remaining content of a given proof
+ * node.
+ *
+ * Notice that ProofNode objects are mutable, and hence this class does not
+ * cache the results of mkNode. A version of this class that caches
+ * immutable version of ProofNode objects could be built as an extension
+ * or layer on top of this class.
+ */
+class ProofNodeManager
+{
+ public:
+  ProofNodeManager(ProofChecker* pc = nullptr);
+  ~ProofNodeManager() {}
+  /**
+   * This constructs a ProofNode with the given arguments. The expected
+   * argument, when provided, indicates the formula that the returned node
+   * is expected to prove. If we find that it does not, based on the underlying
+   * checker, this method returns nullptr.
+   *
+   * @param id The id of the proof node.
+   * @param children The children of the proof node.
+   * @param args The arguments of the proof node.
+   * @param expected (Optional) the expected conclusion of the proof node.
+   * @return the proof node, or nullptr if the given arguments do not
+   * consistute a proof of the expected conclusion according to the underlying
+   * checker, if both are provided. It also returns nullptr if neither the
+   * checker nor the expected field is provided, since in this case the
+   * conclusion is unknown.
+   */
+  std::shared_ptr<ProofNode> mkNode(
+      PfRule id,
+      const std::vector<std::shared_ptr<ProofNode>>& children,
+      const std::vector<Node>& args,
+      Node expected = Node::null());
+  /**
+   * This method updates pn to be a proof of the form <id>( children, args ),
+   * while maintaining its d_proven field. This method returns false if this
+   * proof manager is using a checker, and we compute that the above proof
+   * is not a proof of the fact that pn previously proved.
+   *
+   * @param pn The proof node to update.
+   * @param id The updated id of the proof node.
+   * @param children The updated children of the proof node.
+   * @param args The updated arguments of the proof node.
+   * @return true if the update was successful.
+   *
+   * Notice that updateNode always returns true if there is no underlying
+   * checker.
+   */
+  bool updateNode(ProofNode* pn,
+                  PfRule id,
+                  const std::vector<std::shared_ptr<ProofNode>>& children,
+                  const std::vector<Node>& args);
+
+ private:
+  /** The (optional) proof checker */
+  ProofChecker* d_checker;
+  /** Check internal
+   *
+   * This returns the result of proof checking a ProofNode with the provided
+   * arguments with an expected conclusion, which may not null if there is
+   * no expected conclusion.
+   *
+   * This throws an assertion error if we fail to check such a proof node, or
+   * if expected is provided (non-null) and is different what is proven by the
+   * other arguments.
+   */
+  Node checkInternal(PfRule id,
+                     const std::vector<std::shared_ptr<ProofNode>>& children,
+                     const std::vector<Node>& args,
+                     Node expected);
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__PROOF_NODE_H */