3 # For documentation on this file format, please refer to
4 # src/theory/builtin/kinds.
7 theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h"
9 properties check parametric propagate getNextDecisionRequest presolve
11 rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_strings_rewriter.h"
13 typechecker "theory/strings/theory_strings_type_rules.h"
15 operator STRING_CONCAT 2: "string concat (N-ary)"
16 operator STRING_IN_REGEXP 2 "membership"
17 operator STRING_LENGTH 1 "string length"
18 operator STRING_SUBSTR 3 "string substr (user symbol)"
19 operator STRING_SUBSTR_TOTAL 3 "string substr (internal symbol)"
20 operator STRING_CHARAT 2 "string charat (user symbol)"
21 operator STRING_STRCTN 2 "string contains"
22 operator STRING_STRIDOF 3 "string indexof"
23 operator STRING_STRREPL 3 "string replace"
24 operator STRING_PREFIX 2 "string prefixof"
25 operator STRING_SUFFIX 2 "string suffixof"
26 operator STRING_ITOS 1 "integer to string"
27 operator STRING_STOI 1 "string to integer (total function)"
28 operator STRING_U16TOS 1 "uint16 to string"
29 operator STRING_STOU16 1 "string to uint16"
30 operator STRING_U32TOS 1 "uint32 to string"
31 operator STRING_STOU32 1 "string to uint32"
34 # Cardinality::INTEGERS \
36 # "NodeManager::currentNM()->mkConst(::CVC4::String())" \
41 Cardinality::INTEGERS \
43 "NodeManager::currentNM()->mkConst(::CVC4::String())" \
48 Cardinality::INTEGERS \
50 "NodeManager::currentNM()->mkConst(::CVC4::RegExp())" \
54 enumerator STRING_TYPE \
55 "::CVC4::theory::strings::StringEnumerator" \
56 "theory/strings/type_enumerator.h"
58 #enumerator REGEXP_TYPE \
59 # "::CVC4::theory::strings::RegExpEnumerator" \
60 # "theory/strings/type_enumerator.h"
62 constant CONST_STRING \
64 ::CVC4::strings::StringHashFunction \
66 "a string of characters"
68 constant CONST_REGEXP \
70 ::CVC4::RegExpHashFunction \
72 "a regular expression"
74 typerule CONST_STRING ::CVC4::theory::strings::StringConstantTypeRule
75 typerule CONST_REGEXP ::CVC4::theory::strings::RegExpConstantTypeRule
77 # equal equal / less than / output
78 operator STRING_TO_REGEXP 1 "convert string to regexp"
79 operator REGEXP_CONCAT 2: "regexp concat"
80 operator REGEXP_UNION 2: "regexp union"
81 operator REGEXP_INTER 2: "regexp intersection"
82 operator REGEXP_STAR 1 "regexp *"
83 operator REGEXP_PLUS 1 "regexp +"
84 operator REGEXP_OPT 1 "regexp ?"
85 operator REGEXP_RANGE 2 "regexp range"
86 operator REGEXP_LOOP 2:3 "regexp loop"
88 operator REGEXP_EMPTY 0 "regexp empty"
89 operator REGEXP_SIGMA 0 "regexp all characters"
92 operator REGEXP_RV 1 "regexp rv (internal use only)"
93 typerule REGEXP_RV ::CVC4::theory::strings::RegExpRVTypeRule
96 typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule
97 typerule REGEXP_UNION ::CVC4::theory::strings::RegExpUnionTypeRule
98 typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule
99 typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule
100 typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule
101 typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule
102 typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule
103 typerule REGEXP_LOOP ::CVC4::theory::strings::RegExpLoopTypeRule
105 typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
107 typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
108 typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
109 typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
110 typerule STRING_SUBSTR_TOTAL ::CVC4::theory::strings::StringSubstrTypeRule
111 typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
112 typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
113 typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
114 typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
115 typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule
116 typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule
117 typerule STRING_ITOS ::CVC4::theory::strings::StringIntToStrTypeRule
118 typerule STRING_STOI ::CVC4::theory::strings::StringStrToIntTypeRule
119 typerule STRING_U16TOS ::CVC4::theory::strings::StringIntToStrTypeRule
120 typerule STRING_STOU16 ::CVC4::theory::strings::StringStrToIntTypeRule
121 typerule STRING_U32TOS ::CVC4::theory::strings::StringIntToStrTypeRule
122 typerule STRING_STOU32 ::CVC4::theory::strings::StringStrToIntTypeRule
124 typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
126 typerule REGEXP_EMPTY ::CVC4::theory::strings::EmptyRegExpTypeRule
127 typerule REGEXP_SIGMA ::CVC4::theory::strings::SigmaRegExpTypeRule