Refactoring, generalization of bounded inference module. Simplification of rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.

1 files changed, 12 insertions, 9 deletions

diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index a56fba39b..2a2110cfa 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -56,18 +56,23 @@ public:
 //representative domain
 typedef std::vector< int > RepDomain;
 
+
+class RepBoundExt {
+public:
+  virtual bool setBound( Node owner, int i, TypeNode tn, std::vector< Node >& elements ) = 0;
+};
+
 /** this class iterates over a RepSet */
 class RepSetIterator {
 public:
   enum {
-    ENUM_DOMAIN_ELEMENTS,
-    ENUM_INT_RANGE,
-    ENUM_SET_MEMBERS,
+    ENUM_DEFAULT,
+    ENUM_BOUND_INT,
   };
 private:
   QuantifiersEngine * d_qe;
   //initialize function
-  bool initialize();
+  bool initialize( RepBoundExt* rext = NULL );
   //for int ranges
   std::map< int, Node > d_lower_bounds;
   //for set ranges
@@ -101,9 +106,9 @@ public:
   RepSetIterator( QuantifiersEngine * qe, RepSet* rs );
   ~RepSetIterator(){}
   //set that this iterator will be iterating over instantiations for a quantifier
-  bool setQuantifier( Node f );
+  bool setQuantifier( Node f, RepBoundExt* rext = NULL );
   //set that this iterator will be iterating over the domain of a function
-  bool setFunctionDomain( Node op );
+  bool setFunctionDomain( Node op, RepBoundExt* rext = NULL );
 public:
   //pointer to model
   RepSet* d_rep_set;
@@ -114,9 +119,7 @@ public:
   //types we are considering
   std::vector< TypeNode > d_types;
   //domain we are considering
-  std::vector< RepDomain > d_domain;
-  //intervals
-  std::map< int, Node > d_bounds[2];
+  std::vector< std::vector< Node > > d_domain_elements;
 public:
   /** increment the iterator at index=counter */
   int increment2( int i );