6 files changed, 510 insertions, 292 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index e1f93158f..63b61995a 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -628,47 +628,70 @@ void TheoryArrays::computeCareGraph()
 
 void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){
   m->assertEqualityEngine( &d_equalityEngine );
-  //must determine proper representatives for all array equivalence classes
-  //first, we collect all select terms and array equivalence classes
-  std::map< Node, std::vector< Node > > selects;
-  std::vector< Node > arrays;
+
+  std::map<Node, std::vector<Node> > selects;
+  std::vector<Node> arrays;
+
+  // Go through all equivalence classes
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+  bool isArray, computeRep;
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);
-    if( eqc.getType().isArray() ){
-      arrays.push_back( eqc );
-    }
+    isArray = eqc.getType().isArray();
+    computeRep = false;
     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
     while( !eqc_i.isFinished() ){
       Node n = *eqc_i;
-      if( n.getKind()==kind::SELECT ){
-        selects[ n[0] ].push_back( n );
+      // If this EC is an array type and it contains something other than STORE nodes, we have to compute a representative explicitly
+      if (isArray && n.getKind() != kind::STORE) {
+        arrays.push_back(eqc);
+        computeRep = true;
+      }
+      // If this term is a select, record that the EC rep of its store parameter is being read from using this term
+      if (n.getKind()==kind::SELECT) {
+        selects[d_equalityEngine.getRepresentative(n[0])].push_back(n);
       }
       ++eqc_i;
     }
+    // If this is an array EC but it only contains STORE nodes, then the value of this EC is derived from the others -
+    // no need to do extra work to compute it
+    if (isArray && !computeRep) {
+      m->assertRepresentative(eqc);
+    }
     ++eqcs_i;
   }
