diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-23 18:50:16 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-23 23:50:16 +0000 |
commit | 421803a044faf8f17ebf6d44f94adbdfdbded4a6 (patch) | |
tree | 6d622ae107c5aacf83d383c04fc3402fbfe97f6e | |
parent | 07a47262c405fb37248572d3029883d078273cd7 (diff) |
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.
-rw-r--r-- | src/theory/strings/type_enumerator.cpp | 23 | ||||
-rw-r--r-- | src/theory/strings/type_enumerator.h | 18 |
2 files changed, 41 insertions, 0 deletions
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: |