diff options
Diffstat (limited to 'src/proof/proof_checker.h')
| -rw-r--r-- | src/proof/proof_checker.h | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h index ac5531bf4..f1f10eedb 100644 --- a/src/proof/proof_checker.h +++ b/src/proof/proof_checker.h @@ -29,6 +29,10 @@ namespace cvc5 { class ProofChecker; class ProofNode; +namespace theory { +class RewriteDb; +} + /** A virtual base class for checking a proof rule */ class ProofRuleChecker { @@ -101,7 +105,7 @@ class ProofCheckerStatistics class ProofChecker { public: - ProofChecker(uint32_t pclevel = 0) : d_pclevel(pclevel) {} + ProofChecker(uint32_t pclevel = 0, theory::RewriteDb* rdb = nullptr); ~ProofChecker() {} /** * Return the formula that is proven by proof node pn, or null if pn is not @@ -162,7 +166,8 @@ class ProofChecker uint32_t plevel = 10); /** get checker for */ ProofRuleChecker* getCheckerFor(PfRule id); - + /** get the rewrite database */ + theory::RewriteDb* getRewriteDatabase(); /** * Get the pedantic level for id if it has been assigned a pedantic * level via registerTrustedChecker above, or zero otherwise. @@ -186,6 +191,8 @@ class ProofChecker std::map<PfRule, uint32_t> d_plevel; /** The pedantic level of this checker */ uint32_t d_pclevel; + /** Pointer to the rewrite database */ + theory::RewriteDb* d_rdb; /** * Check internal. This is used by check and checkDebug above. It writes * checking errors on out when enableOutput is true. We treat trusted checkers |