From 7da96102de1894fb96eccec5315234d7c441f017 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 26 May 2020 10:27:45 -0500 Subject: [PATCH] (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. --- src/expr/proof_checker.cpp | 206 ++++++++++++++++++++++++++++++++++--- src/expr/proof_checker.h | 98 ++++++++++++++++-- 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& children, + const std::vector& args) +{ + // convert to witness form + std::vector childrenw = children; + std::vector 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& children, + Node arg) +{ + return check(id, children, {arg}); +} +Node ProofRuleChecker::checkChildren(PfRule id, + const std::vector& 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& 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().sgn() >= 0 + && n.getConst().getNumerator().fitsUnsignedInt()) + { + i = n.getConst().getNumerator().toUnsignedInt(); + return true; + } + return false; +} + +bool ProofRuleChecker::getBool(TNode n, bool& b) +{ + if (n.isConst() && n.getType().isBoolean()) + { + b = n.getConst(); + 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& args, Node expected) { - std::map::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 cchildren; for (const std::shared_ptr& 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& cchildren, + const std::vector& 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& cchildren, + const std::vector& args, + Node expected, + std::stringstream& out, + bool useTrustedChecker) +{ + 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; + 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& children, + const std::vector& args); + /** Single arg version */ + Node checkChildrenArg(PfRule id, const std::vector& children, Node arg); + /** No arg version */ + Node checkChildren(PfRule id, const std::vector& 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& 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& children, - const std::vector& args) = 0; + virtual Node checkInternal(PfRule id, + const std::vector& children, + const std::vector& args) = 0; +}; + +/** Statistics class */ +class ProofCheckerStatistics +{ + public: + ProofCheckerStatistics(); + ~ProofCheckerStatistics(); + /** Counts the number of checks for each kind of proof rule */ + HistogramStat d_ruleChecks; }; /** A class for checking proofs */ @@ -81,12 +134,45 @@ class ProofChecker const std::vector>& children, const std::vector& 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& cchildren, + const std::vector& 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 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& cchildren, + const std::vector& args, + Node expected, + std::stringstream& out, + bool useTrustedChecker); }; } // namespace CVC4 -- 2.30.2