diff options
author | Tim King <taking@google.com> | 2016-01-05 16:29:44 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-05 16:29:44 -0800 |
commit | 5eabda0f55cee3be81aa7ae126269c32e818322f (patch) | |
tree | b873e4cb8e5d37ff3bb70596494bc5964aaef135 /src/prop/theory_proxy.cpp | |
parent | b717513e2a1d956c4456d13e0625957fc84c2449 (diff) |
Add SmtGlobals Class
- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library.
- The option replayLog has been removed due to inconsistent memory management.
- SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently.
- There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine.
- A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction.
- Selected classes have been given a copy of this pointer in their constructors.
- Removed the dependence on Node from Result. Moving Result back into util/.
Diffstat (limited to 'src/prop/theory_proxy.cpp')
-rw-r--r-- | src/prop/theory_proxy.cpp | 55 |
1 files changed, 46 insertions, 9 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 386b12391..d0830b9a5 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -31,6 +31,43 @@ namespace CVC4 { namespace prop { +TheoryProxy::TheoryProxy(PropEngine* propEngine, + TheoryEngine* theoryEngine, + DecisionEngine* decisionEngine, + context::Context* context, + CnfStream* cnfStream, + SmtGlobals* globals) + : d_propEngine(propEngine), + d_cnfStream(cnfStream), + d_decisionEngine(decisionEngine), + d_theoryEngine(theoryEngine), + d_globals(globals), + d_queue(context) +{} + +TheoryProxy::~TheoryProxy() { + /* nothing to do for now */ +} + +/** The lemma input channel we are using. */ +LemmaInputChannel* TheoryProxy::inputChannel() { + return d_globals->getLemmaInputChannel(); +} + +/** The lemma output channel we are using. */ +LemmaOutputChannel* TheoryProxy::outputChannel() { + return d_globals->getLemmaOutputChannel(); +} + +std::ostream* TheoryProxy::replayLog() { + return d_globals->getReplayLog(); +} + +ExprStream* TheoryProxy::replayStream() { + return d_globals->getReplayStream(); +} + + void TheoryProxy::variableNotify(SatVariable var) { d_theoryEngine->preRegister(getNode(SatLiteral(var))); } @@ -108,10 +145,10 @@ void TheoryProxy::notifyRestart() { static uint32_t lemmaCount = 0; - if(options::lemmaInputChannel() != NULL) { - while(options::lemmaInputChannel()->hasNewLemma()) { + if(inputChannel() != NULL) { + while(inputChannel()->hasNewLemma()) { Debug("shared") << "shared" << std::endl; - Expr lemma = options::lemmaInputChannel()->getNewLemma(); + Expr lemma = inputChannel()->getNewLemma(); Node asNode = lemma.getNode(); asNode = theory::Rewriter::rewrite(asNode); @@ -135,7 +172,7 @@ void TheoryProxy::notifyRestart() { void TheoryProxy::notifyNewLemma(SatClause& lemma) { Assert(lemma.size() > 0); - if(options::lemmaOutputChannel() != NULL) { + if(outputChannel() != NULL) { if(lemma.size() == 1) { // cannot share units yet //options::lemmaOutputChannel()->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr()); @@ -148,7 +185,7 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) { if(d_shared.find(n) == d_shared.end()) { d_shared.insert(n); - options::lemmaOutputChannel()->notifyNewLemma(n.toExpr()); + outputChannel()->notifyNewLemma(n.toExpr()); } else { Debug("shared") <<"drop new " << n << std::endl; } @@ -158,8 +195,8 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) { SatLiteral TheoryProxy::getNextReplayDecision() { #ifdef CVC4_REPLAY - if(options::replayStream() != NULL) { - Expr e = options::replayStream()->nextExpr(); + if(replayStream() != NULL) { + Expr e = replayStream()->nextExpr(); if(!e.isNull()) { // we get null node when out of decisions to replay // convert & return ++d_replayedDecisions; @@ -172,9 +209,9 @@ SatLiteral TheoryProxy::getNextReplayDecision() { void TheoryProxy::logDecision(SatLiteral lit) { #ifdef CVC4_REPLAY - if(options::replayLog() != NULL) { + if(replayLog() != NULL) { Assert(lit != undefSatLiteral, "logging an `undef' decision ?!"); - *options::replayLog() << d_cnfStream->getNode(lit) << std::endl; + (*replayLog()) << d_cnfStream->getNode(lit) << std::endl; } #endif /* CVC4_REPLAY */ } |