(proof-new) Update proof checker. (#4511)

This adds new required features to proof checker and the base class of proof rule checker.

This is required as the first dependency towards merging further infrastructure related to proofs.

2 files changed, 282 insertions, 22 deletions

diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
index 95e43620b..7e7a26c5b 100644
--- a/src/expr/proof_checker.cpp
+++ b/src/expr/proof_checker.cpp
@@ -14,8 +14,94 @@
 
 #include "expr/proof_checker.h"
 
+#include "expr/proof_skolem_cache.h"
+#include "smt/smt_statistics_registry.h"
+
+using namespace CVC4::kind;
+
 namespace CVC4 {
 
+Node ProofRuleChecker::check(PfRule id,
+                             const std::vector<Node>& children,
+                             const std::vector<Node>& args)
+{
+  // convert to witness form
+  std::vector<Node> childrenw = children;
+  std::vector<Node> argsw = args;
+  ProofSkolemCache::convertToWitnessFormVec(childrenw);
+  ProofSkolemCache::convertToWitnessFormVec(argsw);
+  Node res = checkInternal(id, childrenw, argsw);
+  // res is in terms of witness form, convert back to Skolem form
+  return ProofSkolemCache::getSkolemForm(res);
+}
+
+Node ProofRuleChecker::checkChildrenArg(PfRule id,
+                                        const std::vector<Node>& children,
+                                        Node arg)
+{
+  return check(id, children, {arg});
+}
+Node ProofRuleChecker::checkChildren(PfRule id,
+                                     const std::vector<Node>& children)
+{
+  return check(id, children, {});
+}
+Node ProofRuleChecker::checkChild(PfRule id, Node child)
+{
+  return check(id, {child}, {});
+}
+Node ProofRuleChecker::checkArg(PfRule id, Node arg)
+{
+  return check(id, {}, {arg});
+}
+
+Node ProofRuleChecker::mkAnd(const std::vector<Node>& a)
+{
+  if (a.empty())
+  {
+    return NodeManager::currentNM()->mkConst(true);
+  }
+  else if (a.size() == 1)
+  {
+    return a[0];
+  }
+  return NodeManager::currentNM()->mkNode(AND, a);
+}
+
+bool ProofRuleChecker::getUInt32(TNode n, uint32_t& i)
+{
+  // must be a non-negative integer constant that fits an unsigned int
+  if (n.isConst() && n.getType().isInteger()
+      && n.getConst<Rational>().sgn() >= 0
+      && n.getConst<Rational>().getNumerator().fitsUnsignedInt())
+  {
+    i = n.getConst<Rational>().getNumerator().toUnsignedInt();
+    return true;
+  }
+  return false;
+}
+
+bool ProofRuleChecker::getBool(TNode n, bool& b)
+{
+  if (n.isConst() && n.getType().isBoolean())
+  {
+    b = n.getConst<bool>();
+    return true;
+  }
+  return false;
+}
+
+ProofCheckerStatistics::ProofCheckerStatistics()
+    : d_ruleChecks("ProofCheckerStatistics::ruleChecks")
+{
+  smtStatisticsRegistry()->registerStat(&d_ruleChecks);
+}
+
+ProofCheckerStatistics::~ProofCheckerStatistics()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_ruleChecks);
+}
+
 Node ProofChecker::check(ProofNode* pn, Node expected)
 {
   return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected);
