From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 14 May 2013 17:11:14 +0000 (-0500)
Subject: Refactoring to separate old and new model building/checking code.
X-Git-Tag: cvc5-1.0.0~7287^2~121
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=126966a8d9cb6564b0ac31dd20f32059cc35156f;p=cvc5.git

Refactoring to separate old and new model building/checking code.
---

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index a9eb72b03..aeac3c79b 100755
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -138,21 +138,21 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
   if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){
     std::map< Node, Node > msum;
     if (QuantArith::getMonomialSumLit( lit, msum )){
-      Trace("bound-integers") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;
+      Trace("bound-integers-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;
       for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-        Trace("bound-integers") << "  ";
+        Trace("bound-integers-debug") << "  ";
         if( !it->second.isNull() ){
-          Trace("bound-integers") << it->second;
+          Trace("bound-integers-debug") << it->second;
           if( !it->first.isNull() ){
-            Trace("bound-integers") << " * ";
+            Trace("bound-integers-debug") << " * ";
           }
         }
         if( !it->first.isNull() ){
-          Trace("bound-integers") << it->first;
+          Trace("bound-integers-debug") << it->first;
         }
-        Trace("bound-integers") << std::endl;
+        Trace("bound-integers-debug") << std::endl;
       }
-      Trace("bound-integers") << std::endl;
+      Trace("bound-integers-debug") << std::endl;
       for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
         if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE ){
           Node veq;
@@ -170,11 +170,11 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
               }
               veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );
             }
-            Trace("bound-integers") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
+            Trace("bound-integers-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
             Node bv = n1.getKind()==BOUND_VARIABLE ? n1 : n2;
             if( !isBound( f, bv ) ){
               if( !hasNonBoundVar( f, n1.getKind()==BOUND_VARIABLE ? n2 : n1 ) ) {
-                Trace("bound-integers") << "The bound is relevant." << std::endl;
+                Trace("bound-integers-debug") << "The bound is relevant." << std::endl;
                 d_bounds[n1.getKind()==BOUND_VARIABLE ? 0 : 1][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1);
               }
             }
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 4904368a2..445f0d6c0 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -186,65 +186,75 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
 }
 
 
-FullModelChecker::FullModelChecker(QuantifiersEngine* qe) : d_qe(qe){
+FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) :
+QModelBuilder( c, qe ){
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
 }
 
-void FullModelChecker::reset(FirstOrderModel * fm) {
-  Trace("fmc") << "---Full Model Check reset() " << std::endl;
-  for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
-    it->second->reset();
-  }
-  d_quant_models.clear();
-  d_models_init.clear();
-  d_rep_ids.clear();
-  d_model_basis_rep.clear();
-  d_star_insts.clear();
-  //process representatives
-  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() ){
-      if( d_type_star.find(it->first)==d_type_star.end() ){
-        Node st = NodeManager::currentNM()->mkSkolem( "star_$$", it->first, "skolem created for full-model checking" );
-        d_type_star[it->first] = st;
-      }
-      Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
-      Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);
-      Node rmbt = fm->getRepresentative(mbt);
-      int mbt_index = -1;
-      Trace("fmc") << "  Model basis term : " << mbt << std::endl;
-      for( size_t a=0; a<it->second.size(); a++ ){
-        //Node r2 = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getRepresentative( it->second[a] );
-        //Node ir = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getInternalRepresentative( it->second[a], Node::null(), 0 );
-        Node r = fm->getRepresentative( it->second[a] );
-        std::vector< Node > eqc;
-        ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
-        Trace("fmc-model-debug") << "   " << (it->second[a]==r) << (r==mbt);
-        Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
-        //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
-        Trace("fmc-model-debug") << " {";
-        //find best selection for representative
-        for( size_t i=0; i<eqc.size(); i++ ){
-          Trace("fmc-model-debug") << eqc[i] << ", ";
-        }
-        Trace("fmc-model-debug") << "}" << std::endl;
 
-        //if this is the model basis eqc, replace with actual model basis term
-        if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) {
-          d_model_basis_rep[it->first] = r;
-          r = mbt;
-          mbt_index = a;
+void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
+  d_addedLemmas = 0;
+  FirstOrderModel* fm = (FirstOrderModel*)m;
+  if( fullModel ){
+    //make function values
+    for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){
+      m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );
+    }
+    TheoryEngineModelBuilder::processBuildModel( m, fullModel );
+    //mark that the model has been set
+    fm->markModelSet();
+  }else{
+    Trace("fmc") << "---Full Model Check reset() " << std::endl;
+    for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
+      it->second->reset();
+    }
+    d_quant_models.clear();
+    d_models_init.clear();
+    d_rep_ids.clear();
+    d_model_basis_rep.clear();
+    d_star_insts.clear();
+    //process representatives
+    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("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+        Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);
+        Node rmbt = fm->getRepresentative(mbt);
+        int mbt_index = -1;
+        Trace("fmc") << "  Model basis term : " << mbt << std::endl;
+        for( size_t a=0; a<it->second.size(); a++ ){
+          //Node r2 = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getRepresentative( it->second[a] );
+          //Node ir = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getInternalRepresentative( it->second[a], Node::null(), 0 );
+          Node r = fm->getRepresentative( it->second[a] );
+          std::vector< Node > eqc;
+          ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
+          Trace("fmc-model-debug") << "   " << (it->second[a]==r) << (r==mbt);
+          Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
+          //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
+          Trace("fmc-model-debug") << " {";
+          //find best selection for representative
+          for( size_t i=0; i<eqc.size(); i++ ){
+            Trace("fmc-model-debug") << eqc[i] << ", ";
+          }
+          Trace("fmc-model-debug") << "}" << std::endl;
+
+          //if this is the model basis eqc, replace with actual model basis term
+          if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) {
+            d_model_basis_rep[it->first] = r;
+            r = mbt;
+            mbt_index = a;
+          }
+          d_rep_ids[it->first][r] = (int)a;
         }
