diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-11 19:58:10 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-11 19:58:10 -0500 |
commit | d44ef0e9af9230e1949b0d3d4b03f1fcd497ad6d (patch) | |
tree | 8de50a73a0730c9f9966b8605de4cd540a075001 /src/theory/rep_set.h | |
parent | dc3cee7cf3d49ad592139042a8e15e3905e55ee9 (diff) |
Refactoring finite bounds in Quantifiers Engine (#3261)
Diffstat (limited to 'src/theory/rep_set.h')
-rw-r--r-- | src/theory/rep_set.h | 30 |
1 files changed, 19 insertions, 11 deletions
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index d972a7a84..2ae5e1c4b 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -121,6 +121,22 @@ typedef std::vector< int > RepDomain; class RepBoundExt; +/** + * Representative set iterator enumeration type, which indicates how the + * bound on a variable was determined. + */ +enum RsiEnumType +{ + // the bound on the variable is invalid + ENUM_INVALID = 0, + // the bound on the variable was determined in the default way, i.e. based + // on an enumeration of terms in the model. + ENUM_DEFAULT, + // The bound on the variable was determined in a custom way, i.e. via a + // quantifiers module like the BoundedIntegers module. + ENUM_CUSTOM, +}; + /** Rep set iterator. * * This class is used for iterating over (tuples of) terms @@ -140,14 +156,6 @@ class RepBoundExt; */ class RepSetIterator { public: - enum RsiEnumType - { - ENUM_INVALID = 0, - ENUM_DEFAULT, - ENUM_BOUND_INT, - }; - -public: RepSetIterator(const RepSet* rs, RepBoundExt* rext = nullptr); ~RepSetIterator() {} /** set that this iterator will be iterating over instantiations for a @@ -264,9 +272,9 @@ class RepBoundExt * iterating over domain elements of the type * of its i^th bound variable. */ - virtual RepSetIterator::RsiEnumType setBound(Node owner, - unsigned i, - std::vector<Node>& elements) = 0; + virtual RsiEnumType setBound(Node owner, + unsigned i, + std::vector<Node>& elements) = 0; /** reset index * * This method initializes iteration for the i^th |