(proof-new) Improve printing and debugging for pedantic checking (#5337)

This improves trace/error messages for proof-new-pedantic, and also merges the proof-new-pedantic-eager with the proof-new-eager-checking option.

diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
index e839c08300670f3a6441de697235c3e0f5854893..a60a82b601f3af4ae7d00dbbe6ec6c9c7425bb8e 100644 (file)
--- a/src/expr/proof_checker.cpp
+++ b/src/expr/proof_checker.cpp
@@ -138,8 +138,9 @@ Node ProofChecker::check(
   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);
+  // proceed without failing here. We always enable output since a failure
+  // implies that we will exit with the error message below.
+  Node res = checkInternal(id, cchildren, args, expected, out, true, true);
   if (res.isNull())
   {
     Trace("pfcheck") << "ProofChecker::check: failed" << std::endl;
@@ -158,10 +159,12 @@ Node ProofChecker::checkDebug(PfRule id,
                               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);
-  if (Trace.isOn(traceTag))
+  bool traceEnabled = Trace.isOn(traceTag);
+  // Since we are debugging, we want to treat trusted (null) checkers as
+  // a failure. We only enable output if the trace is enabled for efficiency.
+  Node res =
+      checkInternal(id, cchildren, args, expected, out, false, traceEnabled);
+  if (traceEnabled)
   {
     Trace(traceTag) << "ProofChecker::checkDebug: " << id;
     if (res.isNull())
@@ -183,13 +186,17 @@ Node ProofChecker::checkInternal(PfRule id,
                                  const std::vector<Node>& args,
                                  Node expected,
                                  std::stringstream& out,
-                                 bool useTrustedChecker)
+                                 bool useTrustedChecker,
+                                 bool enableOutput)
 {
   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;
+    if (enableOutput)
+    {
+      out << "no checker for rule " << id << std::endl;
+    }
     return Node::null();
   }
   else if (it->second == nullptr)
@@ -202,7 +209,10 @@ Node ProofChecker::checkInternal(PfRule id,
     }
     else
     {
-      out << "trusted checker for rule " << id << std::endl;
+      if (enableOutput)
+      {
+        out << "trusted checker for rule " << id << std::endl;
+      }
       return Node::null();
     }
   }
@@ -213,29 +223,42 @@ Node ProofChecker::checkInternal(PfRule id,
     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)
+      if (enableOutput)
       {
-        out << "       arg: " << a << std::endl;
+        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;
       }
-      out << "    result: " << res << std::endl
-          << "  expected: " << expected << std::endl;
       // it did not match the given expectation, fail
       return Node::null();
     }
   }
   // fails if pedantic level is not met
-  if (options::proofNewPedanticEager())
+  if (options::proofNewEagerChecking())
   {
     std::stringstream serr;
-    if (isPedanticFailure(id, serr))
+    if (isPedanticFailure(id, serr, enableOutput))
     {
-      out << serr.str() << std::endl;
+      if (enableOutput)
+      {
+        out << serr.str() << std::endl;
+        if (Trace.isOn("proof-new-pedantic"))
+        {
+          Trace("proof-new-pedantic")
+              << "Failed pedantic check for " << id << std::endl;
+          Trace("proof-new-pedantic") << "Expected: " << expected << std::endl;
+          out << "Expected: " << expected << std::endl;
+        }
+      }
       return Node::null();
     }
   }
@@ -293,7 +316,9 @@ uint32_t ProofChecker::getPedanticLevel(PfRule id) const
   return 0;
 }
 
-bool ProofChecker::isPedanticFailure(PfRule id, std::ostream& out) const
+bool ProofChecker::isPedanticFailure(PfRule id,
+                                     std::ostream& out,
+                                     bool enableOutput) const
 {
   if (d_pclevel == 0)
   {
@@ -304,9 +329,17 @@ bool ProofChecker::isPedanticFailure(PfRule id, std::ostream& out) const
   {
     if (itp->second <= d_pclevel)
     {
-      out << "pedantic level for " << id << " not met (rule level is "
-          << itp->second << " which is at or below the pedantic level "
-          << d_pclevel << ")";
+      if (enableOutput)
+      {
+        out << "pedantic level for " << id << " not met (rule level is "
+            << itp->second << " which is at or below the pedantic level "
+            << d_pclevel << ")";
+        bool pedanticTraceEnabled = Trace.isOn("proof-new-pedantic");
+        if (!pedanticTraceEnabled)
+        {
+          out << ", use -t proof-new-pedantic for details";
+        }
+      }
       return true;
     }
   }

diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index 93e16e63c3562e463ec2c4b1859309972f8b8ded..ab9c244348532b9299cdac4c7801b4b5fef27b1b 100644 (file)
--- a/src/expr/proof_checker.h
+++ b/src/expr/proof_checker.h
@@ -170,9 +170,11 @@ class ProofChecker
 
   /**
    * Is pedantic failure? If so, we return true and write a debug message on the
-   * output stream out.
+   * output stream out if enableOutput is true.
    */
-  bool isPedanticFailure(PfRule id, std::ostream& out) const;
+  bool isPedanticFailure(PfRule id,
+                         std::ostream& out,
+                         bool enableOutput = true) const;
 
  private:
   /** statistics class */
@@ -185,15 +187,17 @@ class ProofChecker
   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
-   * of the map d_checker) as failures if useTrustedChecker = false.
+   * 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 useTrustedChecker,
+                     bool enableOutput);
 };
 
 }  // namespace CVC4

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 683fe61bd46687efdd7bc6a18c4eb18e60d2f84c..54d81eba6caf15330523a6cd9d21535ebadc0143 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -156,14 +156,6 @@ header = "options/smt_options.h"
   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"
-  help       = "check pedantic levels eagerly (during proof rule construction) instead of during final proof construction"
-
 [[option]]
   name       = "proofNewEagerChecking"
   category   = "regular"

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 40e61964c341a9c64b7af2667f3eb81116fb143e..53608fa0a89dcd04c6b92d37f74fb00b5222921d 100644 (file)
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -736,7 +736,7 @@ bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
 {
   PfRule r = pn->getRule();
   // if not doing eager pedantic checking, fail if below threshold
-  if (!options::proofNewPedanticEager())
+  if (!options::proofNewEagerChecking())
   {
     if (!d_pedanticFailure)
     {