diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 12:43:15 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 12:43:31 -0600 |
commit | e8c09abb9165278b13491c83bdcbe17ae535126e (patch) | |
tree | 1101d3e878bcfd9e12cd64aaad3017aa320c896b /src/theory/rep_set.h | |
parent | 0e956da9b32ce8a8fcf20ec65e5a2820b4e31324 (diff) |
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.
Diffstat (limited to 'src/theory/rep_set.h')
-rw-r--r-- | src/theory/rep_set.h | 21 |
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 ); |