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