(Move-only) Refactor and document theory model part 2 (#1305)

* Move type set to its own file and document.

* Move theory engine model builder to its own class.

* Working on documentation.

* Document Theory Model.

* Minor

* Document theory model builder.

* Clang format

* Address review.

9 files changed, 1725 insertions, 1096 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 3648e824b..d370a73bc 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -175,9 +175,13 @@ libcvc4_la_SOURCES = \
 	theory/theory_engine.h \
 	theory/theory_model.cpp \
 	theory/theory_model.h \
+	theory/theory_model_builder.cpp \
+	theory/theory_model_builder.h \
 	theory/theory_registrar.h \
 	theory/theory_test_utils.h \
 	theory/type_enumerator.h \
+	theory/type_set.cpp \
+	theory/type_set.h \
 	theory/unconstrained_simplifier.cpp \
 	theory/unconstrained_simplifier.h \
 	theory/valuation.cpp \
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 2900320bb..2dc561074 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -18,7 +18,7 @@
 #define __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
 
 #include "theory/quantifiers_engine.h"
-#include "theory/theory_model.h"
+#include "theory/theory_model_builder.h"
 #include "theory/uf/theory_uf_model.h"
 
 namespace CVC4 {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 402ba61ff..6c49f2914 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -596,7 +596,7 @@ void TheoryEngine::check(Theory::Effort effort) {
         printAssertions("theory::assertions-model");
       }
       //checks for theories requiring the model go at last call
-      d_curr_model->setNeedsBuild();
+      d_curr_model->reset();
       for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
         if( theoryId!=THEORY_QUANTIFIERS ){
           Theory* theory = d_theoryTable[theoryId];
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 490ed45c9..65810109c 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -13,14 +13,10 @@
  **/
 #include "theory/theory_model.h"
 
+#include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
-#include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
-#include "theory/type_enumerator.h"
-#include "theory/uf/theory_uf_model.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -56,6 +52,7 @@ TheoryModel::~TheoryModel() throw() {
 }
 
 void TheoryModel::reset(){
+  d_modelBuilt = false;
   d_modelCache.clear();
   d_comment_str.clear();
   d_sep_heap = Node::null();
@@ -577,839 +574,5 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() {
   return funcs_to_assign;
 }
 
-TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( te ){
-
-}
-
-
-bool TheoryEngineModelBuilder::isAssignable(TNode n)
-{
-  if( n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL ){
-    // selectors are always assignable (where we guarantee that they are not evaluatable here)
-    if( !options::ufHo() ){
-      Assert( !n.getType().isFunction() );
-      return true;
-    }else{
-      // might be a function field
-      return !n.getType().isFunction();
-    }
-  }else{
-    // non-function variables, and fully applied functions
-    if( !options::ufHo() ){
-      // no functions exist, all functions are fully applied
-      Assert( n.getKind() != kind::HO_APPLY );
-      Assert( !n.getType().isFunction() );
-      return n.isVar() || n.getKind() == kind::APPLY_UF;
-    }else{
-      //Assert( n.getKind() != kind::APPLY_UF );
-      return ( n.isVar() && !n.getType().isFunction() ) || n.getKind() == kind::APPLY_UF || 
-             ( n.getKind() == kind::HO_APPLY && n[0].getType().getNumChildren()==2 );
-    }
-  }
-}
-
-
-void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cache)
-{
-  if (n.getKind()==FORALL || n.getKind()==EXISTS) {
-    return;
-  }
-  if (cache.find(n) != cache.end()) {
-    return;
-  }
-  if (isAssignable(n)) {
-    tm->d_equalityEngine->addTerm(n);
-  }
-  for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
-    checkTerms(*child_it, tm, cache);
-  }
-  cache.insert(n);
-}
-
-void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep ) {
-  d_constantReps[eqc] = const_rep;
-  Trace("model-builder") << "    Assign: Setting constant rep of " << eqc << " to " << const_rep << endl;
-  tm->d_rep_set.setTermForRepresentative(const_rep, eqc);
-}
-
-bool TheoryEngineModelBuilder::isExcludedCdtValue( Node val, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ) {
-  Trace("model-builder-debug") << "Is " << val << " and excluded codatatype value for " << eqc << "? " << std::endl;
-  for (set<Node>::iterator i = repSet->begin(); i != repSet->end(); ++i ) {
-    Assert(assertedReps.find(*i) != assertedReps.end());
-    Node rep = assertedReps[*i];
-    Trace("model-builder-debug") << "  Rep : " << rep << std::endl;
-    //check matching val to rep with eqc as a free variable
-    Node eqc_m;
-    if( isCdtValueMatch( val, rep, eqc, eqc_m ) ){
-      Trace("model-builder-debug") << "  ...matches with " << eqc << " -> " << eqc_m << std::endl;
-      if( eqc_m.getKind()==kind::UNINTERPRETED_CONSTANT ){
-        Trace("model-builder-debug") << "*** " << val << " is excluded datatype for " << eqc << std::endl;
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
-bool TheoryEngineModelBuilder::isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m ) {
-  if( r==v ){
-    return true;
-  }else if( r==eqc ){
-    if( eqc_m.isNull() ){
-      //only if an uninterpreted constant?
-      eqc_m = v;
-      return true;
-    }else{
-      return v==eqc_m;
-    }
-  }else if( v.getKind()==kind::APPLY_CONSTRUCTOR && r.getKind()==kind::APPLY_CONSTRUCTOR ){
-    if( v.getOperator()==r.getOperator() ){
-      for( unsigned i=0; i<v.getNumChildren(); i++ ){
-        if( !isCdtValueMatch( v[i], r[i], eqc, eqc_m ) ){
-          return false;
-        }
-      }
-      return true;
-    }
-  }
-  return false;
-}
-
-bool TheoryEngineModelBuilder::involvesUSort( TypeNode tn ) {
-  if( tn.isSort() ){
-    return true;
-  }else if( tn.isArray() ){
-    return involvesUSort( tn.getArrayIndexType() ) || involvesUSort( tn.getArrayConstituentType() );
-  }else if( tn.isSet() ){
-    return involvesUSort( tn.getSetElementType() );
-  }else if( tn.isDatatype() ){
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    return dt.involvesUninterpretedType();
-  }else{
-    return false;
-  }
-}
-
-bool TheoryEngineModelBuilder::isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited ) {
-  Assert( v.isConst() );
-  if( visited.find( v )==visited.end() ){
-    visited[v] = true;
-    TypeNode tn = v.getType();
-    if( tn.isSort() ){
-      Trace("model-builder-debug") << "Is excluded usort value : " << v << " " << tn << std::endl;
-      unsigned card = eqc_usort_count[tn];
-      Trace("model-builder-debug") << "  Cardinality is " << card << std::endl;
-      unsigned index = v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
-      Trace("model-builder-debug") << "  Index is " << index << std::endl;
-      return index>0 && index>=card;
-    }
-    for( unsigned i=0; i<v.getNumChildren(); i++ ){
-      if( isExcludedUSortValue( eqc_usort_count, v[i], visited ) ){
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
-
-void TheoryEngineModelBuilder::addToTypeList( TypeNode tn, std::vector< TypeNode >& type_list, 
-                                              std::map< TypeNode, bool >& visiting ){
-  if( std::find( type_list.begin(), type_list.end(), tn )==type_list.end() ){
-    if( visiting.find( tn )==visiting.end() ){
-      visiting[tn] = true;
-      /* This must make a recursive call on all types that are subterms of
-       * values of the current type.
-       * Note that recursive traversal here is over enumerated expressions
-       * (very low expression depth). */
-      if( tn.isArray() ){
-        addToTypeList( tn.getArrayIndexType(), type_list, visiting );
-        addToTypeList( tn.getArrayConstituentType(), type_list, visiting );
-      }else if( tn.isSet() ){
-        addToTypeList( tn.getSetElementType(), type_list, visiting );
-      }else if( tn.isDatatype() ){
-        const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-          for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
-            TypeNode ctn = TypeNode::fromType( dt[i][j].getRangeType() );
-            addToTypeList( ctn, type_list, visiting );
-          }
-        }   
-      }
-      Assert( std::find( type_list.begin(), type_list.end(), tn )==type_list.end() );
-      type_list.push_back( tn );
-    }
-  }
-}
-
-bool TheoryEngineModelBuilder::buildModel(Model* m)
-{
-  Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
-  TheoryModel* tm = (TheoryModel*)m;
-
-  // buildModel should only be called once per check
-  Assert(!tm->isBuilt());
-  tm->d_modelBuilt = true;
-
-  // Reset model
-  tm->reset();
-
-  // Collect model info from the theories
-  Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl;
-  d_te->collectModelInfo(tm);
-
-  // model-builder specific initialization
-  if( !preProcessBuildModel(tm) ){
-    return false;
-  }
-
-  // Loop through all terms and make sure that assignable sub-terms are in the equality engine
-  // Also, record #eqc per type (for finite model finding)
-  std::map< TypeNode, unsigned > eqc_usort_count;
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine );
-  {
-    NodeSet cache;
-    for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
-      eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i),tm->d_equalityEngine);
-      for ( ; !eqc_i.isFinished(); ++eqc_i) {
-        checkTerms(*eqc_i, tm, cache);
-      }
-      TypeNode tn = (*eqcs_i).getType();
-      if( tn.isSort() ){
-        if( eqc_usort_count.find( tn )==eqc_usort_count.end() ){
-          eqc_usort_count[tn] = 1;
-        }else{
-          eqc_usort_count[tn]++;
-        }
-      }
-    }
-  }
-
-  Trace("model-builder") << "Collect representatives..." << std::endl;
-
-  // Process all terms in the equality engine, store representatives for each EC
-  d_constantReps.clear();
-  std::map< Node, Node > assertedReps;
-  TypeSet typeConstSet, typeRepSet, typeNoRepSet;
-  TypeEnumeratorProperties tep;
-  if( options::finiteModelFind() ){
-    tep.d_fixed_usort_card = true;
-    for( std::map< TypeNode, unsigned >::iterator it = eqc_usort_count.begin(); it != eqc_usort_count.end(); ++it ){
-      Trace("model-builder") << "Fixed bound (#eqc) for " << it->first << " : " << it->second << std::endl;
-      tep.d_fixed_card[it->first] = Integer(it->second);
-    }
-    typeConstSet.setTypeEnumeratorProperties( &tep );
-  }
-  // AJR: build ordered list of types that ensures that base types are enumerated first.
-  //   (I think) this is only strictly necessary for finite model finding + parametric types 
-  //   instantiated with uninterpreted sorts, but is probably a good idea to do in general
-  //   since it leads to models with smaller term sizes.
-  std::vector< TypeNode > type_list;
-  eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
-  for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
-
-    // eqc is the equivalence class representative
-    Node eqc = (*eqcs_i);
-    Trace("model-builder") << "Processing EC: " << eqc << endl;
-    Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc);
-    TypeNode eqct = eqc.getType();
-    Assert(assertedReps.find(eqc) == assertedReps.end());
-    Assert(d_constantReps.find(eqc) == d_constantReps.end());
-
-    // Loop through terms in this EC
-    Node rep, const_rep;
-    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
-    for ( ; !eqc_i.isFinished(); ++eqc_i) {
-      Node n = *eqc_i;
-      Trace("model-builder") << "  Processing Term: " << n << endl;
-      // Record as rep if this node was specified as a representative
-      if (tm->d_reps.find(n) != tm->d_reps.end()){
-        //AJR: I believe this assertion is too strict, 
-        // e.g. datatypes may assert representative for two constructor terms that are not in the care graph and are merged during collectModelInfo.
-        //Assert(rep.isNull());
-        rep = tm->d_reps[n];
-        Assert(!rep.isNull() );
-        Trace("model-builder") << "  Rep( " << eqc << " ) = " << rep << std::endl;
-      }
-      // Record as const_rep if this node is constant
-      if (n.isConst()) {
-        Assert(const_rep.isNull());
-        const_rep = n;
-        Trace("model-builder") << "  ConstRep( " << eqc << " ) = " << const_rep << std::endl;
-      }
-      //model-specific processing of the term
-      tm->addTerm(n);
-    }
-
-    // Assign representative for this EC
-    if (!const_rep.isNull()) {
-      // Theories should not specify a rep if there is already a constant in the EC
-      //AJR: I believe this assertion is too strict, eqc with asserted reps may merge with constant eqc
-      //Assert(rep.isNull() || rep == const_rep);
-      assignConstantRep( tm, eqc, const_rep );
-      typeConstSet.add(eqct.getBaseType(), const_rep);
-    }
-    else if (!rep.isNull()) {
-      assertedReps[eqc] = rep;
-      typeRepSet.add(eqct.getBaseType(), eqc);
-      std::map< TypeNode, bool > visiting;
-      addToTypeList(eqct.getBaseType(), type_list, visiting);
-    }
-    else {
-      typeNoRepSet.add(eqct, eqc);
-      std::map< TypeNode, bool > visiting;
-      addToTypeList(eqct, type_list, visiting);
-    }
-  }
-
-  // Need to ensure that each EC has a constant representative.
-
-  Trace("model-builder") << "Processing EC's..." << std::endl;
-
-  TypeSet::iterator it;
-  vector<TypeNode>::iterator type_it;
-  set<Node>::iterator i, i2;
-  bool changed, unassignedAssignable, assignOne = false;
-  set<TypeNode> evaluableSet;
-
-  // Double-fixed-point loop
-  // Outer loop handles a special corner case (see code at end of loop for details)
-  for (;;) {
-
-    // Inner fixed-point loop: we are trying to learn constant values for every EC.  Each time through this loop, we process all of the
-    // types by type and may learn some new EC values.  EC's in one type may depend on EC's in another type, so we need a fixed-point loop
-    // to ensure that we learn as many EC values as possible
-    do {
-      changed = false;
-      unassignedAssignable = false;
-      evaluableSet.clear();
-
-      // Iterate over all types we've seen
-      for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it) {
-        TypeNode t = *type_it;
-        TypeNode tb = t.getBaseType();
-        set<Node>* noRepSet = typeNoRepSet.getSet(t);
-
-        // 1. Try to evaluate the EC's in this type
-        if (noRepSet != NULL && !noRepSet->empty()) {
-          Trace("model-builder") << "  Eval phase, working on type: " << t << endl;
-          bool assignable, evaluable, evaluated;
-          d_normalizedCache.clear();
-          for (i = noRepSet->begin(); i != noRepSet->end(); ) {
-            i2 = i;
-            ++i;
-            assignable = false;
-            evaluable = false;
-            evaluated = false;
-            Trace("model-builder-debug") << "Look at eqc : " << (*i2) << std::endl;
-            eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine);
-            for ( ; !eqc_i.isFinished(); ++eqc_i) {
-              Node n = *eqc_i;
-              Trace("model-builder-debug") << "Look at term : " << n << std::endl;
-              if (isAssignable(n)) {
-                assignable = true;
-                Trace("model-builder-debug") << "...assignable" << std::endl;
-              }
-              else {
-                evaluable = true;
-                Trace("model-builder-debug") << "...try to normalize" << std::endl;
-                Node normalized = normalize(tm, n, true);
-                if (normalized.isConst()) {
-                  typeConstSet.add(tb, normalized);
-                  assignConstantRep( tm, *i2, normalized);
-                  Trace("model-builder") << "    Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
-                  changed = true;
-                  evaluated = true;
-                  noRepSet->erase(i2);
-                  break;
-                }
-              }
-            }
-            if (!evaluated) {
-              if (evaluable) {
-                evaluableSet.insert(tb);
-              }
-              if (assignable) {
-                unassignedAssignable = true;
-              }
-            }
-          }
-        }
-
-        // 2. Normalize any non-const representative terms for this type
-        set<Node>* repSet = typeRepSet.getSet(t);
-        if (repSet != NULL && !repSet->empty()) {
-          Trace("model-builder") << "  Normalization phase, working on type: " << t << endl;
-          d_normalizedCache.clear();
-          for (i = repSet->begin(); i != repSet->end(); ) {
-            Assert(assertedReps.find(*i) != assertedReps.end());
-            Node rep = assertedReps[*i];
-            Node normalized = normalize(tm, rep, false);
-            Trace("model-builder") << "    Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl;
-            if (normalized.isConst()) {
-              changed = true;
-              typeConstSet.add(tb, normalized);
-              assignConstantRep( tm, *i, normalized);
-              assertedReps.erase(*i);
-              i2 = i;
-              ++i;
-              repSet->erase(i2);
-            }
-            else {
-              if (normalized != rep) {
-                assertedReps[*i] = normalized;
-                changed = true;
-              }
-              ++i;
-            }
-          }
-        }
-      }
-    } while (changed);
-
-    if (!unassignedAssignable) {
-      break;
-    }
-
-    // 3. Assign unassigned assignable EC's using type enumeration - assign a value *different* from all other EC's if the type is infinite
-    // Assign first value from type enumerator otherwise - for finite types, we rely on polite framework to ensure that EC's that have to be
-    // different are different.
-
-    // Only make assignments on a type if:
-    // 1. there are no terms that share the same base type with un-normalized representatives
-    // 2. there are no terms that share teh same base type that are unevaluated evaluable terms
-    // Alternatively, if 2 or 3 don't hold but we are in a special deadlock-breaking mode where assignOne is true, go ahead and make one assignment
-    changed = false;
-    //must iterate over the ordered type list to ensure that we do not enumerate values with subterms
-    //  having types that we are currently enumerating (when possible)
-    //  for example, this ensures we enumerate uninterpreted sort U before (List of U) and (Array U U)
-    //  however, it does not break cyclic type dependencies for mutually recursive datatypes, but this is handled
-    //  by recording all subterms of enumerated values in TypeSet::addSubTerms.
-    for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it) {
-      TypeNode t = *type_it;
-      // continue if there are no more equivalence classes of this type to assign
-      std::set<Node>* noRepSetPtr = typeNoRepSet.getSet( t );
-      if( noRepSetPtr==NULL ){
-        continue;
-      }
-      set<Node>& noRepSet = *noRepSetPtr;
-      if (noRepSet.empty()) {
-        continue;
-      }
-
-      //get properties of this type
-      bool isCorecursive = false;
-      if( t.isDatatype() ){
-        const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
-        isCorecursive = dt.isCodatatype() && ( !dt.isFinite( t.toType() ) || dt.isRecursiveSingleton( t.toType() ) );
-      }
-#ifdef CVC4_ASSERTIONS
-      bool isUSortFiniteRestricted = false;
-      if( options::finiteModelFind() ){
-        isUSortFiniteRestricted = !t.isSort() && involvesUSort( t );
-      }
-#endif
-      
-      set<Node>* repSet = typeRepSet.getSet(t);
-      TypeNode tb = t.getBaseType();
-      if (!assignOne) {
-        set<Node>* repSet = typeRepSet.getSet(tb);
-        if (repSet != NULL && !repSet->empty()) {
-          continue;
-        }
-        if (evaluableSet.find(tb) != evaluableSet.end()) {
-          continue;
-        }
-      }
-      Trace("model-builder") << "  Assign phase, working on type: " << t << endl;
-      bool assignable, evaluable CVC4_UNUSED;
-      for (i = noRepSet.begin(); i != noRepSet.end(); ) {
-        i2 = i;
-        ++i;
-        eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, tm->d_equalityEngine);
-        assignable = false;
-        evaluable = false;
-        for ( ; !eqc_i.isFinished(); ++eqc_i) {
-          Node n = *eqc_i;
-          if (isAssignable(n)) {
-            assignable = true;
-          }
-          else {
-            evaluable = true;
-          }
-        }
-        Trace("model-builder-debug") << "    eqc " << *i2 << " is assignable=" << assignable << ", evaluable=" << evaluable << std::endl;
-        if (assignable) {
-          Assert(!evaluable || assignOne);
-          Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF);
-          Node n;
-          if (t.getCardinality().isInfinite()) {
-          // if (!t.isInterpretedFinite()) {
-            bool success;
-            do{
-              Trace("model-builder-debug") << "Enumerate term of type " << t << std::endl;
-              n = typeConstSet.nextTypeEnum(t, true);
-              //--- AJR: this code checks whether n is a legal value
-              Assert( !n.isNull() );
-              success = true;
-              Trace("model-builder-debug") << "Check if excluded : " << n << std::endl;
-#ifdef CVC4_ASSERTIONS
-              if( isUSortFiniteRestricted ){
-                //must not involve uninterpreted constants beyond cardinality bound (which assumed to coincide with #eqc)
-                //this is just an assertion now, since TypeEnumeratorProperties should ensure that only legal values are enumerated wrt this constraint.
-                std::map< Node, bool > visited;
-                success = !isExcludedUSortValue( eqc_usort_count, n, visited );
-                if( !success ){
-                  Trace("model-builder") << "Excluded value for " << t << " : " << n << " due to out of range uninterpreted constant." << std::endl;
-                }
-                Assert( success );
-              }
-#endif
-              if( success && isCorecursive ){
-                if (repSet != NULL && !repSet->empty()) {
-                  // in the case of codatatypes, check if it is in the set of values that we cannot assign
-                  // this will check whether n \not\in V^x_I from page 9 of Reynolds/Blanchette CADE 2015
-                  success = !isExcludedCdtValue( n, repSet, assertedReps, *i2 );
-                  if( !success ){
-                    Trace("model-builder") << "Excluded value : " << n << " due to alpha-equivalent codatatype expression." << std::endl;
-                  }
-                }
-              }
-              //---
-            }while( !success );
-          }
-          else {
-            TypeEnumerator te(t);
-            n = *te;
-          }
-          Assert(!n.isNull());
-          assignConstantRep( tm, *i2, n);
-          changed = true;
-          noRepSet.erase(i2);
-          if (assignOne) {
-            assignOne = false;
-            break;
-          }
-        }
-      }
-    }
-
-    // Corner case - I'm not sure this can even happen - but it's theoretically possible to have a cyclical dependency
-    // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}.  In this case, neither one will get assigned because we are waiting
-    // to be able to evaluate.  But we will never be able to evaluate because the variables that need to be assigned are in
-    // these same EC's.  In this case, repeat the whole fixed-point computation with the difference that the first EC
-    // that has both assignable and evaluable expressions will get assigned.
-    if (!changed) {
-      Assert(!assignOne); // check for infinite loop!
-      assignOne = true;
-    }
-  }  
-
-#ifdef CVC4_ASSERTIONS
-  // Assert that all representatives have been converted to constants
-  for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) {
-    set<Node>& repSet = TypeSet::getSet(it);
-    if (!repSet.empty()) {
-      Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl;
-      Assert(false);
-    }
-  }
-#endif /* CVC4_ASSERTIONS */
-
-  Trace("model-builder") << "Copy representatives to model..." << std::endl;
-  tm->d_reps.clear();
-  std::map< Node, Node >::iterator itMap;
-  for (itMap = d_constantReps.begin(); itMap != d_constantReps.end(); ++itMap) {
-    tm->d_reps[itMap->first] = itMap->second;
-    tm->d_rep_set.add(itMap->second.getType(), itMap->second);
-  }
-
-  Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
-  // Make sure every EC has a rep
-  for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) {
-    tm->d_reps[itMap->first] = itMap->second;
-    tm->d_rep_set.add(itMap->second.getType(), itMap->second);
-  }
-  for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
-    set<Node>& noRepSet = TypeSet::getSet(it);
-    set<Node>::iterator i;
-    for (i = noRepSet.begin(); i != noRepSet.end(); ++i) {
-      tm->d_reps[*i] = *i;
-      tm->d_rep_set.add((*i).getType(), *i);
-    }
-  }
-
-  //modelBuilder-specific initialization
-  if( !processBuildModel( tm ) ){
-    return false;
-  }else{
-    return true;
-  }
-}
-
-void TheoryEngineModelBuilder::debugCheckModel(Model* m){
-  TheoryModel* tm = (TheoryModel*)m;
-#ifdef CVC4_ASSERTIONS
-  Assert(tm->isBuilt());
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine );
-  std::map< Node, Node >::iterator itMap;
-  // Check that every term evaluates to its representative in the model
-  for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) {
-    // eqc is the equivalence class representative
-    Node eqc = (*eqcs_i);
-    // get the representative
-    Node rep = tm->getRepresentative( eqc );
-    if( !rep.isConst() && eqc.getType().isBoolean() ){
-      // if Boolean, it does not necessarily have a constant representative, use get value instead
-      rep = tm->getValue(eqc);
-      Assert(rep.isConst());
-    }
-    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
-    for ( ; !eqc_i.isFinished(); ++eqc_i) {
-      Node n = *eqc_i;
-      static int repCheckInstance = 0;
-      ++repCheckInstance;
-      
-      // non-linear mult is not necessarily accurate wrt getValue
-      if( n.getKind()!=kind::NONLINEAR_MULT ){
-        Debug("check-model::rep-checking")
-          << "( " << repCheckInstance <<") "
-          << "n: " << n << endl
-          << "getValue(n): " << tm->getValue(n) << endl
-          << "rep: " << rep << endl;
-        Assert(tm->getValue(*eqc_i) == rep, "run with -d check-model::rep-checking for details");
-      }
-    }
-  }
-#endif /* CVC4_ASSERTIONS */
-
-  // builder-specific debugging
-  debugModel( tm );
-}
-
-Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
-{
-  std::map<Node, Node>::iterator itMap = d_constantReps.find(r);
-  if (itMap != d_constantReps.end()) {
-    return (*itMap).second;
-  }
-  NodeMap::iterator it = d_normalizedCache.find(r);
-  if (it != d_normalizedCache.end()) {
-    return (*it).second;
-  }
-  Trace("model-builder-debug") << "do normalize on " << r << std::endl;
-  Node retNode = r;
-  if (r.getNumChildren() > 0) {
-    std::vector<Node> children;
-    if (r.getMetaKind() == kind::metakind::PARAMETERIZED) {
-      children.push_back(r.getOperator());
-    }
-    bool childrenConst = true;
-    for (size_t i=0; i < r.getNumChildren(); ++i) {
-      Node ri = r[i];
-      bool recurse = true;
-      if (!ri.isConst()) {
-        if (m->d_equalityEngine->hasTerm(ri)) {
-          itMap = d_constantReps.find(m->d_equalityEngine->getRepresentative(ri));
-          if (itMap != d_constantReps.end()) {
-            ri = (*itMap).second;
-            recurse = false;
-          }
-          else if (!evalOnly) {
-            recurse = false;
-          }
-        }
-        if (recurse) {
-          ri = normalize(m, ri, evalOnly);
-        }
-        if (!ri.isConst()) {
-          childrenConst = false;
-        }
-      }
-      children.push_back(ri);
-    }
-    retNode = NodeManager::currentNM()->mkNode( r.getKind(), children );
-    if (childrenConst) {
-      retNode = Rewriter::rewrite(retNode);
-      Assert(retNode.getKind() == kind::APPLY_UF
-             || !retNode.getType().isFirstClass()
-             || retNode.isConst());
-    }
-  }
-  d_normalizedCache[r] = retNode;
-  return retNode;
-}
-
-bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m) {
-  return true;
-}
-
-bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m){
-  assignFunctions(m);
-  return true;
-}
-
-void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) {
-  Assert( !options::ufHo() );
-  uf::UfModelTree ufmt( f );
-  Node default_v;
-  for( size_t i=0; i<m->d_uf_terms[f].size(); i++ ){
-    Node un = m->d_uf_terms[f][i];
-    vector<TNode> children;
-    children.push_back(f);
-    Trace("model-builder-debug") << "  process term : " << un << std::endl;
-    for (size_t j = 0; j < un.getNumChildren(); ++j) {
-      Node rc = m->getRepresentative(un[j]);
-      Trace("model-builder-debug2") << "    get rep : " << un[j] << " returned " << rc << std::endl;
-      Assert( rc.isConst() ); 
-      children.push_back(rc);
-    }
-    Node simp = NodeManager::currentNM()->mkNode(un.getKind(), children);
-    Node v = m->getRepresentative(un);
-    Trace("model-builder") << "  Setting (" << simp << ") to (" << v << ")" << endl;
-    ufmt.setValue(m, simp, v);
-    default_v = v;
-  }
-  if( default_v.isNull() ){
-    //choose default value from model if none exists
-    TypeEnumerator te(f.getType().getRangeType());
-    default_v = (*te);
-  }
-  ufmt.setDefaultValue( m, default_v );
-  bool condenseFuncValues = options::condenseFunctionValues();
-  if(condenseFuncValues) {
-    ufmt.simplify();
-  }
-  std::stringstream ss;
-  ss << "_arg_" << f << "_";
-  Node val = ufmt.getFunctionValue( ss.str().c_str(), condenseFuncValues );
-  m->assignFunctionDefinition( f, val );
-  //ufmt.debugPrint( std::cout, m );
-}
-
-void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f) {
-  Assert( options::ufHo() );
-  TypeNode type = f.getType();
-  std::vector< TypeNode > argTypes = type.getArgTypes();
-  std::vector< Node > args;
-  std::vector< TNode > apply_args;
-  for( unsigned i=0; i<argTypes.size(); i++ ){
-    Node v = NodeManager::currentNM()->mkBoundVar( argTypes[i] );
-    args.push_back( v );
-    if( i>0 ){
-      apply_args.push_back( v );
-    }
-  }
-  //start with the base return value (currently we use the same default value for all functions)
-  TypeEnumerator te(type.getRangeType());
-  Node curr = (*te);
-  std::map< Node, std::vector< Node > >::iterator itht = m->d_ho_uf_terms.find( f );
-  if( itht!=m->d_ho_uf_terms.end() ){
-    for( size_t i=0; i<itht->second.size(); i++ ){
-      Node hn = itht->second[i];
-      Trace("model-builder-debug") << "    process : " << hn << std::endl;
-      Assert( hn.getKind()==kind::HO_APPLY );   
-      Assert( m->areEqual( hn[0], f ) );     
-      Node hni = m->getRepresentative(hn[1]);
-      Trace("model-builder-debug2") << "      get rep : " << hn[0] << " returned " << hni << std::endl;
-      Assert( hni.isConst() );
-      Assert( hni.getType().isSubtypeOf( args[0].getType() ) );
-      hni = Rewriter::rewrite( args[0].eqNode( hni ) );
-      Node hnv = m->getRepresentative(hn);
-      Trace("model-builder-debug2") << "      get rep val : " << hn << " returned " << hnv << std::endl;
-      Assert( hnv.isConst() );
-      if( !apply_args.empty() ){
-        Assert( hnv.getKind()==kind::LAMBDA && hnv[0].getNumChildren()+1==args.size() );
-        std::vector< TNode > largs;
-        for( unsigned j=0; j<hnv[0].getNumChildren(); j++ ){
-          largs.push_back( hnv[0][j] );
-        }
-        Assert( largs.size()==apply_args.size() );
-        hnv = hnv[1].substitute( largs.begin(), largs.end(), apply_args.begin(), apply_args.end() );
-        hnv = Rewriter::rewrite( hnv );
-      }
-      Assert( !TypeNode::leastCommonTypeNode( hnv.getType(), curr.getType() ).isNull() );
-      curr = NodeManager::currentNM()->mkNode( kind::ITE, hni, hnv, curr );
-    }
-  }
-  Node val = NodeManager::currentNM()->mkNode( kind::LAMBDA, 
-               NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, args ), curr );
-  m->assignFunctionDefinition( f, val );
-}
-
-// This struct is used to sort terms by the "size" of their type
-//   The size of the type is the number of nodes in the type, for example
-//  size of Int is 1
-//  size of Function( Int, Int ) is 3
-//  size of Function( Function( Bool, Int ), Int ) is 5
-struct sortTypeSize {
-  // stores the size of the type
-  std::map< TypeNode, unsigned > d_type_size;
-  // get the size of type tn
-  unsigned getTypeSize( TypeNode tn ) {
-    std::map< TypeNode, unsigned >::iterator it = d_type_size.find( tn );
-    if( it!=d_type_size.end() ){
-      return it->second;    
-    }else{
-      unsigned sum = 1;
-      for( unsigned i=0; i<tn.getNumChildren(); i++ ){
-        sum += getTypeSize( tn[i] );
-      }  
-      d_type_size[tn] = sum;
-      return sum;
-    }
-  }
-public:
-  // compares the type size of i and j
-  // returns true iff the size of i is less than that of j
-  // tiebreaks are determined by node value
-  bool operator() (Node i, Node j) {
-    int si = getTypeSize( i.getType() );
-    int sj = getTypeSize( j.getType() );
-    if( si<sj ){
-      return true;
-    }else if( si==sj ){
-      return i<j;
-    }else{
-      return false;
-    }
-  }
-};
-
-void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m) {
-  Trace("model-builder") << "Assigning function values..." << std::endl;
-  std::vector< Node > funcs_to_assign = m->getFunctionsToAssign();
-
-  if( options::ufHo() ){
-    // sort based on type size if higher-order
-    Trace("model-builder") << "Sort functions by type..." << std::endl;
-    sortTypeSize sts;
-    std::sort( funcs_to_assign.begin(), funcs_to_assign.end(), sts );
-  }
-
-  if( Trace.isOn("model-builder") ){
-    Trace("model-builder") << "...have " << funcs_to_assign.size() << " functions to assign:" << std::endl;
-    for( unsigned k=0; k<funcs_to_assign.size(); k++ ){
-      Node f = funcs_to_assign[k];
-      Trace("model-builder") << "  [" << k << "] : " << f << " : " << f.getType() << std::endl;
-    }
-  }
-
-  // construct function values
-  for( unsigned k=0; k<funcs_to_assign.size(); k++ ){
-    Node f = funcs_to_assign[k];
-    Trace("model-builder") << "  Function #" << k << " is " << f << std::endl;
-    //std::map< Node, std::vector< Node > >::iterator itht = m->d_ho_uf_terms.find( f );
-    if( !options::ufHo() ){
-      Trace("model-builder") << "  Assign function value for " << f << " based on APPLY_UF" << std::endl;
-      assignFunction( m, f );
-    }else{
-      Trace("model-builder") << "  Assign function value for " << f << " based on curried HO_APPLY" << std::endl;
-      assignHoFunction( m, f );
-    }
-  }
-  Trace("model-builder") << "Finished assigning function values." << std::endl;
-}
-
 } /* namespace CVC4::theory */
 } /* namespace CVC4 */
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 0d73cd72a..a8726f490 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -21,51 +21,80 @@
 #include <unordered_set>
 
 #include "smt/model.h"
