Merge branch 'master' of https://github.com/CVC4/CVC4.git

Conflicts:
	proofs/signatures/Makefile.am
	src/Makefile.am
	src/expr/datatype.cpp
	src/options/datatypes_options
	src/options/options_template.cpp
	src/options/quantifiers_options
	src/proof/arith_proof.cpp
	src/proof/arith_proof.h
	src/proof/array_proof.cpp
	src/proof/array_proof.h
	src/proof/bitvector_proof.cpp
	src/proof/bitvector_proof.h
	src/proof/cnf_proof.cpp
	src/proof/cnf_proof.h
	src/proof/proof_manager.cpp
	src/proof/proof_manager.h
	src/proof/sat_proof.h
	src/proof/sat_proof_implementation.h
	src/proof/skolemization_manager.h
	src/proof/theory_proof.cpp
	src/proof/theory_proof.h
	src/proof/uf_proof.cpp
	src/proof/uf_proof.h
	src/prop/cnf_stream.cpp
	src/prop/cnf_stream.h
	src/prop/minisat/core/Solver.cc
	src/prop/prop_engine.cpp
	src/prop/prop_engine.h
	src/prop/theory_proxy.cpp
	src/smt/smt_engine.cpp
	src/smt/smt_engine_check_proof.cpp
	src/theory/arrays/array_proof_reconstruction.cpp
	src/theory/arrays/theory_arrays.cpp
	src/theory/bv/eager_bitblaster.cpp
	src/theory/bv/lazy_bitblaster.cpp
	src/theory/datatypes/theory_datatypes.cpp
	src/theory/quantifiers/alpha_equivalence.cpp
	src/theory/quantifiers/candidate_generator.cpp
	src/theory/quantifiers/candidate_generator.h
	src/theory/quantifiers/ce_guided_single_inv.cpp
	src/theory/quantifiers/ceg_instantiator.cpp
	src/theory/quantifiers/conjecture_generator.cpp
	src/theory/quantifiers/equality_infer.cpp
	src/theory/quantifiers/equality_infer.h
	src/theory/quantifiers/inst_match_generator.cpp
	src/theory/quantifiers/inst_propagator.cpp
	src/theory/quantifiers/inst_propagator.h
	src/theory/quantifiers/inst_strategy_e_matching.cpp
	src/theory/quantifiers/inst_strategy_e_matching.h
	src/theory/quantifiers/instantiation_engine.cpp
	src/theory/quantifiers/model_builder.cpp
	src/theory/quantifiers/model_engine.cpp
	src/theory/quantifiers/quant_conflict_find.cpp
	src/theory/quantifiers/quant_conflict_find.h
	src/theory/quantifiers/quant_split.cpp
	src/theory/quantifiers/quant_util.cpp
	src/theory/quantifiers/quantifiers_rewriter.cpp
	src/theory/quantifiers/quantifiers_rewriter.h
	src/theory/quantifiers/term_database.cpp
	src/theory/quantifiers/term_database.h
	src/theory/quantifiers/trigger.cpp
	src/theory/quantifiers/trigger.h
	src/theory/quantifiers_engine.cpp
	src/theory/quantifiers_engine.h
	src/theory/sets/kinds
	src/theory/sets/theory_sets_private.cpp
	src/theory/sets/theory_sets_private.h
	src/theory/sets/theory_sets_rewriter.cpp
	src/theory/sets/theory_sets_type_rules.h
	src/theory/strings/theory_strings.cpp
	src/theory/strings/theory_strings.h
	src/theory/theory_engine.cpp
	src/theory/theory_engine.h
	src/theory/uf/equality_engine.cpp
	test/regress/regress0/fmf/Makefile.am
	test/regress/regress0/quantifiers/Makefile.am
	test/regress/regress0/strings/Makefile.am
	test/regress/regress0/sygus/Makefile.am
	test/regress/regress0/sygus/max2-univ.sy

1 files changed, 33 insertions, 22 deletions

diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 08fc7dd52..ee927de86 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -64,22 +64,42 @@ class RepSetIterator {
 public:
   enum {
     ENUM_DOMAIN_ELEMENTS,
-    ENUM_RANGE,
+    ENUM_INT_RANGE,
+    ENUM_SET_MEMBERS,
   };
 private:
   QuantifiersEngine * d_qe;
   //initialize function
   bool initialize();
-  //for enum ranges
+  //for int ranges
   std::map< int, Node > d_lower_bounds;
+  //for set ranges
+  std::map< int, std::vector< Node > > d_setm_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 );
+  //reset index, 1:success, 0:empty, -1:fail
+  int resetIndex( int i, bool initial = false );
   /** set index order */
   void setIndexOrder( std::vector< int >& indexOrder );
+  /** do reset increment the iterator at index=counter */
+  int do_reset_increment( int counter, bool initial = false );
+  //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;  
+  //are we only considering a strict subset of the domain of the quantifier?
+  bool d_incomplete;
 public:
   RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
   ~RepSetIterator(){}
@@ -92,43 +112,34 @@ public:
   RepSet* d_rep_set;
   //enumeration type?
   std::vector< int > d_enum_type;
-  //index we are considering
+  //current tuple 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;
   //intervals
   std::map< int, Node > d_bounds[2];
 public:
   /** increment the iterator at index=counter */
-  int increment2( int counter );
+  int increment2( int i );
   /** increment the iterator */
   int increment();
   /** is the iterator finished? */
   bool isFinished();
   /** get the i_th term we are considering */
-  Node getTerm( int i );
+  Node getCurrentTerm( int v );
   /** 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 );
+  //get index order, returns var #
+  int getIndexOrder( int v ) { return d_index_order[v]; }
+  //get variable order, returns index #
+  int getVariableOrder( int i ) { return d_var_order[i]; }
+  //is incomplete
+  bool isIncomplete() { return d_incomplete; }
 };/* class RepSetIterator */
 
 }/* CVC4::theory namespace */