diff options
Diffstat (limited to 'src/proof/proof_checker.cpp')
| -rw-r--r-- | src/proof/proof_checker.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp index 96f5197e3..6a9979f75 100644 --- a/src/proof/proof_checker.cpp +++ b/src/proof/proof_checker.cpp @@ -85,6 +85,11 @@ ProofCheckerStatistics::ProofCheckerStatistics() { } +ProofChecker::ProofChecker(uint32_t pclevel, theory::RewriteDb* rdb) + : d_pclevel(pclevel), d_rdb(rdb) +{ +} + Node ProofChecker::check(ProofNode* pn, Node expected) { return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected); @@ -303,6 +308,8 @@ ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id) return it->second; } +theory::RewriteDb* ProofChecker::getRewriteDatabase() { return d_rdb; } + uint32_t ProofChecker::getPedanticLevel(PfRule id) const { std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id); |