diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-04 16:34:17 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-04 16:34:17 +0100 |
commit | 8494e02bf31a08a686e1cf990e512250a9210acc (patch) | |
tree | c94bd7a5658dfd978cafb13b2b3547e15d790c50 /src/theory/strings/kinds | |
parent | 3e9c44a361d287d30d4aa9771f77677a025a766e (diff) |
More cleanup in strings (#2138)
Diffstat (limited to 'src/theory/strings/kinds')
-rw-r--r-- | src/theory/strings/kinds | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index d931e99bc..de4a013cd 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -28,13 +28,6 @@ operator STRING_ITOS 1 "integer to string" operator STRING_STOI 1 "string to integer (total function)" operator STRING_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise" -#sort CHAR_TYPE \ -# Cardinality::INTEGERS \ -# well-founded \ -# "NodeManager::currentNM()->mkConst(::CVC4::String())" \ -# "util/regexp.h" \ -# "String type" - sort STRING_TYPE \ Cardinality::INTEGERS \ well-founded \ @@ -53,10 +46,6 @@ enumerator STRING_TYPE \ "::CVC4::theory::strings::StringEnumerator" \ "theory/strings/type_enumerator.h" -#enumerator REGEXP_TYPE \ -# "::CVC4::theory::strings::RegExpEnumerator" \ -# "theory/strings/type_enumerator.h" - constant CONST_STRING \ ::CVC4::String \ ::CVC4::strings::StringHashFunction \ |