Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --fmf-fun-rlv, fixes bug 723.

9 files changed, 196 insertions, 214 deletions

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 72057e734..6b756428b 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -326,13 +326,15 @@ QModelBuilder( c, qe ){
 }
 
 void FullModelChecker::preProcessBuildModel(TheoryModel* m, bool fullModel) {
+  //standard pre-process
+  preProcessBuildModelStd( m, fullModel );
+  
   FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
   if( !fullModel ){
     Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
     d_preinitialized_types.clear();
     //traverse equality engine
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
-    std::map< TypeNode, int > typ_num;
     while( !eqcs_i.isFinished() ){
       TypeNode tr = (*eqcs_i).getType();
       d_preinitialized_types[tr] = true;
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index b30c2addb..a5ec16e3a 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -39,13 +39,57 @@ TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe
 
 }
 
-bool QModelBuilder::isQuantifierActive( Node f ) {
-  return d_qe->hasOwnership( f );
+bool QModelBuilder::optUseModel() {
+  return options::mbqiMode()!=MBQI_NONE || options::fmfBound();
 }
 
+void QModelBuilder::preProcessBuildModel(TheoryModel* m, bool fullModel) {
+  preProcessBuildModelStd( m, fullModel );
+}
 
-bool QModelBuilder::optUseModel() {
-  return options::mbqiMode()!=MBQI_NONE || options::fmfBound();
+void QModelBuilder::preProcessBuildModelStd(TheoryModel* m, bool fullModel) {
+  if( !fullModel ){
+    if( options::fmfEmptySorts() || options::fmfFunWellDefinedRelevant() ){
+      FirstOrderModel * fm = (FirstOrderModel*)m;
+      //traverse equality engine
+      std::map< TypeNode, bool > eqc_usort;
+      eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
+      while( !eqcs_i.isFinished() ){
+        TypeNode tr = (*eqcs_i).getType();
+        eqc_usort[tr] = true;
+        ++eqcs_i;
+      }
+      //look at quantified formulas
+      for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+        Node q = fm->getAssertedQuantifier( i, true );
+        if( fm->isQuantifierActive( q ) ){
+          //check if any of these quantified formulas can be set inactive
+          if( options::fmfEmptySorts() ){
+            for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+              TypeNode tn = q[0][i].getType();
+              //we are allowed to assume the type is empty
+              if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){
+                Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl;
+                fm->setQuantifierActive( q, false );
+              }
+            }
+          }else if( options::fmfFunWellDefinedRelevant() ){
+            if( q[0].getNumChildren()==1 ){
+              TypeNode tn = q[0][0].getType();
+              if( tn.getAttribute(AbsTypeFunDefAttribute()) ){
+                //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl;
+                //we are allowed to assume the introduced type is empty
+                if( eqc_usort.find( tn )==eqc_usort.end() ){
+                  Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl;
+                  fm->setQuantifierActive( q, false );
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+  }
 }
 
 void QModelBuilder::debugModel( FirstOrderModel* fm ){
@@ -152,9 +196,9 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
       Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
       //check if any quantifiers are un-initialized
       for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-        Node f = fm->getAssertedQuantifier( i );
-        if( isQuantifierActive( f ) ){
-          int lems = initializeQuantifier( f, f );
+        Node q = fm->getAssertedQuantifier( i );
+        if( d_qe->getModel()->isQuantifierActive( q ) ){
+          int lems = initializeQuantifier( q, q );
           d_statistics.d_init_inst_gen_lemmas += lems;
           d_addedLemmas += lems;
           if( d_qe->inConflict() ){
@@ -173,13 +217,10 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
         analyzeModel( fm );
         //analyze the quantifiers
         Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
-        d_quant_sat.clear();
         d_uf_prefs.clear();
         for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-          Node f = fm->getAssertedQuantifier( i );
-          if( isQuantifierActive( f ) ){
-            analyzeQuantifier( fm, f );
-          }
+          Node q = fm->getAssertedQuantifier( i );
+          analyzeQuantifier( fm, q );
         }
 
         //if applicable, find exceptions to model via inst-gen
@@ -194,15 +235,13 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
           Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
           for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
             Node f = fm->getAssertedQuantifier( i );
-            if( isQuantifierActive( f ) ){
+            if( d_qe->getModel()->isQuantifierActive( f ) ){
               int lems = doInstGen( fm, f );
               d_statistics.d_inst_gen_lemmas += lems;
               d_addedLemmas += lems;
               //temporary
               if( lems>0 ){
                 d_numQuantInstGen++;
-              }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
-                d_numQuantSat++;
               }else if( hasInstGen( f ) ){
                 d_numQuantNoInstGen++;
               }else{
@@ -211,7 +250,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
               if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){
                 break;
               }
-            }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
+            }else{
               d_numQuantSat++;
             }
           }
@@ -236,16 +275,6 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
             Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl;
             constructModelUf( fm, it->first );
           }
-          /*
-          //build model for arrays
-          for( std::map< Node, arrays::ArrayModel >::iterator it = fm->d_array_model.begin(); it != fm->d_array_model.end(); ++it ){
-            //consult the model basis select term
-            // i.e. the default value for array A is the value of select( A, e ), where e is the model basis term
-            TypeNode tn = it->first.getType();
-            Node selModelBasis = NodeManager::currentNM()->mkNode( SELECT, it->first, fm->getTermDatabase()->getModelBasisTerm( tn[0] ) );
-            it->second.setDefaultValue( fm->getRepresentative( selModelBasis ) );
-          }
-          */
           Trace("model-engine-debug") << "Done building models." << std::endl;
         }
       }
@@ -378,10 +407,6 @@ QModelBuilderIG::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown);
 }
 
-bool QModelBuilderIG::isQuantifierActive( Node f ){
-  return d_qe->hasOwnership( f ) && d_quant_sat.find( f )==d_quant_sat.end();
-}
-
 bool QModelBuilderIG::isTermActive( Node n ){
   return d_qe->getTermDatabase()->isTermActive( n ) || //it is not congruent to another active term
          ( n.getAttribute(ModelBasisArgAttribute())!=0 && d_basisNoMatch.find( n )==d_basisNoMatch.end() ); //or it has model basis arguments
@@ -389,7 +414,6 @@ bool QModelBuilderIG::isTermActive( Node n ){
                                                                                                       //to another active term
 }
 
-
 //do exhaustive instantiation
 int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
   if( optUseModel() ){
@@ -502,133 +526,135 @@ int QModelBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) {
 }
 
 void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
-  FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
-  Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
-  //the pro/con preferences for this quantifier
-  std::vector< Node > pro_con[2];
-  //the terms in the selection literal we choose
-  std::vector< Node > selectionLitTerms;
-  Trace("inst-gen-debug-quant") << "Inst-gen analyze " << f << std::endl;
-  //for each asserted quantifier f,
-  // - determine selection literals
-  // - check which function/predicates have good and bad definitions for satisfying f
-  if( d_phase_reqs.find( f )==d_phase_reqs.end() ){
-    d_phase_reqs[f].initialize( d_qe->getTermDatabase()->getInstConstantBody( f ), true );
-  }
-  int selectLitScore = -1;
-  for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.end(); ++it ){
-    //the literal n is phase-required for quantifier f
-    Node n = it->first;
-    Node gn = d_qe->getTermDatabase()->getModelBasis( f, n );
-    Debug("fmf-model-req") << "   Req: " << n << " -> " << it->second << std::endl;
-    bool value;
-    //if the corresponding ground abstraction literal has a SAT value
-    if( d_qe->getValuation().hasSatValue( gn, value ) ){
-      //collect the non-ground uf terms that this literal contains
-      //  and compute if all of the symbols in this literal have
-      //  constant definitions.
-      bool isConst = true;
-      std::vector< Node > uf_terms;
-      if( TermDb::hasInstConstAttr(n) ){
-        isConst = false;
-        if( gn.getKind()==APPLY_UF ){
-          uf_terms.push_back( gn );
-          isConst = hasConstantDefinition( gn );
-        }else if( gn.getKind()==EQUAL ){
-          isConst = true;
-          for( int j=0; j<2; j++ ){
-            if( TermDb::hasInstConstAttr(n[j]) ){
-              if( n[j].getKind()==APPLY_UF &&
-                  fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){
-                uf_terms.push_back( gn[j] );
-                isConst = isConst && hasConstantDefinition( gn[j] );
-              }else{
-                isConst = false;
+  if( d_qe->getModel()->isQuantifierActive( f ) ){
+    FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
+    Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
+    //the pro/con preferences for this quantifier
+    std::vector< Node > pro_con[2];
+    //the terms in the selection literal we choose
+    std::vector< Node > selectionLitTerms;
+    Trace("inst-gen-debug-quant") << "Inst-gen analyze " << f << std::endl;
+    //for each asserted quantifier f,
+    // - determine selection literals
+    // - check which function/predicates have good and bad definitions for satisfying f
+    if( d_phase_reqs.find( f )==d_phase_reqs.end() ){
+      d_phase_reqs[f].initialize( d_qe->getTermDatabase()->getInstConstantBody( f ), true );
+    }
+    int selectLitScore = -1;
+    for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.end(); ++it ){
+      //the literal n is phase-required for quantifier f
+      Node n = it->first;
+      Node gn = d_qe->getTermDatabase()->getModelBasis( f, n );
+      Debug("fmf-model-req") << "   Req: " << n << " -> " << it->second << std::endl;
+      bool value;
+      //if the corresponding ground abstraction literal has a SAT value
+      if( d_qe->getValuation().hasSatValue( gn, value ) ){
+        //collect the non-ground uf terms that this literal contains
+        //  and compute if all of the symbols in this literal have
+        //  constant definitions.
+        bool isConst = true;
+        std::vector< Node > uf_terms;
+        if( TermDb::hasInstConstAttr(n) ){
+          isConst = false;
+          if( gn.getKind()==APPLY_UF ){
+            uf_terms.push_back( gn );
+            isConst = hasConstantDefinition( gn );
+          }else if( gn.getKind()==EQUAL ){
+            isConst = true;
+            for( int j=0; j<2; j++ ){
+              if( TermDb::hasInstConstAttr(n[j]) ){
+                if( n[j].getKind()==APPLY_UF &&
+                    fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){
+                  uf_terms.push_back( gn[j] );
+                  isConst = isConst && hasConstantDefinition( gn[j] );
+                }else{
+                  isConst = false;
+                }
               }
             }
           }
         }
-      }
-      //check if the value in the SAT solver matches the preference according to the quantifier
-      int pref = 0;
-      if( value!=it->second ){
-        //we have a possible selection literal
-        bool selectLit = d_quant_selection_lit[f].isNull();
-        bool selectLitConstraints = true;
-        //it is a constantly defined selection literal : the quantifier is sat
-        if( isConst ){
-          selectLit = selectLit || d_quant_sat.find( f )==d_quant_sat.end();
-          d_quant_sat[f] = true;
-          //check if choosing this literal would add any additional constraints to default definitions
-          selectLitConstraints = false;
-          for( int j=0; j<(int)uf_terms.size(); j++ ){
-            Node op = uf_terms[j].getOperator();
-            if( d_uf_prefs[op].d_reconsiderModel ){
-              selectLitConstraints = true;
+        //check if the value in the SAT solver matches the preference according to the quantifier
+        int pref = 0;
+        if( value!=it->second ){
+          //we have a possible selection literal
+          bool selectLit = d_quant_selection_lit[f].isNull();
+          bool selectLitConstraints = true;
+          //it is a constantly defined selection literal : the quantifier is sat
+          if( isConst ){
+            selectLit = selectLit || d_qe->getModel()->isQuantifierActive( f );
+            d_qe->getModel()->setQuantifierActive( f, false );
+            //check if choosing this literal would add any additional constraints to default definitions
+            selectLitConstraints = false;
+            for( int j=0; j<(int)uf_terms.size(); j++ ){
+              Node op = uf_terms[j].getOperator();
+              if( d_uf_prefs[op].d_reconsiderModel ){
+                selectLitConstraints = true;
+              }
+            }
+            if( !selectLitConstraints ){
+              selectLit = true;
             }
           }
-          if( !selectLitConstraints ){
-            selectLit = true;
+          //also check if it is naturally a better literal
+          if( !selectLit ){
+            int score = getSelectionScore( uf_terms );
+            //Trace("inst-gen-debug") << "Check " << score << " < " << selectLitScore << std::endl;
+            selectLit = score<selectLitScore;
           }
-        }
-        //also check if it is naturally a better literal
-        if( !selectLit ){
-          int score = getSelectionScore( uf_terms );
-          //Trace("inst-gen-debug") << "Check " << score << " < " << selectLitScore << std::endl;
-          selectLit = score<selectLitScore;
-        }
-        //see if we wish to choose this as a selection literal
-        d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() );
-        if( selectLit ){
-          selectLitScore = getSelectionScore( uf_terms );
-          Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl;
-          Trace("inst-gen-debug") << "  flags: " << isConst << " " << selectLitConstraints << " " << selectLitScore << std::endl;
-          d_quant_selection_lit[f] = value ? n : n.notNode();
-          selectionLitTerms.clear();
-          selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() );
-          if( !selectLitConstraints ){
-            break;
+          //see if we wish to choose this as a selection literal
+          d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() );
+          if( selectLit ){
+            selectLitScore = getSelectionScore( uf_terms );
+            Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl;
+            Trace("inst-gen-debug") << "  flags: " << isConst << " " << selectLitConstraints << " " << selectLitScore << std::endl;
+            d_quant_selection_lit[f] = value ? n : n.notNode();
+            selectionLitTerms.clear();
+            selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() );
+            if( !selectLitConstraints ){
+              break;
+            }
           }
+          pref = 1;
+        }else{
+          pref = -1;
         }
-        pref = 1;
-      }else{
-        pref = -1;
-      }
-      //if we are not yet SAT, so we will add to preferences
-      if( d_quant_sat.find( f )==d_quant_sat.end() ){
-        Debug("fmf-model-prefs") << "  It is " << ( pref==1 ? "pro" : "con" );
-        Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
-        for( int j=0; j<(int)uf_terms.size(); j++ ){
-          pro_con[ pref==1 ? 0 : 1 ].push_back( uf_terms[j] );
+        //if we are not yet SAT, so we will add to preferences
+        if( d_qe->getModel()->isQuantifierActive( f ) ){
+          Debug("fmf-model-prefs") << "  It is " << ( pref==1 ? "pro" : "con" );
+          Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
+          for( int j=0; j<(int)uf_terms.size(); j++ ){
+            pro_con[ pref==1 ? 0 : 1 ].push_back( uf_terms[j] );
+          }
         }
       }
     }
-  }
-  //process information about selection literal for f
-  if( !d_quant_selection_lit[f].isNull() ){
-    d_quant_selection_lit_terms[f].insert( d_quant_selection_lit_terms[f].begin(), selectionLitTerms.begin(), selectionLitTerms.end() );
-    for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
-      d_term_selection_lit[ selectionLitTerms[i] ] = d_quant_selection_lit[f];
-      d_op_selection_terms[ selectionLitTerms[i].getOperator() ].push_back( selectionLitTerms[i] );
-    }
-  }else{
-    Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals" << std::endl;
-  }
-  //process information about requirements and preferences of quantifier f
-  if( d_quant_sat.find( f )!=d_quant_sat.end() ){
-    Debug("fmf-model-prefs") << "  * Constant SAT due to definition of ops: ";
-    for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
-      Debug("fmf-model-prefs") << selectionLitTerms[i] << " ";
-      d_uf_prefs[ selectionLitTerms[i].getOperator() ].d_reconsiderModel = false;
+    //process information about selection literal for f
+    if( !d_quant_selection_lit[f].isNull() ){
+      d_quant_selection_lit_terms[f].insert( d_quant_selection_lit_terms[f].begin(), selectionLitTerms.begin(), selectionLitTerms.end() );
+      for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
+        d_term_selection_lit[ selectionLitTerms[i] ] = d_quant_selection_lit[f];
+        d_op_selection_terms[ selectionLitTerms[i].getOperator() ].push_back( selectionLitTerms[i] );
+      }
+    }else{
+      Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals" << std::endl;
     }
-    Debug("fmf-model-prefs") << std::endl;
-  }else{
-    //note quantifier's value preferences to models
-    for( int k=0; k<2; k++ ){
-      for( int j=0; j<(int)pro_con[k].size(); j++ ){
-        Node op = pro_con[k][j].getOperator();
-        Node r = fmig->getRepresentative( pro_con[k][j] );
-        d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
+    //process information about requirements and preferences of quantifier f
+    if( !d_qe->getModel()->isQuantifierActive( f ) ){
+      Debug("fmf-model-prefs") << "  * Constant SAT due to definition of ops: ";
+      for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
+        Debug("fmf-model-prefs") << selectionLitTerms[i] << " ";
+        d_uf_prefs[ selectionLitTerms[i].getOperator() ].d_reconsiderModel = false;
+      }
+      Debug("fmf-model-prefs") << std::endl;
+    }else{
+      //note quantifier's value preferences to models
+      for( int k=0; k<2; k++ ){
+        for( int j=0; j<(int)pro_con[k].size(); j++ ){
+          Node op = pro_con[k][j].getOperator();
+          Node r = fmig->getRepresentative( pro_con[k][j] );
+          d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
+        }
       }
     }
   }
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 9b89e5ef6..e1f586585 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -33,11 +33,11 @@ protected:
   context::CDO< FirstOrderModel* > d_curr_model;
   //quantifiers engine
   QuantifiersEngine* d_qe;
+  void preProcessBuildModel(TheoryModel* m, bool fullModel);
+  void preProcessBuildModelStd(TheoryModel* m, bool fullModel);
 public:
   QModelBuilder( context::Context* c, QuantifiersEngine* qe );
   virtual ~QModelBuilder() throw() {}
-  // is quantifier active?
-  virtual bool isQuantifierActive( Node f );
   //do exhaustive instantiation  
   // 0 :  failed, but resorting to true exhaustive instantiation may work
   // >0 : success
@@ -105,7 +105,7 @@ protected:
   virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 0;
 protected:
   //map from quantifiers to if are SAT
-  std::map< Node, bool > d_quant_sat;
+  //std::map< Node, bool > d_quant_sat;
   //which quantifiers have been initialized
   std::map< Node, bool > d_quant_basis_match_added;
   //map from quantifiers to model basis match
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 20f5eae7b..9496f630d 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -183,14 +183,16 @@ int ModelEngine::checkModel(){
   if( Trace.isOn("model-engine") ){
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
       Node f = fm->getAssertedQuantifier( i );
-      int totalInst = 1;
-      for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
-        TypeNode tn = f[0][j].getType();
-        if( fm->d_rep_set.hasType( tn ) ){
-          totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+      if( d_quantEngine->getModel()->isQuantifierActive( f ) && d_quantEngine->hasOwnership( f, this ) ){
+        int totalInst = 1;
+        for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
+          TypeNode tn = f[0][j].getType();
+          if( fm->d_rep_set.hasType( tn ) ){
+            totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+          }
         }
+        d_totalLemmas += totalInst;
       }
-      d_totalLemmas += totalInst;
     }
   }
 
@@ -203,7 +205,7 @@ int ModelEngine::checkModel(){
       Node q = fm->getAssertedQuantifier( i, true );
       Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl;
       //determine if we should check this quantifier
-      if( considerQuantifiedFormula( q ) ){
+      if( d_quantEngine->getModel()->isQuantifierActive( q ) && d_quantEngine->hasOwnership( q, this ) ){
         exhaustiveInstantiate( q, e );
         if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){
           break;
@@ -230,38 +232,7 @@ int ModelEngine::checkModel(){
   return d_addedLemmas;
 }
 
-bool ModelEngine::considerQuantifiedFormula( Node q ) {
-  if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){ 
-    Trace("model-engine-debug") << "Model builder inactive : " << q << std::endl;
-    return false;
-  }else if( !d_quantEngine->getModel()->isQuantifierActive( q ) ){
-    Trace("model-engine-debug") << "Model inactive : " << q << std::endl;
-    return false;
-  }else{
-    if( options::fmfEmptySorts() ){
-      for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-        TypeNode tn = q[0][i].getType();
-        //we are allowed to assume the type is empty
-        if( tn.isSort() && d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn )==0 ){
-          Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl;
-          return false;
-        }
-      }
-    }else if( options::fmfFunWellDefinedRelevant() ){
-      if( q[0].getNumChildren()==1 ){
-        TypeNode tn = q[0][0].getType();
-        if( tn.getAttribute(AbsTypeFunDefAttribute()) ){
-          //we are allowed to assume the introduced type is empty
-          if( d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn )==0 ){
-            Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl;
-            return false;
-          }
-        }
-      }
-    }
-    return true;
-  }
-}
+
 
 void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   //first check if the builder can do the exhaustive instantiation
@@ -331,13 +302,15 @@ void ModelEngine::debugPrint( const char* c ){
   Trace( c ) << "Quantifiers: " << std::endl;
   for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
-    Trace( c ) << "   ";
-    if( !considerQuantifiedFormula( q ) ){
-      Trace( c ) << "*Inactive* ";
-    }else{
-      Trace( c ) << "           ";
+    if( d_quantEngine->hasOwnership( q, this ) ){
+      Trace( c ) << "   ";
+      if( !d_quantEngine->getModel()->isQuantifierActive( q ) ){
+        Trace( c ) << "*Inactive* ";
+      }else{
+        Trace( c ) << "           ";
+      }
+      Trace( c ) << q << std::endl;
     }
-    Trace( c ) << q << std::endl;
   }
   //d_quantEngine->getModel()->debugPrint( c );
 }
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index e89be8d2b..728539e91 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -34,8 +34,6 @@ private:
 private:
   //check model
   int checkModel();
-  //consider quantified formula
-  bool considerQuantifiedFormula( Node q );
   //exhaustively instantiate quantifier (possibly using mbqi)
   void exhaustiveInstantiate( Node f, int effort = 0 );
 private:
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 3168a78e2..a3b6293fb 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -766,7 +766,7 @@ void QuantifiersEngine::propagate( Theory::Effort level ){
 }
 
 Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){
-  unsigned min_priority;
+  unsigned min_priority = 0;
   Node dec;  
   for( unsigned i=0; i<d_modules.size(); i++ ){
     Node n = d_modules[i]->getNextDecisionRequest( priority );
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 86bcb2cac..a2797dd8d 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -29,7 +29,6 @@ void RepSet::clear(){
   d_type_complete.clear();
   d_tmap.clear();
   d_values_to_terms.clear();
-  d_type_rlv_rep.clear();
 }
 
 bool RepSet::hasRep( TypeNode tn, Node n ) {
@@ -117,15 +116,6 @@ bool RepSet::complete( TypeNode t ){
   }
 }
 
-int RepSet::getNumRelevantGroundReps( TypeNode t ) {
-  std::map< TypeNode, int >::iterator it = d_type_rlv_rep.find( t );
-  if( it==d_type_rlv_rep.end() ){
-    return 0;
-  }else{
-    return it->second;
-  }
-}
-
 void RepSet::toStream(std::ostream& out){
   for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
     if( !it->first.isFunction() && !it->first.isPredicate() ){
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index ee927de86..a56fba39b 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -33,7 +33,6 @@ public:
   std::map< TypeNode, std::vector< Node > > d_type_reps;
   std::map< TypeNode, bool > d_type_complete;
   std::map< Node, int > d_tmap;
-  std::map< TypeNode, int > d_type_rlv_rep;
   // map from values to terms they were assigned for
   std::map< Node, Node > d_values_to_terms;
   /** clear the set */
@@ -50,8 +49,6 @@ public:
   int getIndexFor( Node n ) const;
   /** complete all values */
   bool complete( TypeNode t );
-  /** get number of relevant ground representatives for type */
-  int getNumRelevantGroundReps( TypeNode t );
   /** debug print */
   void toStream(std::ostream& out);
 };/* class RepSet */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 3cdaeb106..71d82d5e4 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -602,7 +602,6 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
   // model-builder specific initialization
   preProcessBuildModel(tm, fullModel);
 
-
   // Loop through all terms and make sure that assignable sub-terms are in the equality engine
   // Also, record #eqc per type (for finite model finding)
   std::map< TypeNode, unsigned > eqc_usort_count;
@@ -960,9 +959,6 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
         tm->d_rep_set.add((*i).getType(), *i);
       }
     }
-    for( std::map< TypeNode, std::vector< Node > >::iterator it = tm->d_rep_set.d_type_reps.begin(); it != tm->d_rep_set.d_type_reps.end(); ++it ){
-      tm->d_rep_set.d_type_rlv_rep[it->first] = (int)it->second.size();
-    }
   }
 
   //modelBuilder-specific initialization