-  //for all array equivalence classes
-  for( size_t i=0; i<arrays.size(); i++ ){
-    ArrayModel am( arrays[i], m );
-    //set all values from existing select terms
-    eq::EqClassIterator eqc_i = eq::EqClassIterator( arrays[i], &d_equalityEngine );
-    while( !eqc_i.isFinished() ){
-      for( int i=0; i<(int)selects[ *eqc_i ].size(); i++ ){
-        am.setValue( m, selects[ *eqc_i ][i][1], selects[ *eqc_i ][i] );
-      }
-      ++eqc_i;
+
+  NodeManager* nm = NodeManager::currentNM();
+  Node rep;
+  map<Node, Node> defValues;
+  map<Node, Node>::iterator it;
+  TypeSet defaultValuesSet;
+
+  // Loop through all array equivalence classes that need a representative computed
+  for (size_t i=0; i<arrays.size(); ++i) {
+    TNode n = arrays[i];
+
+    // Compute default value for this array - there is one default value for every mayEqual equivalence class
+    TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(n);
+    it = defValues.find(mayRep);
+    // If this mayEqual EC doesn't have a default value associated, get the next available default value for the associated array element type
+    if (it == defValues.end()) {
+      TypeNode valueType = n.getType().getArrayConstituentType();
+      rep = defaultValuesSet.nextTypeEnum(valueType);
+      defValues[mayRep] = rep;
+    }
+    else {
+      rep = (*it).second;
     }
-    if( fullModel ){
-      ////choose a representative as the default array
-      //am.setDefaultArray( ... );
+    // Build the STORE_ALL term with the default value
+    rep = nm->mkConst(ArrayStoreAll(n.getType().toType(), rep.toExpr()));
+    // For each read, require that the rep stores the right value
+    vector<Node>& reads = selects[n];
+    for (unsigned j = 0; j < reads.size(); ++j) {
+      rep = nm->mkNode(kind::STORE, rep, reads[j][1], reads[j]);
     }
-    //construct the representative
-    Node rep = am.getArrayValue();
-    Assert( !rep.isNull() );
-    m->assertEquality( arrays[i], rep, true );
-    //communicate to the model that it is the representative
-    m->assertRepresentative( rep );
+    m->assertEquality(n, rep, true);
+    m->assertRepresentative(rep);
   }
 }
 
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 96b5d6945..bd9e6aefa 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -29,13 +29,14 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 
 TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFuncModels ) :
-d_substitutions( c ), d_equalityEngine( c, name ), d_enableFuncModels( enableFuncModels ){
+  d_substitutions(c), d_equalityEngine(c, name), d_enableFuncModels(enableFuncModels)
+{
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
   d_equalityEngine.addFunctionKind(kind::SELECT);
-  d_equalityEngine.addFunctionKind(kind::STORE);
+  //  d_equalityEngine.addFunctionKind(kind::STORE);
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
   d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR);
   d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
@@ -76,74 +77,76 @@ Cardinality TheoryModel::getCardinality( Type t ){
   }
 }
 
-void TheoryModel::toStream( std::ostream& out ){
-  /*//for debugging
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-  while( !eqcs_i.isFinished() ){
-    Node eqc = (*eqcs_i);
-    Debug("get-model-debug") << eqc << " : " << eqc.getType() << " : " << std::endl;
-    out << "   ";
-    //add terms to model
-    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-    while( !eqc_i.isFinished() ){
-      out << (*eqc_i) << " ";
-      ++eqc_i;
-    }
-    out << std::endl;
-    ++eqcs_i;
-  }
-  */
+void TheoryModel::toStream( std::ostream& out )
+{
   out << this;
 }
 
-Node TheoryModel::getModelValue( TNode n ){
-  Trace("model") << "TheoryModel::getModelValue " << n << std::endl;
-
-  //// special case: prop engine handles boolean vars
-  //if(n.isVar() && n.getType().isBoolean()) {
-  //  Trace("model") << "-> Propositional variable." << std::endl;
-  //  return d_te->getPropEngine()->getValue( n );
-  //}
-
-  // special case: value of a constant == itself
+Node TheoryModel::getModelValue( TNode n )
+{
   if( n.isConst() ) {
-    Trace("model") << "-> Constant." << std::endl;
     return n;
   }
 
-  Node nn;
-  if( n.getNumChildren()>0 ){
-    std::vector< Node > children;
-    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-      Debug("model-debug") << "get operator: " << n.getOperator() << std::endl;
-      children.push_back( n.getOperator() );
+  TypeNode t = n.getType();
+  if (t.isFunction() || t.isPredicate()) {
+    if (d_enableFuncModels) {
+      if (d_uf_models.find(n) != d_uf_models.end()) {
+        // Existing function
+        return d_uf_models[n];
+      }
+      // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type
+      vector<TypeNode> argTypes = t.getArgTypes();
+      vector<Node> args;
+      NodeManager* nm = NodeManager::currentNM();
+      for (unsigned i = 0; i < argTypes.size(); ++i) {
+        args.push_back(nm->mkBoundVar(argTypes[i]));
+      }
+      Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args);
+      TypeEnumerator te(t.getRangeType());
+      return nm->mkNode(kind::LAMBDA, boundVarList, *te);
+    }
+    // TODO: if func models not enabled, throw an error?
+    Unreachable();
+  }
+
+  if (n.getNumChildren() > 0) {
+    std::vector<Node> children;
+    if (n.getKind() == APPLY_UF) {
+      Node op = n.getOperator();
+      if (d_uf_models.find(op) == d_uf_models.end()) {
+        // Unknown term - return first enumerated value for this type
+        TypeEnumerator te(n.getType());
+        return *te;
+      }
+      // Plug in uninterpreted function model
+      children.push_back(d_uf_models[op]);
+    }
+    else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+      children.push_back(n.getOperator());
     }
     //evaluate the children
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      Node val = getValue( n[i] );
-      Debug("model-debug") << i << " : " << n[i] << " -> " << val << std::endl;
-      Assert( !val.isNull() );
-      children.push_back( val );
-    }
-    Debug("model-debug") << "Done eval children" << std::endl;
-    nn = NodeManager::currentNM()->mkNode( n.getKind(), children );
-  }else{
-    nn = n;
+    for (unsigned i = 0; i < n.getNumChildren(); ++i) {
+      Node val = getValue(n[i]);
+      children.push_back(val);
+    }
+    Node val = Rewriter::rewrite(NodeManager::currentNM()->mkNode(n.getKind(), children));
+    Assert(val.isConst());
+    return val;
   }
-  //interpretation is the rewritten form
-  nn = Rewriter::rewrite( nn );
 
-  // special case: value of a constant == itself
-  if( nn.isConst() ) {
-    Trace("model") << "-> Theory-interpreted term." << std::endl;
-    return nn;
-  }else{
-    Trace("model") << "-> Model-interpreted term." << std::endl;
-    //otherwise, get the interpreted value in the model
-    return getInterpretedValue( nn );
+  if (!d_equalityEngine.hasTerm(n)) {
+    // Unknown term - return first enumerated value for this type
+    TypeEnumerator te(n.getType());
+    return *te;
   }
+  Node val = d_equalityEngine.getRepresentative(n);
+  Assert(d_reps.find(val) != d_reps.end());
+  val = d_reps[val];
+  return val;
 }
 
+
 Node TheoryModel::getInterpretedValue( TNode n ){
   Trace("model") << "Get interpreted value of " << n << std::endl;
   TypeNode type = n.getType();
@@ -166,7 +169,7 @@ Node TheoryModel::getInterpretedValue( TNode n ){
     }else{
       return n;
     }
-  }else{
+  } else{
     Trace("model-debug") << "check rep..." << std::endl;
     Node ret;
     //check if the representative is defined
@@ -232,31 +235,6 @@ Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){
 
 //FIXME: need to ensure that theory enumerators exist for each sort
 Node TheoryModel::getNewDomainValue( TypeNode tn ){
-#if 0
-  if( tn==NodeManager::currentNM()->booleanType() ){
-    if( d_rep_set.d_type_reps[tn].empty() ){
-      return d_false;
-    }else if( d_rep_set.d_type_reps[tn].size()==1 ){
-      return NodeManager::currentNM()->mkConst( areEqual( d_rep_set.d_type_reps[tn][0], d_false ) );
-    }else{
-      return Node::null();
-    }
-  }else if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
-    int val = 0;
-    do{
-      Node r = NodeManager::currentNM()->mkConst( Rational(val) );
-      if( std::find( d_rep_set.d_type_reps[tn].begin(), d_rep_set.d_type_reps[tn].end(), r )==d_rep_set.d_type_reps[tn].end() &&
-          !d_equalityEngine.hasTerm( r ) ){
-        return r;
-      }
-      val++;
-    }while( true );
-  }else{
-    //otherwise must make a variable  FIXME: how to make constants for other sorts?
-    //return NodeManager::currentNM()->mkSkolem( tn );
-    return Node::null();
-  }
-#else
   if( tn.isSort() ){
     return Node::null();
   }else{
@@ -282,7 +260,6 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){
     }
     return Node::null();
   }
-#endif
 }
 
 /** add substitution */
@@ -298,7 +275,7 @@ void TheoryModel::addTerm( Node n ){
     d_equalityEngine.addTerm( n );
   }
   //must collect UF terms
-  if( d_enableFuncModels && n.getKind()==APPLY_UF ){
+  if (n.getKind()==APPLY_UF) {
     Node op = n.getOperator();
     if( std::find( d_uf_terms[ op ].begin(), d_uf_terms[ op ].end(), n )==d_uf_terms[ op ].end() ){
       d_uf_terms[ op ].push_back( n );
@@ -420,119 +397,292 @@ TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( t
 
 }
 
-void TheoryEngineModelBuilder::buildModel( Model* m, bool fullModel ){
+void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
+{
   TheoryModel* tm = (TheoryModel*)m;
-  //reset representative information
+
+  // Reset model
   tm->reset();
-  //collect model info from the theory engine
+
+  // Collect model info from the theories
   Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl;
-  d_te->collectModelInfo( tm, fullModel );
+  d_te->collectModelInfo(tm, fullModel);
+
   Trace("model-builder") << "Collect representatives..." << std::endl;
-  //store asserted representative map
-  std::map< Node, Node > assertedReps;
-  //process all terms in the equality engine, store representatives
+  // Process all terms in the equality engine, store representatives for each EC
+  std::map< Node, Node > assertedReps, constantReps;
+  TypeSet typeConstSet, typeRepSet, typeNoRepSet;
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &tm->d_equalityEngine );
-  while( !eqcs_i.isFinished() ){
+  for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
+
+    // eqc is the equivalence class representative
     Node eqc = (*eqcs_i);
-    if( assertedReps.find( eqc )!=assertedReps.end() ){
-      Trace("model-warn") << "Duplicate equivalence class!!!! " << eqc << std::endl;
-    }else{
-      TypeNode eqct = eqc.getType();
-      Node const_rep;
-      eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &tm->d_equalityEngine );
-      while( !eqc_i.isFinished() ){
-        Node n = *eqc_i;
-        //if this node was specified as a representative
-        if( tm->d_reps.find( n )!=tm->d_reps.end() ){
-          Assert( !tm->d_reps[n].isNull() );
-          //if not already specified
-          if( assertedReps.find( eqc )==assertedReps.end() ){
-            Trace("model-builder") << "Rep( " << eqc << " ) = " << tm->d_reps[n] << std::endl;
-            assertedReps[ eqc ] = tm->d_reps[n];
-          }else{
-            if( n!=assertedReps[eqc] ){   //FIXME : this should be an assertion (EqClassIterator should not give duplicates)
-              //duplicate representative specified
-              Trace("model-warn") << "Duplicate representative specified for equivalence class " << eqc << ": " << std::endl;
-              Trace("model-warn") << "      " << assertedReps[eqc] << ", " << n << std::endl;
-              Trace("model-warn") << "  Type : " << n.getType() << std::endl;
-            }
+    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(constantReps.find(eqc) == 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()){
+        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
+      Assert(rep.isNull() || rep == const_rep);
+      constantReps[eqc] = const_rep;
+      typeConstSet.add(eqct, const_rep);
+    }
+    else if (!rep.isNull()) {
+      assertedReps[eqc] = rep;
+      typeRepSet.add(eqct, eqc);
+    }
+    else {
+      typeNoRepSet.add(eqct, eqc);
+    }
+  }
+
+  // Need to ensure that each EC has a constant representative.
+
+  // Phase 1: For types that do not have asserted reps, assign the unassigned EC's using either evaluation or type enumeration
+  Trace("model-builder") << "Starting phase 1..." << std::endl;
+  TypeSet::iterator it;
+  for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
+    TypeNode t = TypeSet::getType(it);
+    Trace("model-builder") << "  Working on type: " << t << endl;
+    set<Node>& noRepSet = TypeSet::getSet(it);
+    Assert(!noRepSet.empty());
+
+    set<Node>::iterator i, i2;
+    bool changed;
+
+    // Find value for this EC using evaluation if possible
+    do {
+      changed = false;
+      d_normalizedCache.clear();
+      for (i = noRepSet.begin(); i != noRepSet.end(); ) {
+        i2 = i;
+        ++i;
+        eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine);
+        for ( ; !eqc_i.isFinished(); ++eqc_i) {
+          Node n = *eqc_i;
+          Node normalized = normalize(tm, n, constantReps);
+          if (normalized.isConst()) {
+            typeConstSet.add(t, normalized);
+            constantReps[*i2] = normalized;
+            Trace("model-builder") << "  Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl;
+            changed = true;
+            noRepSet.erase(i2);
+            break;
           }
-        }else if( n.isConst() ){
-          //if this is constant, we will use it as representative (if none other specified)
-          const_rep = n;
         }
-        //model-specific processing of the term
-        tm->addTerm( n );
-        ++eqc_i;
       }
-      //if a representative was not specified
-      if( assertedReps.find( eqc )==assertedReps.end() ){
-        if( !const_rep.isNull() ){
-          //use the constant representative
-          assertedReps[ eqc ] = const_rep;
-        }else{
-          if( fullModel ){
-            Trace("model-warn") << "No representative specified for equivalence class " << eqc << std::endl;
-            Trace("model-warn") << "  Type : " << eqc.getType() << std::endl;
-            //TODO: select proper representative
-            //Unimplemented("No representative specified for equivalence class");
+    } while (changed);
+
+    // Skip next step if nothing to do or if fullModel is false (meaning we shouldn't choose any representatives that aren't forced)
+    if (noRepSet.empty() || !fullModel) {
+      continue;
+    }
+
+    // This assertion may be too strong, but hopefully not: we expect that for every type, either all of its EC's have asserted reps (or constants)
+    // or none of its EC's have asserted reps.
+    Assert(typeRepSet.getSet(t) == NULL);
+
+    Node n;
+    for (i = noRepSet.begin(); i != noRepSet.end(); ++i) {
+      n = typeConstSet.nextTypeEnum(t);
+      constantReps[*i] = n;
+      Trace("model-builder") << "  New Const: Setting constant rep of " << (*i) << " to " << n << endl;
+    }
+  }
+
+  // Phase 2: Substitute into asserted reps using constReps.
+  // Iterate until a fixed point is reached.
+  Trace("model-builder") << "Starting phase 2..." << std::endl;
+  bool changed;
+  do {
+    changed = false;
+    d_normalizedCache.clear();
+    for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) {
+      set<Node>& repSet = TypeSet::getSet(it);
+      set<Node>::iterator i;
+      for (i = repSet.begin(); i != repSet.end(); ) {
+        Assert(assertedReps.find(*i) != assertedReps.end());
+        Node rep = assertedReps[*i];
+        Node normalized = normalize(tm, rep, constantReps);
+        Trace("model-builder") << "  Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl;
+        if (normalized.isConst()) {
+          changed = true;
+          constantReps[*i] = normalized;
+          assertedReps.erase(*i);
+          set<Node>::iterator i2 = i;
+          ++i;
+          repSet.erase(i2);
+        }
+        else {
+          if (normalized != rep) {
+            assertedReps[*i] = normalized;
+            changed = true;
           }
-          //assertedReps[ eqc ] = chooseRepresentative( tm, eqc, fullModel );
-          assertedReps[ eqc ] = eqc;
+          ++i;
         }
       }
     }
-    ++eqcs_i;
-  }
-  Trace("model-builder") << "Normalize representatives..." << std::endl;
-  //now, normalize all representatives
-  // this will make every leaf of asserted representatives into a representative
-  std::map< Node, bool > normalized;
-  for( std::map< Node, Node >::iterator it = assertedReps.begin(); it != assertedReps.end(); ++it ){
-    std::map< Node, bool > normalizing;
-    normalizeRepresentative( tm, it->first, assertedReps, normalized, normalizing );
+  } while (changed);
+
+  if (fullModel) {
+    // Assert that all representatives have been converted to constants
+    for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) {
+      set<Node>& repSet = TypeSet::getSet(it);
+      Assert(repSet.empty());
+    }
   }
+
   Trace("model-builder") << "Copy representatives to model..." << std::endl;
-  //assertedReps has the actual representatives we will use, now copy to model
   tm->d_reps.clear();
-  for( std::map< Node, Node >::iterator it = assertedReps.begin(); it != assertedReps.end(); ++it ){
-    tm->d_reps[ it->first ] = it->second;
-    tm->d_rep_set.add( it->second );
+  std::map< Node, Node >::iterator itMap;
+  for (itMap = constantReps.begin(); itMap != constantReps.end(); ++itMap) {
+    tm->d_reps[itMap->first] = itMap->second;
+    tm->d_rep_set.add(itMap->second);
+  }
+
+  if (!fullModel) {
+    // 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);
+    }
+    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);
+      }
+    }
   }
 
   //modelBuilder-specific initialization
   processBuildModel( tm, fullModel );
+
+  if (fullModel) {
+    // 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);
+      Assert(constantReps.find(eqc) != constantReps.end());
+      Node rep = constantReps[eqc];
+      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &tm->d_equalityEngine);
+      for ( ; !eqc_i.isFinished(); ++eqc_i) {
+        Node n = *eqc_i;
+        Assert(tm->getValue(*eqc_i) == rep);
+      }
+    }
+  }
+}
+
+
+Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node, Node >& constantReps)
+{
+  std::map<Node, Node>::iterator itMap = constantReps.find(r);
+  if (itMap != constantReps.end()) {
+    return (*itMap).second;
+  }
+  NodeMap::iterator it = d_normalizedCache.find(r);
+  if (it != d_normalizedCache.end()) {
+    return (*it).second;
+  }
+  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];
+      if (!ri.isConst()) {
+        if (m->d_equalityEngine.hasTerm(ri)) {
+          ri = m->d_equalityEngine.getRepresentative(ri);
+        }
+        ri = normalize(m, ri, constantReps);
+        if (!ri.isConst()) {
+          childrenConst = false;
+        }
+      }
+      children.push_back(ri);
+    }
+    retNode = NodeManager::currentNM()->mkNode( r.getKind(), children );
+    if (childrenConst) {
+      retNode = Rewriter::rewrite(retNode);
+    }
+  }
+  d_normalizedCache[r] = retNode;
+  return retNode;
 }
 
