this repo has no description
dekker.one
1% the sum of bits x = s in binary.
2% s[0], s[1], ..., s[k] where 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% add two binary numbers x, and y and carry in bit ci to get binary s
21predicate binary_add(array[int] of var bool: x,
22 array[int] of var bool: y,
23 var bool: ci,
24 array[int] of var bool: s) =
25 let { int:l = length(x),
26 int:n = length(s), } in
27 assert(l == length(y),
28 "length of binary_add input args must be same",
29 assert(n == l \/ n == l+1, "length of binary_add output " ++
30 "must be equal or one more than inputs",
31 let { array[0..l] of var bool: c } in
32 full_adder(x[0], y[0], ci, s[0], c[0]) /\
33 forall(i in 1..l)(full_adder(x[i], y[i], c[i-1], s[i], c[i])) /\
34 if n > l then s[n] = c[l] else c[l] == false endif ));
35
36predicate full_adder(var bool: x, var bool: y, var bool: ci,
37 var bool: s, var bool: co) =
38 let { var bool: xy = x xor y } in
39 s = (xy xor ci) /\ co = ((x /\ y) \/ (ci /\ xy));