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 | |
| parent | ea8d376b3153c2902c4ce28185b3f4032ca221c5 (diff) | |
Minor improvements to interface for rep set. (#2435)
Diffstat (limited to 'src/theory')
| -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 # */ |