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
|
prelude ";;; generated by SMT-LIB strings"
theory BuiltIn
syntax type string "String"
meta "literal:keep" type string
end
theory string.String
remove prop concat_assoc
remove prop concat_empty
remove prop length_empty
remove prop length_concat
remove prop at_out_of_range
remove prop at_empty
remove prop at_length
remove prop concat_at
remove prop substring_out_of_range
remove prop substring_of_length_zero_or_less
remove prop substring_of_empty
remove prop substring_smaller
remove prop substring_smaller_x
remove prop substring_length
remove prop substring_at
remove prop prefixof_substring
remove prop prefixof_concat
remove prop prefixof_empty
remove prop prefixof_empty2
remove prop suffixof_substring
remove prop suffixof_concat
remove prop suffixof_empty
remove prop suffixof_empty2
remove prop contains_prefixof
remove prop contains_suffixof
remove prop contains_empty
remove prop contains_empty2
remove prop contains_substring
remove prop contains_concat
remove prop contains_at
remove prop indexof_empty
remove prop indexof_empty1
remove prop indexof_contains
remove prop contains_indexof
remove prop not_contains_indexof
remove prop substring_indexof
remove prop indexof_out_of_range
remove prop indexof_in_range
remove prop indexof_contains_substring
remove prop replace_empty
remove prop replace_not_contains
remove prop replace_empty2
remove prop replace_substring_indexof
remove prop to_int_gt_minus_1
remove prop to_int_empty
remove prop from_int_negative
remove prop from_int_to_int
syntax function concat "(str.++ %1 %2)"
syntax function length "(str.len %1)"
syntax function indexof "(str.indexof %1 %2 %3)"
syntax function replace "(str.replace %1 %2 %3)"
syntax function substring "(str.substr %1 %2 %3)"
syntax function s_at "(str.at %1 %2)"
syntax predicate contains "(str.contains %1 %2)"
syntax predicate prefixof "(str.prefixof %1 %2)"
syntax predicate suffixof "(str.suffixof %1 %2)"
(* syntax function is_digit "(str.is_digit %1)" *)
syntax function to_int "(str.to_int %1)"
syntax function from_int "(str.from_int %1)"
syntax predicate lt "(str.< %1 %2)"
syntax predicate le "(str.<= %1 %2)"
syntax function replaceall "(str.replace_all %1 %2 %3)"
end
theory string.StringRealization
prelude ";;; SMT-LIB2: string theory"
syntax function concat "(str.++ %1 %2)"
syntax function length "(str.len %1)"
syntax function indexof "(str.indexof %1 %2 %3)"
syntax function replace "(str.replace %1 %2 %3)"
syntax function substring "(str.substr %1 %2 %3)"
syntax function s_at "(str.at %1 %2)"
syntax predicate contains "(str.contains %1 %2)"
syntax predicate prefixof "(str.prefixof %1 %2)"
syntax predicate suffixof "(str.suffixof %1 %2)"
(* syntax function is_digit "(str.is_digit %1)" *)
syntax function to_int "(str.to_int %1)"
syntax function from_int "(str.from_int %1)"
syntax predicate lt "(str.< %1 %2)"
syntax predicate le "(str.<= %1 %2)"
syntax function replaceall "(str.replace_all %1 %2 %3)"
end
|
