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/prop/theory_proxy.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/prop/theory_proxy.cpp')
-rw-r--r-- | src/prop/theory_proxy.cpp | 67 |
1 files changed, 1 insertions, 66 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index cf7c9f0d9..557dcc413 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -25,8 +25,6 @@ #include "proof/cnf_proof.h" #include "smt/command.h" #include "smt/smt_statistics_registry.h" -#include "smt_util/lemma_input_channel.h" -#include "smt_util/lemma_output_channel.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" #include "util/statistics_registry.h" @@ -41,13 +39,11 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine, context::Context* context, CnfStream* cnfStream, std::ostream* replayLog, - ExprStream* replayStream, - LemmaChannels* channels) + ExprStream* replayStream) : d_propEngine(propEngine), d_cnfStream(cnfStream), d_decisionEngine(decisionEngine), d_theoryEngine(theoryEngine), - d_channels(channels), d_replayLog(replayLog), d_replayStream(replayStream), d_queue(context), @@ -61,17 +57,6 @@ TheoryProxy::~TheoryProxy() { smtStatisticsRegistry()->unregisterStat(&d_replayedDecisions); } -/** The lemma input channel we are using. */ -LemmaInputChannel* TheoryProxy::inputChannel() { - return d_channels->getLemmaInputChannel(); -} - -/** The lemma output channel we are using. */ -LemmaOutputChannel* TheoryProxy::outputChannel() { - return d_channels->getLemmaOutputChannel(); -} - - void TheoryProxy::variableNotify(SatVariable var) { d_theoryEngine->preRegister(getNode(SatLiteral(var))); } @@ -163,56 +148,6 @@ TNode TheoryProxy::getNode(SatLiteral lit) { void TheoryProxy::notifyRestart() { d_propEngine->spendResource(ResourceManager::Resource::RestartStep); d_theoryEngine->notifyRestart(); - - static uint32_t lemmaCount = 0; - - if(inputChannel() != NULL) { - while(inputChannel()->hasNewLemma()) { - Debug("shared") << "shared" << std::endl; - Expr lemma = inputChannel()->getNewLemma(); - Node asNode = lemma.getNode(); - asNode = theory::Rewriter::rewrite(asNode); - - if(d_shared.find(asNode) == d_shared.end()) { - d_shared.insert(asNode); - if(asNode.getKind() == kind::OR) { - ++lemmaCount; - if(lemmaCount % 1 == 0) { - Debug("shared") << "=) " << asNode << std::endl; - } - - d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID); - } else { - Debug("shared") << "=(" << asNode << std::endl; - } - } else { - Debug("shared") <<"drop shared " << asNode << std::endl; - } - } - } -} - -void TheoryProxy::notifyNewLemma(SatClause& lemma) { - Assert(lemma.size() > 0); - if(outputChannel() != NULL) { - if(lemma.size() == 1) { - // cannot share units yet - //options::lemmaOutputChannel()->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr()); - } else { - NodeBuilder<> b(kind::OR); - for(unsigned i = 0, i_end = lemma.size(); i < i_end; ++i) { - b << d_cnfStream->getNode(lemma[i]); - } - Node n = b; - - if(d_shared.find(n) == d_shared.end()) { - d_shared.insert(n); - outputChannel()->notifyNewLemma(n.toExpr()); - } else { - Debug("shared") <<"drop new " << n << std::endl; - } - } - } } SatLiteral TheoryProxy::getNextReplayDecision() { |