From 2de877854e590e8edf89ffb1d940cd4c9717f195 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 12 Nov 2020 09:08:13 -0600 Subject: [PATCH] (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. --- src/expr/proof_checker.cpp | 85 ++++++++++++++++++++++---------- src/expr/proof_checker.h | 14 ++++-- src/options/smt_options.toml | 8 --- src/smt/proof_post_processor.cpp | 2 +- 4 files changed, 69 insertions(+), 40 deletions(-) diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp index e839c0830..a60a82b60 100644 --- 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& args, Node expected, std::stringstream& out, - bool useTrustedChecker) + bool useTrustedChecker, + bool enableOutput) { std::map::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 93e16e63c..ab9c24434 100644 --- 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& cchildren, const std::vector& 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 683fe61bd..54d81eba6 100644 --- 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 40e61964c..53608fa0a 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -736,7 +736,7 @@ bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr pn, { PfRule r = pn->getRule(); // if not doing eager pedantic checking, fail if below threshold - if (!options::proofNewPedanticEager()) + if (!options::proofNewEagerChecking()) { if (!d_pedanticFailure) { -- 2.30.2