diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-22 17:34:23 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-22 17:34:23 -0500 |
commit | 2bf0735176e0ff5fb9720bfb255ca22443584dcc (patch) | |
tree | 16926686e86f182e383efd8153b7d0e11bbc694a /src/theory/rep_set.h | |
parent | b48a369333f077fa7cce117976f760cd6332691a (diff) |
Significant work on bounded integer quantification to handle non-trivial bounds. Refactoring of InstConstantAttribute to be internal to TermDb.
Diffstat (limited to 'src/theory/rep_set.h')
-rw-r--r-- | src/theory/rep_set.h | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index b92d9d2c6..fc8db420d 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -59,22 +59,26 @@ private: ENUM_DOMAIN_ELEMENTS, ENUM_RANGE, }; - + QuantifiersEngine * d_qe; //initialize function - bool initialize(QuantifiersEngine * qe, Node f); + bool initialize(); //enumeration type? std::vector< int > d_enum_type; //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 ); public: - RepSetIterator( RepSet* rs ); + RepSetIterator( QuantifiersEngine * qe, RepSet* rs ); ~RepSetIterator(){} //set that this iterator will be iterating over instantiations for a quantifier - bool setQuantifier( QuantifiersEngine * qe, Node f ); + bool setQuantifier( Node f ); //set that this iterator will be iterating over the domain of a function - bool setFunctionDomain( QuantifiersEngine * qe, Node op ); + bool setFunctionDomain( Node op ); public: //pointer to model RepSet* d_rep_set; |