diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-02-26 00:08:20 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-26 00:08:20 -0800 |
| commit | 50c31e61ab240ccd551a0aea732f8b9a88d7fb32 (patch) | |
| tree | 30531d1f4813ed399209d198ca1eb75ac6f9dc30 /src/theory/theory_engine.h | |
| parent | b28ff31b6713791f27b4860f439aaa3f63aab9d7 (diff) | |
Remove portfolio leftovers (#3821)
Commit 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio
build but there were some leftovers. This commit removes them.
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0770efc7b..a5631059f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -34,7 +34,6 @@ #include "options/theory_options.h" #include "prop/prop_engine.h" #include "smt/command.h" -#include "smt_util/lemma_channels.h" #include "theory/atom_requests.h" #include "theory/decision_manager.h" #include "theory/interrupted.h" @@ -468,15 +467,12 @@ class TheoryEngine { bool d_interrupted; ResourceManager* d_resourceManager; - /** Container for lemma input and output channels. */ - LemmaChannels* d_channels; - -public: - + public: /** Constructs a theory engine */ - TheoryEngine(context::Context* context, context::UserContext* userContext, - RemoveTermFormulas& iteRemover, const LogicInfo& logic, - LemmaChannels* channels); + TheoryEngine(context::Context* context, + context::UserContext* userContext, + RemoveTermFormulas& iteRemover, + const LogicInfo& logic); /** Destroys a theory engine */ ~TheoryEngine(); @@ -491,12 +487,15 @@ public: * there is another theory it will be deleted. */ template <class TheoryClass> - inline void addTheory(theory::TheoryId theoryId) { + inline void addTheory(theory::TheoryId theoryId) + { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId); - d_theoryTable[theoryId] = - new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], - theory::Valuation(this), d_logicInfo); + d_theoryTable[theoryId] = new TheoryClass(d_context, + d_userContext, + *d_theoryOut[theoryId], + theory::Valuation(this), + d_logicInfo); } inline void setPropEngine(prop::PropEngine* propEngine) { |