diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-25 08:41:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-25 08:41:13 -0500 |
commit | 87a64143f02c919df14baeb3c1acdd1295df50e9 (patch) | |
tree | 8a60d9db3d7b37f5436caf456719d4fbc340ef98 /src/proof/proof_checker.h | |
parent | 23c30f6961f9b19d656a3fb513134ce6c50b82ac (diff) | |
parent | 8e1eac35d265eacfbeb5f16be61e5d4caf45d1af (diff) |
Merge branch 'master' into issue6453issue6453
Diffstat (limited to 'src/proof/proof_checker.h')
-rw-r--r-- | src/proof/proof_checker.h | 206 |
1 files changed, 206 insertions, 0 deletions
diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h new file mode 100644 index 000000000..ac5531bf4 --- /dev/null +++ b/src/proof/proof_checker.h @@ -0,0 +1,206 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Proof checker utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_CHECKER_H +#define CVC5__PROOF__PROOF_CHECKER_H + +#include <map> + +#include "expr/node.h" +#include "proof/proof_rule.h" +#include "util/statistics_stats.h" + +namespace cvc5 { + +class ProofChecker; +class ProofNode; + +/** A virtual base class for checking a proof rule */ +class ProofRuleChecker +{ + public: + ProofRuleChecker() {} + virtual ~ProofRuleChecker() {} + /** + * This checks a single step in a proof. + * + * 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*, which is passed to checkInternal below. Rule checkers may + * convert premises to witness form when necessary. + * + * @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<Node>& children, + const std::vector<Node>& args); + + /** 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); + /** 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) {} + + protected: + /** + * This checks a single step in a proof. + * + * @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. + * @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. + */ + virtual Node checkInternal(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args) = 0; +}; + +/** Statistics class */ +class ProofCheckerStatistics +{ + public: + ProofCheckerStatistics(); + /** Counts the number of checks for each kind of proof rule */ + HistogramStat<PfRule> d_ruleChecks; + /** Total number of rule checks */ + IntStat d_totalRuleChecks; +}; + +/** A class for checking proofs */ +class ProofChecker +{ + public: + 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 + * well-formed. If expected is non-null, then we return null if pn does not + * prove expected. + * + * @param pn The proof node to check + * @param expected The (optional) formula that is the expected conclusion of + * the proof node. + * @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 check(ProofNode* pn, Node expected = Node::null()); + /** Same as above, with explicit arguments + * + * @param id The id of the proof node to check + * @param children 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. + * @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 check(PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& 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<Node>& cchildren, + const std::vector<Node>& args, + Node expected = Node::null(), + 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 if enableOutput is true. + */ + bool isPedanticFailure(PfRule id, + std::ostream& out, + bool enableOutput = true) const; + + private: + /** statistics class */ + ProofCheckerStatistics d_stats; + /** 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 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 enableOutput); +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__PROOF_CHECKER_H */ |