diff options
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 \ |