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
|
# 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"
properties check parametric propagate presolve
rewriter ::CVC4::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_CHARAT 2 "string charat"
operator STRING_STRCTN 2 "string contains"
operator STRING_LT 2 "string less than"
operator STRING_LEQ 2 "string less than or equal"
operator STRING_STRIDOF 3 "string indexof"
operator STRING_STRREPL 3 "string replace"
operator STRING_STRREPLALL 3 "string replace all"
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(::CVC4::String())" \
"util/string.h" \
"String type"
sort REGEXP_TYPE \
Cardinality::INTEGERS \
well-founded \
"NodeManager::currentNM()->mkNode(REGEXP_EMPTY, std::vector<Node>() )" \
"util/string.h" \
"RegExp type"
enumerator STRING_TYPE \
"::CVC4::theory::strings::StringEnumerator" \
"theory/strings/type_enumerator.h"
constant CONST_STRING \
::CVC4::String \
::CVC4::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 \
"::CVC4::theory::strings::SequenceProperties::computeCardinality(%TYPE%)" \
"theory/strings/theory_strings_type_rules.h"
well-founded SEQUENCE_TYPE \
"::CVC4::theory::strings::SequenceProperties::isWellFounded(%TYPE%)" \
"::CVC4::theory::strings::SequenceProperties::mkGroundTerm(%TYPE%)" \
"theory/strings/theory_strings_type_rules.h"
enumerator SEQUENCE_TYPE \
"::CVC4::theory::strings::SequenceEnumerator" \
"theory/strings/type_enumerator.h"
constant CONST_SEQUENCE \
::CVC4::ExprSequence \
::CVC4::ExprSequenceHashFunction \
"expr/expr_sequence.h" \
"a sequence of characters"
operator SEQ_UNIT 1 "a sequence of length one"
# 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 \
::CVC4::RegExpRepeat \
::CVC4::RegExpRepeatHashFunction \
"util/regexp.h" \
"operator for regular expression repeat; payload is an instance of the CVC4::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 \
::CVC4::RegExpLoop \
::CVC4::RegExpLoopHashFunction \
"util/regexp.h" \
"operator for regular expression loop; payload is an instance of the CVC4::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 ::CVC4::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 ::CVC4::theory::strings::StringConcatTypeRule
typerule STRING_LENGTH ::CVC4::theory::strings::StringStrToIntTypeRule
typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
typerule STRING_CHARAT ::CVC4::theory::strings::StringAtTypeRule
typerule STRING_STRCTN ::CVC4::theory::strings::StringRelationTypeRule
typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
typerule STRING_STRREPLALL ::CVC4::theory::strings::StringReplaceTypeRule
typerule STRING_PREFIX ::CVC4::theory::strings::StringStrToBoolTypeRule
typerule STRING_SUFFIX ::CVC4::theory::strings::StringStrToBoolTypeRule
typerule STRING_REV ::CVC4::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 ::CVC4::theory::strings::ConstSequenceTypeRule
typerule SEQ_UNIT ::CVC4::theory::strings::SeqUnitTypeRule
endtheory
|
