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.

1 files changed, 13 insertions, 6 deletions

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