From 1c06ccdb1228fc7ef14440e1f29cf016cf5756c9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 11 Aug 2020 21:06:17 -0500 Subject: [PATCH] (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). --- src/expr/proof_checker.cpp | 80 ++++++++++++++++++++++++++++++++++++ src/expr/proof_checker.h | 33 ++++++++++++++- src/options/smt_options.toml | 14 +++++-- 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(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(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::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::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::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 d_checker; + /** Maps proof trusted rules to their pedantic level */ + std::map 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" -- 2.30.2