From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 6 Sep 2018 13:14:08 +0000 (-0500)
Subject: Minor improvements to interface for rep set. (#2435)
X-Git-Tag: cvc5-1.0.0~4674
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=793321a0b4f9d02eb1ba7e416bd2d9fcb407ddf7;p=cvc5.git

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

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 # */