Lazy model construction in TheoryEngine (#2633)

1 files changed, 29 insertions, 1 deletions

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
    *