-#include "theory/uf/equality_engine.h"
 #include "theory/rep_set.h"
 #include "theory/substitutions.h"
 #include "theory/type_enumerator.h"
+#include "theory/type_set.h"
+#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
 
-/**
- * Theory Model class.
- *    For Model m, should call m.initialize() before using.
+/** Theory Model class.
+ *
+ * This class represents a model produced by the TheoryEngine.
+ * The data structures used to represent a model are:
+ * (1) d_equalityEngine : an equality engine object, which stores
+ *     an equivalence relation over all terms that exist in
+ *     the current set of assertions.
+ * (2) d_substitutions : a substitution map storing cases of
+ *     explicitly solved terms, for instance during preprocessing.
+ * (3) d_reps : a map from equivalence class representatives of
+ *     the equality engine to the (constant) representatives
+ *     assigned to that equivalence class.
+ * (4) d_uf_models : a map from uninterpreted functions to their
+ *     lambda representation.
+ * (5) d_rep_set : a data structure that allows interpretations
+ *     for types to be represented as terms. This is useful for
+ *     finite model finding.
+ *
+ * These data structures are built after a full effort check with
+ * no lemmas sent, within a call to:
+ *    TheoryEngineModelBuilder::buildModel(...)
+ * which includes subcalls to TheoryX::collectModelInfo(...) calls.
+ *
+ * These calls may modify the model object using the interface
+ * functions below, including:
+ * - assertEquality, assertPredicate, assertRepresentative,
+ *   assertEqualityEngine.
+ * - assignFunctionDefinition
+ *
+ * During and after this building process, these calls may use
+ * interface functions below to guide the model construction:
+ * - hasTerm, getRepresentative, areEqual, areDisequal
+ * - getEqualityEngine
+ * - getRepSet
+ * - hasAssignedFunctionDefinition, getFunctionsToAssign
+ *
+ * After this building process, the function getValue can be
+ * used to query the value of nodes.
  */
 class TheoryModel : public Model
 {
   friend class TheoryEngineModelBuilder;
-
 public:
   TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
   virtual ~TheoryModel() throw();
 
-  /** get comments */
-  void getComments(std::ostream& out) const;
-  /** is built */
-  bool isBuilt() { return d_modelBuilt; }
-  /** set need build */
-  void setNeedsBuild() { d_modelBuilt = false; }
-  /**
-   * Get value function.  This should be called only after a ModelBuilder has called buildModel(...)
-   * on this model.
+  /** reset the model */
+  virtual void reset();
+  /** is built
+   *
+   * Have we (attempted to) build this model since the last
+   * call to reset? Notice for model building techniques
+   * that are not guaranteed to succeed (such as
+   * when quantified formulas are enabled), a true return
+   * value does not imply that this is a model of the
+   * current assertions.
    */
-  Node getValue( TNode n, bool useDontCares = false ) const;
-
-  //---------------------------- separation logic
-  /** set the heap and value sep.nil is equal to */
-  void setHeapModel(Node h, Node neq);
-  /** get the heap and value sep.nil is equal to */
-  bool getHeapModel(Expr& h, Expr& neq) const;
-  //---------------------------- end separation logic
-
+  bool isBuilt() { return d_modelBuilt; }
+  //---------------------------- for building the model
   /** Adds a substitution from x to t. */
   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
-  /** add term function
-    *   addTerm( n ) will do any model-specific processing necessary for n,
-    *   such as constraining the interpretation of uninterpreted functions,
-    *   and adding n to the equality engine of this model
+  /** add term
+    *  This will do any model-specific processing necessary for n,
+    *  such as constraining the interpretation of uninterpreted functions,
+    *  and adding n to the equality engine of this model.
     */
   virtual void addTerm(TNode n);
   /** assert equality holds in the model */
@@ -81,6 +110,7 @@ public:
     *  functions.
     */
   void assertRepresentative(TNode n);
+  //---------------------------- end building the model
 
   // ------------------- general equality queries
   /** does the equality engine of this model have term a? */
@@ -95,6 +125,23 @@ public:
   eq::EqualityEngine* getEqualityEngine() { return d_equalityEngine; }
   // ------------------- end general equality queries
 
+  /** Get value function.
+   * This should be called only after a ModelBuilder
+   * has called buildModel(...) on this model.
+   *   useDontCares is whether to return Node::null() if
+   *     n does not occur in the equality engine.
+   */
+  Node getValue(TNode n, bool useDontCares = false) const;
+  /** get comments */
+  void getComments(std::ostream& out) const;
+
+  //---------------------------- separation logic
+  /** set the heap and value sep.nil is equal to */
+  void setHeapModel(Node h, Node neq);
+  /** get the heap and value sep.nil is equal to */
+  bool getHeapModel(Expr& h, Expr& neq) const;
+  //---------------------------- end separation logic
+
   /** get the representative set object */
   const RepSet* getRepSet() const { return &d_rep_set; }
   /** get the representative set object (FIXME: remove this, see #1199) */
@@ -145,19 +192,23 @@ public:
   /** true/false nodes */
   Node d_true;
   Node d_false;
-  mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
   /** comment stream to include in printing */
   std::stringstream d_comment_str;
-  /** reset the model */
-  virtual void reset();
-  /**
-   * Get model value function.  This function is called by getValue
+  /** Get model value function.
+   *
+   * This function is a helper function for getValue.
+   *   hasBoundVars is whether n may contain bound variables
+   *   useDontCares is whether to return Node::null() if
+   *     n does not occur in the equality engine.
    */
   Node getModelValue(TNode n,
                      bool hasBoundVars = false,
                      bool useDontCares = false) const;
 
  private:
+  /** cache for getModelValue */
+  mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
+
   //---------------------------- separation logic
   /** the value of the heap */
   Node d_sep_heap;
@@ -170,234 +221,12 @@ public:
   bool d_enableFuncModels;
   /** map from function terms to the (lambda) definitions
   * After the model is built, the domain of this map is all terms of function
-  * type
-  * that appear as terms in d_equalityEngine.
+  * type that appear as terms in d_equalityEngine.
   */
   std::map<Node, Node> d_uf_models;
   //---------------------------- end function values
 };/* class TheoryModel */
 
