1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
|
# kinds -*- sh -*-
#
# For documentation on this file format, please refer to
# src/theory/builtin/kinds.
#
theory THEORY_STRINGS ::cvc5::theory::strings::TheoryStrings "theory/strings/theory_strings.h"
properties check parametric presolve
rewriter ::cvc5::theory::strings::SequencesRewriter "theory/strings/sequences_rewriter.h"
typechecker "theory/strings/theory_strings_type_rules.h"
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"
operator STRING_UPDATE 3 "string update"
operator STRING_CHARAT 2 "string charat"
operator STRING_CONTAINS 2 "string contains"
operator STRING_LT 2 "string less than"
operator STRING_LEQ 2 "string less than or equal"
operator STRING_INDEXOF 3 "string index of substring"
operator STRING_INDEXOF_RE 3 "string index of regular expression match"
operator STRING_REPLACE 3 "string replace"
operator STRING_REPLACE_ALL 3 "string replace all"
operator STRING_REPLACE_RE 3 "string replace regular expression match"
operator STRING_REPLACE_RE_ALL 3 "string replace all regular expression matches"
operator STRING_PREFIX 2 "string prefixof"
operator STRING_SUFFIX 2 "string suffixof"
operator STRING_IS_DIGIT 1 "string isdigit, returns true if argument is a string of length one that represents a digit"
operator STRING_ITOS 1 "integer to string"
operator STRING_STOI 1 "string to integer (total function)"
operator STRING_TO_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise"
operator STRING_FROM_CODE 1 "string from code, returns a string containing a single character whose code point matches the argument to this function, empty string if the argument is out-of-bounds"
operator STRING_TOLOWER 1 "string to lowercase conversion"
operator STRING_TOUPPER 1 "string to uppercase conversion"
operator STRING_REV 1 "string reverse"
sort STRING_TYPE \
Cardinality::INTEGERS \
well-founded \
"NodeManager::currentNM()->mkConst(::cvc5::String())" \
"util/string.h" \
"String type"
sort REGEXP_TYPE \
Cardinality::INTEGERS \
well-founded \
"NodeManager::currentNM()->mkNode(REGEXP_EMPTY)" \
"util/string.h" \
"RegExp type"
enumerator STRING_TYPE \
"::cvc5::theory::strings::StringEnumerator" \
"theory/strings/type_enumerator.h"
enumerator REGEXP_TYPE \
"::cvc5::theory::strings::RegExpEnumerator" \
"theory/strings/regexp_enumerator.h"
constant CONST_STRING \
class \
String \
::cvc5::strings::StringHashFunction \
"util/string.h" \
"a string of characters"
# the type
operator SEQUENCE_TYPE 1 "seuence type, takes as parameter the type of the elements"
cardinality SEQUENCE_TYPE \
"::cvc5::theory::strings::SequenceProperties::computeCardinality(%TYPE%)" \
"theory/strings/theory_strings_type_rules.h"
well-founded SEQUENCE_TYPE \
"::cvc5::theory::strings::SequenceProperties::isWellFounded(%TYPE%)" \
"::cvc5::theory::strings::SequenceProperties::mkGroundTerm(%TYPE%)" \
"theory/strings/theory_strings_type_rules.h"
enumerator SEQUENCE_TYPE \
"::cvc5::theory::strings::SequenceEnumerator" \
"theory/strings/type_enumerator.h"
constant CONST_SEQUENCE \
class \
Sequence \
::cvc5::SequenceHashFunction \
"expr/sequence.h" \
"a sequence of characters"
operator SEQ_UNIT 1 "a sequence of length one"
operator SEQ_NTH 2 "The nth element of a sequence"
operator SEQ_NTH_TOTAL 2 "The nth element of a sequence (internal, for responses to expand definitions only)"
# equal equal / less than / output
operator STRING_TO_REGEXP 1 "convert string to regexp"
operator REGEXP_CONCAT 2: "regexp concat"
operator REGEXP_UNION 2: "regexp union"
operator REGEXP_INTER 2: "regexp intersection"
operator REGEXP_DIFF 2 "regexp difference"
operator REGEXP_STAR 1 "regexp *"
operator REGEXP_PLUS 1 "regexp +"
operator REGEXP_OPT 1 "regexp ?"
operator REGEXP_RANGE 2 "regexp range"
operator REGEXP_COMPLEMENT 1 "regexp complement"
operator REGEXP_EMPTY 0 "regexp empty"
operator REGEXP_SIGMA 0 "regexp all characters"
constant REGEXP_REPEAT_OP \
struct \
RegExpRepeat \
::cvc5::RegExpRepeatHashFunction \
"util/regexp.h" \
"operator for regular expression repeat; payload is an instance of the cvc5::RegExpRepeat class"
parameterized REGEXP_REPEAT REGEXP_REPEAT_OP 1 "regular expression repeat; first parameter is a REGEXP_REPEAT_OP, second is a regular expression term"
constant REGEXP_LOOP_OP \
struct \
RegExpLoop \
::cvc5::RegExpLoopHashFunction \
"util/regexp.h" \
"operator for regular expression loop; payload is an instance of the cvc5::RegExpLoop class"
parameterized REGEXP_LOOP REGEXP_LOOP_OP 1 "regular expression loop; first parameter is a REGEXP_LOOP_OP, second is a regular expression term"
#internal
operator REGEXP_RV 1 "regexp rv (internal use only)"
typerule REGEXP_RV "SimpleTypeRule<RRegExp, AInteger>"
# regular expressions
typerule REGEXP_CONCAT "SimpleTypeRuleVar<RRegExp, ARegExp>"
typerule REGEXP_UNION "SimpleTypeRuleVar<RRegExp, ARegExp>"
typerule REGEXP_INTER "SimpleTypeRuleVar<RRegExp, ARegExp>"
typerule REGEXP_DIFF "SimpleTypeRuleVar<RRegExp, ARegExp>"
typerule REGEXP_STAR "SimpleTypeRule<RRegExp, ARegExp>"
typerule REGEXP_PLUS "SimpleTypeRule<RRegExp, ARegExp>"
typerule REGEXP_OPT "SimpleTypeRule<RRegExp, ARegExp>"
typerule REGEXP_RANGE ::cvc5::theory::strings::RegExpRangeTypeRule
typerule REGEXP_REPEAT_OP "SimpleTypeRule<RBuiltinOperator>"
typerule REGEXP_REPEAT "SimpleTypeRule<RRegExp, ARegExp>"
typerule REGEXP_LOOP_OP "SimpleTypeRule<RBuiltinOperator>"
typerule REGEXP_LOOP "SimpleTypeRule<RRegExp, ARegExp>"
typerule REGEXP_COMPLEMENT "SimpleTypeRule<RRegExp, ARegExp>"
typerule STRING_TO_REGEXP "SimpleTypeRule<RRegExp, AString>"
typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>"
typerule REGEXP_EMPTY "SimpleTypeRule<RRegExp>"
typerule REGEXP_SIGMA "SimpleTypeRule<RRegExp>"
### operators that apply to both strings and sequences
typerule STRING_CONCAT ::cvc5::theory::strings::StringConcatTypeRule
typerule STRING_LENGTH ::cvc5::theory::strings::StringStrToIntTypeRule
typerule STRING_SUBSTR ::cvc5::theory::strings::StringSubstrTypeRule
typerule STRING_UPDATE ::cvc5::theory::strings::StringUpdateTypeRule
typerule STRING_CHARAT ::cvc5::theory::strings::StringAtTypeRule
typerule STRING_CONTAINS ::cvc5::theory::strings::StringRelationTypeRule
typerule STRING_INDEXOF ::cvc5::theory::strings::StringIndexOfTypeRule
typerule STRING_INDEXOF_RE "SimpleTypeRule<RInteger, AString, ARegExp, AInteger>"
typerule STRING_REPLACE ::cvc5::theory::strings::StringReplaceTypeRule
typerule STRING_REPLACE_ALL ::cvc5::theory::strings::StringReplaceTypeRule
typerule STRING_REPLACE_RE "SimpleTypeRule<RString, AString, ARegExp, AString>"
typerule STRING_REPLACE_RE_ALL "SimpleTypeRule<RString, AString, ARegExp, AString>"
typerule STRING_PREFIX ::cvc5::theory::strings::StringStrToBoolTypeRule
typerule STRING_SUFFIX ::cvc5::theory::strings::StringStrToBoolTypeRule
typerule STRING_REV ::cvc5::theory::strings::StringStrToStrTypeRule
### string specific operators
typerule CONST_STRING "SimpleTypeRule<RString>"
typerule STRING_LT "SimpleTypeRule<RBool, AString, AString>"
typerule STRING_LEQ "SimpleTypeRule<RBool, AString, AString>"
typerule STRING_IS_DIGIT "SimpleTypeRule<RBool, AString>"
typerule STRING_ITOS "SimpleTypeRule<RString, AInteger>"
typerule STRING_STOI "SimpleTypeRule<RInteger, AString>"
typerule STRING_TO_CODE "SimpleTypeRule<RInteger, AString>"
typerule STRING_FROM_CODE "SimpleTypeRule<RString, AInteger>"
typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>"
typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>"
### sequence specific operators
typerule CONST_SEQUENCE ::cvc5::theory::strings::ConstSequenceTypeRule
typerule SEQ_UNIT ::cvc5::theory::strings::SeqUnitTypeRule
typerule SEQ_NTH ::cvc5::theory::strings::SeqNthTypeRule
typerule SEQ_NTH_TOTAL ::cvc5::theory::strings::SeqNthTypeRule
endtheory
|
