Lazy model construction in TheoryEngine (#2633)

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<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()
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<TNode> 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<Node, Node>& 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<Node, Node, NodeHashFunction> NodeMap;
   typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap;
@@ -350,6 +352,13 @@ class TheoryEngine {
   context::CDO<bool> 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.
    */
   void conflict(TNode conflict, theory::TheoryId theoryId);
@@ -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
    *