Minor improvements to interface for rep set. (#2435)

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 7fa22e418eb731debb063deb9f7847e2ddc1c597..dcd90c236a20ffdd0232ba018f073bdbc1215934 100644 (file)
--- 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 29cca462a42b7f865b6668c28adfc653125a19ad..d5de1e520dfd338e8d8dafbcd912814e3745031b 100644 (file)
--- 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 # */