-        d_rep_ids[it->first][r] = (int)a;
-      }
-      Trace("fmc-model-debug") << std::endl;
+        Trace("fmc-model-debug") << std::endl;
 
-      if (mbt_index==-1) {
-        std::cout << "   WARNING: model basis term is not a representative!" << std::endl;
-        exit(0);
-      }else{
-        Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl;
+        if (mbt_index==-1) {
+          std::cout << "   WARNING: model basis term is not a representative!" << std::endl;
+          exit(0);
+        }else{
+          Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl;
+        }
       }
     }
   }
@@ -286,7 +296,7 @@ void FullModelChecker::addEntry( FirstOrderModel * fm, Node op, Node c, Node v,
     Node ri = getRepresentative(fm, c[i]);
     children.push_back(ri);
     if (isModelBasisTerm(ri)) {
-      ri = d_type_star[ri.getType()];
+      ri = getStar( ri.getType() );
     }else{
       hasNonStar = true;
     }
@@ -307,14 +317,6 @@ Def * FullModelChecker::getModel(FirstOrderModel * fm, Node op) {
   if( d_models_init.find(op)==d_models_init.end() ){
     if( d_models.find(op)==d_models.end() ){
       d_models[op] = new Def;
-      //make sure star's are defined
-      TypeNode tn = op.getType();
-      for(unsigned i=0; i<tn.getNumChildren()-1; i++) {
-        if( d_type_star.find(tn[i])==d_type_star.end() ){
-          Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn[i], "skolem created for full-model checking" );
-          d_type_star[tn[i]] = st;
-        }
-      }
     }
     //reset the model
     d_models[op]->reset();
@@ -322,13 +324,14 @@ Def * FullModelChecker::getModel(FirstOrderModel * fm, Node op) {
     std::vector< Node > conds;
     std::vector< Node > values;
     std::vector< Node > entry_conds;
-    Trace("fmc-model-debug") << "Model values for " << op << " ... " << std::endl;
+    Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;
     for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
       Node r = getRepresentative(fm, fm->d_uf_terms[op][i]);
       Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;
     }
     Trace("fmc-model-debug") << std::endl;
     //initialize the model
+    /*
     for( int j=0; j<2; j++ ){
       for( int k=1; k>=0; k-- ){
         Trace("fmc-model-debug")<< "Set values " << j << " " << k << " : " << std::endl;
@@ -341,25 +344,23 @@ Def * FullModelChecker::getModel(FirstOrderModel * fm, Node op) {
         }
       }
     }
-    //add for default value
-    if (!fm->d_uf_model_gen[op].d_default_value.isNull()) {
-      Node n = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
-      addEntry(fm, op, n, fm->d_uf_model_gen[op].d_default_value, conds, values, entry_conds);
+    */
+    for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
+      Node n = fm->d_uf_terms[op][i];
+      if( !n.getAttribute(NoMatchAttribute()) ){
+        addEntry(fm, op, n, n, conds, values, entry_conds);
+      }
     }
-
-    //find other default values (TODO: figure out why these entries are added to d_uf_model_gen)
-    if( conds.empty() ){
-      //for( std::map< Node, Node >::iterator it = fm->d_uf_model_gen[op].d_set_values[1][0].begin();
-      //     it != fm->d_uf_model_gen[op].d_set_values[1][0].end(); ++it ){
-      //  Trace("fmc-model-debug") << "   process : " << it->first << " -> " << it->second << std::endl;
-      //  addEntry(fm, op, it->first, it->second, conds, values, entry_conds);
-      //}
-      Trace("fmc-warn") << "WARNING: No entries for " << op << ", make default entry." << std::endl;
-      //choose a complete arbitrary term
-      Node n = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
-      TypeNode tn = n.getType();
-      Node v = fm->d_rep_set.d_type_reps[tn][0];
-      addEntry(fm, op, n, v, conds, values, entry_conds);
+    Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
+    //add default value
+    if( fm->hasTerm( nmb ) ){
+      Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
+      addEntry(fm, op, nmb, nmb, conds, values, entry_conds);
+    }else{
+      Node vmb = getSomeDomainElement( fm, nmb.getType() );
+      Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
+      Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;
+      addEntry(fm, op, nmb, vmb, conds, values, entry_conds);
     }
 
     //sort based on # default arguments
@@ -391,7 +392,7 @@ Def * FullModelChecker::getModel(FirstOrderModel * fm, Node op) {
 
 
 bool FullModelChecker::isStar(Node n) {
-  return n==d_type_star[n.getType()];
+  return n==getStar(n.getType());
 }
 
 bool FullModelChecker::isModelBasisTerm(Node n) {
@@ -432,8 +433,7 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
 }
 
 
-int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, int effort) {
-  int addedLemmas = 0;
+bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) {
   Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
   if (effort==0) {
     //register the quantifier
@@ -491,14 +491,12 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, int ef
           for( unsigned j=0; j<inst.size(); j++) {
             m.set( d_qe, f, j, inst[j] );
           }
-          if (isActive()) {
-            if( d_qe->addInstantiation( f, m ) ){
-              addedLemmas++;
-            }else{
-              //this can happen if evaluation is unknown
-              //might try it next effort level
-              d_star_insts[f].push_back(i);
-            }
+          if( d_qe->addInstantiation( f, m ) ){
+            lemmas++;
+          }else{
+            //this can happen if evaluation is unknown
+            //might try it next effort level
+            d_star_insts[f].push_back(i);
           }
         }else{
           //might try it next effort level
@@ -507,26 +505,29 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, int ef
       }
     }
   }else{
-    Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;
-    Trace("fmc-exh") << "Definition was : " << std::endl;
-    d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);
-    Trace("fmc-exh") << std::endl;
-    Def temp;
-    //simplify the exceptions?
-    for( int i=(d_star_insts[f].size()-1); i>=0; i--) {
-      //get witness for d_star_insts[f][i]
-      int j = d_star_insts[f][i];
-      if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){
-        int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );
-        if( lem==-1 ){
-          return -1;
-        }else{
-          addedLemmas += lem;
+    if (!d_star_insts[f].empty()) {
+      Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;
+      Trace("fmc-exh") << "Definition was : " << std::endl;
+      d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);
+      Trace("fmc-exh") << std::endl;
+      Def temp;
+      //simplify the exceptions?
+      for( int i=(d_star_insts[f].size()-1); i>=0; i--) {
+        //get witness for d_star_insts[f][i]
+        int j = d_star_insts[f][i];
+        if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){
+          int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );
+          if( lem==-1 ){
+            //something went wrong, resort to exhaustive instantiation
+            return false;
+          }else{
+            lemmas += lem;
+          }
         }
       }
     }
   }
