arrays: Move type enumerator implementation to .cpp. (#7216)

This further cleans up the class declaration in the header to comply
with code style guidelines.

3 files changed, 184 insertions, 119 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5dbaa3349..9b2e2e8e2 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -543,6 +543,7 @@ libcvc5_add_sources(
   theory/arrays/theory_arrays_type_rules.cpp
   theory/arrays/theory_arrays_type_rules.h
   theory/arrays/type_enumerator.h
+  theory/arrays/type_enumerator.cpp
   theory/arrays/union_find.cpp
   theory/arrays/union_find.h
   theory/assertion.cpp
diff --git a/src/theory/arrays/type_enumerator.cpp b/src/theory/arrays/type_enumerator.cpp
new file mode 100644
index 000000000..c1187f0da
--- /dev/null
+++ b/src/theory/arrays/type_enumerator.cpp
@@ -0,0 +1,159 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Clark Barrett, Morgan Deters
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * An enumerator for arrays.
+ */
+#include "theory/arrays/type_enumerator.h"
+
+#include "expr/array_store_all.h"
+#include "expr/kind.h"
+#include "expr/type_node.h"
+#include "theory/rewriter.h"
+#include "theory/type_enumerator.h"
+
+namespace cvc5 {
+namespace theory {
+namespace arrays {
+
+ArrayEnumerator::ArrayEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
+    : TypeEnumeratorBase<ArrayEnumerator>(type),
+      d_tep(tep),
+      d_index(type.getArrayIndexType(), tep),
+      d_constituentType(type.getArrayConstituentType()),
+      d_nm(NodeManager::currentNM()),
+      d_indexVec(),
+      d_constituentVec(),
+      d_finished(false),
+      d_arrayConst()
+{
+  d_indexVec.push_back(*d_index);
+  d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
+  d_arrayConst =
+      d_nm->mkConst(ArrayStoreAll(type, (*(*d_constituentVec.back()))));
+  Trace("array-type-enum") << "Array const : " << d_arrayConst << std::endl;
+}
+
+ArrayEnumerator::ArrayEnumerator(const ArrayEnumerator& ae)
+    : TypeEnumeratorBase<ArrayEnumerator>(
+        ae.d_nm->mkArrayType(ae.d_index.getType(), ae.d_constituentType)),
+      d_tep(ae.d_tep),
+      d_index(ae.d_index),
+      d_constituentType(ae.d_constituentType),
+      d_nm(ae.d_nm),
+      d_indexVec(ae.d_indexVec),
+      d_constituentVec(),  // copied below
+      d_finished(ae.d_finished),
+      d_arrayConst(ae.d_arrayConst)
+{
+  for (std::vector<TypeEnumerator*>::const_iterator
+           i = ae.d_constituentVec.begin(),
+           i_end = ae.d_constituentVec.end();
+       i != i_end;
+       ++i)
+  {
+    d_constituentVec.push_back(new TypeEnumerator(**i));
+  }
+}
+
+ArrayEnumerator::~ArrayEnumerator()
+{
+  while (!d_constituentVec.empty())
+  {
+    delete d_constituentVec.back();
+    d_constituentVec.pop_back();
+  }
+}
+
+Node ArrayEnumerator::operator*()
+{
+  if (d_finished)
+  {
+    throw NoMoreValuesException(getType());
+  }
+  Node n = d_arrayConst;
+  for (size_t i = 0, size = d_indexVec.size(); i < size; ++i)
+  {
+    n = d_nm->mkNode(kind::STORE,
+                     n,
+                     d_indexVec[d_indexVec.size() - 1 - i],
+                     *(*(d_constituentVec[i])));
+  }
+  Trace("array-type-enum") << "operator * prerewrite: " << n << std::endl;
+  n = Rewriter::rewrite(n);
+  Trace("array-type-enum") << "operator * returning: " << n << std::endl;
+  return n;
+}
+
+ArrayEnumerator& ArrayEnumerator::operator++()
+{
+  Trace("array-type-enum") << "operator++ called, **this = " << **this
+                           << std::endl;
+
+  if (d_finished)
+  {
+    Trace("array-type-enum") << "operator++ finished!" << std::endl;
+    return *this;
+  }
+  while (!d_constituentVec.empty())
+  {
+    ++(*d_constituentVec.back());
+    if (d_constituentVec.back()->isFinished())
+    {
+      delete d_constituentVec.back();
+      d_constituentVec.pop_back();
+    }
+    else
+    {
+      break;
+    }
+  }
+
+  if (d_constituentVec.empty())
+  {
+    ++d_index;
+    if (d_index.isFinished())
+    {
+      Trace("array-type-enum") << "operator++ finished!" << std::endl;
+      d_finished = true;
+      return *this;
+    }
+    d_indexVec.push_back(*d_index);
+    d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
+    ++(*d_constituentVec.back());
+    if (d_constituentVec.back()->isFinished())
+    {
+      Trace("array-type-enum") << "operator++ finished!" << std::endl;
+      d_finished = true;
+      return *this;
+    }
+  }
+
+  while (d_constituentVec.size() < d_indexVec.size())
+  {
+    d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
+  }
+
+  Trace("array-type-enum") << "operator++ returning, **this = " << **this
+                           << std::endl;
+  return *this;
+}
+
+bool ArrayEnumerator::isFinished()
+{
+  Trace("array-type-enum") << "isFinished returning: " << d_finished
+                           << std::endl;
+  return d_finished;
+}
+
+}  // namespace arrays
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index 6fc026b19..097b16184 100644
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -28,9 +28,29 @@ namespace cvc5 {
 namespace theory {
 namespace arrays {
 
-class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
-  /** type properties */
-  TypeEnumeratorProperties * d_tep;
+class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator>
+{
+ public:
+  /** Constructor. */
+  ArrayEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr);
+
+  /**
+   * Copy Constructor.
+   * An array enumerator could be large, and generally you don't want to
+   * go around copying these things; but a copy ctor is presently required
+   * by the TypeEnumerator framework.
+   */
+  ArrayEnumerator(const ArrayEnumerator& ae);
+
+  /** Destructor. */
+  ~ArrayEnumerator();
+
+  Node operator*() override;
+  ArrayEnumerator& operator++() override;
+  bool isFinished() override;
+
+ private:
+  TypeEnumeratorProperties* d_tep;
   TypeEnumerator d_index;
   TypeNode d_constituentType;
   NodeManager* d_nm;
@@ -38,122 +58,7 @@ class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
   std::vector<TypeEnumerator*> d_constituentVec;
   bool d_finished;
   Node d_arrayConst;
-
- public:
-  ArrayEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
-      : TypeEnumeratorBase<ArrayEnumerator>(type),
-        d_tep(tep),
-        d_index(type.getArrayIndexType(), tep),
-        d_constituentType(type.getArrayConstituentType()),
-        d_nm(NodeManager::currentNM()),
-        d_indexVec(),
-        d_constituentVec(),
-        d_finished(false),
-        d_arrayConst()
-  {
-    d_indexVec.push_back(*d_index);
-    d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
-    d_arrayConst =
-        d_nm->mkConst(ArrayStoreAll(type, (*(*d_constituentVec.back()))));
-    Trace("array-type-enum") << "Array const : " << d_arrayConst << std::endl;
-  }
-
-  // An array enumerator could be large, and generally you don't want to
-  // go around copying these things; but a copy ctor is presently required
-  // by the TypeEnumerator framework.
-  ArrayEnumerator(const ArrayEnumerator& ae)
-      : TypeEnumeratorBase<ArrayEnumerator>(
-            ae.d_nm->mkArrayType(ae.d_index.getType(), ae.d_constituentType)),
-        d_tep(ae.d_tep),
-        d_index(ae.d_index),
-        d_constituentType(ae.d_constituentType),
-        d_nm(ae.d_nm),
-        d_indexVec(ae.d_indexVec),
-        d_constituentVec(),  // copied below
-        d_finished(ae.d_finished),
-        d_arrayConst(ae.d_arrayConst)
-  {
-    for(std::vector<TypeEnumerator*>::const_iterator i =
-          ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end();
-        i != i_end;
-        ++i) {
-      d_constituentVec.push_back(new TypeEnumerator(**i));
-    }
-  }
-
-  ~ArrayEnumerator() {
-    while (!d_constituentVec.empty()) {
-      delete d_constituentVec.back();
-      d_constituentVec.pop_back();
-    }
-  }
-
-  Node operator*() override
-  {
-    if (d_finished) {
-      throw NoMoreValuesException(getType());
-    }
-    Node n = d_arrayConst;
-    for (unsigned i = 0; i < d_indexVec.size(); ++i) {
-      n = d_nm->mkNode(kind::STORE, n, d_indexVec[d_indexVec.size() - 1 - i], *(*(d_constituentVec[i])));
-    }
-    Trace("array-type-enum") << "operator * prerewrite: " << n << std::endl;
-    n = Rewriter::rewrite(n);
-    Trace("array-type-enum") << "operator * returning: " << n << std::endl;
-    return n;
-  }
-
-  ArrayEnumerator& operator++() override
-  {
-    Trace("array-type-enum") << "operator++ called, **this = " << **this << std::endl;
-
-    if (d_finished) {
-      Trace("array-type-enum") << "operator++ finished!" << std::endl;
-      return *this;
-    }
-    while (!d_constituentVec.empty()) {
-      ++(*d_constituentVec.back());
-      if (d_constituentVec.back()->isFinished()) {
-        delete d_constituentVec.back();
-        d_constituentVec.pop_back();
-      }
-      else {
-        break;
-      }
-    }
-
-    if (d_constituentVec.empty()) {
-      ++d_index;
-      if (d_index.isFinished()) {
-        Trace("array-type-enum") << "operator++ finished!" << std::endl;
-        d_finished = true;
-        return *this;
-      }
-      d_indexVec.push_back(*d_index);
-      d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
-      ++(*d_constituentVec.back());
-      if (d_constituentVec.back()->isFinished()) {
-        Trace("array-type-enum") << "operator++ finished!" << std::endl;
-        d_finished = true;
-        return *this;
-      }
-    }
-
-    while (d_constituentVec.size() < d_indexVec.size()) {
-      d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
-    }
-
-    Trace("array-type-enum") << "operator++ returning, **this = " << **this << std::endl;
-    return *this;
-  }
-
-  bool isFinished() override
-  {
-    Trace("array-type-enum") << "isFinished returning: " << d_finished << std::endl;
-    return d_finished;
-  }
-
-};/* class ArrayEnumerator */
+}; /* class ArrayEnumerator */
 
 }  // namespace arrays
 }  // namespace theory