merge from fmf-devel branch. more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models

1 files changed, 216 insertions, 170 deletions

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index cbeeed8d0..b5a9ee74c 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -15,7 +15,6 @@
  **/
 
 #include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/rep_set_iterator.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
@@ -25,11 +24,11 @@
 #include "theory/arrays/theory_arrays_model.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 
 //#define ME_PRINT_WARNINGS
 
 #define EVAL_FAIL_SKIP_MULTIPLE
-//#define ONE_QUANT_PER_ROUND
 
 using namespace std;
 using namespace CVC4;
@@ -40,96 +39,97 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
 //Model Engine constructor
-ModelEngine::ModelEngine( QuantifiersEngine* qe ) :
+ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
 QuantifiersModule( qe ),
-d_builder( qe ),
-d_rel_domain( qe->getModel() ){
+d_builder( c, qe ),
+d_rel_domain( qe, qe->getModel() ){
 
 }
 
 void ModelEngine::check( Theory::Effort e ){
   if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){
-    //first, check if we can minimize the model further
-    if( !((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){
-      return;
-    }
+    FirstOrderModel* fm = d_quantEngine->getModel();
     //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
     int addedLemmas = 0;
+    Trace("model-engine") << "---Model Engine Round---" << std::endl;
     if( d_builder.optUseModel() ){
       //check if any quantifiers are un-initialized
-      for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-        Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
+      for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+        Node f = fm->getAssertedQuantifier( i );
         addedLemmas += initializeQuantifier( f );
       }
     }
-    if( addedLemmas==0 ){
-      //quantifiers are initialized, we begin an instantiation round
-      double clSet = 0;
-      if( Trace.isOn("model-engine") ){
-        clSet = double(clock())/double(CLOCKS_PER_SEC);
-        Trace("model-engine") << "---Model Engine Round---" << std::endl;
-      }
-      Debug("fmf-model-debug") << "---Begin Instantiation Round---" << std::endl;
-      ++(d_statistics.d_inst_rounds);
-      //reset the quantifiers engine
-      d_quantEngine->resetInstantiationRound( e );
-      //initialize the model
-      Debug("fmf-model-debug") << "Build model..." << std::endl;
-      d_builder.buildModel( d_quantEngine->getModel() );
-      d_quantEngine->d_model_set = true;
-      //if builder has lemmas, add and return
-      if( d_builder.d_addedLemmas>0 ){
-        addedLemmas += (int)d_builder.d_addedLemmas;
-      }else{
-        //print debug
-        Debug("fmf-model-complete") << std::endl;
-        debugPrint("fmf-model-complete");
-        //verify we are SAT by trying exhaustive instantiation
-        if( optUseRelevantDomain() ){
-          d_rel_domain.compute();
+    if( addedLemmas>0 ){
+      Trace("model-engine") << "Initialize, Added Lemmas = " << addedLemmas << std::endl;
+    }
+    //two effort levels: first try exhaustive instantiation without axioms, then with.
+    int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
+    for( int effort=startEffort; effort<2; effort++ ){
+      // for effort = 0, we only instantiate non-axioms
+      // for effort = 1, we instantiate everything
+      if( addedLemmas==0 ){
+        //quantifiers are initialized, we begin an instantiation round
+        double clSet = 0;
+        if( Trace.isOn("model-engine") ){
+          clSet = double(clock())/double(CLOCKS_PER_SEC);
         }
-        d_triedLemmas = 0;
-        d_testLemmas = 0;
-        d_relevantLemmas = 0;
-        d_totalLemmas = 0;
-        Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl;
-        for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-          Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
-          if( d_builder.d_quant_sat.find( f )==d_builder.d_quant_sat.end() ){
-            addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() );
-            if( optOneQuantPerRound() && addedLemmas>0 ){
-              break;
-            }
-          }
-#ifdef ME_PRINT_WARNINGS
-          if( addedLemmas>10000 ){
-            break;
+        ++(d_statistics.d_inst_rounds);
+        //reset the quantifiers engine
+        d_quantEngine->resetInstantiationRound( e );
+        //initialize the model
+        Trace("model-engine-debug") << "Build model..." << std::endl;
+        d_builder.setEffort( effort );
+        d_builder.buildModel( fm, false );
+        //if builder has lemmas, add and return
+        if( d_builder.d_addedLemmas>0 ){
+          addedLemmas += (int)d_builder.d_addedLemmas;
+        }else{
+          Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
+          //let the strong solver verify that the model is minimal
+          uf::StrongSolverTheoryUf* uf_ss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
+          //for debugging, this will if there are terms in the model that the strong solver was not notified of
+          uf_ss->debugModel( fm );
+          Trace("model-engine-debug") << "Check model..." << std::endl;
+          //print debug
+          Debug("fmf-model-complete") << std::endl;
+          debugPrint("fmf-model-complete");
+          //successfully built an acceptable model, now check it
+          checkModel( addedLemmas );
+          //print debug information
+          if( Trace.isOn("model-engine") ){
+            Trace("model-engine") << "Instantiate axioms : " << ( d_builder.d_considerAxioms ? "yes" : "no" ) << std::endl;
+            Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
+            Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+            double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+            Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
           }
-#endif
-        }
-        Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
-        Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
-        if( Trace.isOn("model-engine") ){
-          Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
-          Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
-          double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-          Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
         }
-#ifdef ME_PRINT_WARNINGS
-        if( addedLemmas>10000 ){
-          Debug("fmf-exit") << std::endl;
-          debugPrint("fmf-exit");
-          exit( 0 );
+      }
+      if( addedLemmas==0 ){
+        //if we have not added lemmas yet and axiomInstMode=trust, then we are done
+        if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){
+          //we must return unknown if an axiom is asserted
+          if( effort==0 ){
+            d_incomplete_check = true;
+          }
+          break;
         }
-#endif
       }
     }
     if( addedLemmas==0 ){
-      //CVC4 will answer SAT
-      Debug("fmf-consistent") << std::endl;
+      Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
+      //CVC4 will answer SAT or unknown
+      Trace("fmf-consistent") << std::endl;
       debugPrint("fmf-consistent");
-      // finish building the model in the standard way
-      d_builder.finishProcessBuildModel( d_quantEngine->getModel() );
+      if( options::produceModels() ){
+        // finish building the model in the standard way
+        d_builder.buildModel( fm, true );
+        d_quantEngine->d_model_set = true;
+      }
+      //if the check was incomplete, we must set incomplete flag
+      if( d_incomplete_check ){
+        d_quantEngine->getOutputChannel().setIncomplete();
+      }
     }else{
       //otherwise, the search will continue
       d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
@@ -154,11 +154,7 @@ bool ModelEngine::optUseRelevantDomain(){
 }
 
 bool ModelEngine::optOneQuantPerRound(){
-#ifdef ONE_QUANT_PER_ROUND
-  return true;
-#else
-  return false;
-#endif
+  return options::fmfOneQuantPerRound();
 }
 
 int ModelEngine::initializeQuantifier( Node f ){
@@ -178,11 +174,13 @@ int ModelEngine::initializeQuantifier( Node f ){
     //    Notice() << "Unhandled phase req: " << n << std::endl;
     //  }
     //}
+    std::vector< Node > vars;
     std::vector< Node > ics;
     std::vector< Node > terms;
     for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
       Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
       Node t = d_quantEngine->getTermDatabase()->getModelBasisTerm( ic.getType() );
+      vars.push_back( f[0][j] );
       ics.push_back( ic );
       terms.push_back( t );
       //calculate the basis match for f
@@ -193,67 +191,137 @@ int ModelEngine::initializeQuantifier( Node f ){
     Node n = d_quantEngine->getTermDatabase()->getCounterexampleBody( f );
     Node gn = n.substitute( ics.begin(), ics.end(), terms.begin(), terms.end() );
     d_quantEngine->getTermDatabase()->registerModelBasis( n, gn );
-    //add model basis instantiation
-    if( d_quantEngine->addInstantiation( f, terms ) ){
-      return 1;
-    }else{
-      //shouldn't happen usually, but will occur if x != y is a required literal for f.
-      //Notice() << "No model basis for " << f << std::endl;
-      ++(d_statistics.d_num_quants_init_fail);
+    if( d_builder.optInstGen() ){
+      //add model basis instantiation
+      if( d_quantEngine->addInstantiation( f, vars, terms ) ){
+        return 1;
+      }else{
+        //shouldn't happen usually, but will occur if x != y is a required literal for f.
+        //Notice() << "No model basis for " << f << std::endl;
+        ++(d_statistics.d_num_quants_init_fail);
+      }
     }
   }
   return 0;
 }
 
-int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
-  int tests = 0;
-  int addedLemmas = 0;
-  int triedLemmas = 0;
-  Debug("inst-fmf-ei") << "Add matches for " << f << "..." << std::endl;
-  Debug("inst-fmf-ei") << "   Instantiation Constants: ";
-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
+void ModelEngine::checkModel( int& addedLemmas ){
+  FirstOrderModel* fm = d_quantEngine->getModel();
+  //for debugging
+  if( Trace.isOn("model-engine") ){
+    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") << "   ";
+        for( size_t i=0; i<it->second.size(); i++ ){
+          Trace("model-engine-debug") << it->second[i] << "  ";
+        }
+        Trace("model-engine-debug") << std::endl;
+      }
+    }
+  }
+  //verify we are SAT by trying exhaustive instantiation
+  d_incomplete_check = false;
+  if( optUseRelevantDomain() ){
+    d_rel_domain.compute();
   }
-  Debug("inst-fmf-ei") << std::endl;
-  if( d_builder.d_quant_selection_lits[f].empty() ){
-    Debug("inst-fmf-ei") << "WARNING: " << f << " has no model literal definitions (is f clausified?)" << std::endl;
+  d_triedLemmas = 0;
+  d_testLemmas = 0;
+  d_relevantLemmas = 0;
+  d_totalLemmas = 0;
+  Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl;
+  for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+    Node f = fm->getAssertedQuantifier( i );
+    addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() );
 #ifdef ME_PRINT_WARNINGS
-    Message() << "WARNING: " << f << " has no model literal definitions (is f clausified?)" << std::endl;
+    if( addedLemmas>10000 ){
+      Debug("fmf-exit") << std::endl;
+      debugPrint("fmf-exit");
+      exit( 0 );
+    }
 #endif
-  }else{
-    Debug("inst-fmf-ei") << "  Model literal definitions:" << std::endl;
-    for( size_t i=0; i<d_builder.d_quant_selection_lits[f].size(); i++ ){
-      Debug("inst-fmf-ei") << "    " << d_builder.d_quant_selection_lits[f][i] << std::endl;
+    if( optOneQuantPerRound() && addedLemmas>0 ){
+      break;
     }
   }
-  RepSetIterator riter( f, d_quantEngine->getModel() );
-  //set the domain for the iterator (the sufficient set of instantiations to try)
-  if( useRelInstDomain ){
-    riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
+  Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
+  Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+}
+
+int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
+  int addedLemmas = 0;
+  //keep track of total instantiations for statistics
+  int totalInst = 1;
+  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+    TypeNode tn = f[0][i].getType();
+    if( d_quantEngine->getModel()->d_rep_set.hasType( tn ) ){
+      totalInst = totalInst * (int)d_quantEngine->getModel()->d_rep_set.d_type_reps[ tn ].size();
+    }
   }
-  RepSetEvaluator reval( d_quantEngine->getModel(), &riter );
-  while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
-    d_testLemmas++;
-    if( d_builder.optUseModel() ){
-      //see if instantiation is already true in current model
-      Debug("fmf-model-eval") << "Evaluating ";
-      riter.debugPrintSmall("fmf-model-eval");
-      Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
-      tests++;
-      //if evaluate(...)==1, then the instantiation is already true in the model
-      //  depIndex is the index of the least significant variable that this evaluation relies upon
-      int depIndex = riter.getNumTerms()-1;
-      int eval = reval.evaluate( d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), depIndex );
+  d_totalLemmas += totalInst;
+  //if we need to consider this quantifier on this iteration
+  if( d_builder.isQuantifierActive( f ) ){
+    Trace("rel-dom") << "Exhaustive instantiate " << f << std::endl;
+    if( useRelInstDomain ){
+      Trace("rel-dom") << "Relevant domain : " << std::endl;
+      for( size_t i=0; i<d_rel_domain.d_quant_inst_domain[f].size(); i++ ){
+        Trace("rel-dom") << "   " << i << " : ";
+        for( size_t j=0; j<d_rel_domain.d_quant_inst_domain[f][i].size(); j++ ){
+          Trace("rel-dom") << d_rel_domain.d_quant_inst_domain[f][i][j] << " ";
+        }
+        Trace("rel-dom") << std::endl;
+      }
+    }
+    int tests = 0;
+    int triedLemmas = 0;
+    Debug("inst-fmf-ei") << "Add matches for " << f << "..." << std::endl;
+    Debug("inst-fmf-ei") << "   Instantiation Constants: ";
+    for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+      Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
+    }
+    Debug("inst-fmf-ei") << std::endl;
+    RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
+    riter.setQuantifier( f );
+    //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;
+    //set the domain for the iterator (the sufficient set of instantiations to try)
+    if( useRelInstDomain ){
+      riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
+    }
+    d_quantEngine->getModel()->resetEvaluate();
+    while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
+      d_testLemmas++;
+      int eval = 0;
+      int depIndex;
+      if( d_builder.optUseModel() ){
+        //see if instantiation is already true in current model
+        Debug("fmf-model-eval") << "Evaluating ";
+        riter.debugPrintSmall("fmf-model-eval");
+        Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+        tests++;
+        //if evaluate(...)==1, then the instantiation is already true in the model
+        //  depIndex is the index of the least significant variable that this evaluation relies upon
+        depIndex = riter.getNumTerms()-1;
+        eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), depIndex, &riter );
+        if( eval==1 ){
+          Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
+        }else{
+          Debug("fmf-model-eval") << "  Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
+        }
+      }
       if( eval==1 ){
-        Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
+        //instantiation is already true -> skip
         riter.increment2( depIndex );
       }else{
-        Debug("fmf-model-eval") << "  Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
+        //instantiation was not shown to be true, construct the match
         InstMatch m;
-        riter.getMatch( d_quantEngine, m );
+        for( int i=0; i<riter.getNumTerms(); i++ ){
+          m.set( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, riter.d_index_order[i] ), riter.getTerm( i ) );
+        }
         Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
         triedLemmas++;
         d_triedLemmas++;
+        //add as instantiation
         if( d_quantEngine->addInstantiation( f, m ) ){
           addedLemmas++;
 #ifdef EVAL_FAIL_SKIP_MULTIPLE
@@ -270,70 +338,48 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
           riter.increment();
         }
       }
-    }else{
-      InstMatch m;
-      riter.getMatch( d_quantEngine, m );
-      Debug("fmf-model-eval") << "* Add instantiation " << std::endl;
-      triedLemmas++;
-      d_triedLemmas++;
-      if( d_quantEngine->addInstantiation( f, m ) ){
-        addedLemmas++;
-      }
-      riter.increment();
     }
-  }
-  d_statistics.d_eval_formulas += reval.d_eval_formulas;
-  d_statistics.d_eval_uf_terms += reval.d_eval_uf_terms;
-  d_statistics.d_eval_lits += reval.d_eval_lits;
-  d_statistics.d_eval_lits_unknown += reval.d_eval_lits_unknown;
-  int totalInst = 1;
-  int relevantInst = 1;
-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    totalInst = totalInst * (int)d_quantEngine->getModel()->d_rep_set.d_type_reps[ f[0][i].getType() ].size();
-    relevantInst = relevantInst * (int)riter.d_domain[i].size();
-  }
-  d_totalLemmas += totalInst;
-  d_relevantLemmas += relevantInst;
-  Debug("inst-fmf-ei") << "Finished: " << std::endl;
-  Debug("inst-fmf-ei") << "   Inst Total: " << totalInst << std::endl;
-  Debug("inst-fmf-ei") << "   Inst Relevant: " << relevantInst << std::endl;
-  Debug("inst-fmf-ei") << "   Inst Tried: " << triedLemmas << std::endl;
-  Debug("inst-fmf-ei") << "   Inst Added: " << addedLemmas << std::endl;
-  Debug("inst-fmf-ei") << "   # Tests: " << tests << std::endl;
-///-----------
+    d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas;
+    d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms;
+    d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits;
+    d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown;
+    int relevantInst = 1;
+    for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+      relevantInst = relevantInst * (int)riter.d_domain[i].size();
+    }
+    d_relevantLemmas += relevantInst;
+    Debug("inst-fmf-ei") << "Finished: " << std::endl;
+    Debug("inst-fmf-ei") << "   Inst Total: " << totalInst << std::endl;
+    Debug("inst-fmf-ei") << "   Inst Relevant: " << relevantInst << std::endl;
+    Debug("inst-fmf-ei") << "   Inst Tried: " << triedLemmas << std::endl;
+    Debug("inst-fmf-ei") << "   Inst Added: " << addedLemmas << std::endl;
+    Debug("inst-fmf-ei") << "   # Tests: " << tests << std::endl;
 #ifdef ME_PRINT_WARNINGS