-void TheoryEngineModelBuilder::processBuildModel( TheoryModel* m, bool fullModel ){
-  if( fullModel ){
+
+void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel)
+{
+  if (fullModel) {
+    Trace("model-builder") << "Assigning function values..." << endl;
     //construct function values
     for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){
-      Trace("model-func") << "Creating function value..." << it->first << std::endl;
       Node n = it->first;
       if( m->d_uf_models.find( n )==m->d_uf_models.end() ){
         TypeNode type = n.getType();
         uf::UfModelTree ufmt( n );
-        Node default_v;
+        Node default_v, un, simp, v;
         for( size_t i=0; i<it->second.size(); i++ ){
-          Node un = it->second[i];
-          Node v = m->getRepresentative( un );
-          ufmt.setValue( m, un, v );
+          un = it->second[i];
+          vector<TNode> children;
+          children.push_back(n);
+          for (size_t j = 0; j < un.getNumChildren(); ++j) {
+            children.push_back(m->getRepresentative(un[j]));
+          }
+          simp = NodeManager::currentNM()->mkNode(un.getKind(), children);
+          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
-          default_v = m->getInterpretedValue( NodeManager::currentNM()->mkSkolem( "defaultValueQueryVar_$$", type.getRangeType(),
-                                              "a placeholder variable to query for a default value in model construction" ) );
+          TypeEnumerator te(type.getRangeType());
+          default_v = (*te);
         }
         ufmt.setDefaultValue( m, default_v );
         ufmt.simplify();
-        m->d_uf_models[n] = ufmt.getFunctionValue( "$x" );
+        Node val = ufmt.getFunctionValue( "$x" );
+        Trace("model-builder") << "  Assigning (" << n << ") to (" << val << ")" << endl;
+        m->d_uf_models[n] = val;
+        //ufmt.debugPrint( std::cout, m );
       }
     }
   }
 }
 
