diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-10 16:20:42 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-10 16:20:42 -0400 |
| commit | c30a3426c7c2cbaff88b5183b8d8c368a393ac4d (patch) | |
| tree | bd621f3766d2ae330a6c11499fe0a49958afa95d /src/theory/strings/kinds | |
| parent | d4f76fdfaed04bf63bb609a5fd26b0d45a9e94f4 (diff) | |
| parent | e926fd162c6cee95d31044305e3b4df90b59f9fc (diff) | |
Merge remote-tracking branch 'origin/master' into segfaultfix
Diffstat (limited to 'src/theory/strings/kinds')
| -rw-r--r-- | src/theory/strings/kinds | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 48e9957d4..3134fcab0 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -1,4 +1,7 @@ -# kinds [for strings theory] +# kinds -*- sh -*- +# +# For documentation on this file format, please refer to +# src/theory/builtin/kinds. # theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h" @@ -9,8 +12,7 @@ rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_s typechecker "theory/strings/theory_strings_type_rules.h" - -operator STRING_CONCAT 2: "string concat" +operator STRING_CONCAT 2: "string concat (N-ary)" operator STRING_IN_REGEXP 2 "membership" operator STRING_LENGTH 1 "string length" operator STRING_SUBSTR 3 "string substr (user symbol)" @@ -97,7 +99,6 @@ typerule REGEXP_LOOP ::CVC4::theory::strings::RegExpLoopTypeRule 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 |