Eliminate eager model building (#7038)

Previously, we had a special case to support users who directly accessed the model object pointer in the old API.

The special case ensure that the information in the model was eagerly updated after each "sat" response, in the case that the user did not re-request a pointer to the model.

Since users no longer can access the internal model pointer (apart from GetModelCommand), this special case is no longer necessary.

This PR should make us slightly faster for incremental benchmarks where the user asks for the model on some but not all "sat" responses.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0ddac720286525118d52974477ff7ae8e77c7534..61aed2009b84623957f736e82de9cf2e9be9c78d 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1192,12 +1192,11 @@ Model* SmtEngine::getModel() {
 
   Model* m = getAvailableModel("get model");
 
-  // 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.
-  TheoryEngine* te = getTheoryEngine();
-  Assert(te != nullptr);
-  te->setEagerModelBuilding();
+  // Notice that the returned model is (currently) accessed by the
+  // GetModelCommand only, and is not returned to the user. The information
+  // in that model may become stale after it is returned. This is safe
+  // since GetModelCommand always calls this command again when it prints
+  // a model.
 
   if (d_env->getOptions().smt.modelCoresMode
       != options::ModelCoresMode::NONE)

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f42d791e2660ac160e88be8487a7f2ee4af66691..df8346de7fff3962eb6a2f50ecc9ebf21bc6df6c 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -250,6 +250,8 @@ class CVC5_EXPORT SmtEngine
   /**
    * Get the model (only if immediately preceded by a SAT or NOT_ENTAILED
    * query).  Only permitted if produce-models is on.
+   *
+   * TODO (issues#287): eliminate this method.
    */
   smt::Model* getModel();
 

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 12d3fccfebade3731fe6320e23e34330de969cb5..bd621126c0dea7c6915710d587bcd44bd63296c1 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -236,7 +236,6 @@ TheoryEngine::TheoryEngine(Env& env)
       d_quantEngine(nullptr),
       d_decManager(new DecisionManager(d_env.getUserContext())),
       d_relManager(nullptr),
-      d_eager_model_building(false),
       d_inConflict(d_env.getContext(), false),
       d_inSatMode(false),
       d_hasShutDown(false),
@@ -539,14 +538,9 @@ void TheoryEngine::check(Theory::Effort effort) {
       }
       if (!d_inConflict && !needCheck())
       {
-        // 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.
+        // 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_tc->buildModel();
-        }
       }
     }
 

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 1c42e336f5eb5260cd25fcaa8fb24598879a3894..3f2e589b374fcdbf0b4b1958d4f46690edac1bd4 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -562,16 +562,6 @@ class TheoryEngine {
    * call).
    */
   bool buildModel();
-  /** 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 the theory associated to a given Node.