From 421803a044faf8f17ebf6d44f94adbdfdbded4a6 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 23 Sep 2021 18:50:16 -0500
Subject: [PATCH] Generalize string enumerator for fixed length sequences
 (#7234)

This adds a utility to get enumerators for fixed length constants of a given sequence type.

This will be used to construct fixed length gaps in array models.
---
 src/theory/strings/type_enumerator.cpp | 23 +++++++++++++++++++++++
 src/theory/strings/type_enumerator.h   | 18 ++++++++++++++++++
 2 files changed, 41 insertions(+)

diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp
index 5641312cb..e17879e4d 100644
--- a/src/theory/strings/type_enumerator.cpp
+++ b/src/theory/strings/type_enumerator.cpp
@@ -225,6 +225,29 @@ void SeqEnumLen::mkCurr()
       Sequence(d_type.getSequenceElementType(), seq));
 }
 
+SEnumLenSet::SEnumLenSet(TypeEnumeratorProperties* tep) : d_tep(tep) {}
+
+SEnumLen* SEnumLenSet::getEnumerator(size_t len, TypeNode tn)
+{
+  std::pair<size_t, TypeNode> key(len, tn);
+  std::map<std::pair<size_t, TypeNode>, std::unique_ptr<SEnumLen> >::iterator
+      it = d_sels.find(key);
+  if (it != d_sels.end())
+  {
+    return it->second.get();
+  }
+  if (tn.isString())  // string-only
+  {
+    d_sels[key].reset(
+        new StringEnumLen(len, len, utils::getAlphabetCardinality()));
+  }
+  else
+  {
+    d_sels[key].reset(new SeqEnumLen(tn, d_tep, len, len));
+  }
+  return d_sels[key].get();
+}
+
 StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
     : TypeEnumeratorBase<StringEnumerator>(type),
       d_wenum(0, utils::getAlphabetCardinality())
diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h
index 37319a278..e6a7eaccd 100644
--- a/src/theory/strings/type_enumerator.h
+++ b/src/theory/strings/type_enumerator.h
@@ -165,6 +165,24 @@ class SeqEnumLen : public SEnumLen
   void mkCurr();
 };
 
+/** Set of the above class */
+class SEnumLenSet
+{
+ public:
+  /** constructor */
+  SEnumLenSet(TypeEnumeratorProperties* tep = nullptr);
+  /** destructor */
+  ~SEnumLenSet() {}
+  /** Get enumerator for length, type */
+  SEnumLen* getEnumerator(size_t len, TypeNode tn);
+
+ private:
+  /** an enumerator for the element's type */
+  TypeEnumeratorProperties* d_tep;
+  /** for each start length, type */
+  std::map<std::pair<size_t, TypeNode>, std::unique_ptr<SEnumLen> > d_sels;
+};
+
 class StringEnumerator : public TypeEnumeratorBase<StringEnumerator>
 {
  public:
-- 
2.30.2