TheoryEngineModelBuilder::buildModel() is only called once with fullModel=true, within a SAT context. This fixes some outstanding model bugs.

Committing also a Clark-provided assertion the Model code to ensure the call is only done once per context.

(this commit was certified error- and warning-free by the test-and-commit script.)

4 files changed, 32 insertions, 27 deletions

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index d8b095161..e79c2c479 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -26,7 +26,7 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 
 TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels ) :
-  d_substitutions(c), d_equalityEngine(c, name), d_enableFuncModels(enableFuncModels)
+  d_substitutions(c), d_equalityEngine(c, name), d_modelBuilt(c, false), d_enableFuncModels(enableFuncModels)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
@@ -235,9 +235,10 @@ void TheoryModel::assertPredicate( Node a, bool polarity ){
       (a == d_false && (!polarity))) {
     return;
   }
-  if( a.getKind()==EQUAL ){
+  if (a.getKind() == EQUAL) {
+    Trace("model-builder-assertions") << "(assert " << (polarity ? " " : "(not ") << a << (polarity ? ");" : "));") << endl;
     d_equalityEngine.assertEquality( a, polarity, Node::null() );
-  }else{
+  } else {
     Trace("model-builder-assertions") << "(assert " << (polarity ? "" : "(not ") << a << (polarity ? ");" : "));") << endl;
     d_equalityEngine.assertPredicate( a, polarity, Node::null() );
     Assert(d_equalityEngine.consistent());
@@ -382,6 +383,10 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
 {
   TheoryModel* tm = (TheoryModel*)m;
 
+  // buildModel with fullModel = true should only be called once in any context
+  Assert(!tm->d_modelBuilt);
+  tm->d_modelBuilt = fullModel;
+
   // Reset model
   tm->reset();
 
diff --git a/src/theory/model.h b/src/theory/model.h
index 229d1f25e..5b691d4d9 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -47,6 +47,8 @@ public:
   /** true/false nodes */
   Node d_true;
   Node d_false;
+  context::CDO<bool> d_modelBuilt;
+
 protected:
   /** reset the model */
   virtual void reset();
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a76ad41cc..a4b918984 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -9,7 +9,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief The theory engine.
+ ** \brief The theory engine
  **
  ** The theory engine.
  **/
@@ -253,7 +253,7 @@ void TheoryEngine::check(Theory::Effort effort) {
   d_propEngine->checkTime();
 
   // Reset the interrupt flag
-  d_interrupted = false; 
+  d_interrupted = false;
 
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -319,24 +319,22 @@ void TheoryEngine::check(Theory::Effort effort) {
     }
 
     // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
-    if( effort == Theory::EFFORT_FULL &&
-        ! d_inConflict &&
-        ! d_lemmasAdded ) {
-      if( d_logicInfo.isQuantified() ){
-        //quantifiers engine must pass effort last call check
+    if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) {
+      if(d_logicInfo.isQuantified()) {
+        // quantifiers engine must pass effort last call check
         d_quantEngine->check(Theory::EFFORT_LAST_CALL);
         // if we have given up, then possibly flip decision
         if(options::flipDecision()) {
-          if(d_incomplete && !d_inConflict && !d_lemmasAdded) {
+          if(d_incomplete && !d_inConflict && !needCheck()) {
             if( ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->flipDecision() ) {
               d_incomplete = false;
             }
           }
         }
-        //if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built
-      }else if( options::produceModels() ){
-        //must build model at this point
-        d_curr_model_builder->buildModel( d_curr_model, true );
+        // if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built
+      } else if(options::produceModels()) {
+        // must build model at this point
+        d_curr_model_builder->buildModel(d_curr_model, true);
       }
     }
 
@@ -348,7 +346,7 @@ void TheoryEngine::check(Theory::Effort effort) {
 
   // If fulleffort, check all theories
   if(Dump.isOn("theory::fullcheck") && Theory::fullEffort(effort)) {
-    if (!d_inConflict && !d_lemmasAdded) {
+    if (!d_inConflict && !needCheck()) {
       dumpAssertions("theory::fullcheck");
     }
   }
@@ -428,7 +426,7 @@ void TheoryEngine::combineTheories() {
 
 void TheoryEngine::propagate(Theory::Effort effort) {
   // Reset the interrupt flag
-  d_interrupted = false; 
+  d_interrupted = false;
 
   // Definition of the statement that is to be run by every theory
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -440,7 +438,7 @@ void TheoryEngine::propagate(Theory::Effort effort) {
   }
 
   // Reset the interrupt flag
-  d_interrupted = false; 
+  d_interrupted = false;
 
   // Propagate for each theory using the statement above
   CVC4_FOR_EACH_THEORY;
@@ -587,7 +585,7 @@ TheoryModel* TheoryEngine::getModel() {
 
 bool TheoryEngine::presolve() {
   // Reset the interrupt flag
-  d_interrupted = false; 
+  d_interrupted = false;
 
   try {
     // Definition of the statement that is to be run by every theory
@@ -613,7 +611,7 @@ bool TheoryEngine::presolve() {
 
 void TheoryEngine::postsolve() {
   // Reset the interrupt flag
-  d_interrupted = false; 
+  d_interrupted = false;
 
   try {
     // Definition of the statement that is to be run by every theory
@@ -636,7 +634,7 @@ void TheoryEngine::postsolve() {
 
 void TheoryEngine::notifyRestart() {
   // Reset the interrupt flag
-  d_interrupted = false; 
+  d_interrupted = false;
 
   // Definition of the statement that is to be run by every theory
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -653,7 +651,7 @@ void TheoryEngine::notifyRestart() {
 
 void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
   // Reset the interrupt flag
-  d_interrupted = false; 
+  d_interrupted = false;
 
   // Definition of the statement that is to be run by every theory
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 8331ef61d..c65fb7ed7 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -232,7 +232,7 @@ class TheoryEngine {
 
     void safePoint() throw(theory::Interrupted, AssertionException) {
       if (d_engine->d_interrupted)
-        throw theory::Interrupted(); 
+        throw theory::Interrupted();
    }
 
     void conflict(TNode conflictNode) throw(AssertionException) {
@@ -394,8 +394,8 @@ class TheoryEngine {
   Node d_false;
 
   /** Whether we were just interrupted (or not) */
-  bool d_interrupted; 
-  
+  bool d_interrupted;
+
 public:
 
   /** Constructs a theory engine */
@@ -404,8 +404,8 @@ public:
   /** Destroys a theory engine */
   ~TheoryEngine();
 
-  void interrupt() throw(ModalException); 
-  
+  void interrupt() throw(ModalException);
+
   /**
    * Adds a theory. Only one theory per TheoryId can be present, so if
    * there is another theory it will be deleted.