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.h | |
parent | ea8d376b3153c2902c4ce28185b3f4032ca221c5 (diff) |
Minor improvements to interface for rep set. (#2435)
Diffstat (limited to 'src/theory/rep_set.h')
-rw-r--r-- | src/theory/rep_set.h | 8 |
1 files changed, 5 insertions, 3 deletions
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 # */ |