+
 Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ){
   //try to get a new domain value
   Node rep = m->getNewDomainValue( eqc.getType() );
@@ -544,71 +694,3 @@ Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* m, Node eqc, b
     return eqc;
   }
 }
-
-Node TheoryEngineModelBuilder::normalizeRepresentative( TheoryModel* m, Node r, std::map< Node, Node >& reps,
-                                                        std::map< Node, bool >& normalized,
-                                                        std::map< Node, bool >& normalizing ){
-  Trace("temb-normalize") << r << std::endl;
-  if( normalized.find( r )!=normalized.end() ){
-    Trace("temb-normalize") << " -> already normalized, return " << reps[r] << std::endl;
-    return reps[r];
-  }else if( normalizing.find( r )!=normalizing.end() && normalizing[r] ){
-    //this case is to handle things like when store( A, e, i ) is given
-    //       as a representative for array A.
-    Trace("temb-normalize") << " -> currently normalizing, give up : " << r << std::endl;
-    return r;
-  }else if( reps.find( r )!=reps.end() ){
-    normalizing[ r ] = true;
-    Node retNode = normalizeNode( m, reps[r], reps, normalized, normalizing );
-    normalizing[ r ] = false;
-    normalized[ r ] = true;
-    reps[ r ] = retNode;
-    Trace("temb-normalize") << " --> returned " << retNode << " for " << r << std::endl;
-    return retNode;
-  }else if( m->d_equalityEngine.hasTerm( r ) ){
-    normalizing[ r ] = true;
-    //return the normalized representative from the model
-    r = m->d_equalityEngine.getRepresentative( r );
-    Trace("temb-normalize") << " -> it is the representative " << r << std::endl;
-    Node retNode = normalizeRepresentative( m, r, reps, normalized, normalizing );
-    normalizing[ r ] = false;
-    return retNode;
-  }else{
-    if( !r.isConst() ){
-      Trace("model-warn") << "Normalizing representative, unknown term: " << r << std::endl;
-      Trace("model-warn") << "  Type : " << r.getType() << std::endl;
-      Trace("model-warn") << "  Kind : " << r.getKind() << std::endl;
-      normalizing[ r ] = true;
-      r = normalizeNode( m, r, reps, normalized, normalizing );
-      normalizing[ r ] = false;
-    }
-    Trace("temb-normalize") << " -> unknown, return " << r << std::endl;
-    return r;
-  }
-}
-
-Node TheoryEngineModelBuilder::normalizeNode( TheoryModel* m, Node r, std::map< Node, Node >& reps,
-                                              std::map< Node, bool >& normalized,
-                                              std::map< Node, bool >& normalizing ){
-  if( r.getNumChildren()>0 ){
-    Trace("temb-normalize") << " ---> normalize " << r << " " << r.getNumChildren() << " " << r.getKind() << std::endl;
-    //non-leaf case: construct representative from children
-    std::vector< Node > children;
-    if( r.getMetaKind() == kind::metakind::PARAMETERIZED ){
-      children.push_back( r.getOperator() );
-    }
-    for( size_t i=0; i<r.getNumChildren(); i++ ){
-      Node ri = normalizeRepresentative( m, r[i], reps, normalized, normalizing );
-      children.push_back( ri );
-    }
-    Node retNode = NodeManager::currentNM()->mkNode( r.getKind(), children );
-    retNode = Rewriter::rewrite( retNode );
-    //if( retNode!=r ){
-      //assure that it is made equal in the model
-      //m->assertEquality( r, retNode, true );
-    //}
-    return retNode;
-  }else{
-    return r;
-  }
-}
diff --git a/src/theory/model.h b/src/theory/model.h
index de4d57d2e..90cd1e35a 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -23,13 +23,11 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/rep_set.h"
 #include "theory/substitutions.h"
