this repo has no description
dekker.one
1% La suma de bits x = s en binario.
2% s[0], s[1], ..., s[k] en donde 2^k >= length(x) > 2^(k-1)
3predicate binary_sum(array[int] of var bool:x,
4 array[int] of var bool:s)=
5 let { int: l = length(x) } in
6 if l == 1 then s[0] = x[1]
7 elseif l == 2 then
8 s[0] = (x[1] xor x[2]) /\ s[1] = (x[1] /\ x[2])
9 else let { int: ll = (l div 2),
10 array[1..ll] of var bool: f = [ x[i] | i in 1..ll ],
11 array[1..ll] of var bool: t = [x[i]| i in ll+1..2*ll],
12 var bool: b = if ll*2 == l then false else x[l] endif,
13 int: cp = floor(log2(int2float(ll))),
14 array[0..cp] of var bool: fs,
15 array[0..cp] of var bool: ts } in
16 binary_sum(f, fs) /\ binary_sum(t, ts) /\
17 binary_add(fs, ts, b, s)
18 endif;
19
20% Añadir dos números binarios x e y,
21% y llevar en el bit ci para obtener el binario s.
22predicate binary_add(array[int] of var bool: x,
23 array[int] of var bool: y,
24 var bool: ci,
25 array[int] of var bool: s) =
26 let { int:l = length(x),
27 int:n = length(s), } in
28 assert(l == length(y),
29 "La longitud del argumento de entrada binary_add debe ser el mismo",
30 assert(n == l \/ n == l+1, "longitud de salida binaria " ++
31 "debe ser igual o una más que las entradas",
32 let { array[0..l] of var bool: c } in
33 full_adder(x[0], y[0], ci, s[0], c[0]) /\
34 forall(i in 1..l)(full_adder(x[i], y[i], c[i-1], s[i], c[i])) /\
35 if n > l then s[n] = c[l] else c[l] == false endif ));
36
37predicate full_adder(var bool: x, var bool: y, var bool: ci,
38 var bool: s, var bool: co) =
39 let { var bool: xy = x xor y } in
40 s = (xy xor ci) /\ co = ((x /\ y) \/ (ci /\ xy));