-/*
- * Class that encapsulates a map from types to sets of nodes
- */
-class TypeSet {
-public:
-  typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
-  typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
-  typedef TypeSetMap::iterator iterator;
-  typedef TypeSetMap::const_iterator const_iterator;
-private:
-  TypeSetMap d_typeSet;
-  TypeToTypeEnumMap d_teMap;
-  TypeEnumeratorProperties * d_tep;
-
-  /* Note that recursive traversal here is over enumerated expressions
-   * (very low expression depth). */
-  void addSubTerms(TNode n, std::map< TNode, bool >& visited, bool topLevel=true){
-    if( visited.find( n )==visited.end() ){
-      visited[n] = true;
-      if( !topLevel ){
-        add(n.getType(), n);
-      }
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        addSubTerms( n[i], visited, false );
-      }
-    }
-  }
-public:
-  TypeSet() : d_tep(NULL) {}
-  ~TypeSet() {
-    iterator it;
-    for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it) {
-      if ((*it).second != NULL) {
-        delete (*it).second;
-      }
-    }
-    TypeToTypeEnumMap::iterator it2;
-    for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2) {
-      if ((*it2).second != NULL) {
-        delete (*it2).second;
-      }
-    }
-  }
-  void setTypeEnumeratorProperties( TypeEnumeratorProperties * tep ) { d_tep = tep; }
-  void add(TypeNode t, TNode n)
-  {
-    iterator it = d_typeSet.find(t);
-    std::set<Node>* s;
-    if (it == d_typeSet.end()) {
-      s = new std::set<Node>;
-      d_typeSet[t] = s;
-    }
-    else {
-      s = (*it).second;
-    }
-    s->insert(n);
-  }
-
-  std::set<Node>* getSet(TypeNode t) const
-  {
-    const_iterator it = d_typeSet.find(t);
-    if (it == d_typeSet.end()) {
-      return NULL;
-    }
-    return (*it).second;
-  }
-
-  Node nextTypeEnum(TypeNode t, bool useBaseType = false)
-  {
-    TypeEnumerator* te;
-    TypeToTypeEnumMap::iterator it = d_teMap.find(t);
-    if (it == d_teMap.end()) {
-      te = new TypeEnumerator(t, d_tep);
-      d_teMap[t] = te;
-    }
-    else {
-      te = (*it).second;
-    }
-    if (te->isFinished()) {
-      return Node();
-    }
-
-    if (useBaseType) {
-      t = t.getBaseType();
-    }
-    iterator itSet = d_typeSet.find(t);
-    std::set<Node>* s;
-    if (itSet == d_typeSet.end()) {
-      s = new std::set<Node>;
-      d_typeSet[t] = s;
-    }
-    else {
-      s = (*itSet).second;
-    }
-    Node n = **te;
-    while (s->find(n) != s->end()) {
-      ++(*te);
-      if (te->isFinished()) {
-        return Node();
-      }
-      n = **te;
-    }
-    s->insert(n);
-    // add all subterms of n to this set as well
-    // this is necessary for parametric types whose values are constructed from other types 
-    // to ensure that we do not enumerate subterms of other previous enumerated values
-    std::map< TNode, bool > visited;
-    addSubTerms(n, visited);
-    ++(*te);
-    return n;
-  }
-
-  bool empty()
-  {
-    return d_typeSet.empty();
-  }
-
-  iterator begin()
-  {
-    return d_typeSet.begin();
-  }
-
-  iterator end()
-  {
-    return d_typeSet.end();
-  }
-
-  static TypeNode getType(iterator it)
-  {
-    return (*it).first;
-  }
-
-  static std::set<Node>& getSet(iterator it)
-  {
-    return *(*it).second;
-  }
-
-};/* class TypeSet */
-
-/** TheoryEngineModelBuilder class
-  *    This model builder will consult all theories in a theory engine for
-  *    collectModelInfo( ... ) when building a model.
-  */
-class TheoryEngineModelBuilder : public ModelBuilder
-{
-protected:
-  /** pointer to theory engine */
-  TheoryEngine* d_te;
-  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
-  NodeMap d_normalizedCache;
-  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
-  std::map< Node, Node > d_constantReps;
-
-  /** process build model */
-  virtual bool preProcessBuildModel(TheoryModel* m);
-  virtual bool processBuildModel(TheoryModel* m);
-  virtual void debugModel( TheoryModel* m ) {}
-  /** normalize representative */
-  Node normalize(TheoryModel* m, TNode r, bool evalOnly);
-  bool isAssignable(TNode n);
-  void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
-  void assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep );
-  void addToTypeList( TypeNode tn, std::vector< TypeNode >& type_list, std::map< TypeNode, bool >& visiting );
-  /** is v an excluded codatatype value */
-  bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc );
-  bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m );
-  /** involves usort */
-  bool involvesUSort( TypeNode tn );
-  bool isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited );
-protected:
-  /** assign function f based on the model m. 
-  * This construction is based on "table form". For example:
-  * (f 0 1) = 1
-  * (f 0 2) = 2
-  * (f 1 1) = 3
-  * ...
-  * becomes:
-  * f = (lambda xy. (ite (and (= x 0) (= y 1)) 1 
-  *                 (ite (and (= x 0) (= y 2)) 2
-  *                 (ite (and (= x 1) (= y 1)) 3 ...)))
-  */
-  void assignFunction(TheoryModel* m, Node f);
-  /** assign function f based on the model m. 
-  * This construction is based on "dag form". For example:
-  * (f 0 1) = 1
-  * (f 0 2) = 2
-  * (f 1 1) = 3
-  * ...
-  * becomes:
-  * f = (lambda xy. (ite (= x 0) (ite (= y 1) 1
-  *                              (ite (= y 2) 2 ...))
-  *                 (ite (= x 1) (ite (= y 1) 3 ...)
-  *                              ...))
-  * 
-  * where the above is represented as a directed acyclic graph (dag).
-  * This construction is accomplished by assigning values to (f c) 
-  * terms before f, e.g. 
-  * (f 0) = (lambda y. (ite (= y 1) 1
-  *                    (ite (= y 2) 2 ...))
-  * (f 1) = (lambda y. (ite (= y 1) 3 ...))
-  * where
-  * f = (lambda xy. (ite (= x 0) ((f 0) y)
-  *                 (ite (= x 1) ((f 1) y) ...))
-  */
-  void assignHoFunction(TheoryModel* m, Node f);
-  /** Assign all unassigned functions in the model m (those returned by TheoryModel::getFunctionsToAssign), 
-  * using the two functions above. Currently:
-  * If ufHo is disabled, we call assignFunction for all functions. 
-  * If ufHo is enabled, we call assignHoFunction.
-  */
-  void assignFunctions(TheoryModel* m);
-public:
-  TheoryEngineModelBuilder(TheoryEngine* te);
-  virtual ~TheoryEngineModelBuilder(){}
-  /** Build model function.
-   *    Should be called only on TheoryModels m
-   */
-  bool buildModel(Model* m);
-  void debugCheckModel(Model* m);
-};/* class TheoryEngineModelBuilder */
-
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
new file mode 100644
index 000000000..b08c8f1ca
--- /dev/null
+++ b/src/theory/theory_model_builder.cpp
@@ -0,0 +1,1144 @@
+/*********************                                                        */
+/*! \file theory_model_builder.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Clark Barrett, Andrew Reynolds, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of theory model buidler class
+ **/
+#include "theory/theory_model_builder.h"
+
+#include "options/quantifiers_options.h"
+#include "options/smt_options.h"
+#include "options/uf_options.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/theory_uf_model.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+
+TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine* te) : d_te(te)
+{
+}
+
+bool TheoryEngineModelBuilder::isAssignable(TNode n)
+{
+  if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL)
+  {
+    // selectors are always assignable (where we guarantee that they are not
+    // evaluatable here)
+    if (!options::ufHo())
+    {
+      Assert(!n.getType().isFunction());
+      return true;
+    }
+    else
+    {
+      // might be a function field
+      return !n.getType().isFunction();
+    }
+  }
+  else
+  {
+    // non-function variables, and fully applied functions
+    if (!options::ufHo())
+    {
+      // no functions exist, all functions are fully applied
+      Assert(n.getKind() != kind::HO_APPLY);
+      Assert(!n.getType().isFunction());
+      return n.isVar() || n.getKind() == kind::APPLY_UF;
+    }
+    else
+    {
+      // Assert( n.getKind() != kind::APPLY_UF );
+      return (n.isVar() && !n.getType().isFunction())
+             || n.getKind() == kind::APPLY_UF
+             || (n.getKind() == kind::HO_APPLY
+                 && n[0].getType().getNumChildren() == 2);
+    }
+  }
+}
+
+void TheoryEngineModelBuilder::addAssignableSubterms(TNode n,
+                                                     TheoryModel* tm,
+                                                     NodeSet& cache)
+{
+  if (n.getKind() == FORALL || n.getKind() == EXISTS)
+  {
+    return;
+  }
+  if (cache.find(n) != cache.end())
+  {
+    return;
+  }
+  if (isAssignable(n))
+  {
+    tm->d_equalityEngine->addTerm(n);
+  }
+  for (TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it)
+  {
+    addAssignableSubterms(*child_it, tm, cache);
+  }
+  cache.insert(n);
+}
+
+void TheoryEngineModelBuilder::assignConstantRep(TheoryModel* tm,
+                                                 Node eqc,
+                                                 Node const_rep)
+{
+  d_constantReps[eqc] = const_rep;
+  Trace("model-builder") << "    Assign: Setting constant rep of " << eqc
+                         << " to " << const_rep << endl;
+  tm->d_rep_set.setTermForRepresentative(const_rep, eqc);
+}
+
+bool TheoryEngineModelBuilder::isExcludedCdtValue(
+    Node val,
+    std::set<Node>* repSet,
+    std::map<Node, Node>& assertedReps,
+    Node eqc)
+{
+  Trace("model-builder-debug")
+      << "Is " << val << " and excluded codatatype value for " << eqc << "? "
+      << std::endl;
+  for (set<Node>::iterator i = repSet->begin(); i != repSet->end(); ++i)
+  {
+    Assert(assertedReps.find(*i) != assertedReps.end());
+    Node rep = assertedReps[*i];
+    Trace("model-builder-debug") << "  Rep : " << rep << std::endl;
+    // check matching val to rep with eqc as a free variable
+    Node eqc_m;
+    if (isCdtValueMatch(val, rep, eqc, eqc_m))
+    {
+      Trace("model-builder-debug") << "  ...matches with " << eqc << " -> "
+                                   << eqc_m << std::endl;
+      if (eqc_m.getKind() == kind::UNINTERPRETED_CONSTANT)
+      {
+        Trace("model-builder-debug") << "*** " << val
+                                     << " is excluded datatype for " << eqc
+                                     << std::endl;
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+bool TheoryEngineModelBuilder::isCdtValueMatch(Node v,
+                                               Node r,
+                                               Node eqc,
+                                               Node& eqc_m)
+{
+  if (r == v)
+  {
+    return true;
+  }
+  else if (r == eqc)
+  {
+    if (eqc_m.isNull())
+    {
+      // only if an uninterpreted constant?
+      eqc_m = v;
+      return true;
+    }
+    else
+    {
+      return v == eqc_m;
+    }
+  }
+  else if (v.getKind() == kind::APPLY_CONSTRUCTOR
+           && r.getKind() == kind::APPLY_CONSTRUCTOR)
+  {
+    if (v.getOperator() == r.getOperator())
+    {
+      for (unsigned i = 0; i < v.getNumChildren(); i++)
+      {
+        if (!isCdtValueMatch(v[i], r[i], eqc, eqc_m))
+        {
+          return false;
+        }
+      }
+      return true;
+    }
+  }
+  return false;
+}
+
+bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn)
+{
+  if (tn.isSort())
+  {
+    return true;
+  }
+  else if (tn.isArray())
+  {
+    return involvesUSort(tn.getArrayIndexType())
+           || involvesUSort(tn.getArrayConstituentType());
+  }
+  else if (tn.isSet())
+  {
+    return involvesUSort(tn.getSetElementType());
+  }
+  else if (tn.isDatatype())
+  {
+    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    return dt.involvesUninterpretedType();
+  }
+  else
+  {
+    return false;
+  }
+}
+
+bool TheoryEngineModelBuilder::isExcludedUSortValue(
+    std::map<TypeNode, unsigned>& eqc_usort_count,
+    Node v,
+    std::map<Node, bool>& visited)
+{
+  Assert(v.isConst());
+  if (visited.find(v) == visited.end())
+  {
+    visited[v] = true;
+    TypeNode tn = v.getType();
+    if (tn.isSort())
+    {
+      Trace("model-builder-debug") << "Is excluded usort value : " << v << " "
+                                   << tn << std::endl;
+      unsigned card = eqc_usort_count[tn];
+      Trace("model-builder-debug") << "  Cardinality is " << card << std::endl;
+      unsigned index =
+          v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
+      Trace("model-builder-debug") << "  Index is " << index << std::endl;
+      return index > 0 && index >= card;
+    }
+    for (unsigned i = 0; i < v.getNumChildren(); i++)
+    {
+      if (isExcludedUSortValue(eqc_usort_count, v[i], visited))
+      {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+void TheoryEngineModelBuilder::addToTypeList(
+    TypeNode tn,
+    std::vector<TypeNode>& type_list,
+    std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting)
+{
+  if (std::find(type_list.begin(), type_list.end(), tn) == type_list.end())
+  {
+    if (visiting.find(tn) == visiting.end())
+    {
+      visiting.insert(tn);
+      /* This must make a recursive call on all types that are subterms of
+       * values of the current type.
+       * Note that recursive traversal here is over enumerated expressions
+       * (very low expression depth). */
+      if (tn.isArray())
+      {
+        addToTypeList(tn.getArrayIndexType(), type_list, visiting);
+        addToTypeList(tn.getArrayConstituentType(), type_list, visiting);
+      }
+      else if (tn.isSet())
+      {
+        addToTypeList(tn.getSetElementType(), type_list, visiting);
+      }
+      else if (tn.isDatatype())
+      {
+        const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+        for (unsigned i = 0; i < dt.getNumConstructors(); i++)
+        {
+          for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
+          {
+            TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
+            addToTypeList(ctn, type_list, visiting);
+          }
+        }
+      }
+      Assert(std::find(type_list.begin(), type_list.end(), tn)
+             == type_list.end());
+      type_list.push_back(tn);
+    }
+  }
+}
+
+bool TheoryEngineModelBuilder::buildModel(Model* m)
+{
+  Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
+  TheoryModel* tm = (TheoryModel*)m;
+
+  // buildModel should only be called once per check
+  Assert(!tm->isBuilt());
+
+  // Reset model
+  tm->reset();
+
+  // mark as built
+  tm->d_modelBuilt = true;
+
+  // Collect model info from the theories
+  Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..."
+                         << std::endl;
+  d_te->collectModelInfo(tm);
+
+  // model-builder specific initialization
+  if (!preProcessBuildModel(tm))
+  {
+    return false;
+  }
+
+  // Loop through all terms and make sure that assignable sub-terms are in the
+  // equality engine
+  // Also, record #eqc per type (for finite model finding)
+  std::map<TypeNode, unsigned> eqc_usort_count;
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
+  {
+    NodeSet cache;
+    for (; !eqcs_i.isFinished(); ++eqcs_i)
+    {
+      eq::EqClassIterator eqc_i =
+          eq::EqClassIterator((*eqcs_i), tm->d_equalityEngine);
+      for (; !eqc_i.isFinished(); ++eqc_i)
+      {
+        addAssignableSubterms(*eqc_i, tm, cache);
+      }
+      TypeNode tn = (*eqcs_i).getType();
+      if (tn.isSort())
+      {
+        if (eqc_usort_count.find(tn) == eqc_usort_count.end())
+        {
+          eqc_usort_count[tn] = 1;
+        }
+        else
+        {
+          eqc_usort_count[tn]++;
+        }
+      }
+    }
+  }
+
+  Trace("model-builder") << "Collect representatives..." << std::endl;
+
+  // Process all terms in the equality engine, store representatives for each EC
+  d_constantReps.clear();
+  std::map<Node, Node> assertedReps;
+  TypeSet typeConstSet, typeRepSet, typeNoRepSet;
+  TypeEnumeratorProperties tep;
+  if (options::finiteModelFind())
+  {
+    tep.d_fixed_usort_card = true;
+    for (std::map<TypeNode, unsigned>::iterator it = eqc_usort_count.begin();
+         it != eqc_usort_count.end();
+         ++it)
+    {
+      Trace("model-builder") << "Fixed bound (#eqc) for " << it->first << " : "
+                             << it->second << std::endl;
+      tep.d_fixed_card[it->first] = Integer(it->second);
+    }
+    typeConstSet.setTypeEnumeratorProperties(&tep);
+  }
+  // AJR: build ordered list of types that ensures that base types are
+  // enumerated first.
+  //   (I think) this is only strictly necessary for finite model finding +
+  //   parametric types
+  //   instantiated with uninterpreted sorts, but is probably a good idea to do
+  //   in general
+  //   since it leads to models with smaller term sizes.
+  std::vector<TypeNode> type_list;
+  eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
+  for (; !eqcs_i.isFinished(); ++eqcs_i)
+  {
+    // eqc is the equivalence class representative
+    Node eqc = (*eqcs_i);
+    Trace("model-builder") << "Processing EC: " << eqc << endl;
+    Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc);
+    TypeNode eqct = eqc.getType();
+    Assert(assertedReps.find(eqc) == assertedReps.end());
+    Assert(d_constantReps.find(eqc) == d_constantReps.end());
+
+    // Loop through terms in this EC
+    Node rep, const_rep;
+    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
+    for (; !eqc_i.isFinished(); ++eqc_i)
+    {
+      Node n = *eqc_i;
+      Trace("model-builder") << "  Processing Term: " << n << endl;
+      // Record as rep if this node was specified as a representative
+      if (tm->d_reps.find(n) != tm->d_reps.end())
+      {
+        // AJR: I believe this assertion is too strict,
+        // e.g. datatypes may assert representative for two constructor terms
+        // that are not in the care graph and are merged during
+        // collectModelInfo.
+        // Assert(rep.isNull());
+        rep = tm->d_reps[n];
+        Assert(!rep.isNull());
+        Trace("model-builder") << "  Rep( " << eqc << " ) = " << rep
+                               << std::endl;
+      }
+      // Record as const_rep if this node is constant
+      if (n.isConst())
+      {
+        Assert(const_rep.isNull());
+        const_rep = n;
+        Trace("model-builder") << "  ConstRep( " << eqc << " ) = " << const_rep
+                               << std::endl;
+      }
+      // model-specific processing of the term
+      tm->addTerm(n);
+    }
+
+    // Assign representative for this EC
+    if (!const_rep.isNull())
+    {
+      // Theories should not specify a rep if there is already a constant in the
+      // EC
+      // AJR: I believe this assertion is too strict, eqc with asserted reps may
+      // merge with constant eqc
+      // Assert(rep.isNull() || rep == const_rep);
+      assignConstantRep(tm, eqc, const_rep);
+      typeConstSet.add(eqct.getBaseType(), const_rep);
+    }
+    else if (!rep.isNull())
+    {
+      assertedReps[eqc] = rep;
+      typeRepSet.add(eqct.getBaseType(), eqc);
+      std::unordered_set<TypeNode, TypeNodeHashFunction> visiting;
+      addToTypeList(eqct.getBaseType(), type_list, visiting);
+    }
+    else
+    {
+      typeNoRepSet.add(eqct, eqc);
+      std::unordered_set<TypeNode, TypeNodeHashFunction> visiting;
+      addToTypeList(eqct, type_list, visiting);
+    }
+  }
+
+  // Need to ensure that each EC has a constant representative.
+
+  Trace("model-builder") << "Processing EC's..." << std::endl;
+
+  TypeSet::iterator it;
+  vector<TypeNode>::iterator type_it;
+  set<Node>::iterator i, i2;
+  bool changed, unassignedAssignable, assignOne = false;
+  set<TypeNode> evaluableSet;
+
+  // Double-fixed-point loop
+  // Outer loop handles a special corner case (see code at end of loop for
+  // details)
+  for (;;)
+  {
+    // Inner fixed-point loop: we are trying to learn constant values for every
+    // EC.  Each time through this loop, we process all of the
+    // types by type and may learn some new EC values.  EC's in one type may
+    // depend on EC's in another type, so we need a fixed-point loop
+    // to ensure that we learn as many EC values as possible
+    do
+    {
+      changed = false;
+      unassignedAssignable = false;
+      evaluableSet.clear();
+
+      // Iterate over all types we've seen
+      for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
+      {
+        TypeNode t = *type_it;
+        TypeNode tb = t.getBaseType();
+        set<Node>* noRepSet = typeNoRepSet.getSet(t);
+
+        // 1. Try to evaluate the EC's in this type
+        if (noRepSet != NULL && !noRepSet->empty())
+        {
+          Trace("model-builder") << "  Eval phase, working on type: " << t
+                                 << endl;
+          bool assignable, evaluable, evaluated;
+          d_normalizedCache.clear();
+          for (i = noRepSet->begin(); i != noRepSet->end();)
+          {
+            i2 = i;
+            ++i;
+            assignable = false;
+            evaluable = false;
+            evaluated = false;
+            Trace("model-builder-debug") << "Look at eqc : " << (*i2)
+                                         << std::endl;
+            eq::EqClassIterator eqc_i =
+                eq::EqClassIterator(*i2, tm->d_equalityEngine);
+            for (; !eqc_i.isFinished(); ++eqc_i)
+            {
+              Node n = *eqc_i;
+              Trace("model-builder-debug") << "Look at term : " << n
+                                           << std::endl;
+              if (isAssignable(n))
+              {
+                assignable = true;
+                Trace("model-builder-debug") << "...assignable" << std::endl;
+              }
+              else
+              {
+                evaluable = true;
+                Trace("model-builder-debug") << "...try to normalize"
+                                             << std::endl;
+                Node normalized = normalize(tm, n, true);
+                if (normalized.isConst())
+                {
+                  typeConstSet.add(tb, normalized);
+                  assignConstantRep(tm, *i2, normalized);
+                  Trace("model-builder") << "    Eval: Setting constant rep of "
+                                         << (*i2) << " to " << normalized
+                                         << endl;
+                  changed = true;
+                  evaluated = true;
+                  noRepSet->erase(i2);
+                  break;
+                }
+              }
+            }
+            if (!evaluated)
+            {
+              if (evaluable)
+              {
+                evaluableSet.insert(tb);
+              }
+              if (assignable)
+              {
+                unassignedAssignable = true;
+              }
+            }
+          }
+        }
+
+        // 2. Normalize any non-const representative terms for this type
+        set<Node>* repSet = typeRepSet.getSet(t);
+        if (repSet != NULL && !repSet->empty())
+        {
+          Trace("model-builder")
+              << "  Normalization phase, working on type: " << t << endl;
+          d_normalizedCache.clear();
+          for (i = repSet->begin(); i != repSet->end();)
+          {
+            Assert(assertedReps.find(*i) != assertedReps.end());
+            Node rep = assertedReps[*i];
+            Node normalized = normalize(tm, rep, false);
+            Trace("model-builder") << "    Normalizing rep (" << rep
+                                   << "), normalized to (" << normalized << ")"
+                                   << endl;
+            if (normalized.isConst())
+            {
+              changed = true;
+              typeConstSet.add(tb, normalized);
+              assignConstantRep(tm, *i, normalized);
+              assertedReps.erase(*i);
+              i2 = i;
+              ++i;
+              repSet->erase(i2);
+            }
+            else
+            {
+              if (normalized != rep)
+              {
+                assertedReps[*i] = normalized;
+                changed = true;
+              }
+              ++i;
+            }
+          }
+        }
+      }
+    } while (changed);
+
+    if (!unassignedAssignable)
+    {
+      break;
+    }
+
+    // 3. Assign unassigned assignable EC's using type enumeration - assign a
+    // value *different* from all other EC's if the type is infinite
+    // Assign first value from type enumerator otherwise - for finite types, we
+    // rely on polite framework to ensure that EC's that have to be
+    // different are different.
+
+    // Only make assignments on a type if:
+    // 1. there are no terms that share the same base type with un-normalized
+    // representatives
+    // 2. there are no terms that share teh same base type that are unevaluated
+    // evaluable terms
+    // Alternatively, if 2 or 3 don't hold but we are in a special
+    // deadlock-breaking mode where assignOne is true, go ahead and make one
+    // assignment
+    changed = false;
+    // must iterate over the ordered type list to ensure that we do not
+    // enumerate values with subterms
+    //  having types that we are currently enumerating (when possible)
+    //  for example, this ensures we enumerate uninterpreted sort U before (List
+    //  of U) and (Array U U)
+    //  however, it does not break cyclic type dependencies for mutually
+    //  recursive datatypes, but this is handled
+    //  by recording all subterms of enumerated values in TypeSet::addSubTerms.
+    for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
+    {
+      TypeNode t = *type_it;
+      // continue if there are no more equivalence classes of this type to
+      // assign
+      std::set<Node>* noRepSetPtr = typeNoRepSet.getSet(t);
+      if (noRepSetPtr == NULL)
+      {
+        continue;
+      }
+      set<Node>& noRepSet = *noRepSetPtr;
+      if (noRepSet.empty())
+      {
+        continue;
+      }
+
+      // get properties of this type
+      bool isCorecursive = false;
+      if (t.isDatatype())
+      {
+        const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
+        isCorecursive =
+            dt.isCodatatype() && (!dt.isFinite(t.toType())
+                                  || dt.isRecursiveSingleton(t.toType()));
+      }
+#ifdef CVC4_ASSERTIONS
+      bool isUSortFiniteRestricted = false;
+      if (options::finiteModelFind())
+      {
+        isUSortFiniteRestricted = !t.isSort() && involvesUSort(t);
+      }
+#endif
+
+      set<Node>* repSet = typeRepSet.getSet(t);
+      TypeNode tb = t.getBaseType();
+      if (!assignOne)
+      {
+        set<Node>* repSet = typeRepSet.getSet(tb);
+        if (repSet != NULL && !repSet->empty())
+        {
+          continue;
+        }
+        if (evaluableSet.find(tb) != evaluableSet.end())
+        {
+          continue;
+        }
+      }
+      Trace("model-builder") << "  Assign phase, working on type: " << t
+                             << endl;
+      bool assignable, evaluable CVC4_UNUSED;
+      for (i = noRepSet.begin(); i != noRepSet.end();)
+      {
+        i2 = i;
+        ++i;
+        eq::EqClassIterator eqc_i =
+            eq::EqClassIterator(*i2, tm->d_equalityEngine);
+        assignable = false;
+        evaluable = false;
+        for (; !eqc_i.isFinished(); ++eqc_i)
+        {
+          Node n = *eqc_i;
+          if (isAssignable(n))
+          {
+            assignable = true;
+          }
+          else
+          {
+            evaluable = true;
+          }
+        }
+        Trace("model-builder-debug")
+            << "    eqc " << *i2 << " is assignable=" << assignable
+            << ", evaluable=" << evaluable << std::endl;
+        if (assignable)
+        {
+          Assert(!evaluable || assignOne);
+          Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF);
+          Node n;
+          if (t.getCardinality().isInfinite())
+          {
+            // if (!t.isInterpretedFinite()) {
+            bool success;
+            do
+            {
+              Trace("model-builder-debug") << "Enumerate term of type " << t
+                                           << std::endl;
+              n = typeConstSet.nextTypeEnum(t, true);
+              //--- AJR: this code checks whether n is a legal value
+              Assert(!n.isNull());
+              success = true;
+              Trace("model-builder-debug") << "Check if excluded : " << n
+                                           << std::endl;
+#ifdef CVC4_ASSERTIONS
+              if (isUSortFiniteRestricted)
+              {
+                // must not involve uninterpreted constants beyond cardinality
+                // bound (which assumed to coincide with #eqc)
+                // this is just an assertion now, since TypeEnumeratorProperties
+                // should ensure that only legal values are enumerated wrt this
+                // constraint.
+                std::map<Node, bool> visited;
+                success = !isExcludedUSortValue(eqc_usort_count, n, visited);
+                if (!success)
+                {
+                  Trace("model-builder")
+                      << "Excluded value for " << t << " : " << n
+                      << " due to out of range uninterpreted constant."
+                      << std::endl;
+                }
+                Assert(success);
+              }
+#endif
+              if (success && isCorecursive)
+              {
+                if (repSet != NULL && !repSet->empty())
+                {
+                  // in the case of codatatypes, check if it is in the set of
+                  // values that we cannot assign
+                  success = !isExcludedCdtValue(n, repSet, assertedReps, *i2);
+                  if (!success)
+                  {
+                    Trace("model-builder")
+                        << "Excluded value : " << n
+                        << " due to alpha-equivalent codatatype expression."
+                        << std::endl;
+                  }
+                }
+              }
+              //---
+            } while (!success);
+          }
+          else
+          {
+            TypeEnumerator te(t);
+            n = *te;
+          }
+          Assert(!n.isNull());
+          assignConstantRep(tm, *i2, n);
+          changed = true;
+          noRepSet.erase(i2);
+          if (assignOne)
+          {
+            assignOne = false;
+            break;
+          }
+        }
+      }
+    }
+
+    // Corner case - I'm not sure this can even happen - but it's theoretically
+    // possible to have a cyclical dependency
+    // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}.  In
+    // this case, neither one will get assigned because we are waiting
+    // to be able to evaluate.  But we will never be able to evaluate because
+    // the variables that need to be assigned are in
+    // these same EC's.  In this case, repeat the whole fixed-point computation
+    // with the difference that the first EC
+    // that has both assignable and evaluable expressions will get assigned.
+    if (!changed)
+    {
+      Assert(!assignOne);  // check for infinite loop!
+      assignOne = true;
+    }
+  }
+
+#ifdef CVC4_ASSERTIONS
+  // Assert that all representatives have been converted to constants
+  for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it)
+  {
+    set<Node>& repSet = TypeSet::getSet(it);
+    if (!repSet.empty())
+    {
+      Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size()
+                             << ", first = " << *(repSet.begin()) << endl;
+      Assert(false);
+    }
+  }
+#endif /* CVC4_ASSERTIONS */
+
+  Trace("model-builder") << "Copy representatives to model..." << std::endl;
+  tm->d_reps.clear();
+  std::map<Node, Node>::iterator itMap;
+  for (itMap = d_constantReps.begin(); itMap != d_constantReps.end(); ++itMap)
+  {
+    tm->d_reps[itMap->first] = itMap->second;
+    tm->d_rep_set.add(itMap->second.getType(), itMap->second);
+  }
+
+  Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
+  // Make sure every EC has a rep
+  for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap)
+  {
+    tm->d_reps[itMap->first] = itMap->second;
+    tm->d_rep_set.add(itMap->second.getType(), itMap->second);
+  }
+  for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it)
+  {
+    set<Node>& noRepSet = TypeSet::getSet(it);
+    set<Node>::iterator i;
+    for (i = noRepSet.begin(); i != noRepSet.end(); ++i)
+    {
+      tm->d_reps[*i] = *i;
+      tm->d_rep_set.add((*i).getType(), *i);
+    }
+  }
+
+  // modelBuilder-specific initialization
+  if (!processBuildModel(tm))
+  {
+    return false;
+  }
+  else
+  {
+    return true;
+  }
+}
+
+void TheoryEngineModelBuilder::debugCheckModel(Model* m)
+{
+  TheoryModel* tm = (TheoryModel*)m;
+#ifdef CVC4_ASSERTIONS
+  Assert(tm->isBuilt());
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
+  std::map<Node, Node>::iterator itMap;
+  // Check that every term evaluates to its representative in the model
+  for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
+       !eqcs_i.isFinished();
+       ++eqcs_i)
+  {
+    // eqc is the equivalence class representative
+    Node eqc = (*eqcs_i);
+    // get the representative
+    Node rep = tm->getRepresentative(eqc);
+    if (!rep.isConst() && eqc.getType().isBoolean())
+    {
+      // if Boolean, it does not necessarily have a constant representative, use
+      // get value instead
+      rep = tm->getValue(eqc);
+      Assert(rep.isConst());
+    }
+    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
+    for (; !eqc_i.isFinished(); ++eqc_i)
+    {
+      Node n = *eqc_i;
+      static int repCheckInstance = 0;
+      ++repCheckInstance;
+
+      // non-linear mult is not necessarily accurate wrt getValue
+      if (n.getKind() != kind::NONLINEAR_MULT)
+      {
+        Debug("check-model::rep-checking") << "( " << repCheckInstance << ") "
+                                           << "n: " << n << endl
+                                           << "getValue(n): " << tm->getValue(n)
+                                           << endl
+                                           << "rep: " << rep << endl;
+        Assert(tm->getValue(*eqc_i) == rep,
+               "run with -d check-model::rep-checking for details");
+      }
+    }
+  }
+#endif /* CVC4_ASSERTIONS */
+
+  // builder-specific debugging
+  debugModel(tm);
+}
+
+Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
+{
+  std::map<Node, Node>::iterator itMap = d_constantReps.find(r);
+  if (itMap != d_constantReps.end())
+  {
+    return (*itMap).second;
+  }
+  NodeMap::iterator it = d_normalizedCache.find(r);
+  if (it != d_normalizedCache.end())
+  {
+    return (*it).second;
+  }
+  Trace("model-builder-debug") << "do normalize on " << r << std::endl;
+  Node retNode = r;
+  if (r.getNumChildren() > 0)
+  {
+    std::vector<Node> children;
+    if (r.getMetaKind() == kind::metakind::PARAMETERIZED)
+    {
+      children.push_back(r.getOperator());
+    }
+    bool childrenConst = true;
+    for (size_t i = 0; i < r.getNumChildren(); ++i)
+    {
+      Node ri = r[i];
+      bool recurse = true;
+      if (!ri.isConst())
+      {
+        if (m->d_equalityEngine->hasTerm(ri))
+        {
+          itMap =
+              d_constantReps.find(m->d_equalityEngine->getRepresentative(ri));
+          if (itMap != d_constantReps.end())
+          {
+            ri = (*itMap).second;
+            recurse = false;
+          }
+          else if (!evalOnly)
+          {
+            recurse = false;
+          }
+        }
+        if (recurse)
+        {
+          ri = normalize(m, ri, evalOnly);
+        }
+        if (!ri.isConst())
+        {
+          childrenConst = false;
+        }
+      }
+      children.push_back(ri);
+    }
+    retNode = NodeManager::currentNM()->mkNode(r.getKind(), children);
+    if (childrenConst)
+    {
+      retNode = Rewriter::rewrite(retNode);
+      Assert(retNode.getKind() == kind::APPLY_UF
+             || !retNode.getType().isFirstClass()
+             || retNode.isConst());
+    }
+  }
+  d_normalizedCache[r] = retNode;
+  return retNode;
+}
+
+bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m)
+{
+  return true;
+}
+
+bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m)
+{
+  assignFunctions(m);
+  return true;
+}
+
+void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
+{
+  Assert(!options::ufHo());
+  uf::UfModelTree ufmt(f);
+  Node default_v;
+  for (size_t i = 0; i < m->d_uf_terms[f].size(); i++)
+  {
+    Node un = m->d_uf_terms[f][i];
+    vector<TNode> children;
+    children.push_back(f);
+    Trace("model-builder-debug") << "  process term : " << un << std::endl;
+    for (size_t j = 0; j < un.getNumChildren(); ++j)
+    {
+      Node rc = m->getRepresentative(un[j]);
+      Trace("model-builder-debug2") << "    get rep : " << un[j] << " returned "
+                                    << rc << std::endl;
+      Assert(rc.isConst());
+      children.push_back(rc);
+    }
+    Node simp = NodeManager::currentNM()->mkNode(un.getKind(), children);
+    Node v = m->getRepresentative(un);
+    Trace("model-builder") << "  Setting (" << simp << ") to (" << v << ")"
+                           << endl;
+    ufmt.setValue(m, simp, v);
+    default_v = v;
+  }
+  if (default_v.isNull())
+  {
+    // choose default value from model if none exists
+    TypeEnumerator te(f.getType().getRangeType());
+    default_v = (*te);
+  }
+  ufmt.setDefaultValue(m, default_v);
+  bool condenseFuncValues = options::condenseFunctionValues();
+  if (condenseFuncValues)
+  {
+    ufmt.simplify();
+  }
+  std::stringstream ss;
+  ss << "_arg_" << f << "_";
+  Node val = ufmt.getFunctionValue(ss.str().c_str(), condenseFuncValues);
+  m->assignFunctionDefinition(f, val);
+  // ufmt.debugPrint( std::cout, m );
+}
+
+void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f)
+{
+  Assert(options::ufHo());
+  TypeNode type = f.getType();
+  std::vector<TypeNode> argTypes = type.getArgTypes();
+  std::vector<Node> args;
+  std::vector<TNode> apply_args;
+  for (unsigned i = 0; i < argTypes.size(); i++)
+  {
+    Node v = NodeManager::currentNM()->mkBoundVar(argTypes[i]);
+    args.push_back(v);
+    if (i > 0)
+    {
+      apply_args.push_back(v);
+    }
+  }
+  // start with the base return value (currently we use the same default value
+  // for all functions)
+  TypeEnumerator te(type.getRangeType());
+  Node curr = (*te);
+  std::map<Node, std::vector<Node> >::iterator itht = m->d_ho_uf_terms.find(f);
+  if (itht != m->d_ho_uf_terms.end())
+  {
+    for (size_t i = 0; i < itht->second.size(); i++)
+    {
+      Node hn = itht->second[i];
+      Trace("model-builder-debug") << "    process : " << hn << std::endl;
+      Assert(hn.getKind() == kind::HO_APPLY);
+      Assert(m->areEqual(hn[0], f));
+      Node hni = m->getRepresentative(hn[1]);
+      Trace("model-builder-debug2") << "      get rep : " << hn[0]
+                                    << " returned " << hni << std::endl;
+      Assert(hni.isConst());
+      Assert(hni.getType().isSubtypeOf(args[0].getType()));
+      hni = Rewriter::rewrite(args[0].eqNode(hni));
+      Node hnv = m->getRepresentative(hn);
+      Trace("model-builder-debug2") << "      get rep val : " << hn
+                                    << " returned " << hnv << std::endl;
+      Assert(hnv.isConst());
+      if (!apply_args.empty())
+      {
+        Assert(hnv.getKind() == kind::LAMBDA
+               && hnv[0].getNumChildren() + 1 == args.size());
+        std::vector<TNode> largs;
+        for (unsigned j = 0; j < hnv[0].getNumChildren(); j++)
+        {
+          largs.push_back(hnv[0][j]);
+        }
+        Assert(largs.size() == apply_args.size());
+        hnv = hnv[1].substitute(
+            largs.begin(), largs.end(), apply_args.begin(), apply_args.end());
+        hnv = Rewriter::rewrite(hnv);
+      }
+      Assert(!TypeNode::leastCommonTypeNode(hnv.getType(), curr.getType())
+                  .isNull());
+      curr = NodeManager::currentNM()->mkNode(kind::ITE, hni, hnv, curr);
+    }
+  }
+  Node val = NodeManager::currentNM()->mkNode(
+      kind::LAMBDA,
+      NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args),
+      curr);
+  m->assignFunctionDefinition(f, val);
+}
+
+// This struct is used to sort terms by the "size" of their type
+//   The size of the type is the number of nodes in the type, for example
+//  size of Int is 1
+//  size of Function( Int, Int ) is 3
+//  size of Function( Function( Bool, Int ), Int ) is 5
+struct sortTypeSize
+{
+  // stores the size of the type
+  std::map<TypeNode, unsigned> d_type_size;
+  // get the size of type tn
+  unsigned getTypeSize(TypeNode tn)
+  {
+    std::map<TypeNode, unsigned>::iterator it = d_type_size.find(tn);
+    if (it != d_type_size.end())
+    {
+      return it->second;
+    }
+    else
+    {
+      unsigned sum = 1;
+      for (unsigned i = 0; i < tn.getNumChildren(); i++)
+      {
+        sum += getTypeSize(tn[i]);
+      }
+      d_type_size[tn] = sum;
+      return sum;
+    }
+  }
+
+ public:
+  // compares the type size of i and j
+  // returns true iff the size of i is less than that of j
+  // tiebreaks are determined by node value
+  bool operator()(Node i, Node j)
+  {
+    int si = getTypeSize(i.getType());
+    int sj = getTypeSize(j.getType());
+    if (si < sj)
+    {
+      return true;
+    }
+    else if (si == sj)
+    {
+      return i < j;
+    }
+    else
+    {
+      return false;
+    }
+  }
+};
+
+void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
+{
+  Trace("model-builder") << "Assigning function values..." << std::endl;
+  std::vector<Node> funcs_to_assign = m->getFunctionsToAssign();
+
+  if (options::ufHo())
+  {
+    // sort based on type size if higher-order
+    Trace("model-builder") << "Sort functions by type..." << std::endl;
+    sortTypeSize sts;
+    std::sort(funcs_to_assign.begin(), funcs_to_assign.end(), sts);
+  }
+
+  if (Trace.isOn("model-builder"))
+  {
+    Trace("model-builder") << "...have " << funcs_to_assign.size()
+                           << " functions to assign:" << std::endl;
+    for (unsigned k = 0; k < funcs_to_assign.size(); k++)
+    {
+      Node f = funcs_to_assign[k];
+      Trace("model-builder") << "  [" << k << "] : " << f << " : "
+                             << f.getType() << std::endl;
+    }
+  }
+
+  // construct function values
+  for (unsigned k = 0; k < funcs_to_assign.size(); k++)
+  {
+    Node f = funcs_to_assign[k];
+    Trace("model-builder") << "  Function #" << k << " is " << f << std::endl;
+    // std::map< Node, std::vector< Node > >::iterator itht =
+    // m->d_ho_uf_terms.find( f );
+    if (!options::ufHo())
+    {
+      Trace("model-builder") << "  Assign function value for " << f
+                             << " based on APPLY_UF" << std::endl;
+      assignFunction(m, f);
+    }
+    else
+    {
+      Trace("model-builder") << "  Assign function value for " << f
+                             << " based on curried HO_APPLY" << std::endl;
+      assignHoFunction(m, f);
+    }
+  }
+  Trace("model-builder") << "Finished assigning function values." << std::endl;
+}
+
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
new file mode 100644
index 000000000..c24d50cbf
--- /dev/null
+++ b/src/theory/theory_model_builder.h
@@ -0,0 +1,253 @@
+/*********************                                                        */
+/*! \file theory_model.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Clark Barrett, Morgan Deters, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Model class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__THEORY_MODEL_BUILDER_H
+#define __CVC4__THEORY__THEORY_MODEL_BUILDER_H
+
+#include <unordered_map>
+#include <unordered_set>
+
+#include "theory/theory_model.h"
+
+namespace CVC4 {
+namespace theory {
+
+/** TheoryEngineModelBuilder class
+ *
+ * This is the class used by TheoryEngine
+ * for constructing TheoryModel objects, which is the class
+ * that represents models for a set of assertions.
+ *
+ * A call to TheoryEngineModelBuilder::buildModel(...) is made
+ * after a full effort check passes with no theory solvers
+ * adding lemmas or conflicts, and theory combination passes
+ * with no splits on shared terms. If buildModel is successful,
+ * this will set up the data structures in TheoryModel to represent
+ * a model for the current set of assertions.
+ */
+class TheoryEngineModelBuilder : public ModelBuilder
+{
+  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+
+ public:
+  TheoryEngineModelBuilder(TheoryEngine* te);
+  virtual ~TheoryEngineModelBuilder() {}
+  /** Build model function.
+   *
+   * Should be called only on TheoryModels m.
+   *
+   * This constructs the model m, via the following steps:
+   * (1) call TheoryEngine::collectModelInfo,
+   * (2) builder-specified pre-processing,
+   * (3) find the equivalence classes of m's
+   *     equality engine that initially contain constants,
+   * (4) assign constants to all equivalence classes
+   *     of m's equality engine, through alternating
+   *     iterations of evaluation and enumeration,
+   * (5) builder-specific post-processing.
+   *
+   * This function returns false if any of the above
+   * steps results in a lemma sent on an output channel.
+   * Lemmas may be sent on an output channel by this
+   * builder in steps (2) or (5), for instance, if the model we
+   * are building fails to satisfy a quantified formula.
+   */
+  virtual bool buildModel(Model* m) override;
+  /** Debug check model.
+   *
+   * This throws an assertion failure if the model
+   * contains an equivalence class with two terms t1 and t2
+   * such that t1^M != t2^M.
+   */
+  void debugCheckModel(Model* m);
+
+ protected:
+  /** pointer to theory engine */
+  TheoryEngine* d_te;
+
+  //-----------------------------------virtual functions
+  /** pre-process build model
+   * Do pre-processing specific to this model builder.
+   * Called in step (2) of the build construction,
+   * described above.
+   */
+  virtual bool preProcessBuildModel(TheoryModel* m);
+  /** process build model
+   * Do processing specific to this model builder.
+   * Called in step (5) of the build construction,
+   * described above.
+   * By default, this assigns values to each function
+   * that appears in m's equality engine.
+   */
+  virtual bool processBuildModel(TheoryModel* m);
+  /** debug the model
+   * Check assertions and printing debug information for the model.
+   * Calls after step (5) described above is complete.
+   */
+  virtual void debugModel(TheoryModel* m) {}
+  //-----------------------------------end virtual functions
+
+  /** is n assignable?
+   *
+   * A term n is assignable if its value
+   * is unconstrained by a standard model.
+   * Examples of assignable terms are:
+   * - variables,
+   * - applications of array select,
+   * - applications of datatype selectors,
+   * - applications of uninterpreted functions.
+   * Assignable terms must be first-order, that is,
+   * all instances of the above terms are not
+   * assignable if they have a higher-order (function) type.
+   */
+  bool isAssignable(TNode n);
+  /** add assignable subterms
+   * Adds all assignable subterms of n to tm's equality engine.
+   */
+  void addAssignableSubterms(TNode n, TheoryModel* tm, NodeSet& cache);
+  /** normalize representative r
+   *
+   * This returns a term that is equivalent to r's
+   * interpretation in the model m. It may do so
+   * by rewriting the application of r's operator to the
+   * result of normalizing each of r's children, if
+   * each child is constant.
+   */
+  Node normalize(TheoryModel* m, TNode r, bool evalOnly);
+  /** assign constant representative
+   *
+   * Called when equivalence class eqc is assigned a constant
+   * representative const_rep.
+   *
+   * eqc should be a representative of tm's equality engine.
+   */
+  void assignConstantRep(TheoryModel* tm, Node eqc, Node const_rep);
+  /** add to type list
+   *
+   * This adds to type_list the list of types that tn is built from.
+   * For example, if tn is (Array Int Bool) and type_list is empty,
+   * then we append ( Int, Bool, (Array Int Bool) ) to type_list.
+   */
+  void addToTypeList(
+      TypeNode tn,
+      std::vector<TypeNode>& type_list,
+      std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting);
+  /** assign function f based on the model m.
+  * This construction is based on "table form". For example:
+  * (f 0 1) = 1
+  * (f 0 2) = 2
+  * (f 1 1) = 3
+  * ...
+  * becomes:
+  * f = (lambda xy. (ite (and (= x 0) (= y 1)) 1
+  *                 (ite (and (= x 0) (= y 2)) 2
+  *                 (ite (and (= x 1) (= y 1)) 3 ...)))
+  */
+  void assignFunction(TheoryModel* m, Node f);
+  /** assign function f based on the model m.
+  * This construction is based on "dag form". For example:
+  * (f 0 1) = 1
+  * (f 0 2) = 2
+  * (f 1 1) = 3
+  * ...
+  * becomes:
+  * f = (lambda xy. (ite (= x 0) (ite (= y 1) 1
+  *                              (ite (= y 2) 2 ...))
+  *                 (ite (= x 1) (ite (= y 1) 3 ...)
+  *                              ...))
+  *
+  * where the above is represented as a directed acyclic graph (dag).
+  * This construction is accomplished by assigning values to (f c)
+  * terms before f, e.g.
+  * (f 0) = (lambda y. (ite (= y 1) 1
+  *                    (ite (= y 2) 2 ...))
+  * (f 1) = (lambda y. (ite (= y 1) 3 ...))
+  * where
+  * f = (lambda xy. (ite (= x 0) ((f 0) y)
+  *                 (ite (= x 1) ((f 1) y) ...))
+  */
+  void assignHoFunction(TheoryModel* m, Node f);
+  /** assign functions
+   *
+   * Assign all unassigned functions in the model m (those returned by
+   * TheoryModel::getFunctionsToAssign),
+   * using the two functions above. Currently:
+   * If ufHo is disabled, we call assignFunction for all functions.
+   * If ufHo is enabled, we call assignHoFunction.
+   */
+  void assignFunctions(TheoryModel* m);
+
+ private:
+  /** normalized cache
+   * A temporary cache mapping terms to their
+   * normalized form, used during buildModel.
+   */
+  NodeMap d_normalizedCache;
+  /** mapping from terms to the constant associated with their equivalence class
+   */
+  std::map<Node, Node> d_constantReps;
+
+  //------------------------------------for codatatypes
+  /** is v an excluded codatatype value?
+   *
+   * If this returns true, then v is a value
+   * that cannot be used during enumeration in step (4)
+   * of model construction.
+   *
+   * repSet is the set of representatives of the same type as v,
+   * assertedReps is a map from representatives t,
+   * eqc is the equivalence class that v reside.
+   *
+   * This function is used to avoid alpha-equivalent
+   * assignments for codatatype terms, described in
+   * Reynolds/Blanchette CADE 2015. In particular,
+   * this function returns true if v is in
+   * the set V^{x}_I from page 9, where x is eqc
+   * and I is the model we are building.
+   */
+  bool isExcludedCdtValue(Node v,
+                          std::set<Node>* repSet,
+                          std::map<Node, Node>& assertedReps,
+                          Node eqc);
+  /** is codatatype value match
+   *
+   * This returns true if v is r{ eqc -> t } for some t.
+   * If this function returns true, then t above is
+   * stored in eqc_m.
+   */
+  bool isCdtValueMatch(Node v, Node r, Node eqc, Node& eqc_m);
+  //------------------------------------end for codatatypes
+
+  //---------------------------------for debugging finite model finding
+  /** does type tn involve an uninterpreted sort? */
+  bool involvesUSort(TypeNode tn);
+  /** is v an excluded value based on uninterpreted sorts?
+   * This gives an assertion failure in the case that v contains
+   * an uninterpreted constant whose index is out of the bounds
+   * specified by eqc_usort_count.
+   */
+  bool isExcludedUSortValue(std::map<TypeNode, unsigned>& eqc_usort_count,
+                            Node v,
+                            std::map<Node, bool>& visited);
+  //---------------------------------end for debugging finite model finding
+
+}; /* class TheoryEngineModelBuilder */
+
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__THEORY_MODEL_BUILDER_H */
diff --git a/src/theory/type_set.cpp b/src/theory/type_set.cpp
new file mode 100644
index 000000000..e7caa667b
--- /dev/null
+++ b/src/theory/type_set.cpp
@@ -0,0 +1,146 @@
+/*********************                                                        */
+/*! \file type_set.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Clark Barrett, Andrew Reynolds, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of type set class
+ **/
+#include "theory/type_set.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+
+TypeSet::~TypeSet()
+{
+  iterator it;
+  for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it)
+  {
+    if ((*it).second != NULL)
+    {
+      delete (*it).second;
+    }
+  }
+  TypeToTypeEnumMap::iterator it2;
+  for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2)
+  {
+    if ((*it2).second != NULL)
+    {
+      delete (*it2).second;
+    }
+  }
+}
+
+void TypeSet::setTypeEnumeratorProperties(TypeEnumeratorProperties* tep)
+{
+  d_tep = tep;
+}
+
+void TypeSet::add(TypeNode t, TNode n)
+{
+  iterator it = d_typeSet.find(t);
+  std::set<Node>* s;
+  if (it == d_typeSet.end())
+  {
+    s = new std::set<Node>;
+    d_typeSet[t] = s;
+  }
+  else
+  {
+    s = (*it).second;
+  }
+  s->insert(n);
+}
+
+std::set<Node>* TypeSet::getSet(TypeNode t) const
+{
+  const_iterator it = d_typeSet.find(t);
+  if (it == d_typeSet.end())
+  {
+    return NULL;
+  }
+  return (*it).second;
+}
+
+Node TypeSet::nextTypeEnum(TypeNode t, bool useBaseType)
+{
+  TypeEnumerator* te;
+  TypeToTypeEnumMap::iterator it = d_teMap.find(t);
+  if (it == d_teMap.end())
+  {
+    te = new TypeEnumerator(t, d_tep);
+    d_teMap[t] = te;
+  }
+  else
+  {
+    te = (*it).second;
+  }
+  if (te->isFinished())
+  {
+    return Node();
+  }
+
+  if (useBaseType)
+  {
+    t = t.getBaseType();
+  }
+  iterator itSet = d_typeSet.find(t);
+  std::set<Node>* s;
+  if (itSet == d_typeSet.end())
+  {
+    s = new std::set<Node>;
+    d_typeSet[t] = s;
+  }
+  else
+  {
+    s = (*itSet).second;
+  }
+  Node n = **te;
+  while (s->find(n) != s->end())
+  {
+    ++(*te);
+    if (te->isFinished())
+    {
+      return Node();
+    }
+    n = **te;
+  }
+  s->insert(n);
+  // add all subterms of n to this set as well
+  // this is necessary for parametric types whose values are constructed from
+  // other types to ensure that we do not enumerate subterms of other 
+  // previously enumerated values
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  addSubTerms(n, visited);
+  ++(*te);
+  return n;
+}
+
+void TypeSet::addSubTerms(TNode n,
+                          std::unordered_set<TNode, TNodeHashFunction>& visited,
+                          bool topLevel)
+{
+  if (visited.find(n) == visited.end())
+  {
+    visited.insert(n);
+    if (!topLevel)
+    {
+      add(n.getType(), n);
+    }
+    for (unsigned i = 0; i < n.getNumChildren(); i++)
+    {
+      addSubTerms(n[i], visited, false);
+    }
+  }
+}
+
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
diff --git a/src/theory/type_set.h b/src/theory/type_set.h
new file mode 100644
index 000000000..2d9be97be
--- /dev/null
+++ b/src/theory/type_set.h
@@ -0,0 +1,90 @@
+/*********************                                                        */
+/*! \file type_set.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Clark Barrett, Morgan Deters, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Type set class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__TYPE_SET_H
+#define __CVC4__THEORY__TYPE_SET_H
+
+#include <unordered_map>
+#include <unordered_set>
+
+#include "theory/type_enumerator.h"
+
+namespace CVC4 {
+namespace theory {
+
+/* Type set
+ *
+ * This class encapsulates a map from types to sets of nodes.
+ */
+class TypeSet
+{
+ public:
+  typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction>
+      TypeSetMap;
+  typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction>
+      TypeToTypeEnumMap;
+  typedef TypeSetMap::iterator iterator;
+  typedef TypeSetMap::const_iterator const_iterator;
+
+ public:
+  TypeSet() : d_tep(NULL) {}
+  ~TypeSet();
+  /** set the properties of the type set
+   *
+   * These indicate information such as finite bounds
+   * on the number of unique uninterpreted constants that can be
+   * enumerated by this class.
+   */
+  void setTypeEnumeratorProperties(TypeEnumeratorProperties* tep);
+  /** add node n to the set of values of t */
+  void add(TypeNode t, TNode n);
+  /** get the set of values of type t */
+  std::set<Node>* getSet(TypeNode t) const;
+  /** get the next enumerated term of type t
+   *
+   * useBaseType is whether
+   */
+  Node nextTypeEnum(TypeNode t, bool useBaseType = false);
+
+  bool empty() { return d_typeSet.empty(); }
+  iterator begin() { return d_typeSet.begin(); }
+  iterator end() { return d_typeSet.end(); }
+  static TypeNode getType(iterator it) { return (*it).first; }
+  static std::set<Node>& getSet(iterator it) { return *(*it).second; }
+ private:
+  /** sets of values for each type */
+  TypeSetMap d_typeSet;
+  /** type enumerators for each type */
+  TypeToTypeEnumMap d_teMap;
+  /** pointer the type enumerator properties for this class. */
+  TypeEnumeratorProperties* d_tep;
+
+  /* add all sub-terms of n to the sets of this class
+   *
+   * If topLevel is true, then we add strict subterms only.
+   *
+   * Note that recursive traversal here is over enumerated expressions
+   * (very low expression depth).
+   */
+  void addSubTerms(TNode n,
+                   std::unordered_set<TNode, TNodeHashFunction>& visited,
+                   bool topLevel = true);
+}; /* class TypeSet */
+
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__TYPE_SET_H */