this repo has no description
1% La suma de los booleanos es 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 forall(i in 1..c)(x[i] == false)
6 elseif s < c then
7 let
8 {
9 % cp = potencia más cercana de 2 >= c
10 int: cp = pow(2,ceil(log2(int2float(c)))),
11 array[1..cp] of var bool:y, % y es la versión acolchada de x
12 array[1..cp] of var bool:z
13 } in
14 forall(i in 1..c)(y[i] == x[i]) /\
15 forall(i in c+1..cp)(y[i] == false) /\
16 oesort(y, z) /\ z[s] == true /\ z[s+1] == false
17 elseif s == c then forall(i in 1..c)(x[i] == true)
18 else false endif;
19
20include "oesort.mzn";