diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-12-26 17:18:26 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-12-26 17:18:26 -0600 |
| commit | cac85606876d4f0be1c6c54172f7509ce54cdcb5 (patch) | |
| tree | b25e27922f6039f5ec1c5e600932bd497b4f273e /src/theory/strings/kinds | |
| parent | 97b04f18011a56e11fc5057b304fff9e9ab4e753 (diff) | |
new functions in strings
Diffstat (limited to 'src/theory/strings/kinds')
| -rw-r--r-- | src/theory/strings/kinds | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 20db916c9..a421d6fa8 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -11,12 +11,11 @@ typechecker "theory/strings/theory_strings_type_rules.h" operator STRING_CONCAT 2: "string concat" - 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" #sort CHAR_TYPE \ # Cardinality::INTEGERS \ @@ -104,6 +103,8 @@ 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_STRCTN ::CVC4::theory::strings::StringContainTypeRule +typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule |