1 files changed, 25 insertions, 7 deletions
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 24fa7473e..a619915ee 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -23,6 +23,8 @@
 namespace CVC4 {
 namespace theory {
 
+class QuantifiersEngine;
+
 /** this class stores a representative set */
 class RepSet {
 public:
@@ -52,11 +54,27 @@ typedef std::vector< int > RepDomain;
 
 /** this class iterates over a RepSet */
 class RepSetIterator {
+public:
+  enum {
+    ENUM_DOMAIN_ELEMENTS,
+    ENUM_RANGE,
+  };
 private:
+  QuantifiersEngine * d_qe;
   //initialize function
   bool initialize();
+  //for enum ranges
+  std::map< int, Node > d_lower_bounds;
+  //domain size
+  int domainSize( int i );
+  //node this is rep set iterator is for
+  Node d_owner;
+  //reset index
+  bool resetIndex( int i, bool initial = false );
+  /** set index order */
+  void setIndexOrder( std::vector< int >& indexOrder );
 public:
-  RepSetIterator( RepSet* rs );
+  RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
   ~RepSetIterator(){}
   //set that this iterator will be iterating over instantiations for a quantifier
   bool setQuantifier( Node f );
@@ -65,6 +83,8 @@ public:
 public:
   //pointer to model
   RepSet* d_rep_set;
+  //enumeration type?
+  std::vector< int > d_enum_type;
   //index we are considering
   std::vector< int > d_index;
   //types we are considering
@@ -86,15 +106,13 @@ public:
   //  for example, if d_index_order = { 2, 0, 1 }
   //    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
   std::map< int, int > d_var_order;
+  //intervals
+  std::map< int, Node > d_bounds[2];
 public:
-  /** set index order */
-  void setIndexOrder( std::vector< int >& indexOrder );
-  /** set domain */
-  void setDomain( std::vector< RepDomain >& domain );
   /** increment the iterator at index=counter */
-  void increment2( int counter );
+  int increment2( int counter );
   /** increment the iterator */
-  void increment();
+  int increment();
   /** is the iterator finished? */
   bool isFinished();
   /** get the i_th term we are considering */