%--------------------------------------------------------------------% % Requires that a set of tasks given by start times 's', % durations 'd', and resource requirements 'r', % never require more than a global % resource bound 'b' at any one time. % Assumptions: % - forall i, d[i] >= 0 and r[i] >= 0 %--------------------------------------------------------------------% predicate cumulative(array[int] of var int: s, array[int] of var int: d, array[int] of var int: r, var int: b) = assert(index_set(s) == index_set(d) /\ index_set(s) == index_set(r), "cumulative: the array arguments must have identical index sets", assert(lb_array(d) >= 0 /\ lb_array(r) >= 0, "cumulative: durations and resource usages must be non-negative", let { set of int: times = lb_array(s) .. max([ ub(s[i]) + ub(d[i]) | i in index_set(s) ]) } in forall( t in times ) ( b >= sum( i in index_set(s) ) ( bool2int( s[i] <= t /\ t < s[i] + d[i] ) * r[i] ) ) ) );