1 # kinds [for strings theory]
4 theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h"
6 properties check parametric propagate getNextDecisionRequest presolve
8 rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_strings_rewriter.h"
10 typechecker "theory/strings/theory_strings_type_rules.h"
13 operator STRING_CONCAT 2: "string concat"
14 operator STRING_IN_REGEXP 2 "membership"
15 operator STRING_LENGTH 1 "string length"
16 operator STRING_SUBSTR 3 "string substr (user symbol)"
17 operator STRING_SUBSTR_TOTAL 3 "string substr (internal symbol)"
18 operator STRING_CHARAT 2 "string charat (user symbol)"
19 operator STRING_STRCTN 2 "string contains"
20 operator STRING_STRIDOF 3 "string indexof"
21 operator STRING_STRREPL 3 "string replace"
22 operator STRING_PREFIX 2 "string prefixof"
23 operator STRING_SUFFIX 2 "string suffixof"
24 operator STRING_ITOS 1 "integer to string"
25 operator STRING_STOI 1 "string to integer (total function)"
28 # Cardinality::INTEGERS \
30 # "NodeManager::currentNM()->mkConst(::CVC4::String())" \
35 Cardinality::INTEGERS \
37 "NodeManager::currentNM()->mkConst(::CVC4::String())" \
42 Cardinality::INTEGERS \
44 "NodeManager::currentNM()->mkConst(::CVC4::RegExp())" \
48 enumerator STRING_TYPE \
49 "::CVC4::theory::strings::StringEnumerator" \
50 "theory/strings/type_enumerator.h"
52 #enumerator REGEXP_TYPE \
53 # "::CVC4::theory::strings::RegExpEnumerator" \
54 # "theory/strings/type_enumerator.h"
56 constant CONST_STRING \
58 ::CVC4::strings::StringHashFunction \
60 "a string of characters"
62 constant CONST_REGEXP \
64 ::CVC4::RegExpHashFunction \
66 "a regular expression"
68 typerule CONST_STRING ::CVC4::theory::strings::StringConstantTypeRule
69 typerule CONST_REGEXP ::CVC4::theory::strings::RegExpConstantTypeRule
71 # equal equal / less than / output
72 operator STRING_TO_REGEXP 1 "convert string to regexp"
73 operator REGEXP_CONCAT 2: "regexp concat"
74 operator REGEXP_UNION 2: "regexp union"
75 operator REGEXP_INTER 2: "regexp intersection"
76 operator REGEXP_STAR 1 "regexp *"
77 operator REGEXP_PLUS 1 "regexp +"
78 operator REGEXP_OPT 1 "regexp ?"
79 operator REGEXP_RANGE 2 "regexp range"
80 operator REGEXP_LOOP 2:3 "regexp loop"
82 operator REGEXP_EMPTY 0 "regexp empty"
83 operator REGEXP_SIGMA 0 "regexp all charactors"
85 typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule
86 typerule REGEXP_UNION ::CVC4::theory::strings::RegExpUnionTypeRule
87 typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule
88 typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule
89 typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule
90 typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule
91 typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule
92 typerule REGEXP_LOOP ::CVC4::theory::strings::RegExpLoopTypeRule
94 typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
97 typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
98 typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
99 typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
100 typerule STRING_SUBSTR_TOTAL ::CVC4::theory::strings::StringSubstrTypeRule
101 typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
102 typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
103 typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
104 typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
105 typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule
106 typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule
107 typerule STRING_ITOS ::CVC4::theory::strings::StringIntToStrTypeRule
108 typerule STRING_STOI ::CVC4::theory::strings::StringStrToIntTypeRule
110 typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
112 typerule REGEXP_EMPTY ::CVC4::theory::strings::EmptyRegExpTypeRule
113 typerule REGEXP_SIGMA ::CVC4::theory::strings::SigmaRegExpTypeRule