this repo has no description
dekker.one
1% 布尔型变量 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 { % cp = nearest power of 2 >= c
8 int: cp = pow(2,ceil(log2(int2float(c)))),
9 array[1..cp] of var bool:y, % y is padded version of x
10 array[1..cp] of var bool:z } in
11 forall(i in 1..c)(y[i] == x[i]) /\
12 forall(i in c+1..cp)(y[i] == false) /\
13 oesort(y, z) /\ z[s] == true /\ z[s+1] == false
14 elseif s == c then forall(i in 1..c)(x[i] == true)
15 else false endif;
16
17include "oesort.mzn";