diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-06 08:14:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-09-06 08:14:08 -0500 |
| commit | 793321a0b4f9d02eb1ba7e416bd2d9fcb407ddf7 (patch) | |
| tree | 907d9b48348fc9289b1ebefe0995ce4bf32dda70 /src/theory/rep_set.cpp | |
| parent | ea8d376b3153c2902c4ce28185b3f4032ca221c5 (diff) | |
Minor improvements to interface for rep set. (#2435)
Diffstat (limited to 'src/theory/rep_set.cpp')
| -rw-r--r-- | src/theory/rep_set.cpp | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 7fa22e418..dcd90c236 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -403,7 +403,7 @@ int RepSetIterator::increment(){ bool RepSetIterator::isFinished() const { return d_index.empty(); } -Node RepSetIterator::getCurrentTerm(unsigned v, bool valTerm) +Node RepSetIterator::getCurrentTerm(unsigned v, bool valTerm) const { unsigned ii = d_index_order[v]; unsigned curr = d_index[ii]; @@ -422,6 +422,14 @@ Node RepSetIterator::getCurrentTerm(unsigned v, bool valTerm) return t; } +void RepSetIterator::getCurrentTerms(std::vector<Node>& terms) const +{ + for (unsigned i = 0, size = d_index_order.size(); i < size; i++) + { + terms.push_back(getCurrentTerm(i)); + } +} + void RepSetIterator::debugPrint( const char* c ){ for( unsigned v=0; v<d_index.size(); v++ ){ Debug( c ) << v << " : " << getCurrentTerm( v ) << std::endl; |