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
|
var2 $ where ~ex1 p where true: p notin $ & p+1 in $;
allpos $;
defaultwhere1(p) = all1 r: r<p => r in $;
defaultwhere2(P) = all1 p: p in P => all1 r: r<p => r in $;
# we declare a string of 8-bit vectors
var2 bit0 where bit0 sub $, bit1 where bit1 sub $,
bit2 where bit2 sub $, bit3 where bit3 sub $,
bit4 where bit4 sub $, bit5 where bit5 sub $,
bit6 where bit6 sub $, bit7 where bit7 sub $;
macro consecutive_in_set(var1 p, var1 q, var2 P) =
p < q & p in P & q in P & all1 r: p < r & r < q => r notin P;
# ASCII 'a' is 97, which is 01100001
macro is_a(var1 p, var1 q) =
q = p + 1 &
p in bit0 & p notin bit1 & p notin bit2 & p notin bit3 &
p notin bit4 & p in bit5 & p in bit6 & p notin bit7;
# ASCII 'b' is 98, which is 01100010
macro is_b(var1 p, var1 q) =
q = p + 1 &
p notin bit0 & p in bit1 & p notin bit2 & p notin bit3 &
p notin bit4 & p in bit5 & p in bit6 & p notin bit7;
# we concatenate by guessing the intermediate position where
# the string parsed according to the first regular expression
# (in this case "a") ends and the string parsed according to
# the second (in this case "b") starts
pred is_ab(var1 p, var1 q) =
ex1 r where p<=r & r<=q: is_a(p, r) & is_b(r, q);
# a star expression is handled by guessing the set of
# intermediate positions
pred is_ab_star(var1 p, var1 q) =
ex2 P: p in P & q in P &
all1 r, r': consecutive_in_set(r, r', P) => is_ab(r, r');
pred is_a_star(var1 p, var1 q) =
ex2 P: p in P & q in P &
all1 r, r': consecutive_in_set(r, r', P) => is_a(r, r');
pred is_a_star_ab_star(var1 p, var1 q) =
ex1 r where p<=r & r<=q: is_a_star(p, r) & is_ab_star(r, q);
is_a_star_ab_star(0, max($)+1);
|
