summaryrefslogtreecommitdiff
path: root/src/theory/strings/kinds
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/kinds')
-rw-r--r--src/theory/strings/kinds4
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index b30bf8f36..e55891ec2 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -14,9 +14,7 @@ operator STRING_CONCAT 2: "string concat"
operator STRING_IN_REGEXP 2 "membership"
operator STRING_LENGTH 1 "string length"
operator STRING_SUBSTR 3 "string substr (user symbol)"
-operator STRING_SUBSTR_TOTAL 3 "string substr (internal symbol)"
operator STRING_CHARAT 2 "string charat (user symbol)"
-operator STRING_CHARAT_TOTAL 2 "string charat (internal symbol)"
operator STRING_STRCTN 2 "string contains"
operator STRING_STRIDOF 3 "string indexof"
operator STRING_STRREPL 3 "string replace"
@@ -107,9 +105,7 @@ typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
-typerule STRING_SUBSTR_TOTAL ::CVC4::theory::strings::StringSubstrTypeRule
typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
-typerule STRING_CHARAT_TOTAL ::CVC4::theory::strings::StringCharAtTypeRule
typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback