this repo has no description
dekker.one
1% the sum of booleans x = s
2predicate bool_sum_eq(array[int] of var bool:x, int:s) =
3 let { int: c = length(x),
4 array[1..c] of var bool: y = [x[i] | i in index_set(x)]
5 } in
6 rec_bool_sum_eq(y, 1, s);
7
8predicate rec_bool_sum_eq(array[int] of var bool:x, int: f, int:s) =
9 let { int: c = length(x) } in
10 if s < 0 then false
11 elseif s == 0 then
12 forall(i in f..c)(x[i] == false)
13 elseif s < c - f + 1 then
14 (x[f] == true /\ rec_bool_sum_eq(x,f+1,s-1)) \/
15 (x[f] == false /\ rec_bool_sum_eq(x,f+1,s))
16 elseif s == c - f + 1 then
17 forall(i in f..c)(x[i] == true)
18 else false endif;