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
|
# 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::TheoryStringsRewriter "theory/strings/theory_strings_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_ITOS 1 "integer to string"
operator STRING_STOI 1 "string to integer (total function)"
operator STRING_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise"
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/regexp.h" \
"String type"
sort REGEXP_TYPE \
Cardinality::INTEGERS \
well-founded \
"NodeManager::currentNM()->mkNode(REGEXP_EMPTY, std::vector<Node>() )" \
"util/regexp.h" \
"RegExp type"
enumerator STRING_TYPE \
"::CVC4::theory::strings::StringEnumerator" \
"theory/strings/type_enumerator.h"
constant CONST_STRING \
::CVC4::String \
::CVC4::strings::StringHashFunction \
"util/regexp.h" \
"a string of characters"
typerule CONST_STRING "SimpleTypeRule<RString>"
# 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_STAR 1 "regexp *"
operator REGEXP_PLUS 1 "regexp +"
operator REGEXP_OPT 1 "regexp ?"
operator REGEXP_RANGE 2 "regexp range"
operator REGEXP_LOOP 2:3 "regexp loop"
operator REGEXP_EMPTY 0 "regexp empty"
operator REGEXP_SIGMA 0 "regexp all characters"
#internal
operator REGEXP_RV 1 "regexp rv (internal use only)"
typerule REGEXP_RV "SimpleTypeRule<RRegExp, AInteger>"
#typerules
typerule REGEXP_CONCAT "SimpleTypeRuleVar<RRegExp, ARegExp>"
typerule REGEXP_UNION "SimpleTypeRuleVar<RRegExp, ARegExp>"
typerule REGEXP_INTER "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_LOOP "SimpleTypeRule<RRegExp, ARegExp, AInteger, AOptional<AInteger>>"
typerule STRING_TO_REGEXP "SimpleTypeRule<RRegExp, AString>"
typerule STRING_CONCAT "SimpleTypeRuleVar<RString, AString>"
typerule STRING_LENGTH "SimpleTypeRule<RInteger, AString>"
typerule STRING_SUBSTR "SimpleTypeRule<RString, AString, AInteger, AInteger>"
typerule STRING_CHARAT "SimpleTypeRule<RString, AString, AInteger>"
typerule STRING_STRCTN "SimpleTypeRule<RBool, AString, AString>"
typerule STRING_LT "SimpleTypeRule<RBool, AString, AString>"
typerule STRING_LEQ "SimpleTypeRule<RBool, AString, AString>"
typerule STRING_STRIDOF "SimpleTypeRule<RInteger, AString, AString, AInteger>"
typerule STRING_STRREPL "SimpleTypeRule<RString, AString, AString, AString>"
typerule STRING_STRREPLALL "SimpleTypeRule<RString, AString, AString, AString>"
typerule STRING_PREFIX "SimpleTypeRule<RBool, AString, AString>"
typerule STRING_SUFFIX "SimpleTypeRule<RBool, AString, AString>"
typerule STRING_ITOS "SimpleTypeRule<RString, AInteger>"
typerule STRING_STOI "SimpleTypeRule<RInteger, AString>"
typerule STRING_CODE "SimpleTypeRule<RInteger, AString>"
typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>"
typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>"
typerule STRING_REV "SimpleTypeRule<RString, AString>"
typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>"
typerule REGEXP_EMPTY "SimpleTypeRule<RRegExp>"
typerule REGEXP_SIGMA "SimpleTypeRule<RRegExp>"
endtheory
|
