diff options
Diffstat (limited to 'src/expr/proof_checker.h')
| -rw-r--r-- | src/expr/proof_checker.h | 57 |
1 files changed, 40 insertions, 17 deletions
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h index 65ad9f24d..ab9c24434 100644 --- a/src/expr/proof_checker.h +++ b/src/expr/proof_checker.h @@ -5,7 +5,7 @@ ** Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** 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.\endverbatim ** @@ -54,21 +54,15 @@ class ProofRuleChecker Node check(PfRule id, const std::vector<Node>& children, const std::vector<Node>& args); - /** Single arg version */ - Node checkChildrenArg(PfRule id, const std::vector<Node>& children, Node arg); - /** No arg version */ - Node checkChildren(PfRule id, const std::vector<Node>& 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<Node>& 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); + /** 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 +100,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,25 +150,54 @@ 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 if enableOutput is true. + */ + bool isPedanticFailure(PfRule id, + std::ostream& out, + bool enableOutput = true) const; + private: /** statistics class */ ProofCheckerStatistics d_stats; - /** Maps proof steps to their checker */ + /** 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. 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 |