-  if( addedLemmas>1000 ){
-    Notice() << "WARNING: many instantiations produced for " << f << ": " << std::endl;
-    Notice() << "   Inst Total: " << totalInst << std::endl;
-    Notice() << "   Inst Relevant: " << totalRelevant << std::endl;
-    Notice() << "   Inst Tried: " << triedLemmas << std::endl;
-    Notice() << "   Inst Added: " << addedLemmas << std::endl;
-    Notice() << "   # Tests: " << tests << std::endl;
-    Notice() << std::endl;
-    if( !d_builder.d_quant_selection_lits[f].empty() ){
-      Notice() << "  Model literal definitions:" << std::endl;
-      for( size_t i=0; i<d_builder.d_quant_selection_lits[f].size(); i++ ){
-        Notice() << "    " << d_builder.d_quant_selection_lits[f][i] << std::endl;
-      }
+    if( addedLemmas>1000 ){
+      Notice() << "WARNING: many instantiations produced for " << f << ": " << std::endl;
+      Notice() << "   Inst Total: " << totalInst << std::endl;
+      Notice() << "   Inst Relevant: " << totalRelevant << std::endl;
+      Notice() << "   Inst Tried: " << triedLemmas << std::endl;
+      Notice() << "   Inst Added: " << addedLemmas << std::endl;
+      Notice() << "   # Tests: " << tests << std::endl;
       Notice() << std::endl;
     }
-  }
 #endif
-///-----------
+  }
   return addedLemmas;
 }
 
 void ModelEngine::debugPrint( const char* c ){
-  Debug( c ) << "Quantifiers: " << std::endl;
+  Trace( c ) << "Quantifiers: " << std::endl;
   for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
-    Debug( c ) << "   ";
-    if( d_builder.d_quant_sat.find( f )!=d_builder.d_quant_sat.end() ){
-      Debug( c ) << "*SAT* ";
+    Trace( c ) << "   ";
+    if( !d_builder.isQuantifierActive( f ) ){
+      Trace( c ) << "*Inactive* ";
     }else{
-      Debug( c ) << "      ";
+      Trace( c ) << "           ";
     }
-    Debug( c ) << f << std::endl;
+    Trace( c ) << f << std::endl;
   }
   //d_quantEngine->getModel()->debugPrint( c );
 }