diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-04 12:12:30 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-04 12:12:41 -0500 |
commit | 25a01d31bffcdcc339dce332ac893460b5f4cdcf (patch) | |
tree | 2ea257c8240aaec6155992c5dc0231c2f6ef854d /src/theory/rep_set.h | |
parent | 4a919f014c3b6bcdca6bd2f91cfc14d50445887c (diff) |
Add partial support for MBQI with arrays when using --fmf-fmc. Fix constant bounds for bounded integers.
Diffstat (limited to 'src/theory/rep_set.h')
-rw-r--r-- | src/theory/rep_set.h | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index fc8db420d..e703ee467 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -54,16 +54,15 @@ typedef std::vector< int > RepDomain; /** this class iterates over a RepSet */ class RepSetIterator { -private: +public: enum { ENUM_DOMAIN_ELEMENTS, ENUM_RANGE, }; +private: QuantifiersEngine * d_qe; //initialize function bool initialize(); - //enumeration type? - std::vector< int > d_enum_type; //for enum ranges std::map< int, Node > d_lower_bounds; //domain size @@ -82,6 +81,8 @@ public: public: //pointer to model RepSet* d_rep_set; + //enumeration type? + std::vector< int > d_enum_type; //index we are considering std::vector< int > d_index; //types we are considering |