+#include "theory/type_enumerator.h"
 
 namespace CVC4 {
 namespace theory {
 
-class QuantifiersEngine;
-class TheoryEngineModelBuilder;
-
 /** Theory Model class
  *    For Model m, should call m.initialize() before using
  */
@@ -133,6 +131,112 @@ public:
   std::map< Node, Node > d_uf_models;
 };
 
+/*
+ * Class that encapsulates a map from types to sets of nodes
+ */
+class TypeSet {
+public:
+  typedef std::hash_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
+  typedef std::hash_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
+  typedef TypeSetMap::iterator iterator;
+private:
+  TypeSetMap d_typeSet;
+  TypeToTypeEnumMap d_teMap;
+
+  public:
+  ~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 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)
+  {
+    iterator it = d_typeSet.find(t);
+    if (it == d_typeSet.end()) {
+      return NULL;
+    }
+    return (*it).second;
+  }
+
+  Node nextTypeEnum(TypeNode t)
+  {
+    TypeEnumerator* te;
+    TypeToTypeEnumMap::iterator it = d_teMap.find(t);
+    if (it == d_teMap.end()) {
+      te = new TypeEnumerator(t);
+      d_teMap[t] = te;
+    }
+    else {
+      te = (*it).second;
+    }
+    Assert(!te->isFinished());
+
+    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()) {
+      Assert(!te->isFinished());
+      ++(*te);
+      n = **te;
+    }
+    s->insert(n);
+    ++(*te);
+    return n;
+  }
+
+  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;
+  }
+
+};    
+
 /** TheoryEngineModelBuilder class
   *    This model builder will consult all theories in a theory engine for
   *    collectModelInfo( ... ) when building a model.
@@ -142,24 +246,22 @@ class TheoryEngineModelBuilder : public ModelBuilder
 protected:
   /** pointer to theory engine */
   TheoryEngine* d_te;
+  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  NodeMap d_normalizedCache;
+
   /** process build model */
-  virtual void processBuildModel( TheoryModel* m, bool fullModel );
+  virtual void processBuildModel(TheoryModel* m, bool fullModel);
   /** choose representative for unconstrained equivalence class */
-  virtual Node chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel );
+  virtual Node chooseRepresentative(TheoryModel* m, Node eqc, bool fullModel);
   /** normalize representative */
-  Node normalizeRepresentative( TheoryModel* m, Node r, std::map< Node, Node >& reps,
-                                std::map< Node, bool >& normalized,
-                                std::map< Node, bool >& normalizing );
-  Node normalizeNode( TheoryModel* m, Node r, std::map< Node, Node >& reps,
-                      std::map< Node, bool >& normalized,
-                      std::map< Node, bool >& normalizing );
+  Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps);
 public:
-  TheoryEngineModelBuilder( TheoryEngine* te );
+  TheoryEngineModelBuilder(TheoryEngine* te);
   virtual ~TheoryEngineModelBuilder(){}
   /** Build model function.
    *    Should be called only on TheoryModels m
    */
-  void buildModel( Model* m, bool fullModel );
+  void buildModel(Model* m, bool fullModel);
 };
 
 }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0db71aba4..61b66ba3e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -590,6 +590,17 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
       d_theoryTable[theoryId]->collectModelInfo( m, fullModel );
     }
   }