-  return addedLemmas;
+  return true;
 }
 
 int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index) {
@@ -599,15 +600,12 @@ void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) {
   Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;
   if( n.getKind() == kind::BOUND_VARIABLE ){
     d.addEntry(this, mkCondDefault(f), n);
+    Trace("fmc-debug") << "Done with " << n << " " << n.getKind() << std::endl;
   }
   else if( n.getNumChildren()==0 ){
     Node r = n;
     if( !fm->hasTerm(n) ){
-      if (fm->d_rep_set.hasType(n.getType())) {
-        r = fm->d_rep_set.d_type_reps[n.getType()][0];
-      }else{
-        //should never happen?
-      }
+      r = getSomeDomainElement( fm, n.getType() );
     }
     r = getRepresentative(fm, r);
     d.addEntry(this, mkCondDefault(f), r);
@@ -683,6 +681,9 @@ void FullModelChecker::doVariableEquality( FirstOrderModel * fm, Node f, Def & d
     int j = getVariableId(f, eq[0]);
     int k = getVariableId(f, eq[1]);
     TypeNode tn = eq[0].getType();
+    if( !fm->d_rep_set.hasType( tn ) ){
+      getSomeDomainElement( fm, tn );  //to verify the type is initialized
+    }
     for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {
       Node r = getRepresentative( fm, fm->d_rep_set.d_type_reps[tn][i] );
       cond[j+1] = r;
@@ -703,7 +704,7 @@ void FullModelChecker::doVariableRelation( FirstOrderModel * fm, Node f, Def & d
         mkCondVec(dc.d_cond[i],cond);
         cond[j+1] = val;
         d.addEntry(this, mkCond(cond), d_true);
-        cond[j+1] = d_type_star[val.getType()];
+        cond[j+1] = getStar(val.getType());
         d.addEntry(this, mkCond(cond), d_false);
       }else{
         d.addEntry( this, dc.d_cond[i], d_false);
@@ -715,6 +716,7 @@ void FullModelChecker::doVariableRelation( FirstOrderModel * fm, Node f, Def & d
 }
 
 void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {
+  getModel(fm, op);
   Trace("fmc-uf-debug") << "Definition : " << std::endl;
   d_models[op]->debugPrint("fmc-uf-debug", op, this);
   Trace("fmc-uf-debug") << std::endl;
@@ -801,7 +803,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f,
         Trace("fmc-uf-process") << "follow value..." << std::endl;
         doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);
       }
-      Node st = d_type_star[v.getType()];
+      Node st = getStar(v.getType());
       if (curr.d_child.find(st)!=curr.d_child.end()) {
         Trace("fmc-uf-process") << "follow star..." << std::endl;
         doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);
@@ -880,11 +882,33 @@ Node FullModelChecker::mkCondDefault( Node f) {
   return mkCond(cond);
 }
 
+Node FullModelChecker::getStar(TypeNode tn) {
+  if( d_type_star.find(tn)==d_type_star.end() ){
+    Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );
+    d_type_star[tn] = st;
+  }
+  return d_type_star[tn];
+}
+
+Node FullModelChecker::getSomeDomainElement(FirstOrderModel * fm, TypeNode tn){
+  //check if there is even any domain elements at all
+  if (!fm->d_rep_set.hasType(tn)) {
+    Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
+    Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+    fm->d_rep_set.d_type_reps[tn].push_back(mbt);
+  }else if( fm->d_rep_set.d_type_reps[tn].size()==0 ){
+    Message() << "empty reps" << std::endl;
+    exit(0);
+  }
+  return fm->d_rep_set.d_type_reps[tn][0];
+}
+
 void FullModelChecker::mkCondDefaultVec( Node f, std::vector< Node > & cond ) {
   //get function symbol for f
   cond.push_back(d_quant_cond[f]);
   for (unsigned i=0; i<f[0].getNumChildren(); i++) {
-    cond.push_back(d_type_star[f[0][i].getType()]);
+    Node ts = getStar( f[0][i].getType() );
+    cond.push_back(ts);
   }
 }
 
@@ -936,15 +960,12 @@ Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals )
   }
 }
 
