diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-19 16:48:10 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-19 16:48:10 -0500 |
| commit | 22780596b561dff9b0eb5b0620252280a678944e (patch) | |
| tree | 796c7a3a270f0509f36762ba88e938c644d9dfd4 /src/theory/strings/regexp_operation.cpp | |
| parent | e0633c091c37b79f9e3a2517cf95113c788db083 (diff) | |
Convert more uses of strings to words (#4584)
Towards theory of sequences.
This PR also adds support for sequences in default sygus grammars.
Also removes an interface for mkEmptyWord which doesn't have an equivalent for sequences.
Diffstat (limited to 'src/theory/strings/regexp_operation.cpp')
| -rw-r--r-- | src/theory/strings/regexp_operation.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index f43babad2..a91210a7b 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -40,7 +40,7 @@ RegExpOpr::RegExpOpr() std::vector<Node>{})), d_sigma_star(NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, d_sigma)) { - d_emptyString = Word::mkEmptyWord(CONST_STRING); + d_emptyString = Word::mkEmptyWord(NodeManager::currentNM()->stringType()); d_emptySingleton = NodeManager::currentNM()->mkNode(STRING_TO_REGEXP, d_emptyString); |