merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding. Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version

12 files changed, 830 insertions, 643 deletions

diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index ae5b99c06..316e2fbff 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -24,6 +24,8 @@ libquantifiers_la_SOURCES = \
 	term_database.h \
 	term_database.cpp \
 	first_order_model.h \
-	first_order_model.cpp
+	first_order_model.cpp \
+	model_builder.h \
+	model_builder.cpp
 
 EXTRA_DIST = kinds
\ No newline at end of file
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 71a48b33d..766bd31ae 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -17,7 +17,7 @@
 #include "theory/quantifiers/first_order_model.h"

 #include "theory/quantifiers/rep_set_iterator.h"

 #include "theory/quantifiers/model_engine.h"

-#include "theory/uf/theory_uf_strong_solver.h"

+#include "theory/quantifiers/term_database.h"

 

 using namespace std;

 using namespace CVC4;

@@ -26,25 +26,37 @@ using namespace CVC4::context;
 using namespace CVC4::theory;

 using namespace CVC4::theory::quantifiers;

 

-FirstOrderModel::FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ) : DefaultModel( c, name ),

+FirstOrderModel::FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ) : DefaultModel( c, name, true ),

 d_term_db( qe->getTermDatabase() ), d_forall_asserts( c ){

 

 }

 

-void FirstOrderModel::initialize(){

+void FirstOrderModel::reset(){

   //rebuild models

-  d_uf_model.clear();

+  d_uf_model_tree.clear();

+  d_uf_model_gen.clear();

   d_array_model.clear();

+  DefaultModel::reset();

+}

+

+void FirstOrderModel::addTerm( Node n ){

+  //std::vector< Node > added;

+  //d_term_db->addTerm( n, added, false );

+  DefaultModel::addTerm( n );

+}

+

+void FirstOrderModel::initialize(){

+  //this is called after representatives have been chosen and the equality engine has been built

   //for each quantifier, collect all operators we care about

   for( int i=0; i<getNumAssertedQuantifiers(); i++ ){

     Node f = getAssertedQuantifier( i );

-    //initialize model for term

+    //initialize relevant models within bodies of all quantifiers

     initializeModelForTerm( f[1] );

   }

-

+  //for debugging

   if( Options::current()->printModelEngine ){

-    for( std::map< TypeNode, std::vector< Node > >::iterator it = d_ra.d_type_reps.begin(); it != d_ra.d_type_reps.end(); ++it ){

-      if( uf::StrongSolverTheoryUf::isRelevantType( it->first ) ){

+    for( std::map< TypeNode, std::vector< Node > >::iterator it = d_rep_set.d_type_reps.begin(); it != d_rep_set.d_type_reps.end(); ++it ){

+      if( it->first.isSort() ){

         Message() << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;

       }

     }

@@ -54,33 +66,44 @@ void FirstOrderModel::initialize(){
 void FirstOrderModel::initializeModelForTerm( Node n ){

   if( n.getKind()==APPLY_UF ){

     Node op = n.getOperator();

-    if( d_uf_model.find( op )==d_uf_model.end() ){

+    if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){

       TypeNode tn = op.getType();

       tn = tn[ (int)tn.getNumChildren()-1 ];

-      if( tn==NodeManager::currentNM()->booleanType() || uf::StrongSolverTheoryUf::isRelevantType( tn ) ){

-        d_uf_model[ op ] = uf::UfModel( op, this );

+      //only generate models for predicates and functions with uninterpreted range types

+      if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){

+        d_uf_model_tree[ op ] = uf::UfModelTree( op );

+        d_uf_model_gen[ op ].clear();

       }

     }

   }

-  if( n.getKind()!=STORE && n.getType().isArray() ){

-    d_array_model[n] = Node::null();

+  /*

+  if( n.getType().isArray() ){

+    while( n.getKind()==STORE ){

+      n = n[0];

+    }

+    Node nn = getRepresentative( n );

+    if( d_array_model.find( nn )==d_array_model.end() ){

+      d_array_model[nn] = arrays::ArrayModel( nn, this );

+    }

   }

+  */

   for( int i=0; i<(int)n.getNumChildren(); i++ ){

     initializeModelForTerm( n[i] );

   }

 }

 

 void FirstOrderModel::toStreamFunction( Node n, std::ostream& out ){

+  /*

   if( d_uf_model.find( n )!=d_uf_model.end() ){

     //d_uf_model[n].toStream( out );

     Node value = d_uf_model[n].getFunctionValue();

     out << "(" << n << " " << value << ")";

-  //}else if( d_array_model.find( n )!=d_array_model.end() ){

-    //out << "(" << n << " " << d_array_model[n] << ")" << std::endl;

-  //  out << "(" << n << " Array)" << std::endl;

-  }else{

-    DefaultModel::toStreamFunction( n, out );

+  }else if( d_array_model.find( n )!=d_array_model.end() ){

+    Node value = d_array_model[n].getArrayValue();

+    out << "(" << n << " " << value << ")" << std::endl;

   }

+  */

+  DefaultModel::toStreamFunction( n, out );

 }

 

 void FirstOrderModel::toStreamType( TypeNode tn, std::ostream& out ){

@@ -91,14 +114,29 @@ Node FirstOrderModel::getInterpretedValue( TNode n ){
   Debug("fo-model") << "get interpreted value " << n << std::endl;

   TypeNode type = n.getType();

   if( type.isFunction() || type.isPredicate() ){

-    if( d_uf_model.find( n )!=d_uf_model.end() ){

-      return d_uf_model[n].getFunctionValue();

+    if( d_uf_models.find( n )==d_uf_models.end() ){

+      //use the model tree to generate the model

+      Node fn = d_uf_model_tree[n].getFunctionValue();

+      d_uf_models[n] = fn;

+      return fn;

+    }

+  /*

+  }else if( type.isArray() ){

+    if( d_array_model.find( n )!=d_array_model.end() ){

+      return d_array_model[n].getArrayValue();

     }else{

-      return n;

+      //std::cout << "no array model generated for " << n << std::endl;

     }

+  */

   }else if( n.getKind()==APPLY_UF ){

-    int depIndex;

-    return d_uf_model[ n.getOperator() ].getValue( n, depIndex );

+    Node op = n.getOperator();

+    if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){

+      //consult the uf model

+      int depIndex;

+      return d_uf_model_tree[ op ].getValue( this, n, depIndex );

+    }

+  }else if( n.getKind()==SELECT ){

+

   }

   return DefaultModel::getInterpretedValue( n );

 }

@@ -113,14 +151,14 @@ void FirstOrderModel::toStream(std::ostream& out){
 #if 0

   out << "---Current Model---" << std::endl;

   out << "Representatives: " << std::endl;

-  d_ra.toStream( out );

+  d_rep_set.toStream( out );

   out << "Functions: " << std::endl;

   for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){

     it->second.toStream( out );

     out << std::endl;

   }

 #elif 0

-  d_ra.toStream( out );

+  d_rep_set.toStream( out );

   //print everything not related to UF in equality engine

   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );

   while( !eqcs_i.isFinished() ){

diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 832acbee3..825518ed0 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -21,6 +21,7 @@
 

 #include "theory/model.h"

 #include "theory/uf/theory_uf_model.h"

+#include "theory/arrays/theory_arrays_model.h"

 

 namespace CVC4 {

 namespace theory {

@@ -43,6 +44,8 @@ class FirstOrderModel : public DefaultModel
 private:

   //pointer to term database

   TermDb* d_term_db;

+  //add term function

+  void addTerm( Node n );

   //for initialize model

   void initializeModelForTerm( Node n );

   /** to stream functions */

@@ -50,10 +53,12 @@ private:
   void toStreamType( TypeNode tn, std::ostream& out );

 public: //for Theory UF:

   //models for each UF operator

-  std::map< Node, uf::UfModel > d_uf_model;

+  std::map< Node, uf::UfModelTree > d_uf_model_tree;

+  //model generators

+  std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;

 public: //for Theory Arrays:

   //default value for each non-store array

-  std::map< Node, Node > d_array_model;

+  std::map< Node, arrays::ArrayModel > d_array_model;

 public: //for Theory Quantifiers:

   /** list of quantifiers asserted in the current context */

   context::CDList<Node> d_forall_asserts;

@@ -64,11 +69,13 @@ public: //for Theory Quantifiers:
 public:

   FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name );

   virtual ~FirstOrderModel(){}

-  // initialize the model

-  void initialize();

+  // reset the model

+  void reset();

   /** get interpreted value */

   Node getInterpretedValue( TNode n );

 public:

+  // initialize the model

+  void initialize();

   /** get term database */

   TermDb* getTermDatabase();

   /** to stream function */

diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
new file mode 100644
index 000000000..9cd5020fb
--- /dev/null
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -0,0 +1,417 @@
+/*********************                                                        */
+/*! \file model_builder.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of model builder class
+ **/
+
+#include "theory/quantifiers/model_engine.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/theory_uf_model.h"
+#include "theory/uf/theory_uf_instantiator.h"
+#include "theory/arrays/theory_arrays_model.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/model_builder.h"
+
+//#define ME_PRINT_WARNINGS
+
+#define RECONSIDER_FUNC_CONSTANT
+//#define ONE_QUANT_PER_ROUND_INST_GEN
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+ModelEngineBuilder::ModelEngineBuilder( QuantifiersEngine* qe ) :
+TheoryEngineModelBuilder( qe->getTheoryEngine() ),
+d_qe( qe ){
+
+}
+
+Node ModelEngineBuilder::chooseRepresentative( TheoryModel* m, Node eqc ){
+  Assert( m->d_equalityEngine.hasTerm( eqc ) );
+  Assert( m->d_equalityEngine.getRepresentative( eqc )==eqc );
+  //avoid interpreted symbols
+  if( isBadRepresentative( eqc ) ){
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &m->d_equalityEngine );
+    while( !eqc_i.isFinished() ){
+      if( !isBadRepresentative( *eqc_i ) ){
+        return *eqc_i;
+      }
+      ++eqc_i;
+    }
+    //otherwise, make new value?
+    //Message() << "Warning: Bad rep " << eqc << std::endl;
+  }
+  return eqc;
+}
+
+bool ModelEngineBuilder::isBadRepresentative( Node n ){
+  return n.getKind()==SELECT || n.getKind()==APPLY_SELECTOR;
+}
+
+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 functions
+    analyzeModel( fm );
+    //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;
+          }
+        }
+      }
+      if( Options::current()->printModelEngine ){
+        if( d_addedLemmas>0 ){
+          Message() << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
+        }else{
+          Message() << "No InstGen lemmas..." << std::endl;
+        }
+      }
+      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 );
+    }
+  }
+}
+
+void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){
+  //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 ){
+    Node op = it->first;
+    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()) ){
+        Node v = fm->getRepresentative( n );
+        if( i==0 ){
+          d_uf_prefs[op].d_const_val = v;
+        }else if( v!=d_uf_prefs[op].d_const_val ){
+          d_uf_prefs[op].d_const_val = Node::null();
+          break;
+        }
+      }
+    }
+    if( !d_uf_prefs[op].d_const_val.isNull() ){
+      fm->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val );
+      fm->d_uf_model_gen[op].makeModel( fm, it->second );
+      Debug("fmf-model-cons") << "Function " << op << " is the constant function ";
+      fm->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val );
+      Debug("fmf-model-cons") << std::endl;
+      d_uf_model_constructed[op] = true;
+    }else{
+      d_uf_model_constructed[op] = false;
+    }
+  }
+}
+
+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{
+          pref = -1;
+        }
+      }
+      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 = !d_uf_prefs[gn.getOperator()].d_const_val.isNull();
+        }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_tree.find( op )!=fm->d_uf_model_tree.end() ){
+                  uf_terms.push_back( gn[j] );
+                  isConst = isConst && !d_uf_prefs[op].d_const_val.isNull();
+                }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{
+          int pcIndex = pref==1 ? 0 : 1;
+          for( int j=0; j<(int)uf_terms.size(); j++ ){
+            pro_con[pcIndex].push_back( uf_terms[j] );
+          }
+        }
+      }
+    }
+    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{
+      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 );
+        }
+      }
+    }
+  }
+  Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl;
+}
+
+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( 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 applicable, try to add exceptions here
+    if( !tr_terms.empty() ){
+      //make a trigger for these terms, add instantiations
+      inst::Trigger* tr = inst::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 ModelEngineBuilder::finishBuildModel( FirstOrderModel* fm ){
+  //build model for UF
+  for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+    finishBuildModelUf( fm, it->first );
+  }
+  /*
+  //build model for arrays
+  for( std::map< Node, arrays::ArrayModel >::iterator it = fm->d_array_model.begin(); it != fm->d_array_model.end(); ++it ){
+    //consult the model basis select term
+    // i.e. the default value for array A is the value of select( A, e ), where e is the model basis term
+    TypeNode tn = it->first.getType();
+    Node selModelBasis = NodeManager::currentNM()->mkNode( SELECT, it->first, fm->getTermDatabase()->getModelBasisTerm( tn[0] ) );
+    it->second.setDefaultValue( fm->getRepresentative( selModelBasis ) );
+  }
+  */
+  Debug("fmf-model-debug") << "Done building models." << std::endl;
+}
+
+void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, Node op ){
+#ifdef RECONSIDER_FUNC_CONSTANT
+  if( d_uf_model_constructed[op] ){
+    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 v = d_uf_prefs[op].d_const_val;
+      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;
+        fm->d_uf_model_tree[op].clear();
+        fm->d_uf_model_gen[op].clear();
+        d_uf_model_constructed[op] = false;
+      }
+    }
+  }
+#endif
+  if( !d_uf_model_constructed[op] ){
+    //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<fm->d_uf_terms[op].size(); i++ ){
+      Node n = fm->d_uf_terms[op][i];
+      fm->getTermDatabase()->computeModelBasisArgAttribute( n );
+      if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
+        Node v = fm->getRepresentative( n );
+        //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 << " = ";
+        fm->printRepresentativeDebug( "fmf-model-cons", v );
+        Debug("fmf-model-cons") << std::endl;
+        //set it as ground value
+        fm->d_uf_model_gen[op].setValue( fm, n, v );
+        if( fm->d_uf_model_gen[op].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 ){
+            fm->d_uf_model_gen[op].setValue( fm, n, v, false );
+            if( n==defaultTerm ){
+              //incidentally already set, we will not need to find a default value
+              setDefaultVal = false;
+            }
+          }
+        }else{
+          if( n==defaultTerm ){
+            fm->d_uf_model_gen[op].setValue( fm, n, v, false );
+            //incidentally already set, we will not need to find a default value
+            setDefaultVal = 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() );
+      fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
+    }
+    Debug("fmf-model-cons") << "  Making model...";
+    fm->d_uf_model_gen[op].makeModel( fm, fm->d_uf_model_tree[op] );
+    d_uf_model_constructed[op] = true;
+    Debug("fmf-model-cons") << "  Finished constructing model for " << op << "." << std::endl;
+  }
+}
+
+void ModelEngineBuilder::finishProcessBuildModel( TheoryModel* m ){
+  for( std::map< Node, Node >::iterator it = m->d_reps.begin(); it != m->d_reps.end(); ++it ){
+    //build proper representatives (TODO)
+  }
+}
+
+bool ModelEngineBuilder::optUseModel() {
+  return Options::current()->fmfModelBasedInst;
+}
+
+bool ModelEngineBuilder::optInstGen(){
+  return Options::current()->fmfInstGen;
+}
+
+bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){
+#ifdef ONE_QUANT_PER_ROUND_INST_GEN
+  return true;
+#else
+  return false;
+#endif
+}
+
+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);
+}
+
+ModelEngineBuilder::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_pre_sat_quant);
+  StatisticsRegistry::unregisterStat(&d_pre_nsat_quant);
+}
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
new file mode 100644
index 000000000..13d500d8e
--- /dev/null
+++ b/src/theory/quantifiers/model_builder.h
@@ -0,0 +1,91 @@
+/*********************                                                        */

+/*! \file model_builder.h

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: mdeters

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)

+ ** Courant Institute of Mathematical Sciences

+ ** New York University

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Model Builder class

+ **/

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__QUANTIFIERS_MODEL_BUILDER_H

+#define __CVC4__QUANTIFIERS_MODEL_BUILDER_H

+

+#include "theory/quantifiers_engine.h"

+#include "theory/model.h"

+#include "theory/uf/theory_uf_model.h"

+

+namespace CVC4 {

+namespace theory {

+namespace quantifiers {

+

+//the model builder

+class ModelEngineBuilder : public TheoryEngineModelBuilder

+{

+protected:

+  //quantifiers engine

+  QuantifiersEngine* d_qe;

+  //map from operators to model preference data

+  std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;

+  //built model uf

+  std::map< Node, bool > d_uf_model_constructed;

+  /** process build model */

+  void processBuildModel( TheoryModel* m );

+  /** choose representative for unconstrained equivalence class */

+  Node chooseRepresentative( TheoryModel* m, Node eqc );

+  /** bad representative */

+  bool isBadRepresentative( Node n );

+protected:

+  //analyze model

+  void analyzeModel( FirstOrderModel* fm );

+  //analyze quantifiers

+  void analyzeQuantifiers( FirstOrderModel* fm );

+  //build model

+  void finishBuildModel( FirstOrderModel* fm );

+  //theory-specific build models

+  void finishBuildModelUf( FirstOrderModel* fm, Node op );

+  //do InstGen techniques for quantifier, return number of lemmas produced

+  int doInstGen( FirstOrderModel* fm, Node f );

+public:

+  ModelEngineBuilder( QuantifiersEngine* qe );

+  virtual ~ModelEngineBuilder(){}

+  /** finish model */

+  void finishProcessBuildModel( TheoryModel* m );

+public:

+  /** number of lemmas generated while building model */

+  int d_addedLemmas;

+  //map from quantifiers to if are constant SAT

+  std::map< Node, bool > d_quant_sat;

+  //map from quantifiers to the instantiation literals that their model is dependent upon

+  std::map< Node, std::vector< Node > > d_quant_selection_lits;

+public:

+  //map from quantifiers to model basis match

+  std::map< Node, InstMatch > d_quant_basis_match;

+  //options

+  bool optUseModel();

+  bool optInstGen();

+  bool optOneQuantPerRoundInstGen();

+  /** statistics class */

+  class Statistics {

+  public:

+    IntStat d_pre_sat_quant;

+    IntStat d_pre_nsat_quant;

+    Statistics();

+    ~Statistics();

+  };

+  Statistics d_statistics;

+};

+

+}

+}

+}

+

+#endif

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 663f270eb..ddaaa5b6f 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -21,16 +21,13 @@
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/uf/theory_uf_instantiator.h"
+#include "theory/arrays/theory_arrays_model.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 
 //#define ME_PRINT_WARNINGS
 
-//#define DISABLE_EVAL_SKIP_MULTIPLE
-
-#define RECONSIDER_FUNC_CONSTANT
 #define EVAL_FAIL_SKIP_MULTIPLE
-//#define ONE_QUANT_PER_ROUND_INST_GEN
 //#define ONE_QUANT_PER_ROUND
 
 using namespace std;
@@ -41,324 +38,6 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
-ModelEngineBuilder::ModelEngineBuilder( QuantifiersEngine* qe ) :
-TheoryEngineModelBuilder( qe->getTheoryEngine() ),
-d_qe( qe ){
-
-}
-
-Node ModelEngineBuilder::chooseRepresentative( TheoryModel* tm, Node eqc ){
-  return eqc;
-}
-
-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;
-          }
-        }
-      }
-      if( Options::current()->printModelEngine ){
-        if( d_addedLemmas>0 ){
-          Message() << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
-        }else{
-          Message() << "No InstGen lemmas..." << std::endl;
-        }
-      }
-      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 );
-    }
-  }
-}
-
-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{
-          pref = -1;
-        }
-      }
-      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{
-          int pcIndex = pref==1 ? 0 : 1;
-          for( int j=0; j<(int)uf_terms.size(); j++ ){
-            pro_con[pcIndex].push_back( uf_terms[j] );
-          }
-        }
-      }
-    }
-    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{
-      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 );
-        }
-      }
-    }
-  }
-  Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl;
-}
-
-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( 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 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 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 );
-  }
-  //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;
-}
-
-void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, uf::UfModel& model ){
-  Node op = model.getOperator();
-#ifdef RECONSIDER_FUNC_CONSTANT
-  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_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
-  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 << " = ";
-      fm->printRepresentativeDebug( "fmf-model-cons", v );
-      Debug("fmf-model-cons") << std::endl;
-      //set it as ground value
-      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{
-        if( n==defaultTerm ){
-          model.setValue( n, v, false );
-          //incidentally already set, we will not need to find a default value
-          setDefaultVal = 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...";
-    model.setModel();
-    Debug("fmf-model-cons") << "  Finished constructing model for " << op << "." << std::endl;
-  }
-}
-
-bool ModelEngineBuilder::optUseModel() {
-  return Options::current()->fmfModelBasedInst;
-}
-
-bool ModelEngineBuilder::optInstGen(){
-  return Options::current()->fmfInstGen;
-}
-
-bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){
-#ifdef ONE_QUANT_PER_ROUND_INST_GEN
-  return true;
-#else
-  return false;
-#endif
-}
-
-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);
-}
-
-ModelEngineBuilder::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_pre_sat_quant);
-  StatisticsRegistry::unregisterStat(&d_pre_nsat_quant);
-}
-
 //Model Engine constructor
 ModelEngine::ModelEngine( QuantifiersEngine* qe ) :
 QuantifiersModule( qe ),
@@ -448,6 +127,8 @@ void ModelEngine::check( Theory::Effort e ){
       //CVC4 will answer SAT
       Debug("fmf-consistent") << std::endl;
       debugPrint("fmf-consistent");
+      // finish building the model in the standard way
+      d_builder.finishProcessBuildModel( d_quantEngine->getModel() );
     }else{
       //otherwise, the search will continue
       d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
@@ -601,12 +282,13 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
     }
   }
   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;
+  d_statistics.d_eval_lits += reval.d_eval_lits;
+  d_statistics.d_eval_lits_unknown += reval.d_eval_lits_unknown;
   int totalInst = 1;
   int relevantInst = 1;
   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
-    totalInst = totalInst * (int)d_quantEngine->getModel()->d_ra.d_type_reps[ f[0][i].getType() ].size();
+    totalInst = totalInst * (int)d_quantEngine->getModel()->d_rep_set.d_type_reps[ f[0][i].getType() ].size();
     relevantInst = relevantInst * (int)riter.d_domain[i].size();
   }
   d_totalLemmas += totalInst;
@@ -658,15 +340,17 @@ void ModelEngine::debugPrint( const char* c ){
 ModelEngine::Statistics::Statistics():
   d_inst_rounds("ModelEngine::Inst_Rounds", 0),
   d_eval_formulas("ModelEngine::Eval_Formulas", 0 ),
-  d_eval_eqs("ModelEngine::Eval_Equalities", 0 ),
   d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ),
+  d_eval_lits("ModelEngine::Eval_Lits", 0 ),
+  d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ),
   d_num_quants_init("ModelEngine::Num_Quants", 0 ),
   d_num_quants_init_fail("ModelEngine::Num_Quants_No_Basis", 0 )
 {
   StatisticsRegistry::registerStat(&d_inst_rounds);
   StatisticsRegistry::registerStat(&d_eval_formulas);
-  StatisticsRegistry::registerStat(&d_eval_eqs);
   StatisticsRegistry::registerStat(&d_eval_uf_terms);
+  StatisticsRegistry::registerStat(&d_eval_lits);
+  StatisticsRegistry::registerStat(&d_eval_lits_unknown);
   StatisticsRegistry::registerStat(&d_num_quants_init);
   StatisticsRegistry::registerStat(&d_num_quants_init_fail);
 }
@@ -674,8 +358,9 @@ ModelEngine::Statistics::Statistics():
 ModelEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_inst_rounds);
   StatisticsRegistry::unregisterStat(&d_eval_formulas);
-  StatisticsRegistry::unregisterStat(&d_eval_eqs);
   StatisticsRegistry::unregisterStat(&d_eval_uf_terms);
+  StatisticsRegistry::unregisterStat(&d_eval_lits);
+  StatisticsRegistry::unregisterStat(&d_eval_lits_unknown);
   StatisticsRegistry::unregisterStat(&d_num_quants_init);
   StatisticsRegistry::unregisterStat(&d_num_quants_init_fail);
 }
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index b01139826..1139332fe 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -11,81 +11,25 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Model Engine classes
+ ** \brief Model Engine class
  **/
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__MODEL_ENGINE_H
-#define __CVC4__MODEL_ENGINE_H
+#ifndef __CVC4__QUANTIFIERS_MODEL_ENGINE_H
+#define __CVC4__QUANTIFIERS_MODEL_ENGINE_H
 
 #include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/theory_quantifiers.h"
+#include "theory/quantifiers/model_builder.h"
 #include "theory/model.h"
