this repo has no description
dekker.one
1/** @group globals
2 Requires that in each subsequence \a vs[\p i], ..., \a vs[\p i + \a seq - 1] the sum of the
3 values belongs to the interval [\a low, \a up].
4*/
5predicate fzn_sliding_sum(int: low, int: up, int: seq, array[int] of var int: vs) =
6 let { int: lx = min(index_set(vs)),
7 int: ux = max(index_set(vs)),
8 } in
9 forall (i in lx .. ux - seq + 1) (
10 let {
11 var int: sum_of_l = sum(j in i..i + seq - 1) (vs[j])
12 } in
13 low <= sum_of_l /\ sum_of_l <= up
14 );