diff options
| -rw-r--r-- | src/theory/rep_set.cpp | 10 | ||||
| -rw-r--r-- | src/theory/rep_set.h | 8 |
2 files changed, 14 insertions, 4 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; diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 29cca462a..d5de1e520 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -148,7 +148,7 @@ public: }; public: - RepSetIterator(const RepSet* rs, RepBoundExt* rext); + RepSetIterator(const RepSet* rs, RepBoundExt* rext = nullptr); ~RepSetIterator() {} /** set that this iterator will be iterating over instantiations for a * quantifier */ @@ -168,9 +168,11 @@ public: /** get domain size of the i^th field of this iterator */ unsigned domainSize(unsigned i); /** get the i^th term in the tuple we are considering */ - Node getCurrentTerm(unsigned v, bool valTerm = false); + Node getCurrentTerm(unsigned v, bool valTerm = false) const; /** get the number of terms in the tuple we are considering */ - unsigned getNumTerms() { return d_index_order.size(); } + unsigned getNumTerms() const { return d_index_order.size(); } + /** get current terms */ + void getCurrentTerms(std::vector<Node>& terms) const; /** get index order, returns var # */ unsigned getIndexOrder(unsigned v) { return d_index_order[v]; } /** get variable order, returns index # */ |