diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-26 14:40:05 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-26 14:40:16 -0500 |
commit | 0a6fa189e4e2dc2c47f4050df0aad4a6f3d39b4b (patch) | |
tree | cdd99891d51b025e207e8b56c34bb13d77977a4a /src/theory/rep_set.h | |
parent | 323c4ebc21ca9e85b76aadc2168a496404bf91fc (diff) |
Add support for interval models in bounded integers MBQI (in progress).
Diffstat (limited to 'src/theory/rep_set.h')
-rw-r--r-- | src/theory/rep_set.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 672f33b54..a619915ee 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -71,6 +71,8 @@ private: Node d_owner; //reset index bool resetIndex( int i, bool initial = false ); + /** set index order */ + void setIndexOrder( std::vector< int >& indexOrder ); public: RepSetIterator( QuantifiersEngine * qe, RepSet* rs ); ~RepSetIterator(){} @@ -104,9 +106,9 @@ public: // for example, if d_index_order = { 2, 0, 1 } // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 } std::map< int, int > d_var_order; + //intervals + std::map< int, Node > d_bounds[2]; public: - /** set index order */ - void setIndexOrder( std::vector< int >& indexOrder ); /** increment the iterator at index=counter */ int increment2( int counter ); /** increment the iterator */ |