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, 59 insertions, 7 deletions

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