@@ -27,15 +113,17 @@ Node ProofChecker::check(
     const std::vector<Node>& args,
     Node expected)
 {
-  std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
-  if (it == d_checker.end())
+  // optimization: immediately return for ASSUME
+  if (id == PfRule::ASSUME)
   {
-    // no checker for the rule
-    Trace("pfcheck") << "ProofChecker::check: no checker for rule " << id
-                     << std::endl;
-    return Node::null();
+    Assert(children.empty());
+    Assert(args.size() == 1 && args[0].getType().isBoolean());
+    Assert(expected.isNull() || expected == args[0]);
+    return expected;
   }
-  // check it with the corresponding checker
+  // record stat
+  d_stats.d_ruleChecks << id;
+  Trace("pfcheck") << "ProofChecker::check: " << id << std::endl;
   std::vector<Node> cchildren;
   for (const std::shared_ptr<ProofNode>& pc : children)
   {
@@ -43,26 +131,112 @@ Node ProofChecker::check(
     Node cres = pc->getResult();
     if (cres.isNull())
     {
-      Trace("pfcheck")
+      Trace("pfcheck") << "ProofChecker::check: failed child" << std::endl;
+      Unreachable()
           << "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);
+    if (Trace.isOn("pfcheck"))
+    {
+      std::stringstream ssc;
+      pc->printDebug(ssc);
+      Trace("pfcheck") << "     child: " << ssc.str() << " : " << cres
+                       << std::endl;
+    }
   }
-  Node res = it->second->check(id, cchildren, args);
-  if (!expected.isNull() && res != expected)
+  Trace("pfcheck") << "      args: " << args << std::endl;
+  Trace("pfcheck") << "  expected: " << expected << std::endl;
+  std::stringstream out;
+  // we use trusted (null) checkers here, since we want the proof generation to
+  // proceed without failing here.
+  Node res = checkInternal(id, cchildren, args, expected, out, true);
+  if (res.isNull())
   {
-    Trace("pfcheck")
-        << "ProofChecker::check: result does not match expected value."
-        << std::endl;
-    Trace("pfcheck") << "    result: " << res << std::endl;
-    Trace("pfcheck") << "  expected: " << expected << std::endl;
+    Trace("pfcheck") << "ProofChecker::check: failed" << std::endl;
+    Unreachable() << "ProofChecker::check: failed, " << out.str() << std::endl;
     // it did not match the given expectation, fail
     return Node::null();
   }
+  Trace("pfcheck") << "ProofChecker::check: success!" << std::endl;
+  return res;
+}
+
+Node ProofChecker::checkDebug(PfRule id,
+                              const std::vector<Node>& cchildren,
+                              const std::vector<Node>& args,
+                              Node expected,
+                              const char* traceTag)
+{
+  std::stringstream out;
+  // since we are debugging, we want to treat trusted (null) checkers as
+  // a failure.
+  Node res = checkInternal(id, cchildren, args, expected, out, false);
+  Trace(traceTag) << "ProofChecker::checkDebug: " << id;
+  if (res.isNull())
+  {
+    Trace(traceTag) << " failed, " << out.str() << std::endl;
+  }
+  else
+  {
+    Trace(traceTag) << " success" << std::endl;
+  }
+  return res;
+}
+
+Node ProofChecker::checkInternal(PfRule id,
+                                 const std::vector<Node>& cchildren,
+                                 const std::vector<Node>& args,
+                                 Node expected,
+                                 std::stringstream& out,
+                                 bool useTrustedChecker)
+{
+  std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
+  if (it == d_checker.end())
+  {
+    // no checker for the rule
+    out << "no checker for rule " << id << std::endl;
+    return Node::null();
+  }
+  else if (it->second == nullptr)
+  {
+    if (useTrustedChecker)
+    {
+      Notice() << "ProofChecker::check: trusting PfRule " << id << std::endl;
+      // trusted checker
+      return expected;
+    }
+    else
+    {
+      out << "trusted checker for rule " << id << std::endl;
+      return Node::null();
+    }
+  }
+  // check it with the corresponding checker
+  Node res = it->second->check(id, cchildren, args);
+  if (!expected.isNull())
+  {
+    Node expectedw = expected;
+    if (res != expectedw)
+    {
+      out << "result does not match expected value." << std::endl
+          << "    PfRule: " << id << std::endl;
+      for (const Node& c : cchildren)
+      {
+        out << "     child: " << c << std::endl;
+      }
+      for (const Node& a : args)
+      {
+        out << "       arg: " << a << std::endl;
+      }
+      out << "    result: " << res << std::endl
+          << "  expected: " << expected << std::endl;
+      // it did not match the given expectation, fail
+      return Node::null();
+    }
+  }
   return res;
 }
 
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index 48b41453f..99c02b8dc 100644
--- a/src/expr/proof_checker.h
+++ b/src/expr/proof_checker.h
@@ -21,9 +21,12 @@
 
 #include "expr/node.h"
 #include "expr/proof_node.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
+class ProofChecker;
+
 /** A virtual base class for checking a proof rule */
 class ProofRuleChecker
 {
@@ -36,17 +39,67 @@ class ProofRuleChecker
    * 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*. To facilitate checking, this method converts to/from witness
+   * form, calling the subprocedure checkInternal below.
+   *
+   * @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);
+  /** Single arg version */
+  Node checkChildrenArg(PfRule id, const std::vector<Node>& children, Node arg);
+  /** No arg version */
+  Node checkChildren(PfRule id, const std::vector<Node>& children);
+  /** Single child only version */
+  Node checkChild(PfRule id, Node child);
+  /** Single argument only version */
+  Node checkArg(PfRule id, Node arg);
+
+  /** Make AND-kinded node with children a */
+  static Node mkAnd(const std::vector<Node>& a);
+  /** 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);
+
+  /** Register all rules owned by this rule checker into pc. */
+  virtual void registerTo(ProofChecker* pc) {}
+
+ protected:
+  /**
+   * This checks a single step in a proof. It is identical to check above
+   * except that children and args have been converted to "witness form"
+   * (see ProofSkolemCache). Likewise, its output should be in witness form.
+   *
    * @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.
+   * of the proof node we are checking, in witness form.
    * @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.
+   * @return The conclusion of the proof node, in witness form, 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;
+  virtual Node checkInternal(PfRule id,
+                             const std::vector<Node>& children,
+                             const std::vector<Node>& args) = 0;
+};
+
+/** Statistics class */
+class ProofCheckerStatistics
+{
+ public:
+  ProofCheckerStatistics();
+  ~ProofCheckerStatistics();
+  /** Counts the number of checks for each kind of proof rule */
+  HistogramStat<PfRule> d_ruleChecks;
 };
 
 /** A class for checking proofs */
@@ -81,12 +134,45 @@ class ProofChecker
              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,
+                  const char* traceTag);
   /** Indicate that psc is the checker for proof rule id */
   void registerChecker(PfRule id, ProofRuleChecker* psc);
 
  private:
+  /** statistics class */
+  ProofCheckerStatistics d_stats;
   /** Maps proof steps to their checker */
   std::map<PfRule, ProofRuleChecker*> d_checker;
+  /**
+   * Check internal. This is used by check and checkDebug above. It writes
+   * checking errors on out. 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);
 };
 
 }  // namespace CVC4