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.

1 files changed, 94 insertions, 0 deletions

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 */