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
|
(** Why3 driver for CVC5 1.0.0 with string support *)
prelude ";; produced by cvc5_strings.drv ;;"
import "cvc5.drv"
import "smtlib-strings.gen"
theory string.String
remove prop lt_empty
remove prop lt_not_com
remove prop lt_ref
remove prop lt_ref
remove prop lt_trans
remove prop le_empty
remove prop le_ref
remove prop lt_le
remove prop lt_le_eq
remove prop le_trans
remove prop replaceall_empty1
remove prop not_contains_replaceall
end
theory string.RegExpr
syntax type re "RegLan"
syntax function to_re "(str.to_re %1)"
syntax predicate in_re "(str.in_re %1 %2)"
syntax function concat "(re.++ %1 %2)"
syntax function union "(re.union %1 %2)"
syntax function inter "(re.inter %1 %2)"
syntax function star "(re.* %1)"
syntax function plus "(re.+ %1)"
syntax function none "re.none"
syntax function allchar "re.allchar"
syntax function opt "(re.opt %1)"
syntax function range "(re.range %1 %2)"
syntax function power "((_ re.^ %1) %2)"
syntax function loop "((_ re.loop %1 %2) %3)"
end
|
