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/theory/theory_engine.h | 30 +++++++++++++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) (limited to 'src/theory/theory_engine.h') 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