diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2020-04-28 10:54:12 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2020-04-28 10:54:12 -0500 |
| commit | d8dfbd8c67bc8871460e8ad86c73d96597b9b36a (patch) | |
| tree | a10ca23bb7739096e096460dbaa85e123b98fc0a /src/theory/theory_engine.h | |
| parent | b1e45ada416cc0faa41ea6f551312e7cf39e27d2 (diff) | |
Format
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index fa55a25fc..74ae31938 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -29,6 +29,7 @@ #include "base/check.h" #include "context/cdhashset.h" #include "expr/node.h" +#include "expr/proof_checker.h" #include "options/options.h" #include "options/smt_options.h" #include "options/theory_options.h" @@ -37,12 +38,12 @@ #include "theory/atom_requests.h" #include "theory/decision_manager.h" #include "theory/interrupted.h" +#include "theory/proof_engine_output_channel.h" #include "theory/rewriter.h" #include "theory/shared_terms_database.h" #include "theory/sort_inference.h" #include "theory/substitutions.h" #include "theory/term_registration_visitor.h" -#include "theory/proof_engine_output_channel.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" @@ -50,7 +51,6 @@ #include "util/resource_manager.h" #include "util/statistics_registry.h" #include "util/unsafe_interrupt_exception.h" -#include "expr/proof_checker.h" namespace CVC4 { @@ -386,7 +386,8 @@ class TheoryEngine { inline void addTheory(theory::TheoryId theoryId) { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); - d_theoryOut[theoryId] = new theory::ProofEngineOutputChannel(this, theoryId, d_userContext); + d_theoryOut[theoryId] = + new theory::ProofEngineOutputChannel(this, theoryId, d_userContext); d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], |