diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-06-01 15:51:39 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-06-01 15:51:47 -0500 |
commit | 6edc4fac0e5c868b6c6bad13ffc9112b16c1d5f5 (patch) | |
tree | 2d89d797c3b2cf856be60234013c7dae9efae258 /src/theory/rep_set.h | |
parent | ae5236eeda43ff591b9264d653727d4ae7d1de68 (diff) |
Initial infrastructure for bounded set quantification (disabled). Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers.
Diffstat (limited to 'src/theory/rep_set.h')
-rw-r--r-- | src/theory/rep_set.h | 55 |
1 files changed, 33 insertions, 22 deletions
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 08fc7dd52..ee927de86 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -64,22 +64,42 @@ class RepSetIterator { public: enum { ENUM_DOMAIN_ELEMENTS, - ENUM_RANGE, + ENUM_INT_RANGE, + ENUM_SET_MEMBERS, }; private: QuantifiersEngine * d_qe; //initialize function bool initialize(); - //for enum ranges + //for int ranges std::map< int, Node > d_lower_bounds; + //for set ranges + std::map< int, std::vector< Node > > d_setm_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 ); + //reset index, 1:success, 0:empty, -1:fail + int resetIndex( int i, bool initial = false ); /** set index order */ void setIndexOrder( std::vector< int >& indexOrder ); + /** do reset increment the iterator at index=counter */ + int do_reset_increment( int counter, bool initial = false ); + //ordering for variables we are indexing over + // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 }, + // then we consider instantiations in this order: + // a/x a/y a/z + // a/x b/y a/z + // b/x a/y a/z + // b/x b/y a/z + // ... + std::vector< int > d_index_order; + //variables to index they are considered at + // 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; + //are we only considering a strict subset of the domain of the quantifier? + bool d_incomplete; public: RepSetIterator( QuantifiersEngine * qe, RepSet* rs ); ~RepSetIterator(){} @@ -92,43 +112,34 @@ public: RepSet* d_rep_set; //enumeration type? std::vector< int > d_enum_type; - //index we are considering + //current tuple we are considering std::vector< int > d_index; //types we are considering std::vector< TypeNode > d_types; //domain we are considering std::vector< RepDomain > d_domain; - //are we only considering a strict subset of the domain of the quantifier? - bool d_incomplete; - //ordering for variables we are indexing over - // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 }, - // then we consider instantiations in this order: - // a/x a/y a/z - // a/x b/y a/z - // b/x a/y a/z - // b/x b/y a/z - // ... - std::vector< int > d_index_order; - //variables to index they are considered at - // 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: /** increment the iterator at index=counter */ - int increment2( int counter ); + int increment2( int i ); /** increment the iterator */ int increment(); /** is the iterator finished? */ bool isFinished(); /** get the i_th term we are considering */ - Node getTerm( int i ); + Node getCurrentTerm( int v ); /** get the number of terms we are considering */ int getNumTerms() { return (int)d_index_order.size(); } /** debug print */ void debugPrint( const char* c ); void debugPrintSmall( const char* c ); + //get index order, returns var # + int getIndexOrder( int v ) { return d_index_order[v]; } + //get variable order, returns index # + int getVariableOrder( int i ) { return d_var_order[i]; } + //is incomplete + bool isIncomplete() { return d_incomplete; } };/* class RepSetIterator */ }/* CVC4::theory namespace */ |