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 | |
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')
-rw-r--r-- | src/prop/cnf_stream.h | 1 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 39 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 24 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 67 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 26 |
5 files changed, 43 insertions, 114 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index a9b786615..6b528bb81 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -31,7 +31,6 @@ #include "proof/proof_manager.h" #include "prop/registrar.h" #include "prop/theory_proxy.h" -#include "smt_util/lemma_channels.h" namespace CVC4 { diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index bac584236..05704c0fa 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -74,19 +74,22 @@ public: } }; -PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, - Context* userContext, std::ostream* replayLog, - ExprStream* replayStream, LemmaChannels* channels) : - d_inCheckSat(false), - d_theoryEngine(te), - d_decisionEngine(de), - d_context(satContext), - d_theoryProxy(NULL), - d_satSolver(NULL), - d_registrar(NULL), - d_cnfStream(NULL), - d_interrupted(false), - d_resourceManager(NodeManager::currentResourceManager()) +PropEngine::PropEngine(TheoryEngine* te, + DecisionEngine* de, + Context* satContext, + Context* userContext, + std::ostream* replayLog, + ExprStream* replayStream) + : d_inCheckSat(false), + d_theoryEngine(te), + d_decisionEngine(de), + d_context(satContext), + d_theoryProxy(NULL), + d_satSolver(NULL), + d_registrar(NULL), + d_cnfStream(NULL), + d_interrupted(false), + d_resourceManager(NodeManager::currentResourceManager()) { Debug("prop") << "Constructing the PropEngine" << endl; @@ -97,9 +100,13 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_cnfStream = new CVC4::prop::TseitinCnfStream( d_satSolver, d_registrar, userContext, true); - d_theoryProxy = new TheoryProxy( - this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, replayLog, - replayStream, channels); + d_theoryProxy = new TheoryProxy(this, + d_theoryEngine, + d_decisionEngine, + d_context, + d_cnfStream, + replayLog, + replayStream); d_satSolver->initialize(d_context, d_theoryProxy); d_decisionEngine->setSatSolver(d_satSolver); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index efbd82947..42b3ce65f 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -28,7 +28,6 @@ #include "expr/node.h" #include "options/options.h" #include "proof/proof_manager.h" -#include "smt_util/lemma_channels.h" #include "util/resource_manager.h" #include "util/result.h" #include "util/unsafe_interrupt_exception.h" @@ -94,14 +93,16 @@ class PropEngine { /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); -public: - + public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, - context::Context* userContext, std::ostream* replayLog, - ExprStream* replayStream, LemmaChannels* channels); + PropEngine(TheoryEngine*, + DecisionEngine*, + context::Context* satContext, + context::Context* userContext, + std::ostream* replayLog, + ExprStream* replayStream); /** * Destructor. @@ -115,7 +116,7 @@ public: * PropEngine and Theory). For now, there's nothing to do here in * the PropEngine. */ - void shutdown() { } + void shutdown() {} /** * Converts the given formula to CNF and assert the CNF to the SAT solver. @@ -135,7 +136,11 @@ public: * @param removable whether this lemma can be quietly removed based * on an activity heuristic (or not) */ - void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null()); + void assertLemma(TNode node, + bool negated, + bool removable, + ProofRule rule, + TNode from = TNode::null()); /** * If ever n is decided upon, it must be in the given phase. This @@ -243,8 +248,7 @@ public: */ bool properExplanation(TNode node, TNode expl) const; -};/* class PropEngine */ - +}; /* class PropEngine */ }/* CVC4::prop namespace */ }/* CVC4 namespace */ 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() { diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 61c556f34..0d76b473f 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -30,9 +30,6 @@ #include "expr/expr_stream.h" #include "expr/node.h" #include "prop/sat_solver.h" -#include "smt_util/lemma_channels.h" -#include "smt_util/lemma_input_channel.h" -#include "smt_util/lemma_output_channel.h" #include "theory/theory.h" #include "util/resource_manager.h" #include "util/statistics_registry.h" @@ -50,20 +47,19 @@ class CnfStream; /** * The proxy class that allows the SatSolver to communicate with the theories */ -class TheoryProxy { -public: +class TheoryProxy +{ + public: TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, DecisionEngine* decisionEngine, context::Context* context, CnfStream* cnfStream, std::ostream* replayLog, - ExprStream* replayStream, - LemmaChannels* globals); + ExprStream* replayStream); ~TheoryProxy(); - void theoryCheck(theory::Theory::Effort effort); void explainPropagation(SatLiteral l, SatClause& explanation); @@ -87,8 +83,6 @@ public: void notifyRestart(); - void notifyNewLemma(SatClause& lemma); - SatLiteral getNextReplayDecision(); void logDecision(SatLiteral lit); @@ -117,22 +111,12 @@ public: /** The theory engine we are using. */ TheoryEngine* d_theoryEngine; - - /** Container for inputChannel() and outputChannel(). */ - LemmaChannels* d_channels; - /** Stream on which to log replay events. */ std::ostream* d_replayLog; /** Stream for replaying decisions. */ ExprStream* d_replayStream; - /** The lemma input channel we are using. */ - LemmaInputChannel* inputChannel(); - - /** The lemma output channel we are using. */ - LemmaOutputChannel* outputChannel(); - /** Queue of asserted facts */ context::CDQueue<TNode> d_queue; @@ -147,7 +131,7 @@ public: */ IntStat d_replayedDecisions; -};/* class SatSolver */ +}; /* class SatSolver */ }/* CVC4::prop namespace */ |