diff options
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 7b91191f9..03c733451 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -46,6 +46,7 @@ namespace cvc5 { class ResourceManager; class OutputManager; class TheoryEngineProofGenerator; +class ProofChecker; /** * A pair of a theory and a node. This is used to mark the flow of @@ -322,6 +323,9 @@ class TheoryEngine { theoryId, d_theoryTable[theoryId]->getTheoryRewriter()); } + /** Register theory proof rule checkers to the given proof checker */ + void initializeProofChecker(ProofChecker* pc); + void setPropEngine(prop::PropEngine* propEngine) { d_propEngine = propEngine; |