this repo has no description
dekker.one
1% Ordenamiento odd-even.
2% y es la versión ordenada de x, todos los verdaderos (true)
3% antes de los falsos (false).
4predicate oesort(array[int] of var bool:x, array[int] of var bool:y)=
5 let { int: c = card(index_set(x)) } in
6 if c == 1 then x[1] == y[1]
7 elseif c == 2 then comparator(x[1],x[2],y[1],y[2])
8 else
9 let {
10 array[1..c div 2] of var bool:xf = [x[i] | i in 1..c div 2],
11 array[1..c div 2] of var bool:xl = [x[i] | i in c div 2 +1..c],
12 array[1..c div 2] of var bool:tf,
13 array[1..c div 2] of var bool:tl } in
14 oesort(xf,tf) /\ oesort(xl,tl) /\ oemerge(tf ++ tl, y)
15 endif;
16
17% Unión odd-even
18% y es la versión ordenada de x, todos los valores antes de los
19% valores falsos (false).
20% Suponen que la primera y segunda mitad de x está ordenada.
21predicate oemerge(array[int] of var bool:x, array[int] of var bool:y)=
22 let { int: c = card(index_set(x)) } in
23 if c == 1 then x[1] == y[1]
24 elseif c == 2 then comparator(x[1],x[2],y[1],y[2])
25 else
26 let { array[1..c div 2] of var bool:xo =
27 [ x[i] | i in 1..c where i mod 2 == 1],
28 array[1..c div 2] of var bool:xe =
29 [ x[i] | i in 1..c where i mod 2 == 0],
30 array[1..c div 2] of var bool:to,
31 array[1..c div 2] of var bool:te } in
32 oemerge(xo,to) /\ oemerge(xe,te) /\
33 y[1] = to[1] /\
34 forall(i in 1..c div 2 -1)(
35 comparator(te[i],to[i+1],y[2*i],y[2*i+1])) /\
36 y[c] = te[c div 2]
37 endif;
38
39% Como usar:
40% comparator o1 = max(i1,i2), o2 = min(i1,i2)
41predicate comparator(var bool:i1,var bool:i2,var bool:o1,var bool:o2)=
42 (o1 = (i1 \/ i2)) /\ (o2 = (i1 /\ i2));