From 24a904988e764189276794bf37b24d63d9f958cd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Nov 2018 10:56:27 -0600 Subject: Lazy model construction in TheoryEngine (#2633) --- src/smt/smt_engine.cpp | 51 ++++++++++++++++++-------------------------- src/theory/theory_engine.cpp | 29 +++++++++++++++++++++---- src/theory/theory_engine.h | 30 +++++++++++++++++++++++++- 3 files changed, 75 insertions(+), 35 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& 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& 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> 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 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() diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 54ac272cc..fb4075d82 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -297,10 +297,12 @@ TheoryEngine::TheoryEngine(context::Context* context, d_aloc_curr_model(false), d_curr_model_builder(nullptr), d_aloc_curr_model_builder(false), + d_eager_model_building(false), d_ppCache(), d_possiblePropagations(context), d_hasPropagated(context), d_inConflict(context, false), + d_inSatMode(false), d_hasShutDown(false), d_incomplete(context, false), d_propagationMap(context), @@ -619,9 +621,12 @@ void TheoryEngine::check(Theory::Effort effort) { } if (!d_inConflict && !needCheck()) { - if (options::produceModels() && !d_curr_model->isBuilt()) + // If d_eager_model_building is false, then we only mark that we + // are in "SAT mode". We build the model later only if the user asks + // for it via getBuiltModel. + d_inSatMode = true; + if (d_eager_model_building && !d_curr_model->isBuilt()) { - // must build model at this point d_curr_model_builder->buildModel(d_curr_model); } } @@ -852,6 +857,7 @@ bool TheoryEngine::collectModelInfo(theory::TheoryModel* m) } } } + Trace("model-builder") << " CollectModelInfo boolean variables" << std::endl; // Get the Boolean variables vector boolVars; d_propEngine->getBooleanVariables(boolVars); @@ -862,6 +868,8 @@ bool TheoryEngine::collectModelInfo(theory::TheoryModel* m) hasValue = d_propEngine->hasValue(var, value); // TODO: Assert that hasValue is true? if (!hasValue) { + Trace("model-builder-assertions") + << " has no value : " << var << std::endl; value = false; } Trace("model-builder-assertions") << "(assert" << (value ? " " : " (not ") << var << (value ? ");" : "));") << endl; @@ -882,11 +890,23 @@ void TheoryEngine::postProcessModel( theory::TheoryModel* m ){ } } -/* get model */ TheoryModel* TheoryEngine::getModel() { return d_curr_model; } +TheoryModel* TheoryEngine::getBuiltModel() +{ + if (!d_curr_model->isBuilt()) + { + // If this method was called, we should be in SAT mode, and produceModels + // should be true. + AlwaysAssert(d_inSatMode && options::produceModels()); + // must build model at this point + d_curr_model_builder->buildModel(d_curr_model); + } + return d_curr_model; +} + void TheoryEngine::getSynthSolutions(std::map& sol_map) { if (d_quantEngine) @@ -929,7 +949,8 @@ void TheoryEngine::postsolve() { // Reset the decision manager. This clears its decision strategies, which are // user-context-dependent. d_decManager->reset(); - + // no longer in SAT mode + d_inSatMode = false; // Reset the interrupt flag d_interrupted = false; bool CVC4_UNUSED wasInConflict = d_inConflict; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 09f986686..c3281c9ba 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -214,6 +214,8 @@ class TheoryEngine { */ theory::TheoryEngineModelBuilder* d_curr_model_builder; bool d_aloc_curr_model_builder; + /** are we in eager model building mode? (see setEagerModelBuilding). */ + bool d_eager_model_building; typedef std::unordered_map NodeMap; typedef std::unordered_map TNodeMap; @@ -349,6 +351,13 @@ class TheoryEngine { */ context::CDO d_inConflict; + /** + * Are we in "SAT mode"? In this state, the user can query for the model. + * This corresponds to the state in Figure 4.1, page 52 of the SMT-LIB + * standard, version 2.6. + */ + bool d_inSatMode; + /** * Called by the theories to notify of a conflict. */ @@ -733,9 +742,28 @@ public: void postProcessModel( theory::TheoryModel* m ); /** - * Get the current model + * Get the pointer to the model object used by this theory engine. */ theory::TheoryModel* getModel(); + /** + * Get the current model for the current set of assertions. This method + * should only be called immediately after a satisfiable or unknown + * response to a check-sat call, and only if produceModels is true. + * + * If the model is not already built, this will cause this theory engine + * to build to the model. + */ + theory::TheoryModel* getBuiltModel(); + /** set eager model building + * + * If this method is called, then this TheoryEngine will henceforth build + * its model immediately after every satisfiability check that results + * in a satisfiable or unknown result. The motivation for this mode is to + * accomodate API users that get the model object from the TheoryEngine, + * where we want to ensure that this model is always valid. + * TODO (#2648): revisit this. + */ + void setEagerModelBuilding() { d_eager_model_building = true; } /** get synth solutions * -- cgit v1.2.3