+  // Get the Boolean variables
+  vector<TNode> boolVars;
+  d_propEngine->getBooleanVariables(boolVars);
+  vector<TNode>::iterator it, iend = boolVars.end();
+  bool hasValue, value;
+  for (it = boolVars.begin(); it != iend; ++it) {
+    TNode var = *it;
+    hasValue = d_propEngine->hasValue(var, value);
+    // TODO: Assert that hasValue is true?
+    m->assertPredicate(var, hasValue ? value : false);
+  }
 }
 
 /* get model */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 67c1aa9f6..ba7890b80 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -194,27 +194,27 @@ Node TheoryUF::explain(TNode literal) {
 
 void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){
   m->assertEqualityEngine( &d_equalityEngine );
-  if( fullModel ){
-    std::map< TypeNode, TypeEnumerator* > type_enums;
-    //must choose proper representatives
-    // for each equivalence class, specify fresh constant as representative
-    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-    while( !eqcs_i.isFinished() ){
-      Node eqc = (*eqcs_i);
-      TypeNode tn = eqc.getType();
-      if( tn.isSort() ){
-        if( type_enums.find( tn )==type_enums.end() ){
-          type_enums[tn] = new TypeEnumerator( tn );
-        }
-        Node rep = *(*type_enums[tn]);
-        ++(*type_enums[tn]);
-        //specify the constant as the representative
-        m->assertEquality( eqc, rep, true );
-        m->assertRepresentative( rep );
-      }
-      ++eqcs_i;
-    }
-  }
+  // if( fullModel ){
+  //   std::map< TypeNode, TypeEnumerator* > type_enums;
+  //   //must choose proper representatives
+  //   // for each equivalence class, specify fresh constant as representative
+  //   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+  //   while( !eqcs_i.isFinished() ){
+  //     Node eqc = (*eqcs_i);
+  //     TypeNode tn = eqc.getType();
+  //     if( tn.isSort() ){
+  //       if( type_enums.find( tn )==type_enums.end() ){
+  //         type_enums[tn] = new TypeEnumerator( tn );
+  //       }
+  //       Node rep = *(*type_enums[tn]);
+  //       ++(*type_enums[tn]);
+  //       //specify the constant as the representative
+  //       m->assertEquality( eqc, rep, true );
+  //       m->assertRepresentative( rep );
+  //     }
+  //     ++eqcs_i;
+  //   }
+  // }
 }
 
 void TheoryUF::presolve() {
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 424b2c117..5df9868f3 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -142,18 +142,18 @@ Node UfModelTreeNode::getFunctionValue( std::vector< Node >& args, int index, No
     if( d_data.find( Node::null() )!=d_data.end() ){
       defaultValue = d_data[Node::null()].getFunctionValue( args, index+1, argDefaultValue );
     }
-    std::vector< Node > caseValues;
-    std::map< Node, Node > caseArg;
+    std::vector< Node > caseArgs;
+    std::map< Node, Node > caseValues;
     for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
       if( !it->first.isNull() ){
         Node val = it->second.getFunctionValue( args, index+1, defaultValue );
-        caseValues.push_back( val );
-        caseArg[ val ] = it->first;
+        caseArgs.push_back( it->first );
+        caseValues[ it->first ] = val;
       }
     }
     Node retNode = defaultValue;
-    for( int i=((int)caseValues.size()-1); i>=0; i-- ){
-      retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( caseArg[ caseValues[i] ] ), caseValues[i], retNode );
+    for( int i=((int)caseArgs.size()-1); i>=0; i-- ){
+      retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( caseArgs[ i ] ), caseValues[ caseArgs[ i ] ], retNode );
     }
     return retNode;
   }else{