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.

2 files changed, 12 insertions, 9 deletions

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;