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"
19 operator STRING_CHARAT 2 "string charat"
20 operator STRING_STRCTN 2 "string contains"
21 operator STRING_STRIDOF 3 "string indexof"
22 operator STRING_STRREPL 3 "string replace"
23 operator STRING_PREFIX 2 "string prefixof"
24 operator STRING_SUFFIX 2 "string suffixof"
25 operator STRING_ITOS 1 "integer to string"
26 operator STRING_STOI 1 "string to integer (total function)"
29 # Cardinality::INTEGERS \
31 # "NodeManager::currentNM()->mkConst(::CVC4::String())" \
36 Cardinality::INTEGERS \
38 "NodeManager::currentNM()->mkConst(::CVC4::String())" \
43 Cardinality::INTEGERS \
45 "NodeManager::currentNM()->mkConst(::CVC4::RegExp())" \
49 enumerator STRING_TYPE \
50 "::CVC4::theory::strings::StringEnumerator" \
51 "theory/strings/type_enumerator.h"
53 #enumerator REGEXP_TYPE \
54 # "::CVC4::theory::strings::RegExpEnumerator" \
55 # "theory/strings/type_enumerator.h"
57 constant CONST_STRING \
59 ::CVC4::strings::StringHashFunction \
61 "a string of characters"
63 constant CONST_REGEXP \
65 ::CVC4::RegExpHashFunction \
67 "a regular expression"
69 typerule CONST_STRING ::CVC4::theory::strings::StringConstantTypeRule
70 typerule CONST_REGEXP ::CVC4::theory::strings::RegExpConstantTypeRule
72 # equal equal / less than / output
73 operator STRING_TO_REGEXP 1 "convert string to regexp"
74 operator REGEXP_CONCAT 2: "regexp concat"
75 operator REGEXP_UNION 2: "regexp union"
76 operator REGEXP_INTER 2: "regexp intersection"
77 operator REGEXP_STAR 1 "regexp *"
78 operator REGEXP_PLUS 1 "regexp +"
79 operator REGEXP_OPT 1 "regexp ?"
80 operator REGEXP_RANGE 2 "regexp range"
81 operator REGEXP_LOOP 2:3 "regexp loop"
83 operator REGEXP_EMPTY 0 "regexp empty"
84 operator REGEXP_SIGMA 0 "regexp all characters"
87 operator REGEXP_RV 1 "regexp rv (internal use only)"
88 typerule REGEXP_RV ::CVC4::theory::strings::RegExpRVTypeRule
91 typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule
92 typerule REGEXP_UNION ::CVC4::theory::strings::RegExpUnionTypeRule
93 typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule
94 typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule
95 typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule
96 typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule
97 typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule
98 typerule REGEXP_LOOP ::CVC4::theory::strings::RegExpLoopTypeRule
100 typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
102 typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
103 typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
104 typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
105 typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
106 typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
107 typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
108 typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
109 typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule
110 typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule
111 typerule STRING_ITOS ::CVC4::theory::strings::StringIntToStrTypeRule
112 typerule STRING_STOI ::CVC4::theory::strings::StringStrToIntTypeRule
114 typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
116 typerule REGEXP_EMPTY ::CVC4::theory::strings::EmptyRegExpTypeRule
117 typerule REGEXP_SIGMA ::CVC4::theory::strings::SigmaRegExpTypeRule