MiniZinc Documentation - Standard Library

Functions and Predicates
predicate alternative(var opt int: s0, var int: d0, array [int] of var opt int: s, array [int] of var int: d) =
assert(index_set(s)==index_set(d), "alternative: index sets of third and fourth argument must be identical", sum ( i in index_set(s) ) ( bool2int(occurs(s[i])) )<=1 /\ span(s0, d0, s, d))
(standard decomposition from alternative.mzn:8)

Alternative constraint for optional tasks. Task (s0,d0) spans the optional tasks (s[i],d[i]) in the array arguments and at most one can occur

predicate cumulative(array [int] of var opt 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 3 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: tasks = { i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 }, set of int: times = min ( i in tasks ) ( lb(s[i]) )..max ( i in tasks ) ( ub(s[i])+ub(d[i]) ), } in ( forall ( t in times ) ( b>=sum ( i in tasks ) ( bool2int(occurs(s[i]) /\ deopt(s[i])<=t /\ t < deopt(s[i])+d[i])*r[i] ) ))))
(standard decomposition from cumulative_opt.mzn:10)

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. Start times are optional variables, so that absent tasks do not need to be scheduled.

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 3 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", if forall ( i in index_set(r) ) ( is_fixed(r[i]) /\ fix(r[i])==1 ) /\ is_fixed(b) /\ fix(b)==1 then if forall ( i in index_set(d) ) ( is_fixed(d[i]) /\ fix(d[i])==1 ) then alldifferent(s) else disjunctive(s, d) endif else let { set of int: Tasks = { i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 }, int: early = min ( i in Tasks ) ( lb(s[i]) ), int: late = max ( i in Tasks ) ( ub(s[i])+ub(d[i]) ), } in ( if late-early > 5000 then cumulative_task(s, d, r, b) else cumulative_time(s, d, r, b) endif) endif))
(standard decomposition from cumulative.mzn:12)

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 disjunctive(array [int] of var opt int: s, array [int] of var int: d) =
assert(index_set(s)==index_set(d), "disjunctive: the array arguments must have identical index sets", forall ( i in index_set(d) ) ( d[i]>=0 ) /\ if lb_array(d) > 0 then disjunctive_strict(s, d) else forall ( i, j in index_set(d) where i < j ) ( absent(s[i]) \/ absent(s[j]) \/ d[i]==0 \/ d[j]==0 \/ deopt(s[i])+d[i]<=deopt(s[j]) \/ deopt(s[j])+d[j]<=deopt(s[i]) ) endif)
(standard decomposition from disjunctive_opt.mzn:12)

Requires that a set of tasks given by start times s and durations d do not overlap in time. Tasks with duration 0 can be scheduled at any time, even in the middle of other tasks. Start times are optional variables, so that absent tasks do not need to be scheduled.

Assumptions:

  • forall i, d[i] >= 0

predicate disjunctive(array [int] of var int: s, array [int] of var int: d) =
assert(index_set(s)==index_set(d), "disjunctive: the array arguments must have identical index sets", forall ( i in index_set(d) ) ( d[i]>=0 ) /\ if lb_array(d) > 0 then disjunctive_strict(s, d) else forall ( i, j in index_set(d) where i < j ) ( d[i]==0 \/ d[j]==0 \/ s[i]+d[i]<=s[j] \/ s[j]+d[j]<=s[i] ) endif)
(standard decomposition from disjunctive.mzn:11)

Requires that a set of tasks given by start times s and durations d do not overlap in time. Tasks with duration 0 can be scheduled at any time, even in the middle of other tasks.

Assumptions:

  • forall i, d[i] >= 0

predicate disjunctive_strict(array [int] of var opt int: s, array [int] of var int: d) =
assert(index_set(s)==index_set(d), "disjunctive: the array arguments must have identical index sets", forall ( i in index_set(d) ) ( d[i]>=0 ) /\ forall ( i, j in index_set(d) where i < j ) ( absent(s[i]) \/ absent(s[j]) \/ deopt(s[i])+d[i]<=deopt(s[j]) \/ deopt(s[j])+d[j]<=deopt(s[i]) ))
(standard decomposition from disjunctive_strict_opt.mzn:10)

Requires that a set of tasks given by start times s and durations d do not overlap in time. Tasks with duration 0 CANNOT be scheduled at any time, but only when no other task is running. Start times are optional variables, so that absent tasks do not need to be scheduled.

Assumptions:

  • forall i, d[i] >= 0

predicate disjunctive_strict(array [int] of var int: s, array [int] of var int: d) =
assert(index_set(s)==index_set(d), "disjunctive: the array arguments must have identical index sets", forall ( i in index_set(d) ) ( d[i]>=0 ) /\ forall ( i, j in index_set(d) where i < j ) ( s[i]+d[i]<=s[j] \/ s[j]+d[j]<=s[i] ))
(standard decomposition from disjunctive_strict.mzn:9)

Requires that a set of tasks given by start times s and durations d do not overlap in time. Tasks with duration 0 CANNOT be scheduled at any time, but only when no other task is running.

Assumptions:

  • forall i, d[i] >= 0

predicate span(var opt int: s0, var int: d0, array [int] of var opt int: s, array [int] of var int: d) =
assert(index_set(s)==index_set(d), "span: index sets of third and fourth argument must be identical", (occurs(s0) <-> exists ( i in index_set(s) ) ( occurs(s[i]) )) /\ s0==min(s) /\ (absent(s0) -> d0==0) /\ ~+(s0, d0)==max ( i in index_set(s) ) ( ~+(s[i], d[i]) ))
(standard decomposition from span.mzn:5)

Span constraint for optional tasks. Task (s0,d0) spans the optional tasks (s[i],d[i]) in the array arguments.