1 files changed, 112 insertions, 0 deletions
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
new file mode 100644
index 000000000..3427502b1
--- /dev/null
+++ b/src/theory/rep_set.h
@@ -0,0 +1,112 @@
+/*********************                                                        */
+/*! \file rep_set.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Representative set class and utilities
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__REP_SET_H
+#define __CVC4__REP_SET_H
+
+#include "expr/node.h"
+#include <map>
+
+namespace CVC4 {
+namespace theory {
+
+/** this class stores a representative set */
+class RepSet {
+public:
+  RepSet(){}
+  ~RepSet(){}
+  std::map< TypeNode, std::vector< Node > > d_type_reps;
+  std::map< TypeNode, bool > d_type_complete;
+  std::map< Node, int > d_tmap;
+  /** clear the set */
+  void clear();
+  /** has type */
+  bool hasType( TypeNode tn ) { return d_type_reps.find( tn )!=d_type_reps.end(); }
+  /** add representative for type */
+  void add( Node n );
+  /** returns index in d_type_reps for node n */
+  int getIndexFor( Node n ) { return d_tmap.find( n )!=d_tmap.end() ? d_tmap[n] : -1; }
+  /** complete all values */
+  void complete( TypeNode t );
+  /** debug print */
+  void toStream(std::ostream& out);
+};
+
+//representative domain
+typedef std::vector< int > RepDomain;
+
+/** this class iterates over a RepSet */
+class RepSetIterator {
+private:
+  //initialize function
+  void initialize();
+public:
+  RepSetIterator( RepSet* rs );
+  ~RepSetIterator(){}
+  //set that this iterator will be iterating over instantiations for a quantifier
+  void setQuantifier( Node f );
+  //set that this iterator will be iterating over the domain of a function
+  void setFunctionDomain( Node op );
+public:
+  //pointer to model
+  RepSet* d_rep_set;
+  //index we are considering
+  std::vector< int > d_index;
+  //types we are considering
+  std::vector< TypeNode > d_types;
+  //domain we are considering
+  std::vector< RepDomain > d_domain;
+  //are we only considering a strict subset of the domain of the quantifier?
+  bool d_incomplete;
+  //ordering for variables we are indexing over
+  //  for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
+  //    then we consider instantiations in this order:
+  //      a/x a/y a/z
+  //      a/x b/y a/z
+  //      b/x a/y a/z
+  //      b/x b/y a/z
+  //      ...
+  std::vector< int > d_index_order;
+  //variables to index they are considered at
+  //  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;
+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 );
+  /** increment the iterator */
+  void increment();
+  /** is the iterator finished? */
+  bool isFinished();
+  /** get the i_th term we are considering */
+  Node getTerm( int i );
+  /** get the number of terms we are considering */
+  int getNumTerms() { return (int)d_index_order.size(); }
+  /** debug print */
+  void debugPrint( const char* c );
+  void debugPrintSmall( const char* c );
+};
+
+}
+}
+
+#endif
+\ No newline at end of file