-bool FullModelChecker::isActive() {
-  return options::fmfFullModelCheck();
-}
-
 bool FullModelChecker::useSimpleModels() {
   return options::fmfFullModelCheckSimple();
 }
 
 Node FullModelChecker::getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix ) {
+  getModel( fm, op );
   TypeNode type = op.getType();
   std::vector< Node > vars;
   for( size_t i=0; i<type.getNumChildren()-1; i++ ){
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index bf9ed94e4..92c866ffd 100755
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -72,12 +72,11 @@ public:
 };
 
 
-class FullModelChecker
+class FullModelChecker : public QModelBuilder
 {
-private:
+protected:
   Node d_true;
   Node d_false;
-  QuantifiersEngine* d_qe;
   std::map<TypeNode, std::map< Node, int > > d_rep_ids;
   std::map<TypeNode, Node > d_model_basis_rep;
   std::map<Node, Def * > d_models;
@@ -121,26 +120,27 @@ private:
   void mkCondVec( Node n, std::vector< Node > & cond );
   Node evaluateInterpreted( Node n, std::vector< Node > & vals );
 public:
-  FullModelChecker( QuantifiersEngine* qe );
+  FullModelChecker( context::Context* c, QuantifiersEngine* qe );
   ~FullModelChecker(){}
 
   int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }
   bool isStar(Node n);
-  Node getStar(TypeNode tn) { return d_type_star[tn]; }
+  Node getStar(TypeNode tn);
+  Node getSomeDomainElement(FirstOrderModel * fm, TypeNode tn);
   bool isModelBasisTerm(Node n);
   Node getModelBasisTerm(TypeNode tn);
-  void reset(FirstOrderModel * fm);
   Def * getModel(FirstOrderModel * fm, Node op);
 
   void debugPrintCond(const char * tr, Node n, bool dispStar = false);
   void debugPrint(const char * tr, Node n, bool dispStar = false);
 
-  int exhaustiveInstantiate(FirstOrderModel * fm, Node f, int effort);
-  bool hasStarExceptions( Node f ) { return !d_star_insts[f].empty(); }
+  bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas );
 
-  bool isActive();
   bool useSimpleModels();
   Node getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix );
+
+  /** process build model */
+  void processBuildModel(TheoryModel* m, bool fullModel);
 };
 
 }
diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp
index e495b39c0..192e58d7c 100644
--- a/src/theory/quantifiers/inst_gen.cpp
+++ b/src/theory/quantifiers/inst_gen.cpp
@@ -47,7 +47,7 @@ void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, Ins
     if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){
       d_match_values.push_back( val );
       d_matches.push_back( InstMatch( &m ) );
-      qe->getModelEngine()->getModelBuilder()->d_instGenMatches++;
+      ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->d_instGenMatches++;
     }
   }
 }
@@ -92,7 +92,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto
     //for each term we consider, calculate a current match
     for( size_t i=0; i<considerTerms.size(); i++ ){
       Node n = considerTerms[i];
-      bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );
+      bool isSelected = ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->isTermSelected( n );
       bool hadSuccess CVC4_UNUSED = false;
       for( int t=(isSelected ? 0 : 1); t<2; t++ ){
         if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
@@ -193,7 +193,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto
     //process all values
     for( size_t i=0; i<considerTerms.size(); i++ ){
       Node n = considerTerms[i];
-      bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );
+      bool isSelected = ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->isTermSelected( n );
       for( int t=(isSelected ? 0 : 1); t<2; t++ ){
         //do not consider ground case if it is already congruent to another ground term
         if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 677f0c94b..79e36e9f5 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -33,6 +33,19 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
+
+QModelBuilder::QModelBuilder( context::Context* c, QuantifiersEngine* qe ) :
+TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe( qe ){
+  d_considerAxioms = true;
+  d_addedLemmas = 0;
+}
+
+
+bool QModelBuilder::optUseModel() {
+  return options::fmfModelBasedInst();
+}
+
+
 bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
   if( argIndex<(int)n.getNumChildren() ){
     Node r;
@@ -53,13 +66,13 @@ bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
   }
 }
 
-ModelEngineBuilder::ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe ) :
-TheoryEngineModelBuilder( qe->getTheoryEngine() ),
-d_qe( qe ), d_curr_model( c, NULL ){
-  d_considerAxioms = true;
+QModelBuilderIG::QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ) :
+QModelBuilder( c, qe ) {
+
 }
 
-void ModelEngineBuilder::debugModel( FirstOrderModel* fm ){
+
+void QModelBuilderIG::debugModel( FirstOrderModel* fm ){
   //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
   if( Trace.isOn("quant-model-warn") ){
     for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
@@ -88,22 +101,16 @@ void ModelEngineBuilder::debugModel( FirstOrderModel* fm ){
   }
 }
 
-void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
+void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
   FirstOrderModel* fm = (FirstOrderModel*)m;
   if( fullModel ){
     Assert( d_curr_model==fm );
-    if( d_qe->getModelEngine()->getFullModelChecker()->isActive() ){
-      for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
-        fm->d_uf_models[ it->first ] = d_qe->getModelEngine()->getFullModelChecker()->getFunctionValue( fm, it->first, "$x" );
-      }
-    }else{
-      //update models
-      for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
-        it->second.update( fm );
-        Trace("model-func") << "ModelEngineBuilder: Make function value from tree " << it->first << std::endl;
-        //construct function values
-        fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" );
-      }
+    //update models
+    for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+      it->second.update( fm );
+      Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl;
+      //construct function values
+      fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" );
     }
     TheoryEngineModelBuilder::processBuildModel( m, fullModel );
     //mark that the model has been set
@@ -192,7 +199,7 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
           }
         }
         //construct the model if necessary