-#include "theory/uf/theory_uf_model.h"
 #include "theory/quantifiers/relevant_domain.h"
 
 namespace CVC4 {
 namespace theory {
-
-namespace uf{
-  class StrongSolverTheoryUf;
-}
-
 namespace quantifiers {
 
-
-//the model builder
-class ModelEngineBuilder : public TheoryEngineModelBuilder
-{
-protected:
-  //quantifiers engine
-  QuantifiersEngine* d_qe;
-  //map from operators to model preference data
-  std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
-  /** choose representative */
-  Node chooseRepresentative( TheoryModel* tm, Node eqc );
-  /** use constants for representatives */
-  void processBuildModel( TheoryModel* m );
-  //analyze quantifiers
-  void analyzeQuantifiers( FirstOrderModel* fm );
-  //build model
-  void finishBuildModel( FirstOrderModel* fm );
-  //theory-specific build models
-  void finishBuildModelUf( FirstOrderModel* fm, uf::UfModel& model );
-  //do InstGen techniques for quantifier, return number of lemmas produced
-  int doInstGen( FirstOrderModel* fm, Node f );
-public:
-  ModelEngineBuilder( QuantifiersEngine* qe );
-  virtual ~ModelEngineBuilder(){}
-public:
-  /** number of lemmas generated while building model */
-  int d_addedLemmas;
-  //map from quantifiers to if are constant SAT
-  std::map< Node, bool > d_quant_sat;
-  //map from quantifiers to the instantiation literals that their model is dependent upon
-  std::map< Node, std::vector< Node > > d_quant_selection_lits;
-public:
-  //map from quantifiers to model basis match
-  std::map< Node, InstMatch > d_quant_basis_match;
-  //options
-  bool optUseModel();
-  bool optInstGen();
-  bool optOneQuantPerRoundInstGen();
-  /** statistics class */
-  class Statistics {
-  public:
-    IntStat d_pre_sat_quant;
-    IntStat d_pre_nsat_quant;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
-};
-
 class ModelEngine : public QuantifiersModule
 {
-  friend class uf::UfModel;
   friend class RepSetIterator;
 private:
   /** builder class */
@@ -128,8 +72,9 @@ public:
   public:
     IntStat d_inst_rounds;
     IntStat d_eval_formulas;
-    IntStat d_eval_eqs;
     IntStat d_eval_uf_terms;
+    IntStat d_eval_lits;
+    IntStat d_eval_lits_unknown;
     IntStat d_num_quants_init;
     IntStat d_num_quants_init_fail;
     Statistics();
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index e7ae1d1c7..12206e148 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -37,16 +37,16 @@ void RelevantDomain::compute(){
     d_quant_inst_domain[f].resize( f[0].getNumChildren() );

   }

   //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment)

-  for( std::map< Node, uf::UfModel >::iterator it = d_model->d_uf_model.begin();

-       it != d_model->d_uf_model.end(); ++it ){

+  for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin();

+       it != d_model->d_uf_model_tree.end(); ++it ){

     Node op = it->first;

-    for( int i=0; i<(int)it->second.d_ground_asserts.size(); i++ ){

-      Node n = it->second.d_ground_asserts[i];

+    for( size_t i=0; i<d_model->d_uf_terms[op].size(); i++ ){

+      Node n = d_model->d_uf_terms[op][i];

       //add arguments to domain

       for( int j=0; j<(int)n.getNumChildren(); j++ ){

-        if( d_model->d_ra.hasType( n[j].getType() ) ){

+        if( d_model->d_rep_set.hasType( n[j].getType() ) ){

           Node ra = d_model->getRepresentative( n[j] );

-          int raIndex = d_model->d_ra.getIndexFor( ra );

+          int raIndex = d_model->d_rep_set.getIndexFor( ra );

           Assert( raIndex!=-1 );

           if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){

             d_active_domain[op][j].push_back( raIndex );

@@ -54,8 +54,8 @@ void RelevantDomain::compute(){
         }

       }

       //add to range

-      Node r = it->second.d_ground_asserts_reps[i];

-      int raIndex = d_model->d_ra.getIndexFor( r );

+      Node r = d_model->getRepresentative( n );

+      int raIndex = d_model->d_rep_set.getIndexFor( r );

       Assert( raIndex!=-1 );

       if( std::find( d_active_range[op].begin(), d_active_range[op].end(), raIndex )==d_active_range[op].end() ){

         d_active_range[op].push_back( raIndex );

@@ -104,10 +104,10 @@ bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, in
     if( !domainSet ){

       //otherwise, we must consider the entire domain

       TypeNode tn = n.getType();

-      if( d_model->d_ra.hasType( tn ) ){

-        if( rd[vi].size()!=d_model->d_ra.d_type_reps[tn].size() ){

+      if( d_model->d_rep_set.hasType( tn ) ){

+        if( rd[vi].size()!=d_model->d_rep_set.d_type_reps[tn].size() ){

           rd[vi].clear();

-          for( size_t i=0; i<d_model->d_ra.d_type_reps[tn].size(); i++ ){

+          for( size_t i=0; i<d_model->d_rep_set.d_type_reps[tn].size(); i++ ){

             rd[vi].push_back( i );

             domainChanged = true;

           }

@@ -166,7 +166,7 @@ bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){
       }

     }else{

       Node r = d_model->getRepresentative( n );

-      range.push_back( d_model->d_ra.getIndexFor( r ) );

+      range.push_back( d_model->d_rep_set.getIndexFor( r ) );

     }

     return domainChanged;

   }

diff --git a/src/theory/quantifiers/rep_set_iterator.cpp b/src/theory/quantifiers/rep_set_iterator.cpp
index a29f815db..516f85857 100644
--- a/src/theory/quantifiers/rep_set_iterator.cpp
+++ b/src/theory/quantifiers/rep_set_iterator.cpp
@@ -38,8 +38,28 @@ RepSetIterator::RepSetIterator( Node f, FirstOrderModel* model ) : d_f( f ), d_m
     d_var_order[i] = i;

     //store default domain

     d_domain.push_back( RepDomain() );

-    for( int j=0; j<(int)d_model->d_ra.d_type_reps[d_f[0][i].getType()].size(); j++ ){

-      d_domain[i].push_back( j );

+    TypeNode tn = d_f[0][i].getType();

+    if( tn.isSort() ){

+      if( d_model->d_rep_set.hasType( tn ) ){

+        for( int j=0; j<(int)d_model->d_rep_set.d_type_reps[d_f[0][i].getType()].size(); j++ ){

+          d_domain[i].push_back( j );

+        }

+      }else{

+        Unimplemented("Cannot create instantiation iterator for unknown uninterpretted sort");

+      }

+    }else if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){

+      Unimplemented("Cannot create instantiation iterator for arithmetic quantifier");

+    }else if( tn.isDatatype() ){

+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();

+      //if finite, then use type enumerator

+      if( dt.isFinite() ){

+        //DO_THIS: use type enumerator

+        Unimplemented("Not yet implemented: instantiation iterator for finite datatype quantifier");

+      }else{

+        Unimplemented("Cannot create instantiation iterator for infinite datatype quantifier");

+      }

+    }else{

+      Unimplemented("Cannot create instantiation iterator for quantifier");

     }

   }

 }

@@ -103,9 +123,9 @@ void RepSetIterator::getMatch( QuantifiersEngine* qe, InstMatch& m ){
 

 Node RepSetIterator::getTerm( int i ){

   TypeNode tn = d_f[0][d_index_order[i]].getType();

-  Assert( d_model->d_ra.d_type_reps.find( tn )!=d_model->d_ra.d_type_reps.end() );

+  Assert( d_model->d_rep_set.d_type_reps.find( tn )!=d_model->d_rep_set.d_type_reps.end() );

   int index = d_index_order[i];

-  return d_model->d_ra.d_type_reps[tn][d_domain[index][d_index[index]]];

+  return d_model->d_rep_set.d_type_reps[tn][d_domain[index][d_index[index]]];

 }

 

 void RepSetIterator::debugPrint( const char* c ){

@@ -123,14 +143,18 @@ void RepSetIterator::debugPrintSmall( const char* c ){
 }

 

 RepSetEvaluator::RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri ) : d_model( m ), d_riter( ri ){

-

+  d_eval_formulas = 0;

+  d_eval_uf_terms = 0;

+  d_eval_lits = 0;

+  d_eval_lits_unknown = 0;

 }

 

-//if evaluate( n, phaseReq ) = eVal,

-// if eVal = d_riter->d_index.size()

-//   then the formula n instantiated with d_riter cannot be proven to be equal to phaseReq

-// otherwise,

-//   each n{d_riter->d_index[0]/x_0...d_riter->d_index[eVal]/x_eVal, */x_(eVal+1) ... */x_n } is equal to phaseReq in the current model

+//if evaluate( n ) = eVal,

+// let n' = d_riter * n be the formula n instantiated with the current values in r_iter

+// if eVal = 1, then n' is true, if eVal = -1, then n' is false,

+// if eVal = 0, then n' cannot be proven to be equal to phaseReq

+// if eVal is not 0, then

+//   each n{d_riter->d_index[0]/x_0...d_riter->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model

 int RepSetEvaluator::evaluate( Node n, int& depIndex ){

   ++d_eval_formulas;

   //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;

@@ -208,6 +232,7 @@ int RepSetEvaluator::evaluate( Node n, int& depIndex ){
   }else if( n.getKind()==FORALL ){

     return 0;

   }else{

+    ++d_eval_lits;

     ////if we know we will fail again, immediately return

     //if( d_eval_failed.find( n )!=d_eval_failed.end() ){

     //  if( d_eval_failed[n] ){

@@ -215,89 +240,46 @@ int RepSetEvaluator::evaluate( Node n, int& depIndex ){
     //  }

     //}

     //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl;

-    //this should be a literal

-    //Node gn = n.substitute( d_riter->d_ic.begin(), d_riter->d_ic.end(), d_riter->d_terms.begin(), d_riter->d_terms.end() );

-    //Debug("fmf-eval-debug") << "  Ground version = " << gn << std::endl;

     int retVal = 0;

     depIndex = d_riter->getNumTerms()-1;

-    if( n.getKind()==APPLY_UF ){

-      //case for boolean predicates

-      Node val = evaluateTerm( n, depIndex );

-      if( d_model->hasTerm( val ) ){

-        if( d_model->areEqual( val, d_model->d_true ) ){

-          retVal = 1;

-        }else{

-          retVal = -1;

-        }

-      }

-    }else if( n.getKind()==EQUAL ){

-      //case for equality

-      retVal = evaluateEquality( n[0], n[1], depIndex );

-    }else{

-      std::vector< int > cdi;

-      Node val = evaluateTermDefault( n, depIndex, cdi );

-      if( !val.isNull() ){

-        val = Rewriter::rewrite( val );

-        if( val==d_model->d_true ){

-          retVal = 1;

-        }else if( val==d_model->d_false ){

-          retVal = -1;

+    Node val = evaluateTerm( n, depIndex );

+    if( !val.isNull() ){

+      if( d_model->areEqual( val, d_model->d_true ) ){

+        retVal = 1;

+      }else if( d_model->areEqual( val, d_model->d_false ) ){

+        retVal = -1;

+      }else{

+        if( val.getKind()==EQUAL ){

+          if( d_model->areEqual( val[0], val[1] ) ){

+            retVal = 1;

+          }else if( d_model->areDisequal( val[0], val[1] ) ){

+            retVal = -1;

+          }

         }

       }

     }

     if( retVal!=0 ){

-      Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depends = " << depIndex << std::endl;

+      Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl;

     }else{

+      ++d_eval_lits_unknown;

       Debug("fmf-eval-amb") << "Neither true nor false : " << n << std::endl;

       //std::cout << "Neither true nor false : " << n << std::endl;

+      //std::cout << "  Value : " << val << std::endl;

+      //for( int i=0; i<(int)n.getNumChildren(); i++ ){

+      //  std::cout << "   " << i << " : " << n[i].getType() << std::endl;

+      //}

     }

     return retVal;

   }

 }

 

-int RepSetEvaluator::evaluateEquality( Node n1, Node n2, int& depIndex ){

-  ++d_eval_eqs;

-  //Notice() << "Eval eq " << n1 << " " << n2 << std::endl;

-  Debug("fmf-eval-debug") << "Evaluate equality: " << std::endl;

-  Debug("fmf-eval-debug") << "   " << n1 << " = " << n2 << std::endl;

-  int depIndex1, depIndex2;

-  Node val1 = evaluateTerm( n1, depIndex1 );

-  Node val2 = evaluateTerm( n2, depIndex2 );

-  Debug("fmf-eval-debug") << "   Values :  ";

-  d_model->printRepresentativeDebug( "fmf-eval-debug", val1 );

-  Debug("fmf-eval-debug") <<  " = ";

-  d_model->printRepresentativeDebug( "fmf-eval-debug", val2 );

-  Debug("fmf-eval-debug") << std::endl;

-  int retVal = 0;

-  if( !val1.isNull() && !val2.isNull() ){

-    if( d_model->areEqual( val1, val2 ) ){

-      retVal = 1;

-    }else if( d_model->areDisequal( val1, val2 ) ){

-      retVal = -1;

-    }else{

-      Node eq = val1.eqNode( val2 );

-      eq = Rewriter::rewrite( eq );

-      if( eq==d_model->d_true ){

-        retVal = 1;

-      }else if( eq==d_model->d_false ){

-        retVal = -1;

-      }

-    }

-  }

-  if( retVal!=0 ){

-    depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;

-    Debug("fmf-eval-debug") << "   value = " << (retVal==1) << ", depIndex = " << depIndex << std::endl;

-  }else{

-    depIndex = d_riter->getNumTerms()-1;

-    Debug("fmf-eval-amb") << "Neither equal nor disequal : " << n1 << " , " << n2 << std::endl;

-    //std::cout << "Neither equal nor disequal : " << n1 << " , " << n2 << std::endl;

-  }

-  return retVal;

-}

-

 Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){

-  //Notice() << "Eval term " << n << std::endl;

-  if( n.hasAttribute(InstConstantAttribute()) ){

+  //Message() << "Eval term " << n << std::endl;

+  if( !n.hasAttribute(InstConstantAttribute()) ){

+    //if evaluating a ground term, just consult the standard getValue functionality

+    depIndex = -1;

+    return d_model->getValue( n );

+  }else{

     Node val;

     depIndex = d_riter->getNumTerms()-1;

     //check the type of n

@@ -311,7 +293,7 @@ Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){
       if( eval==0 ){

         //evaluate children to see if they are the same

         Node val1 = evaluateTerm( n[ 1 ], depIndex1 );

-        Node val2 = evaluateTerm( n[ 1 ], depIndex1 );

+        Node val2 = evaluateTerm( n[ 2 ], depIndex2 );

         if( val1==val2 ){

           val = val1;

           depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;

@@ -323,19 +305,24 @@ Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){
         depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;

       }

     }else{

-#if 0

+      std::vector< int > children_depIndex;

       //for select, pre-process read over writes

       if( n.getKind()==SELECT ){

-        Node selIndex = evaluateTerm( n[1], depIndex );

-        if( selIndex.isNull() ){

+#if 1

+        //std::cout << "Evaluate " << n << std::endl;

+        Node sel = evaluateTerm( n[1], depIndex );

+        if( sel.isNull() ){

           depIndex = d_riter->getNumTerms()-1;

           return Node::null();

         }

-        Node arr = n[0];

+        Node arr = d_model->getRepresentative( n[0] );

+        //if( n[0]!=d_model->getRepresentative( n[0] ) ){

+        //  std::cout << n[0] << " is " << d_model->getRepresentative( n[0] ) << std::endl;

+        //}

+        int tempIndex;

         int eval = 1;

         while( arr.getKind()==STORE && eval!=0 ){

-          int tempIndex;

-          eval = evaluateEquality( selIndex, arr[1], tempIndex );

+          eval = evaluate( sel.eqNode( arr[1] ), tempIndex );

           depIndex = tempIndex > depIndex ? tempIndex : depIndex;

           if( eval==1 ){

             val = evaluateTerm( arr[2], tempIndex );

@@ -345,90 +332,97 @@ Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){
             arr = arr[0];

           }

         }

-        n = NodeManager::currentNM()->mkNode( SELECT, arr, selIndex );

-      }

+        arr = evaluateTerm( arr, tempIndex );

+        depIndex = tempIndex > depIndex ? tempIndex : depIndex;

+        val = NodeManager::currentNM()->mkNode( SELECT, arr, sel );

+#else

+        val = evaluateTermDefault( n, depIndex, children_depIndex );

 #endif

-      //default term evaluate : evaluate all children, recreate the value

-      std::vector< int > children_depIndex;

-      val = evaluateTermDefault( n, depIndex, children_depIndex );

-      //case split on the type of term

-      if( n.getKind()==APPLY_UF ){

-        Node op = n.getOperator();

-        //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;

-        //if it is a defined UF, then consult the interpretation

-        ++d_eval_uf_terms;

-        int argDepIndex = 0;

-        if( d_model->d_uf_model.find( op )!=d_model->d_uf_model.end() ){

-          //make the term model specifically for n

-          makeEvalUfModel( n );

-          //now, consult the model

-          if( d_eval_uf_use_default[n] ){

-            val = d_model->d_uf_model[op].d_tree.getValue( d_model, val, argDepIndex );

-          }else{

-            val = d_eval_uf_model[ n ].getValue( d_model, val, argDepIndex );

-          }

+      }else{

+        //default term evaluate : evaluate all children, recreate the value

+        val = evaluateTermDefault( n, depIndex, children_depIndex );

+      }

+      if( !val.isNull() ){

+        bool setVal = false;

+        //custom ways of evaluating terms

+        if( n.getKind()==APPLY_UF ){

+          Node op = n.getOperator();

           //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;

-          //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe );

-          Assert( !val.isNull() );

-        }else{

-          d_eval_uf_use_default[n] = true;

-          argDepIndex = (int)n.getNumChildren();

+          //if it is a defined UF, then consult the interpretation

+          if( d_model->d_uf_model_tree.find( op )!=d_model->d_uf_model_tree.end() ){

+            ++d_eval_uf_terms;

+            int argDepIndex = 0;

+            //make the term model specifically for n

+            makeEvalUfModel( n );

+            //now, consult the model

+            if( d_eval_uf_use_default[n] ){

+              val = d_model->d_uf_model_tree[op].getValue( d_model, val, argDepIndex );

+            }else{

+              val = d_eval_uf_model[ n ].getValue( d_model, val, argDepIndex );

+            }

+            //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;

+            //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe );

+            Assert( !val.isNull() );

+            //recalculate the depIndex

+            depIndex = -1;

+            for( int i=0; i<argDepIndex; i++ ){

+              int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];

+              Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;

+              if( children_depIndex[index]>depIndex ){

+                depIndex = children_depIndex[index];

+              }

+            }

+            setVal = true;

+          }

+        }else if( n.getKind()==SELECT ){

+          //we are free to interpret this term however we want

         }

-        //recalculate the depIndex

-        depIndex = -1;

-        for( int i=0; i<argDepIndex; i++ ){

-          int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];

-          Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;

-          if( children_depIndex[index]>depIndex ){

-            depIndex = children_depIndex[index];

+        //if not set already, rewrite and consult model for interpretation

+        if( !setVal ){

+          val = Rewriter::rewrite( val );

+          if( val.getMetaKind()!=kind::metakind::CONSTANT ){

+            //FIXME: we cannot do this until we trust all theories collectModelInfo!

+            //val = d_model->getInterpretedValue( val );

+            //val = d_model->getRepresentative( val );

           }

         }

         Debug("fmf-eval-debug") << "Evaluate term " << n << " = ";

         d_model->printRepresentativeDebug( "fmf-eval-debug", val );

         Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl;

-      }else if( n.getKind()==SELECT ){

-        if( d_model->d_array_model.find( n[0] )!=d_model->d_array_model.end() ){

-          //consult the default value for the array DO_THIS

-          //val = Rewriter::rewrite( val );

-          //val = d_model->d_array_model[ n[0] ];

-          val = Rewriter::rewrite( val );

-        }else{

-          val = Rewriter::rewrite( val );

-        }

-      }else{

-        val = Rewriter::rewrite( val );

       }

     }

     return val;

-  }else{

-    depIndex = -1;

-    return n;

   }

 }

 

 Node RepSetEvaluator::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ){

-  //first we must evaluate the arguments

-  std::vector< Node > children;

-  if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){

-    children.push_back( n.getOperator() );

-  }

   depIndex = -1;

-  //for each argument, calculate its value, and the variables its value depends upon

-  for( int i=0; i<(int)n.getNumChildren(); i++ ){

-    childDepIndex.push_back( -1 );

-    Node nn = evaluateTerm( n[i], childDepIndex[i] );

-    if( nn.isNull() ){

-      depIndex = d_riter->getNumTerms()-1;

-      return nn;

-    }else{

-      children.push_back( nn );

-      if( childDepIndex[i]>depIndex ){

-        depIndex = childDepIndex[i];

+  if( n.getNumChildren()==0 ){

+    return n;

+  }else{

+    //first we must evaluate the arguments

+    std::vector< Node > children;

+    if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){

+      children.push_back( n.getOperator() );

+    }

+    //for each argument, calculate its value, and the variables its value depends upon

+    for( int i=0; i<(int)n.getNumChildren(); i++ ){

+      childDepIndex.push_back( -1 );

+      Node nn = evaluateTerm( n[i], childDepIndex[i] );

+      if( nn.isNull() ){

+        depIndex = d_riter->getNumTerms()-1;

+        return nn;

+      }else{

+        children.push_back( nn );

+        if( childDepIndex[i]>depIndex ){

+          depIndex = childDepIndex[i];

+        }

       }

     }

+    //recreate the value

+    Node val = NodeManager::currentNM()->mkNode( n.getKind(), children );

+    return val;

   }

-  //recreate the value

-  return NodeManager::currentNM()->mkNode( n.getKind(), children );

 }

 

 void RepSetEvaluator::clearEvalFailed( int index ){

@@ -443,8 +437,8 @@ void RepSetEvaluator::makeEvalUfModel( Node n ){
     makeEvalUfIndexOrder( n );

     if( !d_eval_uf_use_default[n] ){

       Node op = n.getOperator();

-      d_eval_uf_model[n] = uf::UfModelTreeOrdered( op, d_eval_term_index_order[n] );

-      d_model->d_uf_model[op].makeModel( d_eval_uf_model[n] );

+      d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] );

+      d_model->d_uf_model_gen[op].makeModel( d_model, d_eval_uf_model[n] );

       //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl;

       //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 );

     }

diff --git a/src/theory/quantifiers/rep_set_iterator.h b/src/theory/quantifiers/rep_set_iterator.h
index 308d09a38..f6312ae5c 100644
--- a/src/theory/quantifiers/rep_set_iterator.h
+++ b/src/theory/quantifiers/rep_set_iterator.h
@@ -85,7 +85,7 @@ private:
 private: //for Theory UF:

   //map from terms to the models used to calculate their value

   std::map< Node, bool > d_eval_uf_use_default;

-  std::map< Node, uf::UfModelTreeOrdered > d_eval_uf_model;

+  std::map< Node, uf::UfModelTree > d_eval_uf_model;

   void makeEvalUfModel( Node n );

   //index ordering to use for each term

   std::map< Node, std::vector< int > > d_eval_term_index_order;

@@ -103,13 +103,13 @@ public:
   virtual ~RepSetEvaluator(){}

   /** evaluate functions */

   int evaluate( Node n, int& depIndex );

-  int evaluateEquality( Node n1, Node n2, int& depIndex );

   Node evaluateTerm( Node n, int& depIndex );

 public:

   //statistics

   int d_eval_formulas;

-  int d_eval_eqs;

   int d_eval_uf_terms;

+  int d_eval_lits;

+  int d_eval_lits_unknown;

 };

 

 

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 55715353d..945c82bf9 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -45,7 +45,7 @@ using namespace CVC4::theory::inst;
    }
  }
 
-void addTermEfficient( Node n, std::set< Node >& added){
+void TermDb::addTermEfficient( Node n, std::set< Node >& added){
   static AvailableInTermDb aitdi;
   if (Trigger::isAtomicTrigger( n ) && !n.getAttribute(aitdi)){
     //Already processed but new in this branch
@@ -60,70 +60,69 @@ void addTermEfficient( Node n, std::set< Node >& added){
 
 
 void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
-   //don't add terms in quantifier bodies
+  //don't add terms in quantifier bodies
   if( withinQuant && !Options::current()->registerQuantBodyTerms ){
     return;
   }
-     if( d_processed.find( n )==d_processed.end() ){
+  if( d_processed.find( n )==d_processed.end() ){
     ++(d_quantEngine->d_statistics.d_term_in_termdb);
     d_processed.insert(n);
+    d_type_map[ n.getType() ].push_back( n );
     n.setAttribute(AvailableInTermDb(),true);
-       //if this is an atomic trigger, consider adding it
+    //if this is an atomic trigger, consider adding it
     //Call the children?
-    if( Trigger::isAtomicTrigger( n ) || n.getKind() == kind::APPLY_CONSTRUCTOR ){
-         if( !n.hasAttribute(InstConstantAttribute()) ){
-           Debug("term-db") << "register trigger term " << n << std::endl;
+    if( Trigger::isAtomicTrigger( n ) ){
+      if( !n.hasAttribute(InstConstantAttribute()) ){
+        Debug("term-db") << "register trigger term " << n << std::endl;
         //std::cout << "register trigger term " << n << std::endl;
-           Node op = n.getOperator();
-           d_op_map[op].push_back( n );
-           d_type_map[ n.getType() ].push_back( n );
+        Node op = n.getOperator();
+        d_op_map[op].push_back( n );
         added.insert( n );
 
-           uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
-           for( int i=0; i<(int)n.getNumChildren(); i++ ){
-             addTerm( n[i], added, withinQuant );
-             if( Options::current()->efficientEMatching ){
-               if( d_parents[n[i]][op].empty() ){
-                 //must add parent to equivalence class info
-                 Node nir = d_ith->getRepresentative( n[i] );
-                 uf::EqClassInfo* eci_nir = d_ith->getEquivalenceClassInfo( nir );
-                 if( eci_nir ){
-                   eci_nir->d_pfuns[ op ] = true;
-                 }
-               }
-               //add to parent structure
-               if( std::find( d_parents[n[i]][op][i].begin(), d_parents[n[i]][op][i].end(), n )==d_parents[n[i]][op][i].end() ){
-                 d_parents[n[i]][op][i].push_back( n );
+        uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
+        for( int i=0; i<(int)n.getNumChildren(); i++ ){
+          addTerm( n[i], added, withinQuant );
+          if( Options::current()->efficientEMatching ){
+            if( d_parents[n[i]][op].empty() ){
+              //must add parent to equivalence class info
+              Node nir = d_ith->getRepresentative( n[i] );
+              uf::EqClassInfo* eci_nir = d_ith->getEquivalenceClassInfo( nir );
+              if( eci_nir ){
+                eci_nir->d_pfuns[ op ] = true;
+              }
+            }
+            //add to parent structure
+            if( std::find( d_parents[n[i]][op][i].begin(), d_parents[n[i]][op][i].end(), n )==d_parents[n[i]][op][i].end() ){
+              d_parents[n[i]][op][i].push_back( n );
               Assert(!getParents(n[i],op,i).empty());
-             }
-           }
-           if( Options::current()->eagerInstQuant ){
-             if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
-               int addedLemmas = 0;
-               for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){
-                 addedLemmas += d_ith->d_op_triggers[op][i]->addTerm( n );
-               }
-               //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
-               d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->getTheory( THEORY_QUANTIFIERS )->getOutputChannel() );
-             }
-           }
-         }
-       }
+            }
+          }
+          if( Options::current()->eagerInstQuant ){
+            if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
+              int addedLemmas = 0;
+              for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){
+                addedLemmas += d_ith->d_op_triggers[op][i]->addTerm( n );
+              }
+              //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
+              d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->getTheory( THEORY_QUANTIFIERS )->getOutputChannel() );
+            }
+          }
+        }
+      }
     }else{
-       for( int i=0; i<(int)n.getNumChildren(); i++ ){
-         addTerm( n[i], added, withinQuant );
-       }
-     }
+      for( int i=0; i<(int)n.getNumChildren(); i++ ){
+        addTerm( n[i], added, withinQuant );
+      }
+    }
   }else{
-     if( Options::current()->efficientEMatching &&
-         !n.hasAttribute(InstConstantAttribute())){
-       //Efficient e-matching must be notified
-       //The term in triggers are not important here
-       Debug("term-db") << "New in this branch term " << n << std::endl;
-       addTermEfficient(n,added);
-   }
- }
-};
+    if( Options::current()->efficientEMatching && !n.hasAttribute(InstConstantAttribute())){
+      //Efficient e-matching must be notified
+      //The term in triggers are not important here
+      Debug("term-db") << "New in this branch term " << n << std::endl;
+      addTermEfficient(n,added);
+    }
+  }
+}
 
  void TermDb::reset( Theory::Effort effort ){
    int nonCongruentCount = 0;
@@ -158,7 +157,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
    for( int i=0; i<2; i++ ){
      Node n = NodeManager::currentNM()->mkConst( i==1 );
      eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getRepresentative( n ),
-                               ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine() );
+                              d_quantEngine->getEqualityQuery()->getEngine() );
      while( !eqc.isFinished() ){
        Node en = (*eqc);
        if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){
@@ -194,12 +193,18 @@ void TermDb::registerModelBasis( Node n, Node gn ){
 
 Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
   if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
-    std::stringstream ss;
-    ss << Expr::setlanguage(Options::current()->outputLanguage);
-    ss << "e_" << tn;
-    d_model_basis_term[tn] = NodeManager::currentNM()->mkVar( ss.str(), tn );
+    Node mbt;
+    if( d_type_map[ tn ].empty() ){
+      std::stringstream ss;
+      ss << Expr::setlanguage(Options::current()->outputLanguage);
+      ss << "e_" << tn;
+      mbt = NodeManager::currentNM()->mkVar( ss.str(), tn );
+    }else{
+      mbt = d_type_map[ tn ][ 0 ];
+    }
     ModelBasisAttribute mba;
-    d_model_basis_term[tn].setAttribute(mba,true);
+    mbt.setAttribute(mba,true);
+    d_model_basis_term[tn] = mbt;
   }
   return d_model_basis_term[tn];
 }
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 5004a82dc..1ebba49b5 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -68,6 +68,9 @@ public:
   void setMatchingActive( bool a ) { d_matching_active = a; }

   /** get active */

   bool getMatchingActive() { return d_matching_active; }

+private:

+  /** for efficient e-matching */

+  void addTermEfficient( Node n, std::set< Node >& added);

 public:

   /** parent structure (for efficient E-matching):

       n -> op -> index -> L