diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-13 19:50:19 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-13 19:50:19 -0500 |
commit | 53b3cf646549200e4986a47872abf6121fcbfe5b (patch) | |
tree | e33a7b9a1140c9196733b0917e18a8e8524d4683 /src/expr/proof_checker.cpp | |
parent | 0fdf29ba194b8f6763ae41bea05b3208345d89b9 (diff) |
(proof-new) Simplifications for proof rule checker interface (#5244)
Some of the interfaces in the proof rule checker are unnecessary now and can be deleted.
This also updates STRING_TRUST to have pedantic level 2.
Diffstat (limited to 'src/expr/proof_checker.cpp')
-rw-r--r-- | src/expr/proof_checker.cpp | 56 |
1 files changed, 13 insertions, 43 deletions
diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp index 7accd08dc..e839c0830 100644 --- a/src/expr/proof_checker.cpp +++ b/src/expr/proof_checker.cpp @@ -30,39 +30,6 @@ Node ProofRuleChecker::check(PfRule id, return checkInternal(id, children, args); } -Node ProofRuleChecker::checkChildrenArg(PfRule id, - const std::vector<Node>& children, - Node arg) -{ - return check(id, children, {arg}); -} -Node ProofRuleChecker::checkChildren(PfRule id, - const std::vector<Node>& 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<Node>& 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 @@ -194,17 +161,20 @@ Node ProofChecker::checkDebug(PfRule id, // 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 + if (Trace.isOn(traceTag)) { - Trace(traceTag) << " success" << std::endl; + Trace(traceTag) << "ProofChecker::checkDebug: " << id; + if (res.isNull()) + { + Trace(traceTag) << " failed, " << out.str() << std::endl; + } + else + { + Trace(traceTag) << " success" << std::endl; + } + Trace(traceTag) << "cchildren: " << cchildren << std::endl; + Trace(traceTag) << " args: " << args << std::endl; } - Trace(traceTag) << "cchildren: " << cchildren << std::endl; - Trace(traceTag) << " args: " << args << std::endl; return res; } @@ -335,7 +305,7 @@ 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 strictly below the required level " + << itp->second << " which is at or below the pedantic level " << d_pclevel << ")"; return true; } |