diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-09 16:23:59 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-09 16:24:43 -0600 |
| commit | 12dae128053342fef8af2f560fd98e1ab6a71cca (patch) | |
| tree | 96d854b38d819affe72d551aee70315821e21e57 /src/theory/strings/kinds | |
| parent | 780448ae48ed8755b11570a6843ab6871d94abef (diff) | |
add constant replace, indexof
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 a421d6fa8..9e0897c00 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -15,7 +15,9 @@ operator STRING_IN_REGEXP 2 "membership" operator STRING_LENGTH 1 "string length" operator STRING_SUBSTR 3 "string substr" operator STRING_STRCTN 2 "string contains" -operator STRING_CHARAT 2 "string char at" +operator STRING_CHARAT 2 "string charat" +operator STRING_STRIDOF 3 "string indexof" +operator STRING_STRREPL 3 "string replace" #sort CHAR_TYPE \ # Cardinality::INTEGERS \ @@ -105,6 +107,8 @@ typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule +typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule +typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule |