Refactor theory model (#1236)

* Refactor theory model, working on making RepSet references const.

* Encapsulation of members of rep set.

* More documentation on rep set.

* Swap names

* Reference issues.

* Minor

* Minor

* New clang format.

15 files changed, 396 insertions, 184 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 936a7261e..cbfad67b5 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1004,33 +1004,54 @@ void CvcPrinter::toStream(std::ostream& out, const Model& m, const Command* c) c
   const theory::TheoryModel& tm = (const theory::TheoryModel&) m;
   if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
-    if( options::modelUninterpDtEnum() && tn.isSort() &&
-        tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
-      out << "DATATYPE" << std::endl;
-      out << "  " << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " = ";
-      for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
-        if (i>0) {
-          out << "| ";
+    if (options::modelUninterpDtEnum() && tn.isSort())
+    {
+      const theory::RepSet* rs = tm.getRepSet();
+      if (rs->d_type_reps.find(tn) != rs->d_type_reps.end())
+      {
+        out << "DATATYPE" << std::endl;
+        out << "  " << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol()
+            << " = ";
+        for (size_t i = 0; i < (*rs->d_type_reps.find(tn)).second.size(); i++)
+        {
+          if (i > 0)
+          {
+            out << "| ";
+          }
+          out << (*rs->d_type_reps.find(tn)).second[i] << " ";
         }
-        out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " ";
+        out << std::endl << "END;" << std::endl;
       }
-      out << std::endl << "END;" << std::endl;
-    } else {
-      if( tn.isSort() ){
-        // print the cardinality
-        if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
-          out << "% cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
+      else
+      {
+        if (tn.isSort())
+        {
+          // print the cardinality
+          if (rs->d_type_reps.find(tn) != rs->d_type_reps.end())
+          {
+            out << "% cardinality of " << tn << " is "
+                << (*rs->d_type_reps.find(tn)).second.size() << std::endl;
+          }
         }
-      }
-      out << c << std::endl;
-      if( tn.isSort() ){
-        // print the representatives
-        if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
-          for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
-            if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
-              out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " : " << tn << ";" << std::endl;
-            }else{
-              out << "% rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
+        out << c << std::endl;
+        if (tn.isSort())
+        {
+          // print the representatives
+          if (rs->d_type_reps.find(tn) != rs->d_type_reps.end())
+          {
+            for (size_t i = 0; i < (*rs->d_type_reps.find(tn)).second.size();
+                 i++)
+            {
+              if ((*rs->d_type_reps.find(tn)).second[i].isVar())
+              {
+                out << (*rs->d_type_reps.find(tn)).second[i] << " : " << tn
+                    << ";" << std::endl;
+              }
+              else
+              {
+                out << "% rep: " << (*rs->d_type_reps.find(tn)).second[i]
+                    << std::endl;
+              }
             }
           }
         }
@@ -1056,9 +1077,11 @@ void CvcPrinter::toStream(std::ostream& out, const Model& m, const Command* c) c
     }
     Node val = Node::fromExpr(tm.getSmtEngine()->getValue(n.toExpr()));
     if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) {
+      const theory::RepSet* rs = tm.getRepSet();
       TypeNode tn = val[1].getType();
-      if (tn.isSort() && tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
-        Cardinality indexCard((*tm.d_rep_set.d_type_reps.find(tn)).second.size());
+      if (tn.isSort() && rs->d_type_reps.find(tn) != rs->d_type_reps.end())
+      {
+        Cardinality indexCard((*rs->d_type_reps.find(tn)).second.size());
         val = theory::arrays::TheoryArraysRewriter::normalizeConstant( val, indexCard );
       }
     }
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 9c9d1fb76..f292c0a2e 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1187,7 +1187,8 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
   const theory::TheoryModel& tm = (const theory::TheoryModel&) m;
   if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
-    const std::map< TypeNode, std::vector< Node > >& type_reps = tm.d_rep_set.d_type_reps;
+    const theory::RepSet* rs = tm.getRepSet();
+    const std::map<TypeNode, std::vector<Node> >& type_reps = rs->d_type_reps;
 
     std::map< TypeNode, std::vector< Node > >::const_iterator tn_iterator = type_reps.find( tn );
     if( options::modelUninterpDtEnum() && tn.isSort() && tn_iterator != type_reps.end() ){
@@ -1241,8 +1242,10 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
     } else {
       if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) {
         TypeNode tn = val[1].getType();
-        if (tn.isSort() && tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
-          Cardinality indexCard((*tm.d_rep_set.d_type_reps.find(tn)).second.size());
+        const theory::RepSet* rs = tm.getRepSet();
+        if (tn.isSort() && rs->d_type_reps.find(tn) != rs->d_type_reps.end())
+        {
+          Cardinality indexCard((*rs->d_type_reps.find(tn)).second.size());
           val = theory::arrays::TheoryArraysRewriter::normalizeConstant( val, indexCard );
         }
       }
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index d1a3a1bec..29bbc6a2c 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -66,7 +66,10 @@ void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps
     //construct children
     for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){
       Trace("abs-model-debug") << "Construct " << it->first << " : " << fapp_child_index[it->first] << " : ";
-      debugPrintUInt( "abs-model-debug", m->d_rep_set.d_type_reps[tn].size(), fapp_child_index[it->first] );
+      const RepSet* rs = m->getRepSet();
+      debugPrintUInt("abs-model-debug",
+                     rs->getNumRepresentatives(tn),
+                     fapp_child_index[it->first]);
       Trace("abs-model-debug") << " : " << it->second.size() << " terms." << std::endl;
       d_def[fapp_child_index[it->first]].construct_func( m, it->second, depth+1 );
     }
@@ -134,7 +137,8 @@ void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsign
       Trace(c) << "V[" << d_value << "]" << std::endl;
     }else{
       TypeNode tn = f[depth].getType();
-      unsigned dSize = m->d_rep_set.getNumRepresentatives( tn );
+      const RepSet* rs = m->getRepSet();
+      unsigned dSize = rs->getNumRepresentatives(tn);
       Assert( dSize<32 );
       for( std::map< unsigned, AbsDef >::const_iterator it = d_def.begin(); it != d_def.end(); ++it ){
         for( unsigned i=0; i<depth; i++ ){ Trace(c) << "  ";}
@@ -179,9 +183,10 @@ bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe,
             success = false;
             index = getId( it->first, index );
             if( index<32 ){
-              Assert( index<m->d_rep_set.d_type_reps[tn].size() );
-              terms[m->d_var_order[q][depth]] = m->d_rep_set.d_type_reps[tn][index];
-              //terms[depth] = m->d_rep_set.d_type_reps[tn][index];
+              const RepSet* rs = m->getRepSet();
+              Assert(index < rs->getNumRepresentatives(tn));
+              terms[m->d_var_order[q][depth]] =
+                  rs->getRepresentative(tn, index);
               if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){
                 //if we are incomplete, and have not yet added an instantiation, keep trying
                 index++;
@@ -279,8 +284,10 @@ void AbsDef::apply_ucompose( FirstOrderModelAbs * m, TNode q,
   if( depth==terms.size() ){
     if( Trace.isOn("ambqi-check-debug2") ){
       Trace("ambqi-check-debug2") << "Add entry ( ";
+      const RepSet* rs = m->getRepSet();
       for( unsigned i=0; i<entry.size(); i++ ){
-        unsigned dSize = m->d_rep_set.d_type_reps[m->getVariable( q, i ).getType()].size();
+        unsigned dSize =
+            rs->getNumRepresentatives(m->getVariable(q, i).getType());
         debugPrintUInt( "ambqi-check-debug2", dSize, entry[i] );
         Trace("ambqi-check-debug2") << " ";
       }
@@ -332,7 +339,7 @@ void AbsDef::construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, uns
     }else{
       Assert( currv==val_none );
       if( curr==val_none ){
-        unsigned numReps = m->d_rep_set.getNumRepresentatives( tn );
+        unsigned numReps = m->getRepSet()->getNumRepresentatives(tn);
         Assert( numReps < 32 );
         for( unsigned i=0; i<numReps; i++ ){
           curr = 1 << i;
@@ -356,7 +363,7 @@ void AbsDef::construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int cur
   }else{
     TypeNode tn = m->getVariable( q, depth ).getType();
     if( v==depth ){
-      unsigned numReps = m->d_rep_set.d_type_reps[tn].size();
+      unsigned numReps = m->getRepSet()->getNumRepresentatives(tn);
       Assert( numReps>0 && numReps < 32 );
       for( unsigned i=0; i<numReps; i++ ){
         d_def[ 1 << i ].construct_var( m, q, v, i, depth+1 );
@@ -374,6 +381,7 @@ void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef
                                 std::map< unsigned, AbsDef * >& children,
                                 std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,
                                 std::vector< unsigned >& entry, std::vector< bool >& entry_def ) {
+  const RepSet* rs = m->getRepSet();
   if( n.getKind()==OR || n.getKind()==AND ){
     // short circuiting
     for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
@@ -419,11 +427,18 @@ void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef
       for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
         Trace("ambqi-check-debug2") << "composite : " << it->first << " : " << it->second->d_value;
         if( it->second->d_value>=0 ){
-          if( it->second->d_value>=(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() ){
-            std::cout << it->second->d_value << " " << n[it->first] << " " << n[it->first].getType() << " " << m->d_rep_set.d_type_reps[n[it->first].getType()].size() << std::endl;
+          if (it->second->d_value
+              >= (int)rs->getNumRepresentatives(n[it->first].getType()))
+          {
+            std::cout << it->second->d_value << " " << n[it->first] << " "
+                      << n[it->first].getType() << " "
+                      << rs->getNumRepresentatives(n[it->first].getType())
+                      << std::endl;
           }
-          Assert( it->second->d_value<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() );
-          values[it->first] = m->d_rep_set.d_type_reps[n[it->first].getType()][it->second->d_value];
+          Assert(it->second->d_value
+                 < (int)rs->getNumRepresentatives(n[it->first].getType()));
+          values[it->first] = rs->getRepresentative(n[it->first].getType(),
+                                                    it->second->d_value);
         }else{
           incomplete = true;
         }
@@ -432,8 +447,10 @@ void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef
       for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){
         Trace("ambqi-check-debug2") << "   basic :  " << it->first << " : " << it->second;
         if( it->second>=0 ){
-          Assert( it->second<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() );
-          values[it->first] = m->d_rep_set.d_type_reps[n[it->first].getType()][it->second];
+          Assert(it->second
+                 < (int)rs->getNumRepresentatives(n[it->first].getType()));
+          values[it->first] =
+              rs->getRepresentative(n[it->first].getType(), it->second);
         }else{
           incomplete = true;
         }
@@ -492,7 +509,9 @@ void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef
           if( Trace.isOn("ambqi-check-debug2") ){
             for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
             Trace("ambqi-check-debug2") << "...process : ";
-            debugPrintUInt("ambqi-check-debug2", m->d_rep_set.d_type_reps[tn].size(), itd->first );
+            debugPrintUInt("ambqi-check-debug2",
+                           rs->getNumRepresentatives(tn),
+                           itd->first);
             Trace("ambqi-check-debug2") << " " << children.size() << " " << cchildren.size() << std::endl;
           }
           entry.push_back( itd->first );
@@ -522,7 +541,8 @@ void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef
       if( Trace.isOn("ambqi-check-debug2") ){
         for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
         Trace("ambqi-check-debug2") << "...process default : ";
-        debugPrintUInt("ambqi-check-debug2", m->d_rep_set.getNumRepresentatives( tn ), def );
+        debugPrintUInt(
+            "ambqi-check-debug2", rs->getNumRepresentatives(tn), def);
         Trace("ambqi-check-debug2") << " " << children.size() << " " << cdchildren.size() << std::endl;
       }
       entry.push_back( def );
@@ -620,17 +640,18 @@ void AbsDef::negate() {
 }
 
 Node AbsDef::getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth ) {
+  const RepSet* rs = m->getRepSet();
   if( depth==vars.size() ){
     TypeNode tn = op.getType();
     if( tn.getNumChildren()>0 ){
       tn = tn[tn.getNumChildren() - 1];
     }
     if( d_value>=0 ){
-      Assert( d_value<(int)m->d_rep_set.d_type_reps[tn].size() );
+      Assert(d_value < (int)rs->getNumRepresentatives(tn));
       if( tn.isBoolean() ){
         return NodeManager::currentNM()->mkConst( d_value==1 );
       }else{
-        return m->d_rep_set.d_type_reps[tn][d_value];
+        return rs->getRepresentative(tn, d_value);
       }
     }else{
       return Node::null();
@@ -642,8 +663,8 @@ Node AbsDef::getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< No
     for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
       if( it->first!=d_default ){
         unsigned id = getId( it->first );
-        Assert( id<m->d_rep_set.d_type_reps[tn].size() );
-        TNode n = m->d_rep_set.d_type_reps[tn][id];
+        Assert(id < rs->getNumRepresentatives(tn));
+        TNode n = rs->getRepresentative(tn, id);
         Node fv = it->second.getFunctionValue( m, op, vars, depth+1 );
         if( !curr.isNull() && !fv.isNull() ){
           curr = NodeManager::currentNM()->mkNode( ITE, vars[depth].eqNode( n ), fv, curr );
@@ -685,8 +706,9 @@ Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< uns
     if( d_value==val_unk ){
       return Node::null();
     }else{
-      Assert( d_value>=0 && d_value<(int)m->d_rep_set.d_type_reps[retTyp].size() );
-      return m->d_rep_set.d_type_reps[retTyp][d_value];
+      const RepSet* rs = m->getRepSet();
+      Assert(d_value >= 0 && d_value < (int)rs->getNumRepresentatives(retTyp));
+      return rs->getRepresentative(retTyp, d_value);
     }
   }else{
     std::map< unsigned, AbsDef >::iterator it = d_def.find( iargs[depth] );
@@ -725,6 +747,7 @@ bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) {
   Trace("ambqi-debug") << "process build model " << std::endl;
   FirstOrderModel* f = (FirstOrderModel*)m;
   FirstOrderModelAbs* fm = f->asFirstOrderModelAbs();
+  RepSet* rs = m->getRepSetPtr();
   fm->initialize();
   //process representatives
   fm->d_rep_id.clear();
@@ -732,16 +755,19 @@ bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) {
 
   //initialize boolean sort
   TypeNode b = d_true.getType();
-  fm->d_rep_set.d_type_reps[b].clear();
-  fm->d_rep_set.d_type_reps[b].push_back( d_false );
-  fm->d_rep_set.d_type_reps[b].push_back( d_true );
+  rs->d_type_reps[b].clear();
+  rs->d_type_reps[b].push_back(d_false);
+  rs->d_type_reps[b].push_back(d_true);
   fm->d_rep_id[d_false] = 0;
   fm->d_rep_id[d_true] = 1;
 
   //initialize unintpreted sorts
   Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl;
-  for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
-       it != fm->d_rep_set.d_type_reps.end(); ++it ){
+  for (std::map<TypeNode, std::vector<Node> >::iterator it =
+           rs->d_type_reps.begin();
+       it != rs->d_type_reps.end();
+       ++it)
+  {
     if( it->first.isSort() ){
       Assert( !it->second.empty() );
       //set the domain
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 5afee3d57..2a2ba8d4f 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -738,8 +738,10 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va
     Assert( q[0][v]==d_set[q][i] );
     Node t = rsi->getCurrentTerm( v );
     Trace("bound-int-rsi") << "term : " << t << std::endl;
-    if( rsi->d_rep_set->d_values_to_terms.find( t )!=rsi->d_rep_set->d_values_to_terms.end() ){
-      t = rsi->d_rep_set->d_values_to_terms[t];
+    Node tt = rsi->d_rep_set->getTermForRepresentative(t);
+    if (!tt.isNull())
+    {
+      t = tt;
       Trace("bound-int-rsi") << "term (post-rep) : " << t << std::endl;
     }
     vars.push_back( d_set[q][i] );
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 4acc3e6b8..fb8ac4195 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -123,9 +123,10 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
     if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){
       //map back from values assigned by model, if any
       if( d_qe->getModel() ){
-        std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
-        if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){
-          r = it->second;
+        Node tr = d_qe->getModel()->getRepSet()->getTermForRepresentative(r);
+        if (!tr.isNull())
+        {
+          r = tr;
           r = getRepresentative( r );
         }else{
           if( r.getType().isSort() ){
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index ddf7becf2..db43d8bca 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -66,8 +66,10 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
       //for star: check if all children are defined and have generalizations
       if( c[index]==st ){     ///options::fmfFmcCoverSimplify()
         //check if all children exist and are complete
-        int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0);
-        if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){
+        unsigned num_child_def =
+            d_child.size() - (d_child.find(st) != d_child.end() ? 1 : 0);
+        if (num_child_def == m->getRepSet()->getNumRepresentatives(tn))
+        {
           bool complete = true;
           for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
             if( !m->isStar(it->first) ){
@@ -375,8 +377,12 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
   d_rep_ids.clear();
   d_star_insts.clear();
   //process representatives
-  for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
-       it != fm->d_rep_set.d_type_reps.end(); ++it ){
+  RepSet* rs = fm->getRepSetPtr();
+  for (std::map<TypeNode, std::vector<Node> >::iterator it =
+           rs->d_type_reps.begin();
+       it != rs->d_type_reps.end();
+       ++it)
+  {
     if( it->first.isSort() ){
       Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
       for( size_t a=0; a<it->second.size(); a++ ){
@@ -435,7 +441,9 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
       }else{
         Node vmb = getSomeDomainElement(fm, nmb.getType());
         Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
-        Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;
+        Trace("fmc-model-debug")
+            << fm->getRepSet()->getNumRepresentatives(nmb.getType())
+            << std::endl;
         add_conds.push_back( nmb );
         add_values.push_back( vmb );
       }
@@ -940,11 +948,15 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def
     if( tn.isSort() ){
       int j = fm->getVariableId(f, eq[0]);
       int k = fm->getVariableId(f, eq[1]);
-      if( !fm->d_rep_set.hasType( tn ) ){
+      const RepSet* rs = fm->getRepSet();
+      if (!rs->hasType(tn))
+      {
         getSomeDomainElement( fm, tn );  //to verify the type is initialized
       }
-      for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {
-        Node r = fm->getRepresentative( fm->d_rep_set.d_type_reps[tn][i] );
+      unsigned nreps = rs->getNumRepresentatives(tn);
+      for (unsigned i = 0; i < nreps; i++)
+      {
+        Node r = fm->getRepresentative(rs->getRepresentative(tn, i));
         cond[j+1] = r;
         cond[k+1] = r;
         d.addEntry( fm, mkCond(cond), d_true);
@@ -1319,7 +1331,7 @@ Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals )
 }
 
 Node FullModelChecker::getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ) {
-  bool addRepId = !fm->d_rep_set.hasType( tn );
+  bool addRepId = !fm->getRepSet()->hasType(tn);
   Node de = fm->getSomeDomainElement(tn);
   if( addRepId ){
     d_rep_ids[tn][de] = 0;
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index ced62d8f5..7c5259cb7 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -55,7 +55,8 @@ bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) {
     FirstOrderModel * fm = (FirstOrderModel*)m;
     //traverse equality engine
     std::map< TypeNode, bool > eqc_usort;
-    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
+    eq::EqClassesIterator eqcs_i =
+        eq::EqClassesIterator(fm->getEqualityEngine());
     while( !eqcs_i.isFinished() ){
       TypeNode tr = (*eqcs_i).getType();
       eqc_usort[tr] = true;
@@ -107,7 +108,7 @@ void QModelBuilder::debugModel( TheoryModel* m ){
       for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
         vars.push_back( f[0][j] );
       }
-      RepSetIterator riter( d_qe, &(fm->d_rep_set) );
+      RepSetIterator riter(d_qe, fm->getRepSetPtr());
       if( riter.setQuantifier( f ) ){
         while( !riter.isFinished() ){
           tests++;
@@ -117,7 +118,8 @@ void QModelBuilder::debugModel( TheoryModel* m ){
           }
           Node n = d_qe->getInstantiation( f, vars, terms );
           Node val = fm->getValue( n );
-          if( val!=fm->d_true ){
+          if (val != d_qe->getTermUtil()->d_true)
+          {
             Trace("quant-check-model") << "*******  Instantiation " << n << " for " << std::endl;
             Trace("quant-check-model") << "         " << f << std::endl;
             Trace("quant-check-model") << "         Evaluates to " << val << std::endl;
@@ -411,7 +413,7 @@ QModelBuilderIG::Statistics::~Statistics(){
 //do exhaustive instantiation
 int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
   if( optUseModel() ){
-    RepSetIterator riter( d_qe, &(d_qe->getModel()->d_rep_set) );
+    RepSetIterator riter(d_qe, d_qe->getModel()->getRepSetPtr());
     if( riter.setQuantifier( f ) ){
       FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel();
       Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
@@ -668,7 +670,8 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
       std::vector< Node > tr_terms;
       if( lit.getKind()==APPLY_UF ){
         //only match predicates that are contrary to this one, use literal matching
-        Node eq = NodeManager::currentNM()->mkNode( EQUAL, lit, !phase ? fm->d_true : fm->d_false );
+        Node eq = NodeManager::currentNM()->mkNode(
+            EQUAL, lit, NodeManager::currentNM()->mkConst(!phase));
         tr_terms.push_back( eq );
       }else if( lit.getKind()==EQUAL ){
         //collect trigger terms
@@ -733,7 +736,9 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
         Node n = itut->second[i];
         // only consider unique up to congruence (in model equality engine)?
         Node v = fmig->getRepresentative( n );
-        Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl;
+        Trace("fmf-model-cons") << "Set term " << n << " : "
+                                << fmig->getRepSet()->getIndexFor(v) << " " << v
+                                << std::endl;
         //if this assertion did not help the model, just consider it ground
         //set n = v in the model tree
         //set it as ground value
@@ -763,14 +768,19 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
       //chose defaultVal based on heuristic, currently the best ratio of "pro" responses
       Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
       if( defaultVal.isNull() ){
-        if (!fmig->d_rep_set.hasType(defaultTerm.getType())) {
+        if (!fmig->getRepSet()->hasType(defaultTerm.getType()))
+        {
           Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(defaultTerm.getType());
-          fmig->d_rep_set.d_type_reps[defaultTerm.getType()].push_back(mbt);
+          fmig->getRepSetPtr()->d_type_reps[defaultTerm.getType()].push_back(
+              mbt);
         }
-        defaultVal = fmig->d_rep_set.d_type_reps[defaultTerm.getType()][0];
+        defaultVal =
+            fmig->getRepSet()->getRepresentative(defaultTerm.getType(), 0);
       }
       Assert( !defaultVal.isNull() );
-      Trace("fmf-model-cons") << "Set default term : " << fmig->d_rep_set.getIndexFor( defaultVal ) << std::endl;
+      Trace("fmf-model-cons")
+          << "Set default term : " << fmig->getRepSet()->getIndexFor(defaultVal)
+          << std::endl;
       fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
     }
     Debug("fmf-model-cons") << "  Making model...";
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 081d4e66a..b3acb408f 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -165,11 +165,15 @@ int ModelEngine::checkModel(){
 
   //flatten the representatives
   //Trace("model-engine-debug") << "Flattening representatives...." << std::endl;
-  //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps );
+  // d_quantEngine->getEqualityQuery()->flattenRepresentatives(
+  // fm->getRepSet()->d_type_reps );
 
   //for debugging, setup
-  for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
-       it != fm->d_rep_set.d_type_reps.end(); ++it ){
+  for (std::map<TypeNode, std::vector<Node> >::iterator it =
+           fm->getRepSetPtr()->d_type_reps.begin();
+       it != fm->getRepSetPtr()->d_type_reps.end();
+       ++it)
+  {
     if( it->first.isSort() ){
       Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
       Trace("model-engine-debug") << "        Reps : ";
@@ -199,8 +203,10 @@ int ModelEngine::checkModel(){
         int totalInst = 1;
         for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
           TypeNode tn = f[0][j].getType();
-          if( fm->d_rep_set.hasType( tn ) ){
-            totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+          if (fm->getRepSet()->hasType(tn))
+          {
+            totalInst =
+                totalInst * (int)fm->getRepSet()->getNumRepresentatives(tn);
           }
         }
         d_totalLemmas += totalInst;
@@ -271,7 +277,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
       Trace("fmf-exh-inst-debug") << std::endl;
     }
     //create a rep set iterator and iterate over the (relevant) domain of the quantifier
-    RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
+    RepSetIterator riter(d_quantEngine,
+                         d_quantEngine->getModel()->getRepSetPtr());
     if( riter.setQuantifier( f ) ){
       Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
       if( !riter.isIncomplete() ){
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index b0f548625..a8930de6e 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1711,7 +1711,7 @@ eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
 
 eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() {
   if( d_useModelEe ){
-    return d_model->d_equalityEngine;
+    return d_model->getEqualityEngine();
   }else{
     return d_te->getMasterEqualityEngine();
   }
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 303e65eff..dd139d5ec 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -12,6 +12,8 @@
  ** \brief Implementation of representative set
  **/
 
+#include <unordered_set>
+
 #include "theory/rep_set.h"
 #include "theory/type_enumerator.h"
 #include "theory/quantifiers/bounded_integers.h"
@@ -31,8 +33,10 @@ void RepSet::clear(){
   d_values_to_terms.clear();
 }
 
-bool RepSet::hasRep( TypeNode tn, Node n ) {
-  std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.find( tn );
+bool RepSet::hasRep(TypeNode tn, Node n) const
+{
+  std::map<TypeNode, std::vector<Node> >::const_iterator it =
+      d_type_reps.find(tn);
   if( it==d_type_reps.end() ){
     return false;
   }else{
@@ -40,18 +44,29 @@ bool RepSet::hasRep( TypeNode tn, Node n ) {
   }
 }
 
-int RepSet::getNumRepresentatives( TypeNode tn ) const{
+unsigned RepSet::getNumRepresentatives(TypeNode tn) const
+{
   std::map< TypeNode, std::vector< Node > >::const_iterator it = d_type_reps.find( tn );
   if( it!=d_type_reps.end() ){
-    return (int)it->second.size();
+    return it->second.size();
   }else{
     return 0;
   }
 }
 
-bool containsStoreAll( Node n, std::vector< Node >& cache ){
+Node RepSet::getRepresentative(TypeNode tn, unsigned i) const
+{
+  std::map<TypeNode, std::vector<Node> >::const_iterator it =
+      d_type_reps.find(tn);
+  Assert(it != d_type_reps.end());
+  Assert(i < it->second.size());
+  return it->second[i];
+}
+
+bool containsStoreAll(Node n, std::unordered_set<Node, NodeHashFunction>& cache)
+{
   if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
-    cache.push_back( n );
+    cache.insert(n);
     if( n.getKind()==STORE_ALL ){
       return true;
     }else{
@@ -68,7 +83,7 @@ bool containsStoreAll( Node n, std::vector< Node >& cache ){
 void RepSet::add( TypeNode tn, Node n ){
   //for now, do not add array constants FIXME
   if( tn.isArray() ){
-    std::vector< Node > cache;
+    std::unordered_set<Node, NodeHashFunction> cache;
     if( containsStoreAll( n, cache ) ){
       return;
     }
@@ -116,6 +131,43 @@ bool RepSet::complete( TypeNode t ){
   }
 }
 
+Node RepSet::getTermForRepresentative(Node n) const
+{
+  std::map<Node, Node>::const_iterator it = d_values_to_terms.find(n);
+  if (it != d_values_to_terms.end())
+  {
+    return it->second;
+  }
+  else
+  {
+    return Node::null();
+  }
+}
+
+void RepSet::setTermForRepresentative(Node n, Node t)
+{
+  d_values_to_terms[n] = t;
+}
+
+Node RepSet::getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const
+{
+  std::map<TypeNode, std::vector<Node> >::const_iterator it =
+      d_type_reps.find(tn);
+  if (it != d_type_reps.end())
+  {
+    // try to find a pre-existing arbitrary element
+    for (size_t i = 0; i < it->second.size(); i++)
+    {
+      if (std::find(exclude.begin(), exclude.end(), it->second[i])
+          == exclude.end())
+      {
+        return it->second[i];
+      }
+    }
+  }
+  return Node::null();
+}
+
 void RepSet::toStream(std::ostream& out){
   for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
     if( !it->first.isFunction() && !it->first.isPredicate() ){
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 41044b526..a20e56184 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -17,40 +17,97 @@
 #ifndef __CVC4__THEORY__REP_SET_H
 #define __CVC4__THEORY__REP_SET_H
 
-#include "expr/node.h"
 #include <map>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace theory {
 
 class QuantifiersEngine;
 
-/** this class stores a representative set */
+/** representative set
+ *
+ * This class contains finite lists of values for types, typically values and
+ * types that exist
+ * in the equality engine of a model object.  In the following, "representative"
+ * means a value that exists in this set.
+ *
+ * This class is used for finite model finding and other exhaustive
+ * instantiation-based
+ * methods. The class goes beyond just maintaining a list of values that occur
+ * in the equality engine in the following ways:
+ 
+ * (1) It maintains a partial mapping from representatives to a term that has
+ * that value in the current
+ * model.  This is important because algorithms like the instantiation method in
+ * Reynolds et al CADE 2013
+ * act on "term models" where domains in models are interpreted as a set of
+ * representative terms. Hence,
+ * instead of instantiating with e.g. uninterpreted constants u, we instantiate
+ * with the corresponding term that is interpreted as u.
+ 
+ * (2) It is mutable, calls to add(...) and complete(...) may modify this class
+ * as necessary, for instance
+ * in the case that there are no ground terms of a type that occurs in a
+ * quantified formula, or for
+ * exhaustive instantiation strategies that enumerate over small interpreted
+ * finite types.
+ */
 class RepSet {
 public:
   RepSet(){}
   ~RepSet(){}
+  /** map from types to the list of representatives
+   * TODO : as part of #1199, encapsulate this
+   */
   std::map< TypeNode, std::vector< Node > > d_type_reps;
-  std::map< TypeNode, bool > d_type_complete;
-  std::map< Node, int > d_tmap;
-  // map from values to terms they were assigned for
-  std::map< Node, Node > d_values_to_terms;
   /** clear the set */
   void clear();
-  /** has type */
+  /** does this set have representatives of type tn? */
   bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); }
-  /** has rep */
-  bool hasRep( TypeNode tn, Node n );
-  /** get cardinality for type */
-  int getNumRepresentatives( TypeNode tn ) const;
-  /** add representative for type */
+  /** does this set have representative n of type tn? */
+  bool hasRep(TypeNode tn, Node n) const;
+  /** get the number of representatives for type */
+  unsigned getNumRepresentatives(TypeNode tn) const;
+  /** get representative at index */
+  Node getRepresentative(TypeNode tn, unsigned i) const;
+  /** add representative n for type tn, where n has type tn */
   void add( TypeNode tn, Node n );
   /** returns index in d_type_reps for node n */
   int getIndexFor( Node n ) const;
-  /** complete all values */
+  /** complete the list for type t
+   * Resets d_type_reps[tn] and repopulates by running the type enumerator for
+   * that type exhaustively.
+   * This should only be called for small finite interpreted types.
+   */
   bool complete( TypeNode t );
+  /** get term for representative
+   * Returns a term that is interpreted as representative n in the current
+   * model, null otherwise.
+   */
+  Node getTermForRepresentative(Node n) const;
+  /** set term for representative
+   * Called when t is interpreted as value n. Subsequent class to
+   * getTermForRepresentative( n ) will return t.
+   */
+  void setTermForRepresentative(Node n, Node t);
+  /** get existing domain value, with possible exclusions
+    *   This function returns a term in d_type_reps[tn] but not in exclude
+    */
+  Node getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const;
   /** debug print */
   void toStream(std::ostream& out);
+
+ private:
+  /** whether the list of representatives for types are complete */
+  std::map<TypeNode, bool> d_type_complete;
+  /** map from representatives to their index in d_type_reps */
+  std::map<Node, int> d_tmap;
+  /** map from values to terms they were assigned for */
+  std::map<Node, Node> d_values_to_terms;
 };/* class RepSet */
 
 //representative domain
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index a4b36b87c..490ed45c9 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -252,7 +252,11 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c
           // TODO: if func models not enabled, throw an error?
           Unreachable();
         }
-      }else if(t.isRegExp()) {
+      }
+      else if (!t.isFirstClass())
+      {
+        // this is the class for regular expressions
+        // we simply invoke the rewriter on them
         ret = Rewriter::rewrite(ret);
       } else {
         if (options::omitDontCares() && useDontCares) {
@@ -279,18 +283,6 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c
   return ret;
 }
 
-Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){
-  if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){
-    //try to find a pre-existing arbitrary element
-    for( size_t i=0; i<d_rep_set.d_type_reps[tn].size(); i++ ){
-      if( std::find( exclude.begin(), exclude.end(), d_rep_set.d_type_reps[tn][i] )==exclude.end() ){
-        return d_rep_set.d_type_reps[tn][i];
-      }
-    }
-  }
-  return Node::null();
-}
-
 /** add substitution */
 void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
   if( !d_substitutions.hasSubstitution( x ) ){
@@ -415,7 +407,8 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>*
         if (first) {
           rep = (*eqc_i);
           //add the term (this is specifically for the case of singleton equivalence classes)
-          if( !rep.getType().isRegExp() ){
+          if (rep.getType().isFirstClass())
+          {
             d_equalityEngine->addTerm( rep );
             Trace("model-builder-debug") << "Add term to ee within assertEqualityEngine: " << rep << std::endl;
           }
@@ -636,7 +629,7 @@ void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cac
 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.d_values_to_terms[const_rep] = eqc;
+  tm->d_rep_set.setTermForRepresentative(const_rep, eqc);
 }
 
 bool TheoryEngineModelBuilder::isExcludedCdtValue( Node val, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ) {
@@ -1238,7 +1231,9 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
     retNode = NodeManager::currentNM()->mkNode( r.getKind(), children );
     if (childrenConst) {
       retNode = Rewriter::rewrite(retNode);
-      Assert(retNode.getKind()==kind::APPLY_UF || retNode.getType().isRegExp() || retNode.isConst());
+      Assert(retNode.getKind() == kind::APPLY_UF
+             || !retNode.getType().isFirstClass()
+             || retNode.isConst());
     }
   }
   d_normalizedCache[r] = retNode;
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 00dd215e9..0d73cd72a 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -36,46 +36,13 @@ namespace theory {
 class TheoryModel : public Model
 {
   friend class TheoryEngineModelBuilder;
-protected:
-  /** substitution map for this model */
-  SubstitutionMap d_substitutions;
-  bool d_modelBuilt;
+
 public:
   TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
   virtual ~TheoryModel() throw();
 
-  /** special local context for our equalityEngine so we can clear it independently of search context */
-  context::Context* d_eeContext;
-  /** equality engine containing all known equalities/disequalities */
-  eq::EqualityEngine* d_equalityEngine;
-  /** map of representatives of equality engine to used representatives in representative set */
-  std::map< Node, Node > d_reps;
-  /** stores set of representatives for each type */
-  RepSet d_rep_set;
-  /** true/false nodes */
-  Node d_true;
-  Node d_false;
-  mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
-public: 
-  /** comment stream to include in printing */
-  std::stringstream d_comment_str;
   /** get comments */
   void getComments(std::ostream& out) const;
-private:
-  /** information for separation logic */
-  Node d_sep_heap;
-  Node d_sep_nil_eq;
-public:
-  void setHeapModel( Node h, Node neq );
-  bool getHeapModel( Expr& h, Expr& neq ) const;
-protected:
-  /** reset the model */
-  virtual void reset();
-  /**
-   * Get model value function.  This function is called by getValue
-   */
-  Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const;
-public:
   /** is built */
   bool isBuilt() { return d_modelBuilt; }
   /** set need build */
@@ -86,11 +53,13 @@ public:
    */
   Node getValue( TNode n, bool useDontCares = false ) const;
 
-  /** get existing domain value, with possible exclusions
-    *   This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude
-    */
-  Node getDomainValue( TypeNode tn, std::vector< Node >& exclude );
-public:
+  //---------------------------- 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
+
   /** Adds a substitution from x to t. */
   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
   /** add term function
@@ -112,33 +81,36 @@ public:
     *  functions.
     */
   void assertRepresentative(TNode n);
-public:
-  /** general queries */
+
+  // ------------------- general equality queries
+  /** does the equality engine of this model have term a? */
   bool hasTerm(TNode a);
+  /** get the representative of a in the equality engine of this model */
   Node getRepresentative(TNode a);
+  /** are a and b equal in the equality engine of this model? */
   bool areEqual(TNode a, TNode b);
+  /** are a and b disequal in the equality engine of this model? */
   bool areDisequal(TNode a, TNode b);
-public:
+  /** get the equality engine for this model */
+  eq::EqualityEngine* getEqualityEngine() { return d_equalityEngine; }
+  // ------------------- end general equality queries
+
+  /** get the representative set object */
+  const RepSet* getRepSet() const { return &d_rep_set; }
+  /** get the representative set object (FIXME: remove this, see #1199) */
+  RepSet* getRepSetPtr() { return &d_rep_set; }
   /** return whether this node is a don't-care */
   bool isDontCare(Expr expr) const;
   /** get value function for Exprs. */
   Expr getValue( Expr expr ) const;
   /** get cardinality for sort */
   Cardinality getCardinality( Type t ) const;
-public:
   /** print representative debug function */
   void printRepresentativeDebug( const char* c, Node r );
   /** print representative function */
   void printRepresentative( std::ostream& out, Node r );
-private:
-  /** 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.
-  */
-  std::map< Node, Node > d_uf_models;
-public:
-  /** whether function models are enabled */
-  bool d_enableFuncModels;
+
+  //---------------------------- function values
   /** a map from functions f to a list of all APPLY_UF terms with operator f */
   std::map< Node, std::vector< Node > > d_uf_terms;
   /** a map from functions f to a list of all HO_APPLY terms with first argument f */
@@ -154,6 +126,55 @@ public:
   * which is required for "dag form" model construction (see TheoryModelBuilder::assignHoFunction).
   */
   std::vector< Node > getFunctionsToAssign();
+  //---------------------------- end function values
+ protected:
+  /** substitution map for this model */
+  SubstitutionMap d_substitutions;
+  /** whether this model has been built */
+  bool d_modelBuilt;
+  /** special local context for our equalityEngine so we can clear it
+   * independently of search context */
+  context::Context* d_eeContext;
+  /** equality engine containing all known equalities/disequalities */
+  eq::EqualityEngine* d_equalityEngine;
+  /** map of representatives of equality engine to used representatives in
+   * representative set */
+  std::map<Node, Node> d_reps;
+  /** stores set of representatives for each type */
+  RepSet d_rep_set;
+  /** 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
+   */
+  Node getModelValue(TNode n,
+                     bool hasBoundVars = false,
+                     bool useDontCares = false) const;
+
+ private:
+  //---------------------------- separation logic
+  /** the value of the heap */
+  Node d_sep_heap;
+  /** the value of the nil element */
+  Node d_sep_nil_eq;
+  //---------------------------- end separation logic
+
+  //---------------------------- function values
+  /** whether function models are enabled */
+  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.
+  */
+  std::map<Node, Node> d_uf_models;
+  //---------------------------- end function values
 };/* class TheoryModel */
 
 /*
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 1b7437a7e..54e99cdba 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -437,7 +437,7 @@ Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel*
     //consider finding another value, if possible
     Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl;
     TypeNode tn = defaultTerm.getType();
-    Node newDefaultVal = m->getDomainValue( tn, d_values );
+    Node newDefaultVal = m->getRepSet()->getDomainValue(tn, d_values);
     if( !newDefaultVal.isNull() ){
       defaultVal = newDefaultVal;
       Debug("fmf-model-cons-debug") << "-> Change default value to ";
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 4b6a326cf..eb9e5e987 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -851,8 +851,8 @@ bool SortModel::minimize( OutputChannel* out, TheoryModel* m ){
 #if 0
       // ensure that the constructed model is minimal
       // if the model has terms that the strong solver does not know about
-      if( (int)m->d_rep_set.d_type_reps[ d_type ].size()>d_cardinality ){
-        eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine );
+      if( (int)rs->d_type_reps[ d_type ].size()>d_cardinality ){
+        eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->getEqualityEngine() );
         while( !eqcs_i.isFinished() ){
           Node eqc = (*eqcs_i);
           if( eqc.getType()==d_type ){
@@ -1550,7 +1550,8 @@ void SortModel::debugPrint( const char* c ){
 bool SortModel::debugModel( TheoryModel* m ){
   if( Trace.isOn("uf-ss-warn") ){
     std::vector< Node > eqcs;
-    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( m->d_equalityEngine );
+    eq::EqClassesIterator eqcs_i =
+        eq::EqClassesIterator(m->getEqualityEngine());
     while( !eqcs_i.isFinished() ){
       Node eqc = (*eqcs_i);
       if( eqc.getType()==d_type ){
@@ -1567,7 +1568,8 @@ bool SortModel::debugModel( TheoryModel* m ){
       ++eqcs_i;
     }
   }
-  int nReps = m->d_rep_set.d_type_reps.find( d_type )==m->d_rep_set.d_type_reps.end() ? 0 : (int)m->d_rep_set.d_type_reps[d_type].size();
+  RepSet* rs = m->getRepSetPtr();
+  int nReps = (int)rs->getNumRepresentatives(d_type);
   if( nReps!=(d_maxNegCard+1) ){
     Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl;
     Trace("uf-ss-warn") << "   Max neg cardinality : " << d_maxNegCard << std::endl;
@@ -1576,16 +1578,17 @@ bool SortModel::debugModel( TheoryModel* m ){
       /*
       for( unsigned i=0; i<d_fresh_aloc_reps.size(); i++ ){
         if( add>0 && !m->d_equalityEngine->hasTerm( d_fresh_aloc_reps[i] ) ){
-          m->d_rep_set.d_type_reps[d_type].push_back( d_fresh_aloc_reps[i] );
+          rs->d_type_reps[d_type].push_back( d_fresh_aloc_reps[i] );
           add--;
         }
       }
       for( int i=0; i<add; i++ ){
         std::stringstream ss;
         ss << "r_" << d_type << "_";
-        Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "enumeration to meet negative card constraint" );
+        Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type,
+      "enumeration to meet negative card constraint" );
         d_fresh_aloc_reps.push_back( nn );
-        m->d_rep_set.d_type_reps[d_type].push_back( nn );
+        rs->d_type_reps[d_type].push_back( nn );
       }
       */
       while( (int)d_fresh_aloc_reps.size()<=d_maxNegCard ){
@@ -1595,7 +1598,7 @@ bool SortModel::debugModel( TheoryModel* m ){
         d_fresh_aloc_reps.push_back( nn );
       }
       if( d_maxNegCard==0 ){
-        m->d_rep_set.d_type_reps[d_type].push_back( d_fresh_aloc_reps[0] );
+        rs->d_type_reps[d_type].push_back(d_fresh_aloc_reps[0]);
       }else{
         //must add lemma
         std::vector< Node > force_cl;