1 files changed, 206 insertions, 0 deletions
diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h
new file mode 100644
index 000000000..ac5531bf4
--- /dev/null
+++ b/src/proof/proof_checker.h
@@ -0,0 +1,206 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Proof checker utility.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__PROOF_CHECKER_H
+#define CVC5__PROOF__PROOF_CHECKER_H
+
+#include <map>
+
+#include "expr/node.h"
+#include "proof/proof_rule.h"
+#include "util/statistics_stats.h"
+
+namespace cvc5 {
+
+class ProofChecker;
+class ProofNode;
+
+/** 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.
+   *
+   * Note that the input/output of this method expects to be terms in *Skolem
+   * form*, which is passed to checkInternal below. Rule checkers may
+   * convert premises to witness form when necessary.
+   *
+   * @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 in Skolem form.
+   * @param args The arguments of the proof node to check
+   * @return The conclusion of the proof node, in Skolem form, if successful or
+   * null if such a proof node is malformed.
+   */
+  Node check(PfRule id,
+             const std::vector<Node>& children,
+             const std::vector<Node>& args);
+
+  /** get an index from a node, return false if we fail */
+  static bool getUInt32(TNode n, uint32_t& i);
+  /** get a Boolean from a node, return false if we fail */
+  static bool getBool(TNode n, bool& b);
+  /** get a Kind from a node, return false if we fail */
+  static bool getKind(TNode n, Kind& k);
+  /** Make a Kind into a node */
+  static Node mkKindNode(Kind k);
+
+  /** Register all rules owned by this rule checker into pc. */
+  virtual void registerTo(ProofChecker* pc) {}
+
+ protected:
+  /**
+   * This checks a single step in a proof.
+   *
+   * @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 checkInternal(PfRule id,
+                             const std::vector<Node>& children,
+                             const std::vector<Node>& args) = 0;
+};
+
+/** Statistics class */
+class ProofCheckerStatistics
+{
+ public:
+  ProofCheckerStatistics();
+  /** Counts the number of checks for each kind of proof rule */
+  HistogramStat<PfRule> d_ruleChecks;
+  /** Total number of rule checks */
+  IntStat d_totalRuleChecks;
+};
+
+/** A class for checking proofs */
+class ProofChecker
+{
+ public:
+  ProofChecker(uint32_t pclevel = 0) : d_pclevel(pclevel) {}
+  ~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());
+  /**
+   * Same as above, without conclusions instead of proof node children. This
+   * is used for debugging. In particular, this function does not throw an
+   * assertion failure when a proof step is malformed and can be used without
+   * constructing proof nodes.
+   *
+   * @param id The id of the proof node to check
+   * @param children The conclusions of 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.
+   * @param traceTag The trace tag to print debug information to
+   * @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 checkDebug(PfRule id,
+                  const std::vector<Node>& cchildren,
+                  const std::vector<Node>& args,
+                  Node expected = Node::null(),
+                  const char* traceTag = "");
+  /** Indicate that psc is the checker for proof rule id */
+  void registerChecker(PfRule id, ProofRuleChecker* psc);
+  /**
+   * Indicate that id is a trusted rule with the given pedantic level, e.g.:
+   *  0: (mandatory) always a failure to use the given id
+   *  1: (major) failure on all (non-zero) pedantic levels
+   * 10: (minor) failure only on pedantic levels >= 10.
+   */
+  void registerTrustedChecker(PfRule id,
+                              ProofRuleChecker* psc,
+                              uint32_t plevel = 10);
+  /** get checker for */
+  ProofRuleChecker* getCheckerFor(PfRule id);
+
+  /**
+   * Get the pedantic level for id if it has been assigned a pedantic
+   * level via registerTrustedChecker above, or zero otherwise.
+   */
+  uint32_t getPedanticLevel(PfRule id) const;
+
+  /**
+   * Is pedantic failure? If so, we return true and write a debug message on the
+   * output stream out if enableOutput is true.
+   */
+  bool isPedanticFailure(PfRule id,
+                         std::ostream& out,
+                         bool enableOutput = true) const;
+
+ private:
+  /** statistics class */
+  ProofCheckerStatistics d_stats;
+  /** Maps proof rules to their checker */
+  std::map<PfRule, ProofRuleChecker*> d_checker;
+  /** Maps proof trusted rules to their pedantic level */
+  std::map<PfRule, uint32_t> d_plevel;
+  /** The pedantic level of this checker */
+  uint32_t d_pclevel;
+  /**
+   * Check internal. This is used by check and checkDebug above. It writes
+   * checking errors on out when enableOutput is true. We treat trusted checkers
+   * (nullptr in the range of the map d_checker) as failures if
+   * useTrustedChecker = false.
+   */
+  Node checkInternal(PfRule id,
+                     const std::vector<Node>& cchildren,
+                     const std::vector<Node>& args,
+                     Node expected,
+                     std::stringstream& out,
+                     bool useTrustedChecker,
+                     bool enableOutput);
+};
+
+}  // namespace cvc5
+
+#endif /* CVC5__PROOF__PROOF_CHECKER_H */