this repo has no description
dekker.one
1predicate fzn_maximum_arg_bool(array[int] of var bool: x, var int: i) =
2 let { int: l = min(index_set(x));
3 int: u = max(index_set(x));
4 } in
5 if exists(j in l..u)(is_fixed(x[j]) /\ fix(x[j]))
6 then % special case: max is known to be 1
7 let { array[l..u] of var bool: d; } in
8 x[i] = true /\ % ith case must be equal to ub
9 forall(j in l..u)(x[j] -> i <= j) /\ % lower bound
10 d[l] = x[l] /\
11 forall(j in l+1..u)(d[j] <-> (d[j-1] \/ x[j])) /\
12 forall(j in l..u)(not d[j] -> i >= j+1) % upper bound
13 else
14 % general case: min could be 0 or 1
15 let { array[l..u] of var bool: y;
16 array[l..u] of var l..u: mi; } in
17 y[l] = x[l] /\ mi[l] = l /\ i = mi[u] /\
18 forall (j in l+1 .. u) ( y[j] == (x[j] \/ y[j-1]) /\
19 mi[j] = if (y[j-1] \/ not x[j]) then mi[j-1] else j endif )
20 endif;