diff options
Diffstat (limited to 'src/prop/theory_proxy.cpp')
-rw-r--r-- | src/prop/theory_proxy.cpp | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 10d2aee8c..9ed2202fe 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -25,6 +25,7 @@ #include "theory/rewriter.h" #include "expr/expr_stream.h" #include "decision/decision_engine.h" +#include "decision/options.h" #include "util/lemma_input_channel.h" #include "util/lemma_output_channel.h" @@ -94,7 +95,7 @@ SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) { if(stopSearch) { Trace("decision") << " *** Decision Engine stopped search *** " << std::endl; } - return Options::current()->decisionOptions.stopOnly ? undefSatLiteral : ret; + return options::decisionStopOnly() ? undefSatLiteral : ret; } bool TheoryProxy::theoryNeedCheck() const { @@ -115,10 +116,10 @@ void TheoryProxy::notifyRestart() { static uint32_t lemmaCount = 0; - if(Options::current()->lemmaInputChannel != NULL) { - while(Options::current()->lemmaInputChannel->hasNewLemma()) { + if(options::lemmaInputChannel() != NULL) { + while(options::lemmaInputChannel()->hasNewLemma()) { Debug("shared") << "shared" << std::endl; - Expr lemma = Options::current()->lemmaInputChannel->getNewLemma(); + Expr lemma = options::lemmaInputChannel()->getNewLemma(); Node asNode = lemma.getNode(); asNode = theory::Rewriter::rewrite(asNode); @@ -142,10 +143,10 @@ void TheoryProxy::notifyRestart() { void TheoryProxy::notifyNewLemma(SatClause& lemma) { Assert(lemma.size() > 0); - if(Options::current()->lemmaOutputChannel != NULL) { + if(options::lemmaOutputChannel() != NULL) { if(lemma.size() == 1) { // cannot share units yet - //Options::current()->lemmaOutputChannel->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr()); + //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) { @@ -155,7 +156,7 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) { if(d_shared.find(n) == d_shared.end()) { d_shared.insert(n); - Options::current()->lemmaOutputChannel->notifyNewLemma(n.toExpr()); + options::lemmaOutputChannel()->notifyNewLemma(n.toExpr()); } else { Debug("shared") <<"drop new " << n << std::endl; } @@ -165,8 +166,8 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) { SatLiteral TheoryProxy::getNextReplayDecision() { #ifdef CVC4_REPLAY - if(Options::current()->replayStream != NULL) { - Expr e = Options::current()->replayStream->nextExpr(); + if(options::replayStream() != NULL) { + Expr e = options::replayStream()->nextExpr(); if(!e.isNull()) { // we get null node when out of decisions to replay // convert & return return d_cnfStream->getLiteral(e); @@ -179,9 +180,9 @@ SatLiteral TheoryProxy::getNextReplayDecision() { void TheoryProxy::logDecision(SatLiteral lit) { #ifdef CVC4_REPLAY - if(Options::current()->replayLog != NULL) { + if(options::replayLog() != NULL) { Assert(lit != undefSatLiteral, "logging an `undef' decision ?!"); - *Options::current()->replayLog << d_cnfStream->getNode(lit) << std::endl; + *options::replayLog() << d_cnfStream->getNode(lit) << std::endl; } #endif /* CVC4_REPLAY */ } |