merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.

1 files changed, 474 insertions, 1193 deletions

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index a72b103d1..ad259f864 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -15,19 +15,23 @@
  **/
 
 #include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/rep_set_iterator.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/uf/theory_uf_instantiator.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
 
-//#define ME_PRINT_PROCESS_TIMES
+//#define ME_PRINT_WARNINGS
 
 //#define DISABLE_EVAL_SKIP_MULTIPLE
-#define RECONSIDER_FUNC_DEFAULT_VALUE
+
 #define RECONSIDER_FUNC_CONSTANT
-#define USE_INDEX_ORDERING
-//#define ONE_INST_PER_QUANT_PER_ROUND
+#define EVAL_FAIL_SKIP_MULTIPLE
+//#define ONE_QUANT_PER_ROUND_INST_GEN
+//#define ONE_QUANT_PER_ROUND
 
 using namespace std;
 using namespace CVC4;
@@ -36,570 +40,417 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-void printRepresentative( const char* c, QuantifiersEngine* qe, Node r ){
-  if( r.getType()==NodeManager::currentNM()->booleanType() ){
-    if( qe->getEqualityQuery()->areEqual( r, NodeManager::currentNM()->mkConst( true ) ) ){
-      Debug( c ) << "true";
-    }else{
-      Debug( c ) << "false";
-    }
-  }else{
-    Debug( c ) << qe->getEqualityQuery()->getRepresentative( r );
-  }
-}
-
-RepAlphabet::RepAlphabet( RepAlphabet& ra, QuantifiersEngine* qe ){
-  //translate to current representatives
-  for( std::map< TypeNode, std::vector< Node > >::iterator it = ra.d_type_reps.begin(); it != ra.d_type_reps.end(); ++it ){
-    std::vector< Node > reps;
-    for( int i=0; i<(int)it->second.size(); i++ ){
-      //reps.push_back( ie->getEqualityQuery()->getRepresentative( it->second[i] ) );
-      reps.push_back( it->second[i] );
-    }
-    set( it->first, reps );
-  }
-}
-
-void RepAlphabet::set( TypeNode t, std::vector< Node >& reps ){
-  d_type_reps[t].insert( d_type_reps[t].begin(), reps.begin(), reps.end() );
-  for( int i=0; i<(int)reps.size(); i++ ){
-    d_tmap[ reps[i] ] = i;
-  }
-}
-
-void RepAlphabet::debugPrint( const char* c, QuantifiersEngine* qe ){
-  for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
-    Debug( c ) << it->first << " : " << std::endl;
-    for( int i=0; i<(int)it->second.size(); i++ ){
-      Debug( c ) << "   " << i << ": " << it->second[i] << std::endl;
-      Debug( c ) << "         eq_class( " << it->second[i] << " ) : ";
-      ((uf::InstantiatorTheoryUf*)qe->getInstantiator( THEORY_UF ))->outputEqClass( c, it->second[i] );
-      Debug( c ) << std::endl;
-    }
-  }
-}
-
-RepAlphabetIterator::RepAlphabetIterator( QuantifiersEngine* qe, Node f, ModelEngine* model ){
-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    d_index_order.push_back( i );
-  }
-  initialize( qe, f, model );
-}
-
-RepAlphabetIterator::RepAlphabetIterator( QuantifiersEngine* qe, Node f, ModelEngine* model, std::vector< int >& indexOrder ){
-  d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
-  initialize( qe, f, model );
-}
-
-void RepAlphabetIterator::initialize( QuantifiersEngine* qe, Node f, ModelEngine* model ){
-  d_f = f;
-  d_model = model;
-  //store instantiation constants
-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    d_ic.push_back( qe->getInstantiationConstant( d_f, i ) );
-    d_index.push_back( 0 );
-  }
-  //make the d_var_order mapping
-  for( size_t i=0; i<d_index_order.size(); i++ ){
-    d_var_order[d_index_order[i]] = i;
-  }
-  //for testing
-  d_inst_tried = 0;
-  d_inst_tests = 0;
-}
-
-void RepAlphabetIterator::increment2( QuantifiersEngine* qe, int counter ){
-  Assert( !isFinished() );
-  //increment d_index
-  while( counter>=0 && d_index[counter]==(int)(d_model->getReps()->d_type_reps[d_f[0][d_index_order[counter]].getType()].size()-1) ){
-    counter--;
-  }
-  if( counter==-1 ){
-    d_index.clear();
-  }else{
-    for( int i=(int)d_index.size()-1; i>counter; i-- ){
-      d_index[i] = 0;
-      d_model->clearEvalFailed( i );
-    }
-    d_index[counter]++;
-    d_model->clearEvalFailed( counter );
-  }
-}
-
-void RepAlphabetIterator::increment( QuantifiersEngine* qe ){
-  if( !isFinished() ){
-    increment2( qe, (int)d_index.size()-1 );
-  }
-}
+ModelEngineBuilder::ModelEngineBuilder( QuantifiersEngine* qe ) :
+TheoryEngineModelBuilder( qe->getTheoryEngine() ),
+d_qe( qe ){
 
-bool RepAlphabetIterator::isFinished(){
-  return d_index.empty();
 }
 
-void RepAlphabetIterator::getMatch( QuantifiersEngine* ie, InstMatch& m ){
-  for( int i=0; i<(int)d_index.size(); i++ ){
-    m.d_map[ ie->getInstantiationConstant( d_f, i ) ] = getTerm( i );
-  }
+Node ModelEngineBuilder::chooseRepresentative( TheoryModel* tm, Node eqc ){
+  return eqc;
 }
 
-Node RepAlphabetIterator::getTerm( int i ){
-  TypeNode tn = d_f[0][d_index_order[i]].getType();
-  Assert( d_model->getReps()->d_type_reps.find( tn )!=d_model->getReps()->d_type_reps.end() );
-  return d_model->getReps()->d_type_reps[tn][d_index[d_index_order[i]]];
-}
-
-void RepAlphabetIterator::calculateTerms( QuantifiersEngine* qe ){
-  d_terms.clear();
-  for( int i=0; i<qe->getNumInstantiationConstants( d_f ); i++ ){
-    d_terms.push_back( getTerm( i ) );
-  }
-}
-
-void RepAlphabetIterator::debugPrint( const char* c ){
-  for( int i=0; i<(int)d_index.size(); i++ ){
-    Debug( c ) << i << ": " << d_index[i] << ", (" << getTerm( i ) << " / " << d_ic[ i ] << std::endl;
-  }
-}
-
-void RepAlphabetIterator::debugPrintSmall( const char* c ){
-  Debug( c ) << "RI: ";
-  for( int i=0; i<(int)d_index.size(); i++ ){
-    Debug( c ) << d_index[i] << ": " << getTerm( i ) << " ";
-  }
-  Debug( c ) << std::endl;
-}
-
-//set value function
-void UfModelTree::setValue( QuantifiersEngine* qe, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){
-  if( d_data.empty() ){
-    d_value = v;
-  }else if( !d_value.isNull() && d_value!=v ){
-    d_value = Node::null();
-  }
-  if( argIndex<(int)n.getNumChildren() ){
-    //take r = null when argument is the model basis
-    Node r;
-    if( ground || !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ){
-      r = qe->getEqualityQuery()->getRepresentative( n[ indexOrder[argIndex] ] );
-    }
-    d_data[ r ].setValue( qe, n, v, indexOrder, ground, argIndex+1 );
-  }
-}
-
-//get value function
-Node UfModelTree::getValue( QuantifiersEngine* qe, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){
-  if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){
-    //Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl;
-    depIndex = argIndex;
-    return d_value;
-  }else{
-    Node val;
-    int childDepIndex[2] = { argIndex, argIndex };
-    for( int i=0; i<2; i++ ){
-      //first check the argument, then check default
-      Node r;
-      if( i==0 ){
-        r = qe->getEqualityQuery()->getRepresentative( n[ indexOrder[argIndex] ] );
+void ModelEngineBuilder::processBuildModel( TheoryModel* m ) {
+  d_addedLemmas = 0;
+  //only construct first order model if optUseModel() is true
+  if( optUseModel() ){
+    FirstOrderModel* fm = (FirstOrderModel*)m;
+    //initialize model
+    fm->initialize();
+    //analyze the quantifiers
+    Debug("fmf-model-debug") << "Analyzing quantifiers..." << std::endl;
+    analyzeQuantifiers( fm );
+    //if applicable, find exceptions
+    if( optInstGen() ){
+      //now, see if we know that any exceptions via InstGen exist
+      Debug("fmf-model-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
+      for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+        Node f = fm->getAssertedQuantifier( i );
+        if( d_quant_sat.find( f )==d_quant_sat.end() ){
+          d_addedLemmas += doInstGen( fm, f );
+          if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){
+            break;
+          }
+        }
       }
-      std::map< Node, UfModelTree >::iterator it = d_data.find( r );
-      if( it!=d_data.end() ){
-        val = it->second.getValue( qe, n, indexOrder, childDepIndex[i], argIndex+1 );
-        if( !val.isNull() ){
-          break;
+      if( Options::current()->printModelEngine ){
+        if( d_addedLemmas>0 ){
+          Message() << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
+        }else{
+          Message() << "No InstGen lemmas..." << std::endl;
         }
-      }else{
-        //argument is not a defined argument: thus, it depends on this argument
-        childDepIndex[i] = argIndex+1;
       }
+      Debug("fmf-model-debug") << "---> Added lemmas = " << d_addedLemmas << std::endl;
+    }
+    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
+      Debug("fmf-model-debug") << "Building model..." << std::endl;
+      finishBuildModel( fm );
     }
-    //update depIndex
-    depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1];
-    //Notice() << "Return " << val << ", depIndex = " << depIndex;
-    //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl;
-    return val;
   }
 }
 
-//simplify function
-void UfModelTree::simplify( Node op, Node defaultVal, int argIndex ){
-  if( argIndex<(int)op.getType().getNumChildren()-1 ){
-    std::vector< Node > eraseData;
-    //first process the default argument
-    Node r;
-    std::map< Node, UfModelTree >::iterator it = d_data.find( r );
-    if( it!=d_data.end() ){
-      if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
-        eraseData.push_back( r );
-      }else{
-        it->second.simplify( op, defaultVal, argIndex+1 );
-        if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){
-          defaultVal = it->second.d_value;
+void ModelEngineBuilder::analyzeQuantifiers( FirstOrderModel* fm ){
+  d_quant_selection_lits.clear();
+  d_quant_sat.clear();
+  d_uf_prefs.clear();
+  int quantSatInit = 0;
+  int nquantSatInit = 0;
+  //analyze the preferences of each quantifier
+  for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){
+    Node f = fm->getAssertedQuantifier( i );
+    Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
+    std::vector< Node > pro_con[2];
+    std::vector< Node > constantSatOps;
+    bool constantSatReconsider;
+    //for each asserted quantifier f,
+    // - determine which literals form model basis for each quantifier
+    // - check which function/predicates have good and bad definitions according to f
+    for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin();
+         it != d_qe->d_phase_reqs[f].end(); ++it ){
+      Node n = it->first;
+      Node gn = d_qe->getTermDatabase()->getModelBasis( n );
+      Debug("fmf-model-req") << "   Req: " << n << " -> " << it->second << std::endl;
+      //calculate preference
+      int pref = 0;
+      bool value;
+      if( d_qe->getValuation().hasSatValue( gn, value ) ){
+        if( value!=it->second ){
+          //store this literal as a model basis literal
+          //  this literal will force a default values in model that (modulo exceptions) shows
+          //  that f is satisfied by the model
+          d_quant_selection_lits[f].push_back( value ? n : n.notNode() );
+          pref = 1;
         }else{
-          defaultVal = Node::null();
+          pref = -1;
         }
       }
-    }
-    //now see if any children can be removed, and simplify the ones that cannot
-    for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
-      if( !it->first.isNull() ){
-        if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
-          eraseData.push_back( it->first );
+      if( pref!=0 ){
+        //Store preferences for UF
+        bool isConst = !n.hasAttribute(InstConstantAttribute());
+        std::vector< Node > uf_terms;
+        if( gn.getKind()==APPLY_UF ){
+          uf_terms.push_back( gn );
+          isConst = fm->d_uf_model[gn.getOperator()].isConstant();
+        }else if( gn.getKind()==EQUAL ){
+          isConst = true;
+          for( int j=0; j<2; j++ ){
+            if( n[j].hasAttribute(InstConstantAttribute()) ){
+              if( n[j].getKind()==APPLY_UF ){
+                Node op = gn[j].getOperator();
+                if( fm->d_uf_model.find( op )!=fm->d_uf_model.end() ){
+                  uf_terms.push_back( gn[j] );
+                  isConst = isConst && fm->d_uf_model[op].isConstant();
+                }else{
+                  isConst = false;
+                }
+              }else{
+                isConst = false;
+              }
+            }
+          }
+        }
+        Debug("fmf-model-prefs") << "  It is " << ( pref==1 ? "pro" : "con" );
+        Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
+        if( pref==1 && isConst ){
+          d_quant_sat[f] = true;
+          //instead, just note to the model for each uf term that f is pro its definition
+          constantSatReconsider = false;
+          constantSatOps.clear();
+          for( int j=0; j<(int)uf_terms.size(); j++ ){
+            Node op = uf_terms[j].getOperator();
+            constantSatOps.push_back( op );
+            if( d_uf_prefs[op].d_reconsiderModel ){
+              constantSatReconsider = true;
+            }
+          }
+          if( !constantSatReconsider ){
+            break;
+          }
         }else{
-          it->second.simplify( op, defaultVal, argIndex+1 );
+          int pcIndex = pref==1 ? 0 : 1;
+          for( int j=0; j<(int)uf_terms.size(); j++ ){
+            pro_con[pcIndex].push_back( uf_terms[j] );
+          }
         }
       }
     }
-    for( int i=0; i<(int)eraseData.size(); i++ ){
-      d_data.erase( eraseData[i] );
-    }
-  }
-}
-
-//is total function
-bool UfModelTree::isTotal( Node op, int argIndex ){
-  if( argIndex==(int)(op.getType().getNumChildren()-1) ){
-    return !d_value.isNull();
-  }else{
-    Node r;
-    std::map< Node, UfModelTree >::iterator it = d_data.find( r );
-    if( it!=d_data.end() ){
-      return it->second.isTotal( op, argIndex+1 );
+    if( d_quant_sat.find( f )!=d_quant_sat.end() ){
+      Debug("fmf-model-prefs") << "  * Constant SAT due to definition of ops: ";
+      for( int i=0; i<(int)constantSatOps.size(); i++ ){
+        Debug("fmf-model-prefs") << constantSatOps[i] << " ";
+        d_uf_prefs[constantSatOps[i]].d_reconsiderModel = false;
+      }
+      Debug("fmf-model-prefs") << std::endl;
+      quantSatInit++;
+      d_statistics.d_pre_sat_quant += quantSatInit;
     }else{
-      return false;
-    }
-  }
-}
-
-Node UfModelTree::getConstantValue( QuantifiersEngine* qe, Node n, std::vector< int >& indexOrder, int argIndex ){
-  return d_value;
-}
-
-void indent( const char* c, int ind ){
-  for( int i=0; i<ind; i++ ){
-    Debug( c ) << " ";
-  }
-}
-
-void UfModelTree::debugPrint( const char* c, QuantifiersEngine* qe, std::vector< int >& indexOrder, int ind, int arg ){
-  if( !d_data.empty() ){
-    for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
-      if( !it->first.isNull() ){
-        indent( c, ind );
-        Debug( c ) << "if x_" << indexOrder[arg] << " == " << it->first << std::endl;
-        it->second.debugPrint( c, qe, indexOrder, ind+2, arg+1 );
+      nquantSatInit++;
+      d_statistics.d_pre_nsat_quant += quantSatInit;
+      //note quantifier's value preferences to models
+      for( int k=0; k<2; k++ ){
+        for( int j=0; j<(int)pro_con[k].size(); j++ ){
+          Node op = pro_con[k][j].getOperator();
+          Node r = fm->getRepresentative( pro_con[k][j] );
+          d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
+        }
       }
     }
-    if( d_data.find( Node::null() )!=d_data.end() ){
-      d_data[ Node::null() ].debugPrint( c, qe, indexOrder, ind, arg+1 );
-    }
-  }else{
-    indent( c, ind );
-    Debug( c ) << "return ";
-    printRepresentative( c, qe, d_value );
-    //Debug( c ) << " { ";
-    //for( int i=0; i<(int)d_explicit.size(); i++ ){
-    //  Debug( c ) << d_explicit[i] << " ";
-    //}
-    //Debug( c ) << "}";
-    Debug( c ) << std::endl;
   }
+  Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl;
 }
 
-UfModel::UfModel( Node op, ModelEngine* me ) : d_op( op ), d_me( me ), 
-  d_model_constructed( false ), d_reconsider_model( false ){
-
-  d_tree = UfModelTreeOrdered( op );  TypeNode tn = d_op.getType();  tn = tn[(int)tn.getNumChildren()-1];  Assert( tn==NodeManager::currentNM()->booleanType() || uf::StrongSolverTheoryUf::isRelevantType( tn ) );  //look at ground assertions
-  for( int i=0; i<(int)d_me->getQuantifiersEngine()->getTermDatabase()->d_op_map[ d_op ].size(); i++ ){
-    Node n = d_me->getQuantifiersEngine()->getTermDatabase()->d_op_map[ d_op ][i];
-    bool add = true;
-    if( n.getAttribute(NoMatchAttribute()) ){
-      add = false;
-      //determine if it has model basis attribute
-      for( int j=0; j<(int)n.getNumChildren(); j++ ){
-        if( n[j].getAttribute(ModelBasisAttribute()) ){
-          add = true;
-          break;
+int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){
+  //we wish to add all known exceptions to our model basis literal(s)
+  //  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,
+  //  effectively acting as partial instantiations instead of pointwise instantiations.
+  int addedLemmas = 0;
+  for( int i=0; i<(int)d_quant_selection_lits[f].size(); i++ ){
+    bool phase = d_quant_selection_lits[f][i].getKind()!=NOT;
+    Node lit = d_quant_selection_lits[f][i].getKind()==NOT ? d_quant_selection_lits[f][i][0] : d_quant_selection_lits[f][i];
+    Assert( lit.hasAttribute(InstConstantAttribute()) );
+    std::vector< Node > tr_terms;
+    if( lit.getKind()==APPLY_UF ){
+      //only match predicates that are contrary to this one, use literal matching
+      Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false );
+      fm->getTermDatabase()->setInstantiationConstantAttr( eq, f );
+      tr_terms.push_back( eq );
+    }else if( lit.getKind()==EQUAL ){
+      //collect trigger terms
+      for( int j=0; j<2; j++ ){
+        if( lit[j].hasAttribute(InstConstantAttribute()) ){
+          if( lit[j].getKind()==APPLY_UF ){
+            tr_terms.push_back( lit[j] );
+          }else{
+            tr_terms.clear();
+            break;
+          }
         }
       }
-    }
-    if( add ){
-      d_ground_asserts.push_back( n );
-      Node r = d_me->getQuantifiersEngine()->getEqualityQuery()->getRepresentative( n );
-      d_ground_asserts_reps.push_back( r );
-    }
-  }
-  //determine if it is constant
-  if( !d_ground_asserts.empty() ){
-    bool isConstant = true;
-    for( int i=1; i<(int)d_ground_asserts.size(); i++ ){
-      if( d_ground_asserts_reps[0]!=d_ground_asserts_reps[i] ){
-        isConstant = false;
-        break;
+      if( tr_terms.size()==1 && !phase ){
+        //equality between a function and a ground term, use literal matching
+        tr_terms.clear();
+        tr_terms.push_back( lit );
       }
     }
-    if( isConstant ){
-      //set constant value
-      Node t = d_me->getModelBasisApplyUfTerm( d_op );
-      Node r = d_ground_asserts_reps[0];
-      setValue( t, r, false );
-      setModel();
-      d_reconsider_model = true;
-      Debug("fmf-model-cons") << "Function " << d_op << " is the constant function ";
-      printRepresentative( "fmf-model-cons", d_me->getQuantifiersEngine(), r );
-      Debug("fmf-model-cons") << std::endl;
+    //if applicable, try to add exceptions here
+    if( !tr_terms.empty() ){
+      //make a trigger for these terms, add instantiations
+      Trigger* tr = Trigger::mkTrigger( d_qe, f, tr_terms );
+      //Notice() << "Trigger = " << (*tr) << std::endl;
+      tr->resetInstantiationRound();
+      tr->reset( Node::null() );
+      //d_qe->d_optInstMakeRepresentative = false;
+      //d_qe->d_optMatchIgnoreModelBasis = true;
+      addedLemmas += tr->addInstantiations( d_quant_basis_match[f] );
     }
   }
+  return addedLemmas;
 }
 
-void UfModel::setValue( Node n, Node v, bool ground ){
-  d_set_values[ ground ? 1 : 0 ][n] = v;
-}
-
-void UfModel::setModel(){
-  makeModel( d_me->getQuantifiersEngine(), d_tree );
-  d_model_constructed = true;
-}
-
-void UfModel::clearModel(){
-  for( int k=0; k<2; k++ ){
-    d_set_values[k].clear();
+void ModelEngineBuilder::finishBuildModel( FirstOrderModel* fm ){
+  //build model for UF
+  for( std::map< Node, uf::UfModel >::iterator it = fm->d_uf_model.begin(); it != fm->d_uf_model.end(); ++it ){
+    finishBuildModelUf( fm, it->second );
   }
-  d_tree.clear();
-  d_model_constructed = false;
-}
-
-Node UfModel::getConstantValue( QuantifiersEngine* qe, Node n ){
-  if( d_model_constructed ){
-    return d_tree.getConstantValue( qe, n );
-  }else{
-    return Node::null();
+  //build model for arrays
+  for( std::map< Node, Node >::iterator it = fm->d_array_model.begin(); it != fm->d_array_model.end(); ++it ){
+    //consult the model basis select term
+    // i.e. the default value for array A is the value of select( A, e ), where e is the model basis term
+    TypeNode tn = it->first.getType();
+    Node selModelBasis = NodeManager::currentNM()->mkNode( SELECT, it->first, fm->getTermDatabase()->getModelBasisTerm( tn[0] ) );
+    it->second = fm->getRepresentative( selModelBasis );
   }
+  Debug("fmf-model-debug") << "Done building models." << std::endl;
 }
 
-bool UfModel::isConstant(){
-  Node gn = d_me->getModelBasisApplyUfTerm( d_op );
-  Node n = getConstantValue( d_me->getQuantifiersEngine(), gn );
-  return !n.isNull();
-}
-
-void UfModel::buildModel(){
+void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, uf::UfModel& model ){
+  Node op = model.getOperator();
 #ifdef RECONSIDER_FUNC_CONSTANT
-  if( d_model_constructed ){
-    if( d_reconsider_model ){
+  if( model.isModelConstructed() && model.isConstant() ){
+    if( d_uf_prefs[op].d_reconsiderModel ){
       //if we are allowed to reconsider default value, then see if the default value can be improved
-      Node t = d_me->getModelBasisApplyUfTerm( d_op );
-      Node v = d_set_values[0][t];
-      if( d_value_pro_con[1][v].size()>d_value_pro_con[0][v].size() ){
-        Debug("fmf-model-cons-debug") << "Consider changing the default value for " << d_op << std::endl;
-        clearModel();
+      Node t = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
+      Node v = model.getConstantValue( t );
+      if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){
+        Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl;
+        model.clearModel();
       }
     }
   }
 #endif
-  //now, construct models for each uninterpretted function/predicate
-  if( !d_model_constructed ){
-    Debug("fmf-model-cons") << "Construct model for " << d_op << "..." << std::endl;
-    //now, set the values in the model
-    for( int i=0; i<(int)d_ground_asserts.size(); i++ ){
-      Node n = d_ground_asserts[i];
-      Node v = d_ground_asserts_reps[i];
+  if( !model.isModelConstructed() ){
+    //construct the model for the uninterpretted function/predicate
+    bool setDefaultVal = true;
+    Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
+    Debug("fmf-model-cons") << "Construct model for " << op << "..." << std::endl;
+    //set the values in the model
+    for( size_t i=0; i<model.d_ground_asserts.size(); i++ ){
+      Node n = model.d_ground_asserts[i];
+      Node v = model.d_ground_asserts_reps[i];
       //if this assertion did not help the model, just consider it ground
       //set n = v in the model tree
       Debug("fmf-model-cons") << "  Set " << n << " = ";
-      printRepresentative( "fmf-model-cons", d_me->getQuantifiersEngine(), v );
+      fm->printRepresentativeDebug( "fmf-model-cons", v );
       Debug("fmf-model-cons") << std::endl;
       //set it as ground value
-      setValue( n, v );
-    }
-    //set the default value
-    //chose defaultVal based on heuristic (the best proportion of "pro" responses)
-    Node defaultVal;
-    double maxScore = -1;
-    for( int i=0; i<(int)d_values.size(); i++ ){
-      Node v = d_values[i];
-      double score = ( 1.0 + (double)d_value_pro_con[0][v].size() )/( 1.0 + (double)d_value_pro_con[1][v].size() );
-      Debug("fmf-model-cons") << "  - score( ";
-      printRepresentative( "fmf-model-cons", d_me->getQuantifiersEngine(), v );
-      Debug("fmf-model-cons") << " ) = " << score << std::endl;
-      if( score>maxScore ){
-        defaultVal = v;
-        maxScore = score;
-      }
-    }
-#ifdef RECONSIDER_FUNC_DEFAULT_VALUE
-    if( maxScore<1.0 ){
-      //consider finding another value, if possible
-      Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl;
-      TypeNode tn = d_op.getType();
-      Node newDefaultVal = d_me->getArbitraryElement( tn[(int)tn.getNumChildren()-1], d_values );
-      if( !newDefaultVal.isNull() ){
-        defaultVal = newDefaultVal;
-        Debug("fmf-model-cons-debug") << "-> Change default value to ";
-        printRepresentative( "fmf-model-cons-debug", d_me->getQuantifiersEngine(), defaultVal );
-        Debug("fmf-model-cons-debug") << std::endl;
+      model.setValue( n, v );
+      if( model.optUsePartialDefaults() ){
+        //also set as default value if necessary
+        //if( n.getAttribute(ModelBasisArgAttribute())==1 && !d_term_pro_con[0][n].empty() ){
+        if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){
+          model.setValue( n, v, false );
+          if( n==defaultTerm ){
+            //incidentally already set, we will not need to find a default value
+            setDefaultVal = false;
+          }
+        }
       }else{
-        Debug("fmf-model-cons-debug") << "-> Could not find arbitrary element of type " << tn[(int)tn.getNumChildren()-1] << std::endl;
-        Debug("fmf-model-cons-debug") << "      Excluding: ";
-        for( int i=0; i<(int)d_values.size(); i++ ){
-          Debug("fmf-model-cons-debug") << d_values[i] << " ";
+        if( n==defaultTerm ){
+          model.setValue( n, v, false );
+          //incidentally already set, we will not need to find a default value
+          setDefaultVal = false;
         }
-        Debug("fmf-model-cons-debug") << std::endl;
       }
     }
-#endif
-    Assert( !defaultVal.isNull() );
-    //get the default term (this term must be defined non-ground in model)
-    Node defaultTerm = d_me->getModelBasisApplyUfTerm( d_op );
-    Debug("fmf-model-cons") << "  Choose ";
-    printRepresentative("fmf-model-cons", d_me->getQuantifiersEngine(), defaultVal );
-    Debug("fmf-model-cons") << " as default value (" << defaultTerm << ")" << std::endl;
-    Debug("fmf-model-cons") << "     # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl;
-    Debug("fmf-model-cons") << "     # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl;
-    setValue( defaultTerm, defaultVal, false );
+    //set the overall default value if not set already  (is this necessary??)
+    if( setDefaultVal ){
+      Debug("fmf-model-cons") << "  Choose default value..." << std::endl;
+      //chose defaultVal based on heuristic, currently the best ratio of "pro" responses
+      Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
+      Assert( !defaultVal.isNull() );
+      model.setValue( defaultTerm, defaultVal, false );
+    }
     Debug("fmf-model-cons") << "  Making model...";
-    setModel();
-    Debug("fmf-model-cons") << "  Finished constructing model for " << d_op << "." << std::endl;
+    model.setModel();
+    Debug("fmf-model-cons") << "  Finished constructing model for " << op << "." << std::endl;
   }
 }
 
-void UfModel::setValuePreference( Node f, Node n, bool isPro ){
-  Node v = d_me->getQuantifiersEngine()->getEqualityQuery()->getRepresentative( n );
-  //Notice() << "Set value preference " << n << " = " << v << " " << isPro << std::endl;
-  if( std::find( d_values.begin(), d_values.end(), v )==d_values.end() ){
-    d_values.push_back( v );
-  }
-  int index = isPro ? 0 : 1;
-  if( std::find( d_value_pro_con[index][v].begin(), d_value_pro_con[index][v].end(), f )==d_value_pro_con[index][v].end() ){
-    d_value_pro_con[index][v].push_back( f );
-  }
+bool ModelEngineBuilder::optUseModel() {
+  return Options::current()->fmfModelBasedInst;
 }
 
-void UfModel::makeModel( QuantifiersEngine* qe, UfModelTreeOrdered& tree ){
-  for( int k=0; k<2; k++ ){
-    for( std::map< Node, Node >::iterator it = d_set_values[k].begin(); it != d_set_values[k].end(); ++it ){
-      tree.setValue( qe, it->first, it->second, k==1 );
-    }
-  }
-  tree.simplify();
+bool ModelEngineBuilder::optInstGen(){
+  return Options::current()->fmfInstGen;
+}
+
+bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){
+#ifdef ONE_QUANT_PER_ROUND_INST_GEN
+  return true;
+#else
+  return false;
+#endif
 }
 
-void UfModel::debugPrint( const char* c ){
-  //Debug( c ) << "Function " << d_op << std::endl;
-  //Debug( c ) << "   Type: " << d_op.getType() << std::endl;
-  //Debug( c ) << "   Ground asserts:" << std::endl;
-  //for( int i=0; i<(int)d_ground_asserts.size(); i++ ){
-  //  Debug( c ) << "      " << d_ground_asserts[i] << " = ";
-  //  printRepresentative( c, d_me->getQuantifiersEngine(), d_ground_asserts[i] );
-  //  Debug( c ) << std::endl;
-  //}
-  //Debug( c ) << "   Model:" << std::endl;
+ModelEngineBuilder::Statistics::Statistics():
+  d_pre_sat_quant("ModelEngineBuilder::Status_quant_pre_sat", 0),
+  d_pre_nsat_quant("ModelEngineBuilder::Status_quant_pre_non_sat", 0)
+{
+  StatisticsRegistry::registerStat(&d_pre_sat_quant);
+  StatisticsRegistry::registerStat(&d_pre_nsat_quant);
+}
 
-  TypeNode t = d_op.getType();
-  Debug( c ) << d_op << "( ";
-  for( int i=0; i<(int)(t.getNumChildren()-1); i++ ){
-    Debug( c ) << "x_" << i << " : " << t[i];
-    if( i<(int)(t.getNumChildren()-2) ){
-      Debug( c ) << ", ";
-    }
-  }
-  Debug( c ) << " ) : " << t[(int)t.getNumChildren()-1] << std::endl;
-  if( d_tree.isEmpty() ){
-    Debug( c ) << "   [undefined]" << std::endl;
-  }else{
-    d_tree.debugPrint( c, d_me->getQuantifiersEngine(), 3 );
-    Debug( c ) << std::endl;
-  }
-  //Debug( c ) << "   Phase reqs:" << std::endl;  //for( int i=0; i<2; i++ ){
-  //  for( std::map< Node, std::vector< Node > >::iterator it = d_reqs[i].begin(); it != d_reqs[i].end(); ++it ){
-  //    Debug( c ) << "      " << it->first << std::endl;
-  //    for( int j=0; j<(int)it->second.size(); j++ ){
-  //      Debug( c ) << "         " << it->second[j] << " -> " << (i==1) << std::endl;
-  //    }
-  //  }
-  //}
-  //Debug( c ) << std::endl;
-  //for( int i=0; i<2; i++ ){
-  //  for( std::map< Node, std::map< Node, std::vector< Node > > >::iterator it = d_eq_reqs[i].begin(); it != d_eq_reqs[i].end(); ++it ){
-  //    Debug( c ) << "      " << "For " << it->first << ":" << std::endl;
-  //    for( std::map< Node, std::vector< Node > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-  //      for( int j=0; j<(int)it2->second.size(); j++ ){
-  //        Debug( c ) << "         " << it2->first << ( i==1 ? "==" : "!=" ) << it2->second[j] << std::endl;
-  //      }
-  //    }
-  //  }
-  //}
+ModelEngineBuilder::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_pre_sat_quant);
+  StatisticsRegistry::unregisterStat(&d_pre_nsat_quant);
 }
 
 //Model Engine constructor
-ModelEngine::ModelEngine( TheoryQuantifiers* th ){
-  d_th = th;
-  d_quantEngine = th->getQuantifiersEngine();
-  d_ss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->getTheory( THEORY_UF ))->getStrongSolver();
+ModelEngine::ModelEngine( QuantifiersEngine* qe ) :
+QuantifiersModule( qe ),
+d_builder( qe ),
+d_rel_domain( qe->getModel() ){
+
 }
 
 void ModelEngine::check( Theory::Effort e ){
-  if( e==Theory::EFFORT_LAST_CALL ){
-    bool quantsInit = true;
+  if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){
     //first, check if we can minimize the model further
-    if( !d_ss->minimize() ){
+    if( !((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->getTheory( THEORY_UF ))->getStrongSolver()->minimize() ){
       return;
     }
-    if( useModel() ){
-      //now, check if any quantifiers are un-initialized
-      for( int i=0; i<d_quantEngine->getNumAssertedQuantifiers(); i++ ){
-        Node f = d_quantEngine->getAssertedQuantifier( i );
-        if( !initializeQuantifier( f ) ){
-          quantsInit = false;
-        }
+    //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
+    int addedLemmas = 0;
+    if( d_builder.optUseModel() ){
+      //check if any quantifiers are un-initialized
+      for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+        Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
+        addedLemmas += initializeQuantifier( f );
       }
     }
-    if( quantsInit ){
-#ifdef ME_PRINT_PROCESS_TIMES
-      Notice() << "---Instantiation Round---" << std::endl;
-#endif
+    if( addedLemmas==0 ){
+      //quantifiers are initialized, we begin an instantiation round
+      double clSet = 0;
+      if( Options::current()->printModelEngine ){
+        clSet = double(clock())/double(CLOCKS_PER_SEC);
+        Message() << "---Model Engine Round---" << std::endl;
+      }
       Debug("fmf-model-debug") << "---Begin Instantiation Round---" << std::endl;
       ++(d_statistics.d_inst_rounds);
-      d_quantEngine->getTermDatabase()->reset( e );
-      //build the representatives
-      Debug("fmf-model-debug") << "Building representatives..." << std::endl;
-      buildRepresentatives();
-      if( useModel() ){
-        //initialize the model
-        Debug("fmf-model-debug") << "Initializing model..." << std::endl;
-        initializeModel();
-        //analyze the quantifiers
-        Debug("fmf-model-debug") << "Analyzing quantifiers..." << std::endl;
-        analyzeQuantifiers();
-        //build the model
-        Debug("fmf-model-debug") << "Building model..." << std::endl;
-        for( std::map< Node, UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
-          it->second.buildModel();
+      //reset the quantifiers engine
+      d_quantEngine->resetInstantiationRound( e );
+      //initialize the model
+      Debug("fmf-model-debug") << "Build model..." << std::endl;
+      d_builder.buildModel( d_quantEngine->getModel() );
+      d_quantEngine->d_model_set = true;
+      //if builder has lemmas, add and return
+      if( d_builder.d_addedLemmas>0 ){
+        addedLemmas += (int)d_builder.d_addedLemmas;
+      }else{
+        //print debug
+        Debug("fmf-model-complete") << std::endl;
+        debugPrint("fmf-model-complete");
+        //verify we are SAT by trying exhaustive instantiation
+        if( optUseRelevantDomain() ){
+          d_rel_domain.compute();
         }
-      }
-      //print debug
-      debugPrint("fmf-model-complete");
-      //try exhaustive instantiation
-      Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl;
-      int addedLemmas = 0;
-      for( int i=0; i<d_quantEngine->getNumAssertedQuantifiers(); i++ ){
-        Node f = d_quantEngine->getAssertedQuantifier( i );
-        if( d_quant_sat.find( f )==d_quant_sat.end() ){
-          addedLemmas += instantiateQuantifier( f );
+        d_triedLemmas = 0;
+        d_testLemmas = 0;
+        d_relevantLemmas = 0;
+        d_totalLemmas = 0;
+        Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl;
+        for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+          Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
+          if( d_builder.d_quant_sat.find( f )==d_builder.d_quant_sat.end() ){
+            addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() );
+            if( optOneQuantPerRound() && addedLemmas>0 ){
+              break;
+            }
+          }
+#ifdef ME_PRINT_WARNINGS
+          if( addedLemmas>10000 ){
+            break;
+          }
+#endif
+        }
+        Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
+        Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+        if( Options::current()->printModelEngine ){
+          Message() << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
+          Message() << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+          double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+          Message() << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
+        }
+#ifdef ME_PRINT_WARNINGS
+        if( addedLemmas>10000 ){
+          Debug("fmf-exit") << std::endl;
+          debugPrint("fmf-exit");
+          exit( 0 );
         }
-      }
-#ifdef ME_PRINT_PROCESS_TIMES
-      Notice() << "Added Lemmas = " << addedLemmas << std::endl;
 #endif
-      if( addedLemmas==0 ){
-        //debugPrint("fmf-consistent");
-        //for( std::map< Node, UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
-        //  it->second.simplify();
-        //}
-        Debug("fmf-consistent") << std::endl;
-        debugPrint("fmf-consistent");
       }
     }
-    d_quantEngine->flushLemmas( &d_th->getOutputChannel() );
+    if( addedLemmas==0 ){
+      //CVC4 will answer SAT
+      Debug("fmf-consistent") << std::endl;
+      debugPrint("fmf-consistent");
+    }else{
+      //otherwise, the search will continue
+      d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
+    }
   }
 }
 
@@ -611,19 +462,31 @@ void ModelEngine::assertNode( Node f ){
 
 }
 
-bool ModelEngine::useModel() {
-  return Options::current()->fmfModelBasedInst;
+bool ModelEngine::optOneInstPerQuantRound(){
+  return Options::current()->fmfOneInstPerRound;
+}
+
+bool ModelEngine::optUseRelevantDomain(){
+  return Options::current()->fmfRelevantDomain;
+}
+
+bool ModelEngine::optOneQuantPerRound(){
+#ifdef ONE_QUANT_PER_ROUND
+  return true;
+#else
+  return false;
+#endif
 }
 
-bool ModelEngine::initializeQuantifier( Node f ){
+int ModelEngine::initializeQuantifier( Node f ){
   if( d_quant_init.find( f )==d_quant_init.end() ){
     d_quant_init[f] = true;
     Debug("inst-fmf-init") << "Initialize " << f << std::endl;
     //add the model basis instantiation
     // This will help produce the necessary information for model completion.
-    // We do this by extending distinguish ground assertions (those 
+    // We do this by extending distinguish ground assertions (those
     //   containing terms with "model basis" attribute) to hold for all cases.
-    
+
     ////first, check if any variables are required to be equal
     //for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin();
     //    it != d_quantEngine->d_phase_reqs[f].end(); ++it ){
@@ -632,747 +495,167 @@ bool ModelEngine::initializeQuantifier( Node f ){
     //    Notice() << "Unhandled phase req: " << n << std::endl;
     //  }
     //}
-
+    std::vector< Node > ics;
     std::vector< Node > terms;
     for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
-      terms.push_back( getModelBasisTerm( f[0][j].getType() ) );
+      Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
+      Node t = d_quantEngine->getTermDatabase()->getModelBasisTerm( ic.getType() );
+      ics.push_back( ic );
+      terms.push_back( t );
+      //calculate the basis match for f
+      d_builder.d_quant_basis_match[f].d_map[ ic ] = t;
     }
     ++(d_statistics.d_num_quants_init);
+    //register model basis body
+    Node n = d_quantEngine->getTermDatabase()->getCounterexampleBody( f );
+    Node gn = n.substitute( ics.begin(), ics.end(), terms.begin(), terms.end() );
+    d_quantEngine->getTermDatabase()->registerModelBasis( n, gn );
+    //add model basis instantiation
     if( d_quantEngine->addInstantiation( f, terms ) ){
-      return false;
+      return 1;
     }else{
-      //usually shouldn't happen
+      //shouldn't happen usually, but will occur if x != y is a required literal for f.
       //Notice() << "No model basis for " << f << std::endl;
       ++(d_statistics.d_num_quants_init_fail);
     }
   }
-  return true;
-}
-
-void ModelEngine::buildRepresentatives(){
-  d_ra.clear();
-  //collect all representatives for all types and store as representative alphabet
-  for( int i=0; i<d_ss->getNumCardinalityTypes(); i++ ){
-    TypeNode tn = d_ss->getCardinalityType( i );
-    std::vector< Node > reps;
-    d_ss->getRepresentatives( tn, reps );
-    Assert( !reps.empty() );
-    //if( (int)reps.size()!=d_ss->getCardinality( tn ) ){
-    //  Notice() << "InstStrategyFinteModelFind::processResetInstantiationRound: Bad representatives for type." << std::endl;
-    //  Notice() << "   " << tn << " has cardinality " << d_ss->getCardinality( tn );
-    //  Notice() << " but only " << (int)reps.size() << " were given." << std::endl;
-    //  Unimplemented( 27 );
-    //}
-    Debug("fmf-model-debug") << "   " << tn << " -> " << reps.size() << std::endl;
-    Debug("fmf-model-debug") << "      ";
-    for( int i=0; i<(int)reps.size(); i++ ){
-      Debug("fmf-model-debug") << reps[i] << " ";
-    }
-    Debug("fmf-model-debug") << std::endl;
-    //set them in the alphabet
-    d_ra.set( tn, reps );
-#ifdef ME_PRINT_PROCESS_TIMES
-    Notice() << tn << " has " << reps.size() << " representatives. " << std::endl;
-#endif
-  }
+  return 0;
 }
 
-void ModelEngine::initializeModel(){
-  d_uf_model.clear();
-  d_quant_sat.clear();
-  for( int k=0; k<2; k++ ){
-    d_pro_con_quant[k].clear();
-  }
-
-  ////now analyze quantifiers (temporary)
-  //for( int i=0; i<(int)d_quantEngine->getNumAssertedQuantifiers(); i++ ){
-  //  Node f = d_quantEngine->getAssertedQuantifier( i );
-  //  Debug("fmf-model-req") << "Phase requirements for " << f << ": " << std::endl;
-  //  for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin();
-  //       it != d_quantEngine->d_phase_reqs[f].end(); ++it ){
-  //    Node n = it->first;
-  //    Debug("fmf-model-req") << "   " << n << " -> " << it->second << std::endl;
-  //    if( n.getKind()==APPLY_UF ){
-  //      processPredicate( f, n, it->second );
-  //    }else if( n.getKind()==EQUAL ){
-  //      processEquality( f, n, it->second );
-  //    }
-  //  }
-  //}
-  for( int i=0; i<(int)d_quantEngine->getNumAssertedQuantifiers(); i++ ){
-    Node f = d_quantEngine->getAssertedQuantifier( i );
-    initializeUf( f[1] );
-    //register model basis terms
-    std::vector< Node > vars;
-    std::vector< Node > subs;
-    for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
-      vars.push_back( d_quantEngine->getInstantiationConstant( f, j ) );
-      subs.push_back( getModelBasisTerm( f[0][j].getType() ) );
-    }
-    Node n = d_quantEngine->getCounterexampleBody( f );
-    Node gn = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-    registerModelBasis( n, gn );
-  }
-}
-
-void ModelEngine::analyzeQuantifiers(){
-  int quantSatInit = 0;
-  int nquantSatInit = 0;
-  //analyze the preferences of each quantifier
-  for( int i=0; i<(int)d_quantEngine->getNumAssertedQuantifiers(); i++ ){
-    Node f = d_quantEngine->getAssertedQuantifier( i );
-    Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
-    std::vector< Node > pro_con[2];
-    std::vector< Node > pro_con_patterns[2];
-    //check which model basis terms have good and bad definitions according to f
-    for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin();
-         it != d_quantEngine->d_phase_reqs[f].end(); ++it ){
-      Node n = it->first;
-      Node gn = d_model_basis[n];
-      Debug("fmf-model-req") << "   Req: " << n << " -> " << it->second << std::endl;
-      int pref = 0;
-      bool isConst = true;
-      std::vector< Node > uf_terms;
-      std::vector< Node > uf_term_patterns;
-      if( gn.getKind()==APPLY_UF ){
-        if( d_quantEngine->getEqualityQuery()->hasTerm( gn ) ){
-          uf_terms.push_back( gn );
-          uf_term_patterns.push_back( n );
-          bool phase = areEqual( gn, NodeManager::currentNM()->mkConst( true ) );
-          pref = phase!=it->second ? 1 : -1;
-        }
-      }else if( gn.getKind()==EQUAL ){
-        bool success = true;
-        for( int j=0; j<2; j++ ){
-          if( n[j].getKind()==APPLY_UF ){
-            Node op = gn[j].getOperator();
-            if( d_uf_model.find( op )!=d_uf_model.end() ){
-              Assert( gn[j].getKind()==APPLY_UF );
-              uf_terms.push_back( gn[j] );
-              uf_term_patterns.push_back( n[j] );
-            }else{
-              //found undefined uf operator
-              success = false;
-            }
-          }else if( n[j].hasAttribute(InstConstantAttribute()) ){
-            isConst = false;
-          }
-        }
-        if( success && !uf_terms.empty() ){
-          if( (!it->second && areEqual( gn[0], gn[1] )) || (it->second && areDisequal( gn[0], gn[1] )) ){
-            pref = 1;
-          }else if( (it->second && areEqual( gn[0], gn[1] )) || (!it->second && areDisequal( gn[0], gn[1] )) ){
-            pref = -1;
-          }
-        }
-      }
-      if( pref!=0 ){
-        Debug("fmf-model-prefs") << "  It is " << ( pref==1 ? "pro" : "con" );
-        Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
-        if( pref==1 ){
-          if( isConst ){
-            for( int j=0; j<(int)uf_terms.size(); j++ ){
-              //the only uf that is initialized are those that are constant
-              Node op = uf_terms[j].getOperator();
-              Assert( d_uf_model.find( op )!=d_uf_model.end() );
-              if( !d_uf_model[op].isConstant() ){
-                isConst = false;
-                break;
-              }
-            }
-            if( isConst ){
-              d_quant_sat[f] = true;
-              //we only need to consider current term definition(s) for this quantifier to be satisified, ignore the others
-              for( int k=0; k<2; k++ ){
-                pro_con[k].clear();
-                pro_con_patterns[k].clear();
-              } 
-              //instead, just note to the model for each uf term that f is pro its definition
-              for( int j=0; j<(int)uf_terms.size(); j++ ){
-                Node op = uf_terms[j].getOperator();
-                d_uf_model[op].d_reconsider_model = false;
-              }
-            }
-          }
-        }
-        if( d_quant_sat.find( f )!=d_quant_sat.end() ){
-          Debug("fmf-model-prefs") << "  * Constant SAT due to definition of " << n << std::endl;
-          break;
-        }else{
-          int pcIndex = pref==1 ? 0 : 1;
-          for( int j=0; j<(int)uf_terms.size(); j++ ){
-            pro_con[pcIndex].push_back( uf_terms[j] );
-            pro_con_patterns[pcIndex].push_back( uf_term_patterns[j] );
-          }
-        }
-      }
-    }
-    if( d_quant_sat.find( f )!=d_quant_sat.end() ){
-      quantSatInit++;
-      d_statistics.d_pre_sat_quant += quantSatInit;
-    }else{
-      nquantSatInit++;
-      d_statistics.d_pre_nsat_quant += quantSatInit;
-    }
-    //add quantifier's preferences to vector
-    for( int k=0; k<2; k++ ){
-      for( int j=0; j<(int)pro_con[k].size(); j++ ){
-        Node op = pro_con[k][j].getOperator();
-        d_uf_model[op].setValuePreference( f, pro_con[k][j], k==0 );
-        d_pro_con_quant[k][ f ].push_back( pro_con_patterns[k][j] );
-      }
-    }
-  }
-  Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl;
-}
-
-int ModelEngine::instantiateQuantifier( Node f ){
+int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
+  int tests = 0;
   int addedLemmas = 0;
+  int triedLemmas = 0;
   Debug("inst-fmf-ei") << "Add matches for " << f << "..." << std::endl;
   Debug("inst-fmf-ei") << "   Instantiation Constants: ";
   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    Debug("inst-fmf-ei") << d_quantEngine->getInstantiationConstant( f, i ) << " ";
+    Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
   }
   Debug("inst-fmf-ei") << std::endl;
-  for( int k=0; k<2; k++ ){
-    Debug("inst-fmf-ei") << "  " << ( k==0 ? "Pro" : "Con" ) << " definitions:" << std::endl;
-    for( int i=0; i<(int)d_pro_con_quant[k][f].size(); i++ ){
-      Debug("inst-fmf-ei") << "    " << d_pro_con_quant[k][f][i] << std::endl;
-    }
-  }
-  if( d_pro_con_quant[0][f].empty() ){
-    Debug("inst-fmf-ei") << "WARNING: " << f << " has no pros for default literal definitions" << std::endl;
-  }
-  d_eval_failed_lits.clear();
-  d_eval_failed.clear();
-  d_eval_term_model.clear();
-  //d_eval_term_vals.clear();
-  //d_eval_term_fv_deps.clear();
-  RepAlphabetIterator riter( d_quantEngine, f, this );
-  increment( &riter );
-#ifdef ONE_INST_PER_QUANT_PER_ROUND
-  while( !riter.isFinished() && addedLemmas==0 ){
-#else
-  while( !riter.isFinished() ){
+  if( d_builder.d_quant_selection_lits[f].empty() ){
+    Debug("inst-fmf-ei") << "WARNING: " << f << " has no model literal definitions (is f clausified?)" << std::endl;
+#ifdef ME_PRINT_WARNINGS
+    Message() << "WARNING: " << f << " has no model literal definitions (is f clausified?)" << std::endl;
 #endif
-    InstMatch m;
-    riter.getMatch( d_quantEngine, m );
-    Debug("fmf-model-eval") << "* Add instantiation " << std::endl;
-    riter.d_inst_tried++;
-    if( d_quantEngine->addInstantiation( f, m ) ){
-      addedLemmas++;
-    }
-    riter.increment( d_quantEngine );
-    increment( &riter );
-  }
-  if( Debug.isOn("inst-fmf-ei") ){
-    int totalInst = 1;
-    for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
-      totalInst = totalInst * (int)getReps()->d_type_reps[ f[0][i].getType() ].size();
-    }
-    Debug("inst-fmf-ei") << "Finished: " << std::endl;
-    Debug("inst-fmf-ei") << "   Inst Skipped: " << (totalInst-riter.d_inst_tried) << std::endl;
-    Debug("inst-fmf-ei") << "   Inst Tried: " << riter.d_inst_tried << std::endl;
-    Debug("inst-fmf-ei") << "   Inst Added: " << addedLemmas << std::endl;
-    Debug("inst-fmf-ei") << "   # Tests: " << riter.d_inst_tests << std::endl;
-  }
-  return addedLemmas;
-}
-
-void ModelEngine::registerModelBasis( Node n, Node gn ){
-  if( d_model_basis.find( n )==d_model_basis.end() ){
-    d_model_basis[n] = gn;
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      registerModelBasis( n[i], gn[i] );
-    }
-  }
-}
-
-Node ModelEngine::getArbitraryElement( TypeNode tn, std::vector< Node >& exclude ){
-  Node retVal;
-  if( tn==NodeManager::currentNM()->booleanType() ){
-    if( exclude.empty() ){
-      retVal = NodeManager::currentNM()->mkConst( false );
-    }else if( exclude.size()==1 ){
-      retVal = NodeManager::currentNM()->mkConst( areEqual( exclude[0], NodeManager::currentNM()->mkConst( false ) ) );
-    }
-  }else if( d_ra.d_type_reps.find( tn )!=d_ra.d_type_reps.end() ){
-    for( int i=0; i<(int)d_ra.d_type_reps[tn].size(); i++ ){
-      if( std::find( exclude.begin(), exclude.end(), d_ra.d_type_reps[tn][i] )==exclude.end() ){
-        retVal = d_ra.d_type_reps[tn][i];
-        break;
-      }
-    }
-  }
-  if( !retVal.isNull() ){
-    return d_quantEngine->getEqualityQuery()->getRepresentative( retVal );
   }else{
-    return Node::null();
-  }
-}
-
-Node ModelEngine::getModelBasisTerm( TypeNode tn, int i ){
-  return d_ss->getCardinalityTerm( tn );
-}
-
-Node ModelEngine::getModelBasisApplyUfTerm( Node op ){
-  if( d_model_basis_term.find( op )==d_model_basis_term.end() ){
-    TypeNode t = op.getType();
-    std::vector< Node > children;
-    children.push_back( op );
-    for( int i=0; i<(int)t.getNumChildren()-1; i++ ){
-      children.push_back( getModelBasisTerm( t[i] ) );
-    }
-    d_model_basis_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children );
-  }
-  return d_model_basis_term[op];
-}
-
-bool ModelEngine::isModelBasisTerm( Node op, Node n ){
-  if( n.getOperator()==op ){
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( !n[i].getAttribute(ModelBasisAttribute()) ){
-        return false;
-      }
-    }
-    return true;
-  }else{
-    return false;
-  }
-}
-
-void ModelEngine::initializeUf( Node n ){
-  std::vector< Node > terms;
-  collectUfTerms( n, terms );
-  for( int i=0; i<(int)terms.size(); i++ ){
-    initializeUfModel( terms[i].getOperator() );
-  }
-}
-
-void ModelEngine::collectUfTerms( Node n, std::vector< Node >& terms ){
-  if( n.getKind()==APPLY_UF ){
-    terms.push_back( n );
-  }
-  for( int i=0; i<(int)n.getNumChildren(); i++ ){
-    collectUfTerms( n[i], terms );
-  }
-}
-
-void ModelEngine::initializeUfModel( Node op ){
-  if( d_uf_model.find( op )==d_uf_model.end() ){
-    TypeNode tn = op.getType();
-    tn = tn[ (int)tn.getNumChildren()-1 ];
-    if( tn==NodeManager::currentNM()->booleanType() || uf::StrongSolverTheoryUf::isRelevantType( tn ) ){
-      d_uf_model[ op ] = UfModel( op, this );
-    }
-  }
-}
-
-void ModelEngine::makeEvalTermModel( Node n ){
-  if( d_eval_term_model.find( n )==d_eval_term_model.end() ){
-    makeEvalTermIndexOrder( n );
-    if( !d_eval_term_use_default_model[n] ){
-      Node op = n.getOperator();
-      d_eval_term_model[n] = UfModelTreeOrdered( op, d_eval_term_index_order[n] );
-      d_uf_model[op].makeModel( d_quantEngine, d_eval_term_model[n] );
-      Debug("fmf-model-index-order") << "Make model for " << n << " : " << std::endl;
-      d_eval_term_model[n].debugPrint( "fmf-model-index-order", d_quantEngine, 2 );
-    }
-  }
-}
-
-struct sortGetMaxVariableNum {
-  std::map< Node, int > d_max_var_num;
-  int computeMaxVariableNum( Node n ){
-    if( n.getKind()==INST_CONSTANT ){
-      return n.getAttribute(InstVarNumAttribute());
-    }else if( n.hasAttribute(InstConstantAttribute()) ){
-      int maxVal = -1;
-      for( int i=0; i<(int)n.getNumChildren(); i++ ){
-        int val = getMaxVariableNum( n[i] );
-        if( val>maxVal ){
-          maxVal = val;
-        }
-      }
-      return maxVal;
-    }else{
-      return -1;
-    }
-  }
-  int getMaxVariableNum( Node n ){
-    std::map< Node, int >::iterator it = d_max_var_num.find( n );
-    if( it==d_max_var_num.end() ){
-      int num = computeMaxVariableNum( n );
-      d_max_var_num[n] = num;
-      return num;
-    }else{
-      return it->second;
-    }
-  }
-  bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));}
-};
-
-void ModelEngine::makeEvalTermIndexOrder( Node n ){
-  if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){
-    //sort arguments in order of least significant vs. most significant variable in default ordering
-    std::map< Node, std::vector< int > > argIndex;
-    std::vector< Node > args;
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( argIndex.find( n[i] )==argIndex.end() ){
-        args.push_back( n[i] );
-      }
-      argIndex[n[i]].push_back( i );
-    }
-    sortGetMaxVariableNum sgmvn;
-    std::sort( args.begin(), args.end(), sgmvn );
-    for( int i=0; i<(int)args.size(); i++ ){
-      for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){
-        d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] );
-      }
-    }
-    bool useDefault = true;
-    for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
-      if( i!=d_eval_term_index_order[n][i] ){
-        useDefault = false;
-        break;
-      }
-    }
-    d_eval_term_use_default_model[n] = useDefault;
-    Debug("fmf-model-index-order") << "Will consider the following index ordering for " << n << " : ";
-    for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
-      Debug("fmf-model-index-order") << d_eval_term_index_order[n][i] << " ";
-    }
-    Debug("fmf-model-index-order") << std::endl;
-  }
-}
-
-//void ModelEngine::processPredicate( Node f, Node p, bool phase ){
-//  Node op = p.getOperator();
-//  initializeUfModel( op );
-//  d_uf_model[ op ].addRequirement( f, p, phase );
-//}
-//
-//void ModelEngine::processEquality( Node f, Node eq, bool phase ){
-//  for( int i=0; i<2; i++ ){
-//    int j = i==0 ? 1 : 0;
-//    if( eq[i].getKind()==APPLY_UF && eq[i].hasAttribute(InstConstantAttribute()) ){
-//      Node op = eq[i].getOperator();
-//      initializeUfModel( op );
-//      d_uf_model[ op ].addEqRequirement( f, eq[i], eq[j], phase );
-//    }
-//  }
-//}
-
-void ModelEngine::increment( RepAlphabetIterator* rai ){
-  if( useModel() ){
-    bool success;
-    do{
-      success = true;
-      if( !rai->isFinished() ){
-        //see if instantiation is already true in current model
-        Debug("fmf-model-eval") << "Evaulating ";
-        rai->debugPrintSmall("fmf-model-eval");
-        //calculate represenative terms we are currently considering
-        rai->calculateTerms( d_quantEngine );
-        rai->d_inst_tests++;
-        //if eVal is not (int)rai->d_index.size(), then the instantiation is already true in the model,
-        // and eVal is the highest index in rai which we can safely iterate
-        int depIndex;
-        if( evaluate( rai, d_quantEngine->getCounterexampleBody( rai->d_f ), depIndex )==1 ){
-          Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
-          //Notice() << "Returned eVal = " << eVal << "/" << rai->d_index.size() << std::endl;
-          if( depIndex<(int)rai->d_index.size() ){
-#ifdef DISABLE_EVAL_SKIP_MULTIPLE
-            depIndex = (int)rai->d_index.size()-1;
-#endif
-            rai->increment2( d_quantEngine, depIndex );
-            success = false;
+    Debug("inst-fmf-ei") << "  Model literal definitions:" << std::endl;
+    for( size_t i=0; i<d_builder.d_quant_selection_lits[f].size(); i++ ){
+      Debug("inst-fmf-ei") << "    " << d_builder.d_quant_selection_lits[f][i] << std::endl;
+    }
+  }
+  RepSetIterator riter( f, d_quantEngine->getModel() );
+  //set the domain for the iterator (the sufficient set of instantiations to try)
+  if( useRelInstDomain ){
+    riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
+  }
+  RepSetEvaluator reval( d_quantEngine->getModel(), &riter );
+  while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
+    d_testLemmas++;
+    if( d_builder.optUseModel() ){
+      //see if instantiation is already true in current model
+      Debug("fmf-model-eval") << "Evaluating ";
+      riter.debugPrintSmall("fmf-model-eval");
+      Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+      tests++;
+      //if evaluate(...)==1, then the instantiation is already true in the model
+      //  depIndex is the index of the least significant variable that this evaluation relies upon
+      int depIndex = riter.getNumTerms()-1;
+      int eval = reval.evaluate( d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), depIndex );
+      if( eval==1 ){
+        Debug("fmf-model-eval") << "  Returned success with depIndex = " << depIndex << std::endl;
+        riter.increment2( depIndex );
+      }else{
+        Debug("fmf-model-eval") << "  Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
+        InstMatch m;
+        riter.getMatch( d_quantEngine, m );
+        Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+        triedLemmas++;
+        d_triedLemmas++;
+        if( d_quantEngine->addInstantiation( f, m ) ){
+          addedLemmas++;
+#ifdef EVAL_FAIL_SKIP_MULTIPLE
+          if( eval==-1 ){
+            riter.increment2( depIndex );
+          }else{
+            riter.increment();
           }
+#else
+          riter.increment();
+#endif
         }else{
-          Debug("fmf-model-eval") << "  Returned failure." << std::endl;
-        }
-      }
-    }while( !success );
-  }
-}
-
-//if evaluate( rai, n, phaseReq ) = eVal,
-// if eVal = rai->d_index.size()
-//   then the formula n instantiated with rai cannot be proven to be equal to phaseReq
-// otherwise,
-//   each n{rai->d_index[0]/x_0...rai->d_index[eVal]/x_eVal, */x_(eVal+1) ... */x_n } is equal to phaseReq in the current model
-int ModelEngine::evaluate( RepAlphabetIterator* rai, Node n, int& depIndex ){
-  ++(d_statistics.d_eval_formulas);
-  //Debug("fmf-model-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;
-  if( n.getKind()==NOT ){
-    int val = evaluate( rai, n[0], depIndex );
-    return val==1 ? -1 : ( val==-1 ? 1 : 0 );
-  }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){
-    int baseVal = n.getKind()==AND ? 1 : -1;
-    int eVal = baseVal;
-    int posDepIndex = (int)rai->d_index.size();
-    int negDepIndex = -1;
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      //evaluate subterm
-      int childDepIndex;
-      Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i];
-      int eValT = evaluate( rai, nn, childDepIndex );
-      if( eValT==baseVal ){
-        if( eVal==baseVal ){
-          if( childDepIndex>negDepIndex ){
-            negDepIndex = childDepIndex;
-          }
-        }
-      }else if( eValT==-baseVal ){
-        eVal = -baseVal;
-        if( childDepIndex<posDepIndex ){
-          posDepIndex = childDepIndex;
-          if( posDepIndex==-1 ){
-            break;
-          }
-        }
-      }else if( eValT==0 ){
-        if( eVal==baseVal ){
-          eVal = 0;
+          Debug("ajr-temp") << "* Failed Add instantiation " << m << std::endl;
+          riter.increment();
         }
       }
-    }
-    if( eVal!=0 ){
-      depIndex = eVal==-baseVal ? posDepIndex : negDepIndex;
-      return eVal;
-    }else{
-      return 0;
-    }
-  }else if( n.getKind()==IFF || n.getKind()==XOR ){
-    int depIndex1;
-    int eVal = evaluate( rai, n[0], depIndex1 );
-    if( eVal!=0 ){
-      int depIndex2;
-      int eVal2 = evaluate( rai, n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2 );
-      if( eVal2!=0 ){
-        depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
-        return eVal==eVal2 ? 1 : -1;
-      }
-    }
-    return 0;
-  }else if( n.getKind()==ITE ){
-    int depIndex1;
-    int eVal = evaluate( rai, n[0], depIndex1 );
-    if( eVal==0 ){
-      //DO_THIS: evaluate children to see if they are the same value?
-      return 0;
     }else{
-      int depIndex2;
-      int eValT = evaluate( rai, n[eVal==1 ? 1 : 2], depIndex2 );
-      depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
-      return eValT;
-    }
-  }else if( n.getKind()==FORALL ){
-    return 0;
-  }else{
-    ////if we know we will fail again, immediately return
-    //if( d_eval_failed.find( n )!=d_eval_failed.end() ){
-    //  if( d_eval_failed[n] ){
-    //    return -1;
-    //  }
-    //}
-    //Debug("fmf-model-eval-debug") << "Evaluate literal " << n << std::endl;
-    //this should be a literal
-    Node gn = n.substitute( rai->d_ic.begin(), rai->d_ic.end(), rai->d_terms.begin(), rai->d_terms.end() );
-    //Debug("fmf-model-eval-debug") << "  Ground version = " << gn << std::endl;
-    int retVal = 0;
-    std::vector< Node > fv_deps;
-    if( n.getKind()==APPLY_UF ){
-      //case for boolean predicates
-      Node val = evaluateTerm( n, gn, fv_deps );
-      if( d_quantEngine->getEqualityQuery()->hasTerm( val ) ){
-        if( areEqual( val, NodeManager::currentNM()->mkConst( true ) ) ){
-          retVal = 1;
-        }else{
-          retVal = -1;
-        }
-      }
-    }else if( n.getKind()==EQUAL ){
-      //case for equality
-      retVal = evaluateEquality( n[0], n[1], gn[0], gn[1], fv_deps );
-    }
-    if( retVal!=0 ){
-      int maxIndex = -1;
-      for( int i=0; i<(int)fv_deps.size(); i++ ){
-        int index = rai->d_var_order[ fv_deps[i].getAttribute(InstVarNumAttribute()) ];
-        if( index>maxIndex ){
-          maxIndex = index;
-          if( index==(int)rai->d_index.size()-1 ){
-            break;
-          }
-        }
+      InstMatch m;
+      riter.getMatch( d_quantEngine, m );
+      Debug("fmf-model-eval") << "* Add instantiation " << std::endl;
+      triedLemmas++;
+      d_triedLemmas++;
+      if( d_quantEngine->addInstantiation( f, m ) ){
+        addedLemmas++;
       }
-      Debug("fmf-model-eval-debug") << "Evaluate literal: return " << retVal << ", depends = " << maxIndex << std::endl;
-      depIndex = maxIndex;
+      riter.increment();
     }
-    return retVal;
-  }
-}
-
-int ModelEngine::evaluateEquality( Node n1, Node n2, Node gn1, Node gn2, std::vector< Node >& fv_deps ){
-  ++(d_statistics.d_eval_eqs);
-  Debug("fmf-model-eval-debug") << "Evaluate equality: " << std::endl;
-  Debug("fmf-model-eval-debug") << "   " << n1 << " = " << n2 << std::endl;
-  Debug("fmf-model-eval-debug") << "   " << gn1 << " = " << gn2 << std::endl;
-  Node val1 = evaluateTerm( n1, gn1, fv_deps );
-  Node val2 = evaluateTerm( n2, gn2, fv_deps );
-  Debug("fmf-model-eval-debug") << "   Values :  ";
-  printRepresentative( "fmf-model-eval-debug", d_quantEngine, val1 );
-  Debug("fmf-model-eval-debug") <<  " = ";
-  printRepresentative( "fmf-model-eval-debug", d_quantEngine, val2 );
-  Debug("fmf-model-eval-debug") << std::endl;
-  int retVal = 0;
-  if( areEqual( val1, val2 ) ){
-    retVal = 1;
-  }else if( areDisequal( val1, val2 ) ){
-    retVal = -1;
-  }
-  if( retVal!=0 ){
-    Debug("fmf-model-eval-debug") << "   ---> Success, value = " << (retVal==1) << std::endl;
-  }else{
-    Debug("fmf-model-eval-debug") << "   ---> Failed" << std::endl;
-  }
-  Debug("fmf-model-eval-debug") << "       Value depends on variables: ";
-  for( int i=0; i<(int)fv_deps.size(); i++ ){
-    Debug("fmf-model-eval-debug") << fv_deps[i] << " ";
   }
-  Debug("fmf-model-eval-debug") << std::endl;
-  return retVal;
-}
-
-Node ModelEngine::evaluateTerm( Node n, Node gn, std::vector< Node >& fv_deps ){
-  if( n.hasAttribute(InstConstantAttribute()) ){
-    if( n.getKind()==INST_CONSTANT ){
-      fv_deps.push_back( n );
-      return gn;
-    //}else if( d_eval_term_fv_deps.find( n )!=d_eval_term_fv_deps.end() && 
-    //          d_eval_term_fv_deps[n].find( gn )!=d_eval_term_fv_deps[n].end() ){
-    //  fv_deps.insert( fv_deps.end(), d_eval_term_fv_deps[n][gn].begin(), d_eval_term_fv_deps[n][gn].end() );
-    //  return d_eval_term_vals[gn];
-    }else{
-      //Debug("fmf-model-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
-      //first we must evaluate the arguments
-      Node val = gn;
-      if( n.getKind()==APPLY_UF ){
-        Node op = gn.getOperator();
-        //if it is a defined UF, then consult the interpretation
-        Node gnn = gn;
-        ++(d_statistics.d_eval_uf_terms);
-        int depIndex = 0;
-        //first we must evaluate the arguments
-        bool childrenChanged = false;
-        std::vector< Node > children;
-        children.push_back( op );
-        std::map< int, std::vector< Node > > children_var_deps;
-        //for each argument, calculate its value, and the variables its value depends upon
-        for( int i=0; i<(int)n.getNumChildren(); i++ ){
-          Node nn = evaluateTerm( n[i], gn[i], children_var_deps[i] );
-          children.push_back( nn );
-          childrenChanged = childrenChanged || nn!=gn[i];
-        }
-        //remake gn if changed
-        if( childrenChanged ){
-          gnn = NodeManager::currentNM()->mkNode( APPLY_UF, children );
-        }
-        if( d_uf_model.find( op )!=d_uf_model.end() ){
-#ifdef USE_INDEX_ORDERING
-          //make the term model specifically for n
-          makeEvalTermModel( n );
-          //now, consult the model
-          if( d_eval_term_use_default_model[n] ){
-            val = d_uf_model[op].d_tree.getValue( d_quantEngine, gnn, depIndex );
-          }else{
-            val = d_eval_term_model[ n ].getValue( d_quantEngine, gnn, depIndex );
-          }
-          //Debug("fmf-model-eval-debug") << "Evaluate term " << n << " (" << gn << ", " << gnn << ")" << std::endl;
-          //d_eval_term_model[ n ].debugPrint("fmf-model-eval-debug", d_quantEngine );
-          Assert( !val.isNull() );
-#else
-          //now, consult the model
-          val = d_uf_model[op].d_tree.getValue( d_quantEngine, gnn, depIndex );
-#endif
-        }else{
-          d_eval_term_use_default_model[n] = true;
-          val = gnn;
-          depIndex = (int)n.getNumChildren();
-        }
-        Debug("fmf-model-eval-debug") << "Evaluate term " << n << " = " << gn << " = " << gnn << " = ";
-        printRepresentative( "fmf-model-eval-debug", d_quantEngine, val );
-        Debug("fmf-model-eval-debug") << ", depIndex = " << depIndex << std::endl;
-        if( !val.isNull() ){
-#ifdef USE_INDEX_ORDERING
-          for( int i=0; i<depIndex; i++ ){
-            int index = d_eval_term_use_default_model[n] ? i : d_eval_term_index_order[n][i];
-            Debug("fmf-model-eval-debug") << "Add variables from " << index << "..." << std::endl;
-            fv_deps.insert( fv_deps.end(), children_var_deps[index].begin(),
-                            children_var_deps[index].end() );
-          }
-#else
-          //calculate the free variables that the value depends on : take those in children_var_deps[0...depIndex-1]
-          for( std::map< int, std::vector< Node > >::iterator it = children_var_deps.begin(); it != children_var_deps.end(); ++it ){
-            if( it->first<depIndex ){
-              fv_deps.insert( fv_deps.end(), it->second.begin(), it->second.end() );
-            }
-          }
-#endif
-        }
-        ////cache the result
-        //d_eval_term_vals[gn] = val;
-        //d_eval_term_fv_deps[n][gn].insert( d_eval_term_fv_deps[n][gn].end(), fv_deps.begin(), fv_deps.end() );
+  d_statistics.d_eval_formulas += reval.d_eval_formulas;
+  d_statistics.d_eval_eqs += reval.d_eval_eqs;
+  d_statistics.d_eval_uf_terms += reval.d_eval_uf_terms;
+  int totalInst = 1;
+  int relevantInst = 1;
+  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+    totalInst = totalInst * (int)d_quantEngine->getModel()->d_ra.d_type_reps[ f[0][i].getType() ].size();
+    relevantInst = relevantInst * (int)riter.d_domain[i].size();
+  }
+  d_totalLemmas += totalInst;
+  d_relevantLemmas += relevantInst;
+  Debug("inst-fmf-ei") << "Finished: " << std::endl;
+  Debug("inst-fmf-ei") << "   Inst Total: " << totalInst << std::endl;
+  Debug("inst-fmf-ei") << "   Inst Relevant: " << relevantInst << std::endl;
+  Debug("inst-fmf-ei") << "   Inst Tried: " << triedLemmas << std::endl;
+  Debug("inst-fmf-ei") << "   Inst Added: " << addedLemmas << std::endl;
+  Debug("inst-fmf-ei") << "   # Tests: " << tests << std::endl;
+///-----------
+#ifdef ME_PRINT_WARNINGS
+  if( addedLemmas>1000 ){
+    Notice() << "WARNING: many instantiations produced for " << f << ": " << std::endl;
+    Notice() << "   Inst Total: " << totalInst << std::endl;
+    Notice() << "   Inst Relevant: " << totalRelevant << std::endl;
+    Notice() << "   Inst Tried: " << triedLemmas << std::endl;
+    Notice() << "   Inst Added: " << addedLemmas << std::endl;
+    Notice() << "   # Tests: " << tests << std::endl;
+    Notice() << std::endl;
+    if( !d_builder.d_quant_selection_lits[f].empty() ){
+      Notice() << "  Model literal definitions:" << std::endl;
+      for( size_t i=0; i<d_builder.d_quant_selection_lits[f].size(); i++ ){
+        Notice() << "    " << d_builder.d_quant_selection_lits[f][i] << std::endl;
       }
-      return val;
+      Notice() << std::endl;
     }
-  }else{
-    return n;
-  }
-}
-
-void ModelEngine::clearEvalFailed( int index ){
-  for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){
-    d_eval_failed[ d_eval_failed_lits[index][i] ] = false;
   }
-  d_eval_failed_lits[index].clear();
-}
-
-bool ModelEngine::areEqual( Node a, Node b ){
-  return d_quantEngine->getEqualityQuery()->areEqual( a, b );
-}
-
-bool ModelEngine::areDisequal( Node a, Node b ){
-  return d_quantEngine->getEqualityQuery()->areDisequal( a, b );
+#endif
+///-----------
+  return addedLemmas;
 }
 
 void ModelEngine::debugPrint( const char* c ){
-  Debug( c ) << "---Current Model---" << std::endl;
-  Debug( c ) << "Representatives: " << std::endl;
-  d_ra.debugPrint( c, d_quantEngine );
   Debug( c ) << "Quantifiers: " << std::endl;
-  for( int i=0; i<(int)d_quantEngine->getNumAssertedQuantifiers(); i++ ){
-    Node f = d_quantEngine->getAssertedQuantifier( i );
+  for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+    Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
     Debug( c ) << "   ";
-    if( d_quant_sat.find( f )!=d_quant_sat.end() ){
+    if( d_builder.d_quant_sat.find( f )!=d_builder.d_quant_sat.end() ){
       Debug( c ) << "*SAT* ";
     }else{
       Debug( c ) << "      ";
     }
     Debug( c ) << f << std::endl;
   }
-  Debug( c ) << "Functions: " << std::endl;
-  for( std::map< Node, UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
-    it->second.debugPrint( c );
-    Debug( c ) << std::endl;
-  }
+  //d_quantEngine->getModel()->debugPrint( c );
 }
 
 ModelEngine::Statistics::Statistics():
   d_inst_rounds("ModelEngine::Inst_Rounds", 0),
-  d_pre_sat_quant("ModelEngine::Status_quant_pre_sat", 0),
-  d_pre_nsat_quant("ModelEngine::Status_quant_pre_non_sat", 0),
   d_eval_formulas("ModelEngine::Eval_Formulas", 0 ),
   d_eval_eqs("ModelEngine::Eval_Equalities", 0 ),
   d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ),
@@ -1380,8 +663,6 @@ ModelEngine::Statistics::Statistics():
   d_num_quants_init_fail("ModelEngine::Num_Quants_No_Basis", 0 )
 {
   StatisticsRegistry::registerStat(&d_inst_rounds);
-  StatisticsRegistry::registerStat(&d_pre_sat_quant);
-  StatisticsRegistry::registerStat(&d_pre_nsat_quant);
   StatisticsRegistry::registerStat(&d_eval_formulas);
   StatisticsRegistry::registerStat(&d_eval_eqs);
   StatisticsRegistry::registerStat(&d_eval_uf_terms);
@@ -1391,11 +672,11 @@ ModelEngine::Statistics::Statistics():
 
 ModelEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_inst_rounds);
-  StatisticsRegistry::unregisterStat(&d_pre_sat_quant);
-  StatisticsRegistry::unregisterStat(&d_pre_nsat_quant);
   StatisticsRegistry::unregisterStat(&d_eval_formulas);
   StatisticsRegistry::unregisterStat(&d_eval_eqs);
   StatisticsRegistry::unregisterStat(&d_eval_uf_terms);
   StatisticsRegistry::unregisterStat(&d_num_quants_init);
   StatisticsRegistry::unregisterStat(&d_num_quants_init_fail);
 }
+
+