diff options
Diffstat (limited to 'src/theory/strings/kinds')
| -rw-r--r-- | src/theory/strings/kinds | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 34237f69e..d931e99bc 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -18,6 +18,8 @@ operator STRING_LENGTH 1 "string length" operator STRING_SUBSTR 3 "string substr" operator STRING_CHARAT 2 "string charat" operator STRING_STRCTN 2 "string contains" +operator STRING_LT 2 "string less than" +operator STRING_LEQ 2 "string less than or equal" operator STRING_STRIDOF 3 "string indexof" operator STRING_STRREPL 3 "string replace" operator STRING_PREFIX 2 "string prefixof" @@ -97,7 +99,9 @@ typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule -typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule +typerule STRING_STRCTN ::CVC4::theory::strings::StringRelationTypeRule +typerule STRING_LT ::CVC4::theory::strings::StringRelationTypeRule +typerule STRING_LEQ ::CVC4::theory::strings::StringRelationTypeRule typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule |