diff options
Diffstat (limited to 'src/prop/theory_proxy.cpp')
-rw-r--r-- | src/prop/theory_proxy.cpp | 35 |
1 files changed, 2 insertions, 33 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 557dcc413..38c99f551 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -18,7 +18,6 @@ #include "context/context.h" #include "decision/decision_engine.h" -#include "expr/expr_stream.h" #include "options/decision_options.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" @@ -37,24 +36,17 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, DecisionEngine* decisionEngine, context::Context* context, - CnfStream* cnfStream, - std::ostream* replayLog, - ExprStream* replayStream) + CnfStream* cnfStream) : d_propEngine(propEngine), d_cnfStream(cnfStream), d_decisionEngine(decisionEngine), d_theoryEngine(theoryEngine), - d_replayLog(replayLog), - d_replayStream(replayStream), - d_queue(context), - d_replayedDecisions("prop::theoryproxy::replayedDecisions", 0) + d_queue(context) { - smtStatisticsRegistry()->registerStat(&d_replayedDecisions); } TheoryProxy::~TheoryProxy() { /* nothing to do for now */ - smtStatisticsRegistry()->unregisterStat(&d_replayedDecisions); } void TheoryProxy::variableNotify(SatVariable var) { @@ -150,29 +142,6 @@ void TheoryProxy::notifyRestart() { d_theoryEngine->notifyRestart(); } -SatLiteral TheoryProxy::getNextReplayDecision() { -#ifdef CVC4_REPLAY - if(d_replayStream != NULL) { - Expr e = d_replayStream->nextExpr(); - if(!e.isNull()) { // we get null node when out of decisions to replay - // convert & return - ++d_replayedDecisions; - return d_cnfStream->getLiteral(e); - } - } -#endif /* CVC4_REPLAY */ - return undefSatLiteral; -} - -void TheoryProxy::logDecision(SatLiteral lit) { -#ifdef CVC4_REPLAY - if(d_replayLog != NULL) { - Assert(lit != undefSatLiteral) << "logging an `undef' decision ?!"; - (*d_replayLog) << d_cnfStream->getNode(lit) << std::endl; - } -#endif /* CVC4_REPLAY */ -} - void TheoryProxy::spendResource(ResourceManager::Resource r) { d_theoryEngine->spendResource(r); |