diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-27 10:56:27 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-11-27 10:56:27 -0600 |
commit | 24a904988e764189276794bf37b24d63d9f958cd (patch) | |
tree | 4460cc36a22e7b26dfa683d9f0e4c5c1469c1850 /src/smt | |
parent | 99a1da848889776586436f7f9aec9a1b088703c1 (diff) |
Lazy model construction in TheoryEngine (#2633)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 51 |
1 files changed, 21 insertions, 30 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7bf86f092..1de3e3756 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1022,12 +1022,6 @@ void SmtEngine::shutdown() { internalPop(true); } - // check to see if a postsolve() is pending - if(d_needPostsolve) { - d_theoryEngine->postsolve(); - d_needPostsolve = false; - } - if(d_propEngine != NULL) { d_propEngine->shutdown(); } @@ -3568,11 +3562,6 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, "(try --incremental)"); } - // check to see if a postsolve() is pending - if(d_needPostsolve) { - d_theoryEngine->postsolve(); - d_needPostsolve = false; - } // Note that a query has been made d_queryMade = true; // reset global negation @@ -3677,8 +3666,6 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, } } - d_propEngine->resetTrail(); - // Pop the context if (didInternalPush) { @@ -4122,7 +4109,7 @@ Expr SmtEngine::getValue(const Expr& ex) const } Trace("smt") << "--- getting value of " << n << endl; - TheoryModel* m = d_theoryEngine->getModel(); + TheoryModel* m = d_theoryEngine->getBuiltModel(); Node resultNode; if(m != NULL) { resultNode = m->getValue(n); @@ -4209,7 +4196,7 @@ vector<pair<Expr, Expr>> SmtEngine::getAssignment() if (d_assignments != nullptr) { TypeNode boolType = d_nodeManager->booleanType(); - TheoryModel* m = d_theoryEngine->getModel(); + TheoryModel* m = d_theoryEngine->getBuiltModel(); for (AssignmentSet::key_iterator i = d_assignments->key_begin(), iend = d_assignments->key_end(); i != iend; @@ -4260,7 +4247,6 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool if(/* userVisible && */ (!d_fullyInited || options::produceModels()) && (flags & ExprManager::VAR_FLAG_DEFINED) == 0) { - doPendingPops(); if(flags & ExprManager::VAR_FLAG_GLOBAL) { d_modelGlobalCommands.push_back(c.clone()); } else { @@ -4307,7 +4293,12 @@ Model* SmtEngine::getModel() { "Cannot get model when produce-models options is off."; throw ModalException(msg); } - TheoryModel* m = d_theoryEngine->getModel(); + TheoryModel* m = d_theoryEngine->getBuiltModel(); + + // Since model m is being returned to the user, we must ensure that this + // model object remains valid with future check-sat calls. Hence, we set + // the theory engine into "eager model building" mode. TODO #2648: revisit. + d_theoryEngine->setEagerModelBuilding(); if (options::modelCoresMode() != MODEL_CORES_NONE) { @@ -4341,7 +4332,7 @@ std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void) NodeManagerScope nms(d_nodeManager); Expr heap; Expr nil; - Model* m = getModel(); + Model* m = d_theoryEngine->getBuiltModel(); if (m->getHeapModel(heap, nil)) { return std::make_pair(heap, nil); @@ -4434,7 +4425,7 @@ void SmtEngine::checkModel(bool hardFailure) { // and if Notice() is on, the user gave --verbose (or equivalent). Notice() << "SmtEngine::checkModel(): generating model" << endl; - TheoryModel* m = d_theoryEngine->getModel(); + TheoryModel* m = d_theoryEngine->getBuiltModel(); // check-model is not guaranteed to succeed if approximate values were used if (m->hasApproximations()) @@ -4950,11 +4941,6 @@ void SmtEngine::push() throw ModalException("Cannot push when not solving incrementally (use --incremental)"); } - // check to see if a postsolve() is pending - if(d_needPostsolve) { - d_theoryEngine->postsolve(); - d_needPostsolve = false; - } // The problem isn't really "extended" yet, but this disallows // get-model after a push, simplifying our lives somewhat and @@ -4981,12 +4967,6 @@ void SmtEngine::pop() { throw ModalException("Cannot pop beyond the first user frame"); } - // check to see if a postsolve() is pending - if(d_needPostsolve) { - d_theoryEngine->postsolve(); - d_needPostsolve = false; - } - // The problem isn't really "extended" yet, but this disallows // get-model after a pop, simplifying our lives somewhat. It might // not be strictly necessary to do so, since the pops occur lazily, @@ -5036,7 +5016,13 @@ void SmtEngine::internalPop(bool immediate) { } void SmtEngine::doPendingPops() { + Trace("smt") << "SmtEngine::doPendingPops()" << endl; Assert(d_pendingPops == 0 || options::incrementalSolving()); + // check to see if a postsolve() is pending + if (d_needPostsolve) + { + d_propEngine->resetTrail(); + } while(d_pendingPops > 0) { TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); d_propEngine->pop(); @@ -5044,6 +5030,11 @@ void SmtEngine::doPendingPops() { d_userContext->pop(); --d_pendingPops; } + if (d_needPostsolve) + { + d_theoryEngine->postsolve(); + d_needPostsolve = false; + } } void SmtEngine::reset() |