this repo has no description
dekker.one
1predicate fzn_cumulative_reif(array[int] of var int: s,
2 array[int] of var int: d,
3 array[int] of var int: r, var int: b, var bool: bb) =
4 let {
5 set of int: Tasks =
6 {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 }
7 } in
8 if 0==card(Tasks) then bb <-> ( 0==card(index_set(s)) \/ b>=0 )
9 else
10 let {
11 int: early = min([ lb(s[i]) | i in Tasks ]),
12 int: late = max([ ub(s[i]) + ub(d[i]) | i in Tasks ])
13 } in (
14 if late - early > 5000 then
15 fzn_cumulative_task_reif(s, d, r, b, bb)
16 else
17 fzn_cumulative_time_reif(s, d, r, b, bb)
18 endif
19 )
20 endif
21 ;
22
23
24predicate fzn_cumulative_time_reif(array[int] of var int: s,
25 array[int] of var int: d,
26 array[int] of var int: r, var int: b, var bool: bb) =
27 let {
28 set of int: Tasks =
29 {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 },
30 int: early = min([ lb(s[i]) | i in Tasks ]),
31 int: late = max([ ub(s[i]) + ub(d[i]) | i in Tasks ])
32 } in (
33 bb <-> forall( t in early..late ) (
34 b >= sum( i in Tasks ) (
35 bool2int(s[i] <= t /\ t < s[i] + d[i]) * r[i]
36 )
37 )
38 );
39
40predicate fzn_cumulative_task_reif(array[int] of var int: s,
41 array[int] of var int: d,
42 array[int] of var int: r, var int: b, var bool: bb) =
43 let {
44 set of int: Tasks =
45 {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 }
46 } in (
47 bb <-> forall( j in Tasks ) (
48 b >= r[j] + sum( i in Tasks where i != j ) (
49 bool2int(s[i] <= s[j] /\ s[j] < s[i] + d[i] ) * r[i]
50 )
51 )
52 );
53