Minor improvements to theory model builder interface. (#2408)

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d75f7843de3a4337dc55a2aa7e8e7e262c86eec0..41ab451706a6be7f674e1ce234ada22d5198606f 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -636,17 +636,12 @@ void TheoryEngine::check(Theory::Effort effort) {
         AlwaysAssert(d_curr_model->isBuiltSuccess());
         if (options::produceModels())
         {
-          // if we are incomplete, there is no guarantee on the model.
-          // thus, we do not check the model here. (related to #1693)
-          // we also don't debug-check the model if the checkModels()
-          // is not enabled.
-          if (!d_incomplete && options::checkModels())
-          {
-            d_curr_model_builder->debugCheckModel(d_curr_model);
-          }
           // Do post-processing of model from the theories (used for THEORY_SEP
           // to construct heap model)
           postProcessModel(d_curr_model);
+          // also call the model builder's post-process model
+          d_curr_model_builder->postProcessModel(d_incomplete.get(),
+                                                 d_curr_model);
         }
       }
     }

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index bcc4f7eafd5ab7c774ff340880a93b386d962e55..a9742b2bad8198a63872a7e74eb5a20c37a5490d 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -808,16 +808,30 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
   {
     return false;
   }
-  else
+
+  tm->d_modelBuiltSuccess = true;
+  return true;
+}
+
+void TheoryEngineModelBuilder::postProcessModel(bool incomplete, Model* m)
+{
+  // if we are incomplete, there is no guarantee on the model.
+  // thus, we do not check the model here. (related to #1693).
+  if (incomplete)
   {
-    tm->d_modelBuiltSuccess = true;
-    return true;
+    return;
+  }
+  TheoryModel* tm = static_cast<TheoryModel*>(m);
+  Assert(tm != nullptr);
+  // debug-check the model if the checkModels() is enabled.
+  if (options::checkModels())
+  {
+    debugCheckModel(tm);
   }
 }
 
-void TheoryEngineModelBuilder::debugCheckModel(Model* m)
+void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm)
 {
-  TheoryModel* tm = (TheoryModel*)m;
 #ifdef CVC4_ASSERTIONS
   Assert(tm->isBuilt());
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);

diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index 68e8c6b49b6524b2d1f8ebb178aa0f0fcaa7a2a8..bff230b5c8eb51a10957e0d11106ba2d1ae433da 100644 (file)
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -68,13 +68,14 @@ class TheoryEngineModelBuilder : public ModelBuilder
    * are building fails to satisfy a quantified formula.
    */
   bool buildModel(Model* m) override;
-  /** Debug check model.
+
+  /** postprocess model
    *
-   * This throws an assertion failure if the model
-   * contains an equivalence class with two terms t1 and t2
-   * such that t1^M != t2^M.
+   * This is called when m is a model that will be returned to the user. This
+   * method checks the internal consistency of the model if we are in a debug
+   * build.
    */
-  void debugCheckModel(Model* m);
+  void postProcessModel(bool incomplete, Model* m);
 
  protected:
   /** pointer to theory engine */
@@ -102,6 +103,13 @@ class TheoryEngineModelBuilder : public ModelBuilder
   virtual void debugModel(TheoryModel* m) {}
   //-----------------------------------end virtual functions
 
+  /** Debug check model.
+   *
+   * This throws an assertion failure if the model contains an equivalence
+   * class with two terms t1 and t2 such that t1^M != t2^M.
+   */
+  void debugCheckModel(TheoryModel* m);
+
   /** is n assignable?
    *
    * A term n is assignable if its value