Merge branch 'master' into fixErrorSetfixErrorSet

1 files changed, 49 insertions, 0 deletions

diff --git a/src/theory/strings/regexp_enumerator.cpp b/src/theory/strings/regexp_enumerator.cpp
new file mode 100644
index 000000000..261d0008e
--- /dev/null
+++ b/src/theory/strings/regexp_enumerator.cpp
@@ -0,0 +1,49 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Implementation of enumerator for regular expressions.
+ */
+
+#include "theory/strings/regexp_enumerator.h"
+
+namespace cvc5 {
+namespace theory {
+namespace strings {
+
+RegExpEnumerator::RegExpEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
+    : TypeEnumeratorBase<RegExpEnumerator>(type), d_senum(type, tep)
+{
+}
+
+RegExpEnumerator::RegExpEnumerator(const RegExpEnumerator& enumerator)
+    : TypeEnumeratorBase<RegExpEnumerator>(enumerator.getType()),
+      d_senum(enumerator.d_senum)
+{
+}
+
+Node RegExpEnumerator::operator*()
+{
+  NodeManager* nm = NodeManager::currentNM();
+  return nm->mkNode(kind::STRING_TO_REGEXP, *d_senum);
+}
+
+RegExpEnumerator& RegExpEnumerator::operator++()
+{
+  ++d_senum;
+  return *this;
+}
+
+bool RegExpEnumerator::isFinished() { return d_senum.isFinished(); }
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace cvc5