-        if( d_addedLemmas==0 || optExhInstNonInstGenQuant() ){
+        if( d_addedLemmas==0 ){
           //if no immediate exceptions, build the model
           //  this model will be an approximation that will need to be tested via exhaustive instantiation
           Trace("model-engine-debug") << "Building model..." << std::endl;
@@ -218,7 +225,7 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
   }
 }
 
-int ModelEngineBuilder::initializeQuantifier( Node f, Node fp ){
+int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){
   if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){
     //create the basis match if necessary
     if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){
@@ -261,7 +268,7 @@ int ModelEngineBuilder::initializeQuantifier( Node f, Node fp ){
   return 0;
 }
 
-void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){
+void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
   d_uf_model_constructed.clear();
   //determine if any functions are constant
   for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
@@ -303,7 +310,7 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){
   }
 }
 
-bool ModelEngineBuilder::hasConstantDefinition( Node n ){
+bool QModelBuilderIG::hasConstantDefinition( Node n ){
   Node lit = n.getKind()==NOT ? n[0] : n;
   if( lit.getKind()==APPLY_UF ){
     Node op = lit.getOperator();
@@ -314,31 +321,19 @@ bool ModelEngineBuilder::hasConstantDefinition( Node n ){
   return false;
 }
 
-bool ModelEngineBuilder::optUseModel() {
-  return options::fmfModelBasedInst();
-}
-
-bool ModelEngineBuilder::optInstGen(){
+bool QModelBuilderIG::optInstGen(){
   return options::fmfInstGen();
 }
 
-bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){
+bool QModelBuilderIG::optOneQuantPerRoundInstGen(){
   return options::fmfInstGenOneQuantPerRound();
 }
 
-bool ModelEngineBuilder::optExhInstNonInstGenQuant(){
-  return options::fmfNewInstGen();
-}
-
-void ModelEngineBuilder::setEffort( int effort ){
-  d_considerAxioms = effort>=1;
-}
-
-ModelEngineBuilder::Statistics::Statistics():
-  d_num_quants_init("ModelEngineBuilder::Number_Quantifiers", 0),
-  d_num_partial_quants_init("ModelEngineBuilder::Number_Partial_Quantifiers", 0),
-  d_init_inst_gen_lemmas("ModelEngineBuilder::Initialize_Inst_Gen_Lemmas", 0 ),
-  d_inst_gen_lemmas("ModelEngineBuilder::Inst_Gen_Lemmas", 0 )
+QModelBuilderIG::Statistics::Statistics():
+  d_num_quants_init("QModelBuilder::Number_Quantifiers", 0),
+  d_num_partial_quants_init("QModelBuilder::Number_Partial_Quantifiers", 0),
+  d_init_inst_gen_lemmas("QModelBuilder::Initialize_Inst_Gen_Lemmas", 0 ),
+  d_inst_gen_lemmas("QModelBuilder::Inst_Gen_Lemmas", 0 )
 {
   StatisticsRegistry::registerStat(&d_num_quants_init);
   StatisticsRegistry::registerStat(&d_num_partial_quants_init);
@@ -346,18 +341,18 @@ ModelEngineBuilder::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_inst_gen_lemmas);
 }
 
-ModelEngineBuilder::Statistics::~Statistics(){
+QModelBuilderIG::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_num_quants_init);
   StatisticsRegistry::unregisterStat(&d_num_partial_quants_init);
   StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas);
   StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas);
 }
 
