blob: a421d6fa89223bb71e81c217353a87f5ee942c0e (
plain)
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
|
# kinds [for strings theory]
#
theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h"
properties check parametric propagate getNextDecisionRequest 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"
operator STRING_IN_REGEXP 2 "membership"
operator STRING_LENGTH 1 "string length"
operator STRING_SUBSTR 3 "string substr"
operator STRING_STRCTN 2 "string contains"
operator STRING_CHARAT 2 "string char at"
#sort CHAR_TYPE \
# Cardinality::INTEGERS \
# well-founded \
# "NodeManager::currentNM()->mkConst(::CVC4::String())" \
# "util/regexp.h" \
# "String type"
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()->mkConst(::CVC4::RegExp())" \
"util/regexp.h" \
"RegExp type"
enumerator STRING_TYPE \
"::CVC4::theory::strings::StringEnumerator" \
"theory/strings/type_enumerator.h"
#enumerator REGEXP_TYPE \
# "::CVC4::theory::strings::RegExpEnumerator" \
# "theory/strings/type_enumerator.h"
constant CONST_STRING \
::CVC4::String \
::CVC4::strings::StringHashFunction \
"util/regexp.h" \
"a string of characters"
constant CONST_REGEXP \
::CVC4::RegExp \
::CVC4::RegExpHashFunction \
"util/regexp.h" \
"a regular expression"
typerule CONST_STRING ::CVC4::theory::strings::StringConstantTypeRule
typerule CONST_REGEXP ::CVC4::theory::strings::RegExpConstantTypeRule
# equal equal / less than / output
operator STRING_TO_REGEXP 1 "convert string to regexp"
operator REGEXP_CONCAT 2: "regexp concat"
operator REGEXP_OR 2: "regexp or"
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"
#constant REGEXP_EMPTY \
# ::CVC4::RegExp \
# ::CVC4::RegExpHashFunction \
# "util/string.h" \
# "a regexp contains nothing"
#constant REGEXP_ALL \
# ::CVC4::RegExp \
# ::CVC4::RegExpHashFunction \
# "util/string.h" \
# "a regexp contains all strings"
#constant REGEXP_SIGMA \
# ::CVC4::RegExp \
# ::CVC4::RegExpHashFunction \
# "util/string.h" \
# "a regexp contains an arbitrary charactor"
typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule
typerule REGEXP_OR ::CVC4::theory::strings::RegExpOrTypeRule
typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule
typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule
typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule
typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule
typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule
typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
typerule STRING_STRCTN ::CVC4::theory::strings::StringContainTypeRule
typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
endtheory
|
