(proof-new) Extensions to proof checker interface (#4857)

This includes support for pedantic levels, as well as a utility for wrapping Kind in a Node (for the updated CONG rule, to be updated in a later PR).

3 files changed, 122 insertions, 5 deletions

diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
index 8f786052b..5e942b7a3 100644
--- a/src/expr/proof_checker.cpp
+++ b/src/expr/proof_checker.cpp
@@ -15,6 +15,7 @@
 #include "expr/proof_checker.h"
 
 #include "expr/skolem_manager.h"
+#include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
 
 using namespace CVC4::kind;
@@ -85,6 +86,27 @@ bool ProofRuleChecker::getBool(TNode n, bool& b)
   return false;
 }
 
+bool ProofRuleChecker::getKind(TNode n, Kind& k)
+{
+  uint32_t i;
+  if (!getUInt32(n, i))
+  {
+    return false;
+  }
+  k = static_cast<Kind>(i);
+  return true;
+}
+
+Node ProofRuleChecker::mkKindNode(Kind k)
+{
+  if (k == UNDEFINED_KIND)
+  {
+    // UNDEFINED_KIND is negative, hence return null to avoid cast
+    return Node::null();
+  }
+  return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(k)));
+}
+
 ProofCheckerStatistics::ProofCheckerStatistics()
     : d_ruleChecks("ProofCheckerStatistics::ruleChecks"),
     d_totalRuleChecks("ProofCheckerStatistics::totalRuleChecks", 0)
@@ -237,6 +259,16 @@ Node ProofChecker::checkInternal(PfRule id,
       return Node::null();
     }
   }
+  // fails if pedantic level is not met
+  if (options::proofNewPedanticEager())
+  {
+    std::stringstream serr;
+    if (isPedanticFailure(id, serr))
+    {
+      out << serr.str() << std::endl;
+      return Node::null();
+    }
+  }
   return res;
 }
 
@@ -253,6 +285,24 @@ void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc)
   d_checker[id] = psc;
 }
 
+void ProofChecker::registerTrustedChecker(PfRule id,
+                                          ProofRuleChecker* psc,
+                                          uint32_t plevel)
+{
+  AlwaysAssert(plevel <= 10) << "ProofChecker::registerTrustedChecker: "
+                                "pedantic level must be 0-10, got "
+                             << plevel << " for " << id;
+  registerChecker(id, psc);
+  // overwrites if already there
+  if (d_plevel.find(id) != d_plevel.end())
+  {
+    Notice() << "ProofChecker::registerTrustedRule: already provided pedantic "
+                "level for "
+             << id << std::endl;
+  }
+  d_plevel[id] = plevel;
+}
+
 ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id)
 {
   std::map<PfRule, ProofRuleChecker*>::const_iterator it = d_checker.find(id);
@@ -263,4 +313,34 @@ ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id)
   return it->second;
 }
 
+uint32_t ProofChecker::getPedanticLevel(PfRule id) const
+{
+  std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id);
+  if (itp != d_plevel.end())
+  {
+    return itp->second;
+  }
+  return 0;
+}
+
+bool ProofChecker::isPedanticFailure(PfRule id, std::ostream& out) const
+{
+  if (d_pclevel == 0)
+  {
+    return false;
+  }
+  std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id);
+  if (itp != d_plevel.end())
+  {
+    if (itp->second <= d_pclevel)
+    {
+      out << "pedantic level for " << id << " not met (rule level is "
+          << itp->second << " which is strictly below the required level "
+          << d_pclevel << ")";
+      return true;
+    }
+  }
+  return false;
+}
+
 }  // namespace CVC4
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index 65ad9f24d..245bd351a 100644
--- a/src/expr/proof_checker.h
+++ b/src/expr/proof_checker.h
@@ -69,6 +69,10 @@ class ProofRuleChecker
   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) {}
@@ -106,7 +110,7 @@ class ProofCheckerStatistics
 class ProofChecker
 {
  public:
-  ProofChecker() {}
+  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
@@ -156,14 +160,39 @@ class ProofChecker
                   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.
+   */
+  bool isPedanticFailure(PfRule id, std::ostream& out) const;
+
  private:
   /** statistics class */
   ProofCheckerStatistics d_stats;
-  /** Maps proof steps to their checker */
+  /** 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. We treat trusted checkers (nullptr in the range
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 3fecab5c9..d14a8e1cf 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -168,11 +168,19 @@ header = "options/smt_options.h"
 [[option]]
   name       = "proofNewPedantic"
   category   = "regular"
-  long       = "proof-new-pedantic"
+  long       = "proof-new-pedantic=N"
+  type       = "uint32_t"
+  default    = "0"
+  read_only  = true
+  help       = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof-new"
+
+[[option]]
+  name       = "proofNewPedanticEager"
+  category   = "regular"
+  long       = "proof-new-pedantic-eager"
   type       = "bool"
   default    = "false"
-  read_only  = true
-  help       = "assertion failure for any incorrect rule application or untrusted lemma for fully supported portions with proof-new"
+  help       = "check pedantic levels eagerly (during proof rule construction) instead of during final proof construction"
 
 [[option]]
   name       = "dumpInstantiations"