1 files changed, 26 insertions, 30 deletions

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 0bbca88eb..5d575969f 100644..100755
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -153,27 +153,23 @@ int ModelEngine::checkModel(){
   //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps );
 
   //for debugging
-  if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){
-    for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
-         it != fm->d_rep_set.d_type_reps.end(); ++it ){
-      if( it->first.isSort() ){
-        Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
-        if( Trace.isOn("model-engine-debug") ){
-          Trace("model-engine-debug") << "        Reps : ";
-          for( size_t i=0; i<it->second.size(); i++ ){
-            Trace("model-engine-debug") << it->second[i] << "  ";
-          }
-          Trace("model-engine-debug") << std::endl;
-          Trace("model-engine-debug") << "   Term reps : ";
-          for( size_t i=0; i<it->second.size(); i++ ){
-            Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
-            Trace("model-engine-debug") << r << " ";
-          }
-          Trace("model-engine-debug") << std::endl;
-          Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
-          Trace("model-engine-debug") << "  Basis term : " << mbt << std::endl;
-        }
+  for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+       it != fm->d_rep_set.d_type_reps.end(); ++it ){
+    if( it->first.isSort() ){
+      Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+      Trace("model-engine-debug") << "        Reps : ";
+      for( size_t i=0; i<it->second.size(); i++ ){
+        Trace("model-engine-debug") << it->second[i] << "  ";
       }
+      Trace("model-engine-debug") << std::endl;
+      Trace("model-engine-debug") << "   Term reps : ";
+      for( size_t i=0; i<it->second.size(); i++ ){
+        Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
+        Trace("model-engine-debug") << r << " ";
+      }
+      Trace("model-engine-debug") << std::endl;
+      Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
+      Trace("model-engine-debug") << "  Basis term : " << mbt << std::endl;
     }
   }
 
@@ -221,11 +217,12 @@ int ModelEngine::checkModel(){
 
   //print debug information
   if( d_quantEngine->inConflict() ){
-    Trace("model-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound() << std::endl;
+    Trace("model-engine") << "Conflict, added lemmas = ";
   }else{
-    Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
-    Trace("model-engine") << d_totalLemmas << std::endl;
-  }
+    Trace("model-engine") << "Added Lemmas = ";
+  } 
+  Trace("model-engine") << d_addedLemmas << " / " << d_triedLemmas << " / ";
+  Trace("model-engine") << d_totalLemmas << std::endl;
   return d_addedLemmas;
 }
 
@@ -281,15 +278,15 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
     RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
     if( riter.setQuantifier( f ) ){
-      Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.d_incomplete << "..." << std::endl;
-      if( !riter.d_incomplete ){
+      Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
+      if( !riter.isIncomplete() ){
         int triedLemmas = 0;
         int addedLemmas = 0;
         while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
           //instantiation was not shown to be true, construct the match
           InstMatch m( f );
           for( int i=0; i<riter.getNumTerms(); i++ ){
-            m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) );
+            m.set( d_quantEngine, i, riter.getCurrentTerm( i ) );
           }
           Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
           triedLemmas++;
@@ -309,11 +306,10 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
         d_statistics.d_exh_inst_lemmas += addedLemmas;
       }
     }else{
-      Trace("fmf-exh-inst") << "...exhaustive instantiation failed to set, incomplete=" << riter.d_incomplete << "..." << std::endl;
-      Assert( riter.d_incomplete );
+      Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
     }
     //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
-    d_incomplete_check = d_incomplete_check || riter.d_incomplete;
+    d_incomplete_check = d_incomplete_check || riter.isIncomplete();
   }
 }