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.cpp | |
| 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.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9ef228865..dec648688 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -37,7 +37,6 @@ #include "proof/theory_proof.h" #include "smt/logic_exception.h" #include "smt/term_formula_removal.h" -#include "smt_util/lemma_output_channel.h" #include "smt_util/node_visitor.h" #include "theory/arith/arith_ite_utils.h" #include "theory/bv/theory_bv_utils.h" @@ -314,8 +313,7 @@ void TheoryEngine::eqNotifyNewClass(TNode t){ TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveTermFormulas& iteRemover, - const LogicInfo& logicInfo, - LemmaChannels* channels) + const LogicInfo& logicInfo) : d_propEngine(nullptr), d_decisionEngine(nullptr), d_context(context), @@ -349,7 +347,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_false(), d_interrupted(false), d_resourceManager(NodeManager::currentResourceManager()), - d_channels(channels), d_inPreregister(false), d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), @@ -1867,11 +1864,6 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, << CheckSatCommand(n.toExpr()); } - // Share with other portfolio threads - if(d_channels->getLemmaOutputChannel() != NULL) { - d_channels->getLemmaOutputChannel()->notifyNewLemma(node.toExpr()); - } - AssertionPipeline additionalLemmas; // Run theory preprocessing, maybe |