-bool ModelEngineBuilder::isQuantifierActive( Node f ){
+bool QModelBuilderIG::isQuantifierActive( Node f ){
   return ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end();
 }
 
-bool ModelEngineBuilder::isTermActive( Node n ){
+bool QModelBuilderIG::isTermActive( Node n ){
   return !n.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term
          ( n.getAttribute(ModelBasisArgAttribute())!=0 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments
                                                                                                       //and is not congruent modulo model basis
@@ -367,7 +362,7 @@ bool ModelEngineBuilder::isTermActive( Node n ){
 
 
 
-void ModelEngineBuilderDefault::reset( FirstOrderModel* fm ){
+void QModelBuilderDefault::reset( FirstOrderModel* fm ){
   d_quant_selection_lit.clear();
   d_quant_selection_lit_candidates.clear();
   d_quant_selection_lit_terms.clear();
@@ -376,7 +371,7 @@ void ModelEngineBuilderDefault::reset( FirstOrderModel* fm ){
 }
 
 
-int ModelEngineBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) {
+int QModelBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) {
   /*
   size_t maxChildren = 0;
   for( size_t i=0; i<uf_terms.size(); i++ ){
@@ -390,7 +385,7 @@ int ModelEngineBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms
   return 0;
 }
 
-void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
+void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
   Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
   //the pro/con preferences for this quantifier
   std::vector< Node > pro_con[2];
@@ -520,7 +515,7 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f )
   }
 }
 
-int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
+int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
   int addedLemmas = 0;
   //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
   //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
@@ -571,7 +566,7 @@ int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
   return addedLemmas;
 }
 
-void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
+void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
   if( optReconsiderFuncConstants() ){
     //reconsider constant functions that weren't necessary
     if( d_uf_model_constructed[op] ){
@@ -649,7 +644,7 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op )
 
 //////////////////////  Inst-Gen style Model Builder ///////////
 
-void ModelEngineBuilderInstGen::reset( FirstOrderModel* fm ){
+void QModelBuilderInstGen::reset( FirstOrderModel* fm ){
   //for new inst gen
   d_quant_selection_formula.clear();
   d_term_selected.clear();
@@ -657,15 +652,15 @@ void ModelEngineBuilderInstGen::reset( FirstOrderModel* fm ){
   //d_sub_quant_inst_trie.clear();//*
 }
 
-int ModelEngineBuilderInstGen::initializeQuantifier( Node f, Node fp ){
-  int addedLemmas = ModelEngineBuilder::initializeQuantifier( f, fp );
+int QModelBuilderInstGen::initializeQuantifier( Node f, Node fp ){
+  int addedLemmas = QModelBuilderIG::initializeQuantifier( f, fp );
   for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
     addedLemmas += initializeQuantifier( d_sub_quants[f][i], fp );
   }
   return addedLemmas;
 }
 
-void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){
+void QModelBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){
   //Node fp = getParentQuantifier( f );//*
   //bool quantRedundant = ( f!=fp && d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) );
   //if( f==fp || d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ){//*
@@ -699,7 +694,7 @@ void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f )
 }
 
 
-int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
+int QModelBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
   int addedLemmas = 0;
   if( d_quant_sat.find( f )==d_quant_sat.end() ){
     Node fp = d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f];
@@ -816,7 +811,7 @@ Node mkAndSelectionFormula( Node n1, Node n2 ){
 
 //if possible, returns a formula n' such that n' => ( n <=> polarity ), and n' is true in the current context,
 //   and NULL otherwise
-Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){
+Node QModelBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){
   Trace("sel-form-debug") << "Looking for selection formula " << n << " " << polarity << std::endl;
   Node ret;
   if( n.getKind()==NOT ){
@@ -925,7 +920,7 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar
   return ret;
 }
 
-int ModelEngineBuilderInstGen::getSelectionFormulaScore( Node fn ){
+int QModelBuilderInstGen::getSelectionFormulaScore( Node fn ){
   if( fn.getType().isBoolean() ){
     if( fn.getKind()==APPLY_UF ){
       Node op = fn.getOperator();
@@ -943,7 +938,7 @@ int ModelEngineBuilderInstGen::getSelectionFormulaScore( Node fn ){
   }
 }
 
-void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){
+void QModelBuilderInstGen::setSelectedTerms( Node s ){
 
   //if it is apply uf and has model basis arguments, then mark term as being "selected"
   if( s.getKind()==APPLY_UF ){
@@ -959,7 +954,7 @@ void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){
   }
 }
 
-bool ModelEngineBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption ){
+bool QModelBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption ){
   if( n.getKind()==FORALL ){
     return false;
   }else if( n.getKind()!=APPLY_UF ){
@@ -978,7 +973,7 @@ bool ModelEngineBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption
   return true;
 }
 
-void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){
+void QModelBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){
   if( f!=fp ){
     //std::cout << "gpqm " << fp << " " << f << " " << m << std::endl;
     //std::cout << "     " << fp[0].getNumChildren() << " " << f[0].getNumChildren() << std::endl;
@@ -1002,7 +997,7 @@ void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp
   }
 }
 
-void ModelEngineBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){
+void QModelBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){
   bool setDefaultVal = true;
   Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
   //set the values in the model
@@ -1030,6 +1025,6 @@ void ModelEngineBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op )
   d_uf_model_constructed[op] = true;
 }
 
-bool ModelEngineBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
+bool QModelBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
   return d_child_sub_quant_inst_trie[f].existsInstMatch( d_qe, f, m, modEq, true );
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 31448acee..2b38f3381 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -25,6 +25,35 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+
+class QModelBuilder : public TheoryEngineModelBuilder
+{
+protected:
+  //the model we are working with
+  context::CDO< FirstOrderModel* > d_curr_model;
+  //quantifiers engine
+  QuantifiersEngine* d_qe;
+public:
+  QModelBuilder( context::Context* c, QuantifiersEngine* qe );
+  virtual ~QModelBuilder(){}
+  // is quantifier active?
+  virtual bool isQuantifierActive( Node f ) { return true; }
+  //do exhaustive instantiation
+  virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) { return false; }
+  //whether to construct model
+  virtual bool optUseModel();
+  /** number of lemmas generated while building model */
+  int d_addedLemmas;
+  //consider axioms
+  bool d_considerAxioms;
+  /** exist instantiation ? */
+  virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
+};
+
+
+
+
+
 /** Attribute true for nodes that should not be used when considered for inst-gen basis */
 struct BasisNoMatchAttributeId {};
 /** use the special for boolean flag */
@@ -47,17 +76,13 @@ public:
 /** model builder class
   *  This class is capable of building candidate models based on the current quantified formulas
   *  that are asserted.  Use:
-  *  (1) call ModelEngineBuilder::buildModel( m, false );, where m is a FirstOrderModel
+  *  (1) call QModelBuilder::buildModel( m, false );, where m is a FirstOrderModel
   *  (2) if candidate model is determined to be a real model,
-           then call ModelEngineBuilder::buildModel( m, true );
+           then call QModelBuilder::buildModel( m, true );
   */
-class ModelEngineBuilder : public TheoryEngineModelBuilder
+class QModelBuilderIG : public QModelBuilder
 {
 protected:
-  //quantifiers engine
-  QuantifiersEngine* d_qe;
-  //the model we are working with
-  context::CDO< FirstOrderModel* > d_curr_model;
   //map from operators to model preference data
   std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
   //built model uf
@@ -90,25 +115,15 @@ protected:  //helper functions
   /** term has constant definition */
   bool hasConstantDefinition( Node n );
 public:
-  ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe );
-  virtual ~ModelEngineBuilder(){}
-  /** number of lemmas generated while building model */
-  int d_addedLemmas;
-  //consider axioms
-  bool d_considerAxioms;
-  // set effort
-  void setEffort( int effort );
+  QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
+  virtual ~QModelBuilderIG(){}
   //debug model
   void debugModel( FirstOrderModel* fm );
 public:
-  //whether to construct model
-  virtual bool optUseModel();
   //whether to add inst-gen lemmas
   virtual bool optInstGen();
   //whether to only consider only quantifier per round of inst-gen
   virtual bool optOneQuantPerRoundInstGen();
-  //whether we should exhaustively instantiate quantifiers where inst-gen is not working
-  virtual bool optExhInstNonInstGenQuant();
   /** statistics class */
   class Statistics {
   public:
@@ -120,18 +135,16 @@ public:
     ~Statistics();
   };
   Statistics d_statistics;
-  // is quantifier active?
-  bool isQuantifierActive( Node f );
   // is term active
   bool isTermActive( Node n );
   // is term selected
   virtual bool isTermSelected( Node n ) { return false; }
-  /** exist instantiation ? */
-  virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
   /** quantifier has inst-gen definition */
   virtual bool hasInstGen( Node f ) = 0;
   /** did inst gen this round? */
   bool didInstGen() { return d_didInstGen; }
+  // is quantifier active?
+  bool isQuantifierActive( Node f );
 
   //temporary stats
   int d_numQuantSat;
@@ -140,10 +153,10 @@ public:
   int d_numQuantNoSelForm;
   //temporary stat
   int d_instGenMatches;
-};/* class ModelEngineBuilder */
+};/* class QModelBuilder */
 
 
-class ModelEngineBuilderDefault : public ModelEngineBuilder
+class QModelBuilderDefault : public QModelBuilderIG
 {
 private:    ///information for (old) InstGen
   //map from quantifiers to their selection literals
@@ -167,15 +180,15 @@ protected:
   //theory-specific build models
   void constructModelUf( FirstOrderModel* fm, Node op );
 public:
-  ModelEngineBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){}
-  ~ModelEngineBuilderDefault(){}
+  QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
+  ~QModelBuilderDefault(){}
   //options
   bool optReconsiderFuncConstants() { return true; }
   //has inst gen
   bool hasInstGen( Node f ) { return !d_quant_selection_lit[f].isNull(); }
 };
 
-class ModelEngineBuilderInstGen : public ModelEngineBuilder
+class QModelBuilderInstGen : public QModelBuilderIG
 {
 private:    ///information for (new) InstGen
   //map from quantifiers to their selection formulas
@@ -217,8 +230,8 @@ private:
   //get parent quantifier
   Node getParentQuantifier( Node f ) { return d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f]; }
 public:
-  ModelEngineBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){}
-  ~ModelEngineBuilderInstGen(){}
+  QModelBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
+  ~QModelBuilderInstGen(){}
   // is term selected
   bool isTermSelected( Node n ) { return d_term_selected.find( n )!=d_term_selected.end(); }
   /** exist instantiation ? */
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index bc900d9a9..b9dcef282 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -36,13 +36,14 @@ using namespace CVC4::theory::inst;
 //Model Engine constructor
 ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
 QuantifiersModule( qe ),
-d_rel_domain( qe, qe->getModel() ),
-d_fmc( qe ){
+d_rel_domain( qe, qe->getModel() ){
 
-  if( options::fmfNewInstGen() ){
-    d_builder = new ModelEngineBuilderInstGen( c, qe );
+  if( options::fmfFullModelCheck() ){
+    d_builder = new fmcheck::FullModelChecker( c, qe );
+  }else if( options::fmfNewInstGen() ){
+    d_builder = new QModelBuilderInstGen( c, qe );
   }else{
-    d_builder = new ModelEngineBuilderDefault( c, qe );
+    d_builder = new QModelBuilderDefault( c, qe );
   }
 
 }
@@ -67,7 +68,7 @@ void ModelEngine::check( Theory::Effort e ){
         Trace("model-engine") << "---Model Engine Round---" << std::endl;
         //initialize the model
         Trace("model-engine-debug") << "Build model..." << std::endl;
-        d_builder->setEffort( effort );
+        d_builder->d_considerAxioms = effort>=1;
         d_builder->buildModel( fm, false );
         addedLemmas += (int)d_builder->d_addedLemmas;
         //if builder has lemmas, add and return
@@ -76,22 +77,13 @@ void ModelEngine::check( Theory::Effort e ){
           //let the strong solver verify that the model is minimal
           //for debugging, this will if there are terms in the model that the strong solver was not notified of
           ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm );
-          //for full model checking
-          if( d_fmc.isActive() ){
-            Trace("model-engine-debug") << "Reset full model checker..." << std::endl;
-            d_fmc.reset( fm );
-          }
           Trace("model-engine-debug") << "Check model..." << std::endl;
           d_incomplete_check = false;
           //print debug
           Debug("fmf-model-complete") << std::endl;
           debugPrint("fmf-model-complete");
           //successfully built an acceptable model, now check it
-          addedLemmas += checkModel( check_model_full );
-        }else if( d_builder->didInstGen() && d_builder->optExhInstNonInstGenQuant() ){
-          Trace("model-engine-debug") << "Check model for non-inst gen quantifiers..." << std::endl;
-          //check quantifiers that inst-gen didn't apply to
-          addedLemmas += checkModel( check_model_no_inst_gen );
+          addedLemmas += checkModel();
         }
       }
       if( addedLemmas==0 ){
@@ -157,7 +149,7 @@ bool ModelEngine::optExhInstEvalSkipMultiple(){
 #endif
 }
 
-int ModelEngine::checkModel( int checkOption ){
+int ModelEngine::checkModel(){
   int addedLemmas = 0;
   FirstOrderModel* fm = d_quantEngine->getModel();
   //for debugging
@@ -179,11 +171,13 @@ int ModelEngine::checkModel( int checkOption ){
     }
   }
   //full model checking: construct models for all functions
+  /*
   if( d_fmc.isActive() ){
     for (std::map< Node, uf::UfModelTreeGenerator >::iterator it = fm->d_uf_model_gen.begin(); it != fm->d_uf_model_gen.end(); ++it) {
       d_fmc.getModel(fm, it->first);
     }
   }
+  */
   //compute the relevant domain if necessary
   if( optUseRelevantDomain() ){
     d_rel_domain.compute();
@@ -193,7 +187,7 @@ int ModelEngine::checkModel( int checkOption ){
   d_relevantLemmas = 0;
   d_totalLemmas = 0;
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
-  int e_max = d_fmc.isActive() ? 2 : 1;
+  int e_max = options::fmfFullModelCheck() ? 2 : 1;
   for( int e=0; e<e_max; e++) {
     if (addedLemmas==0) {
       for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
@@ -207,15 +201,8 @@ int ModelEngine::checkModel( int checkOption ){
           }
         }
         d_totalLemmas += totalInst;
-        //determine if we should check this quantifiers
-        bool checkQuant = false;
-        if( checkOption==check_model_full ){
-          checkQuant = d_builder->isQuantifierActive( f );
-        }else if( checkOption==check_model_no_inst_gen ){
-          checkQuant = !d_builder->hasInstGen( f );
-        }
-        //if we need to consider this quantifier on this iteration
-        if( checkQuant ){
+        //determine if we should check this quantifier
+        if( d_builder->isQuantifierActive( f ) ){
           addedLemmas += exhaustiveInstantiate( f, e );
           if( Trace.isOn("model-engine-warn") ){
             if( addedLemmas>10000 ){
@@ -243,18 +230,7 @@ int ModelEngine::checkModel( int checkOption ){
 
 int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
   int addedLemmas = 0;
-
-  bool useModel = d_builder->optUseModel();
-  if (d_fmc.isActive() && effort==0) {
-    addedLemmas = d_fmc.exhaustiveInstantiate(d_quantEngine->getModel(), f, effort);
-  }else if( !d_fmc.isActive() || (effort==1 && d_fmc.hasStarExceptions(f)) ) {
-    if(d_fmc.isActive()){
-      useModel = false;
-      int lem = d_fmc.exhaustiveInstantiate(d_quantEngine->getModel(), f, effort);
-      if( lem!=-1 ){
-        return lem;
-      }
-    }
+  if( !d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort, addedLemmas ) ){
     Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
     Debug("inst-fmf-ei") << "   Instantiation Constants: ";
     for( size_t i=0; i<f[0].getNumChildren(); i++ ){
@@ -276,7 +252,7 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
         d_testLemmas++;
         int eval = 0;
         int depIndex;
-        if( useModel ){
+        if( d_builder->optUseModel() ){
           //see if instantiation is already true in current model
           Debug("fmf-model-eval") << "Evaluating ";
           riter.debugPrintSmall("fmf-model-eval");
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index d88a36d01..97aa085ed 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -32,12 +32,10 @@ class ModelEngine : public QuantifiersModule
   friend class RepSetIterator;
 private:
   /** builder class */
-  ModelEngineBuilder* d_builder;
+  QModelBuilder* d_builder;
 private:    //analysis of current model:
   //relevant domain
   RelevantDomain d_rel_domain;
-  //full model checker
-  fmcheck::FullModelChecker d_fmc;
   //is the exhaustive instantiation incomplete?
   bool d_incomplete_check;
 private:
@@ -47,12 +45,8 @@ private:
   bool optOneQuantPerRound();
   bool optExhInstEvalSkipMultiple();
 private:
-  enum{
-    check_model_full,
-    check_model_no_inst_gen,
-  };
   //check model
-  int checkModel( int checkOption );
+  int checkModel();
   //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced
   int exhaustiveInstantiate( Node f, int effort = 0 );
 private:
@@ -65,8 +59,7 @@ public:
   ModelEngine( context::Context* c, QuantifiersEngine* qe );
   ~ModelEngine(){}
   //get the builder
-  ModelEngineBuilder* getModelBuilder() { return d_builder; }
-  fmcheck::FullModelChecker* getFullModelChecker() { return &d_fmc; }
+  QModelBuilder* getModelBuilder() { return d_builder; }
 public:
   void check( Theory::Effort e );
   void registerQuantifier( Node f );