this repo has no description
dekker.one
1% La suma de booleanos x = s
2predicate bool_sum_eq(array[int] of var bool:x, int:s) =
3 let { int: c = length(x) } in
4 if s < 0 then false
5 elseif s == 0 then
6 forall(i in 1..c)(x[i] == false)
7 elseif s < c then
8 let {
9 % cp = número de bits necesarios para representar 0..c
10 int: cp = floor(log2(int2float(c))),
11 % z es la suma de x en binario
12 array[0..cp] of var bool:z } in
13 binary_sum(x, z) /\
14 % z == s
15 forall(i in 0..cp)(z[i] == ((s div pow(2,i)) mod 2 == 1))
16 elseif s == c then
17 forall(i in 1..c)(x[i] == true)
18 else false endif;
19
20include "binarysum.mzn";