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.

diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp
index 5641312cb9ae1f958bcd22fa2c36e6232a6fb315..e17879e4d21f4e989a670573fa57b964458d759f 100644 (file)
--- 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 37319a278beb0f821d91109be526621a40f5c456..e6a7eaccdb35b00f9c0b52783384c5e88eca781c 100644 (file)
--- 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: