From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 20 Aug 2021 01:51:33 +0000 (-0500)
Subject: Eliminate eager model building (#7038)
X-Git-Tag: cvc5-1.0.0~1360
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6c47289737ca3c9a1345d4bf5666eaed4011edcc;p=cvc5.git

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 0ddac7202..61aed2009 100644
--- 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 f42d791e2..df8346de7 100644
--- 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 12d3fccfe..bd621126c 100644
--- 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 1c42e336f..3f2e589b3 100644
--- 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.