diff options
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; |