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

8 files changed, 279 insertions, 281 deletions

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 );