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, 55 insertions, 29 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 );
         }
       }