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.

6 files changed, 115 insertions, 57 deletions

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() ){