this repo has no description
dekker.one
1/** @group globals.scheduling
2 Requires that a set of tasks given by start times \a s, durations \a d, and
3 resource requirements \a r, never require more than a global resource bound
4 \a b at any one time.
5
6 Assumptions:
7 - forall \p i, \a d[\p i] >= 0 and \a r[\p i] >= 0
8
9 Linear version.
10*/
11
12%% A global cumulative with SCIP
13predicate fzn_cumulative(array[int] of var int: s,
14 array[int] of int: d,
15 array[int] of int: r, int: b);
16
17
18predicate fzn_cumulative(array[int] of var int: s,
19 array[int] of var int: d,
20 array[int] of var int: r, var int: b) =
21 assert(index_set(s) == index_set(d) /\ index_set(s) == index_set(r),
22 "cumulative: the 3 array arguments must have identical index sets",
23 if 0==length(s) then true else
24 assert(lb_array(d) >= 0 /\ lb_array(r) >= 0,
25 "cumulative: durations and resource usages must be non-negative",
26 if mzn_in_redundant_constraint() /\ fMZN__IgnoreRedundantCumulative then
27 true
28 else
29 let {
30 set of int: tasks =
31 {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 },
32 set of int: times = dom_array( [ s[i] | i in tasks ] )
33 } in
34 if 0==card(tasks) then /*true*/ 0==card(index_set(s)) \/ b>=0
35 else
36 if nMZN__UnarySizeMax_cumul>=card(times)*card(tasks) then %%% -- Mem overflow on rcmsp. PARAMETER? TODO
37 cumulative_time_decomp(s, d, r, b, times)
38 else
39 cumulative_task_decomp(s, d, r, b)
40 endif
41 endif
42 endif
43 ) endif );
44
45%% Can be called with a given set of times:
46predicate cumulative_set_times(array[int] of var int: s,
47 array[int] of var int: d,
48 array[int] of var int: r,
49 var int: b,
50 set of int: TIMES01) =
51 assert(index_set(s) == index_set(d) /\ index_set(s) == index_set(r),
52 "cumulative: the 3 array arguments must have identical index sets",
53 assert(lb_array(d) >= 0 /\ lb_array(r) >= 0,
54 "cumulative: durations and resource usages must be non-negative",
55 let {
56 set of int: tasks =
57 {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 },
58 set of int: times = dom_array( [ s[i] | i in tasks ] )
59 intersect TIMES01
60 } in
61 if false then %%% 100>=card(times) then %% PARAMETER ?
62 cumulative_time_decomp(s, d, r, b, times)
63 else
64 cumulative_task_decomp(s, d, r, b)
65 endif ));
66
67predicate cumulative_time_decomp(array[int] of var int: s,
68 array[int] of var int: d,
69 array[int] of var int: r,
70 var int: b,
71 set of int: TIMES01) =
72let {
73 set of int: tasks =
74 {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 },
75 set of int: times =
76 { i | i in min([ lb(s[i]) | i in tasks ]) ..
77 max([ ub(s[i]) + ub(d[i]) | i in tasks ]) where i in TIMES01 }
78}
79in
80% my_trace(" cumul_time: " ++ show(card(tasks)) ++ " tasks, " ++ show(card(times)) ++ " times\n") /\
81 forall( t in times ) (
82 b >= sum( i in tasks ) (
83 if is_fixed(d[i]) then
84 bool2int( s[i] in t-fix(d[i])+1..t )
85 else
86 bool2int( s[i] <= t /\ t < s[i] + d[i] )
87 endif
88 * r[i]
89 )
90 );
91
92predicate cumulative_task_decomp(array[int] of var int: s,
93 array[int] of var int: d,
94 array[int] of var int: r,
95 var int: b) =
96let {
97 set of int: tasks =
98 {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 }
99}
100in
101% my_trace(" cumul_tasks: " ++ show(card(tasks)) ++ " tasks\n") /\
102 forall( j in tasks) (
103 b-r[j] >= sum( i in tasks where i != j
104 /\ lb(s[i])<=ub(s[j]) /\ lb(s[j])<ub(s[i]+d[i]) %% -- seems slower on mspsp ???
105 ) (
106 r[i] * %% r[i] * !
107 bool2int( s[i] <= s[j] /\ s[j] < s[i]+d[i] )) )
108 ;