diff --git a/.github/ci/flatzinc-tools-smoke.sh b/.github/ci/flatzinc-tools-smoke.sh index 22b8667eb8..1e1b9bb4d5 100644 --- a/.github/ci/flatzinc-tools-smoke.sh +++ b/.github/ci/flatzinc-tools-smoke.sh @@ -17,4 +17,52 @@ output ["gcd=", show(g), "\n"]; MZN ) [[ "$result" == *"gcd=6"* ]] + + # Shared explicit ends and a zero-duration task with excessive usage. + # Exercise the MiniZinc dispatch as well as all three explicit-end bindings. + result=$("$prefix/bin/mzn-gecode" - <<'MZN' +include "gecode.mzn"; +include "cumulative.mzn"; +include "cumulatives.mzn"; +array[1..3] of var 0..2: d; +array[1..3] of var 1..100: r; +var 1..3: b; +array[1..3] of var 0..3: e; +constraint d = [2,0,1] /\ r = [2,100,1]; +constraint forall(i in 1..3)(e[i] = [0,1,0][i] + d[i]); +constraint fzn_cumulative([0,1,0],d,r,b) :: gecode_full_propagation; +constraint gecode_unary_flex([0,2],[2,1],[e[1],3]); +constraint gecode_cumulative_flex([0,0],[2,1],[e[1],e[3]],[2,1],b); +constraint gecode_cumulatives_flex([0,0],[2,2],[e[1],e[1]], + [3,-2],[0,0],[1],true); +% Keep usages variable so this call uses the alternate-machine encoding. +array[1..2] of var 1..2: zero_r; +var 1..3: zero_b; +constraint sum(zero_r) = 3; +constraint fzn_cumulative([0,0],[0,2],zero_r,zero_b); +% Large usages must use a decomposition with a representable resource sum. +var {0,1000000000}: large_usage; +var {0,1000000000}: large_capacity; +constraint fzn_cumulative([0,0,0,0],[1,1,1,1], + [large_usage,large_usage,large_usage,large_usage],large_capacity); +% Unbounded MiniZinc domains retain Gecode's implicit finite bounds. +array[1..2] of var int: wide_start; +array[1..2] of var 0..infinity: wide_duration; +array[1..2] of var 0..infinity: wide_usage; +var 0..infinity: wide_capacity; +constraint fzn_cumulative(wide_start,wide_duration,wide_usage,wide_capacity); +% Explicit end domains must not exceed Gecode's limit after flattening. +array[1..2] of var 2147483645..2147483646: late_start; +array[1..2] of var 0..2: late_duration; +array[1..2] of var 0..2: late_usage; +constraint fzn_cumulative(late_start,late_duration,late_usage,zero_b); +constraint fzn_cumulatives(late_start,late_duration,late_usage,[0,0],[2],true,0); +solve :: int_search([large_usage,large_capacity],input_order,indomain_max,complete) + minimize b + zero_b; +output ["capacity=",show(b)," empty-capacity=",show(zero_b), + " large-usage=",show(large_usage),"\n"]; +MZN + ) + [[ "$result" == *"capacity=3 empty-capacity=1 large-usage=0"* ]] + fi diff --git a/gecode/flatzinc/mznlib/fzn_cumulative.mzn b/gecode/flatzinc/mznlib/fzn_cumulative.mzn index 71e5f50bd5..91b3bb585c 100644 --- a/gecode/flatzinc/mznlib/fzn_cumulative.mzn +++ b/gecode/flatzinc/mznlib/fzn_cumulative.mzn @@ -32,11 +32,156 @@ % % -predicate fzn_cumulative(array[int] of var int: s, - array[int] of var int: d, - array[int] of var int: r, var int: b) = - gecode_cumulatives(s, d, r, b); +predicate gecode_unary_flex( + array[int] of var int: s, + array[int] of var int: d, + array[int] of var int: e, +); +predicate gecode_cumulative_flex( + array[int] of var int: s, + array[int] of var int: d, + array[int] of var int: e, + array[int] of int: r, + var int: b, +); +predicate gecode_cumulative_flex_optional( + array[int] of var int: s, + array[int] of var int: d, + array[int] of var int: e, + array[int] of int: r, + var int: b, + array[int] of var bool: present, +); +predicate gecode_cumulatives_flex( + array[int] of var int: s, + array[int] of var int: d, + array[int] of var int: e, + array[int] of var int: r, + array[int] of var int: m, + array[int] of int: b, + bool: upper, +); -predicate gecode_cumulatives(array[int] of var int: s, - array[int] of var int: d, - array[int] of var int: r, var int: b); +predicate fzn_cumulative( + array[int] of var int: s, + array[int] of var int: d, + array[int] of var int: r, + var int: b, +) = + if length(s) = 0 then + true + elseif length(s) = 1 then + (d[min(index_set(d))] > 0 -> r[min(index_set(r))] <= b) + elseif lb(b) < 0 then + % Retain the legacy treatment of negative capacity domains. + gecode_cumulatives(s, d, r, b) + else + let { + % Model-level task bounds must fit Gecode's implicit integer domain. + int: int_limit = 2147483646; + array[int] of var -int_limit .. int_limit: start = array1d(s); + array[int] of var -int_limit .. int_limit: duration = array1d(d); + array[int] of var -int_limit .. int_limit: usage = array1d(r); + var -int_limit .. int_limit: capacity = b; + array[int] of var -int_limit .. int_limit: end = [start[i] + duration[i] | i in index_set(start)]; + bool: positive_durations = forall (di in duration) ( + lb(di) > 0 + ); + int: earliest_start = min([lb(si) | si in start]); + int: latest_end = max([ub(ei) | ei in end]); + array[int] of int: min_usages = sort([lb(ri) | ri in usage]); + bool: is_disjunctive = positive_durations /\ + (min_usages[1] > ub(capacity) div 2 \/ (min_usages[2] > ub(capacity) div 2 /\ + min_usages[1] + min_usages[2] > ub(capacity))); + } in + if is_disjunctive then + forall (ri in usage) ( + ri <= capacity + ) /\ + if is_fixed(duration) then + gecode_schedule_unary(start, fix(duration)) + else + gecode_unary_flex(start, duration, end) + endif + elseif is_fixed(usage) then + if positive_durations then + if is_fixed(duration) then + gecode_schedule_cumulative_optional( + start, + fix(duration), + fix(usage), + [true | i in index_set(start)], + capacity, + ) + else + gecode_cumulative_flex(start, duration, end, fix(usage), capacity) + endif + else + % MiniZinc's zero-duration tasks consume no capacity. + gecode_cumulative_flex_optional( + start, + duration, + end, + fix(usage), + capacity, + [duration[i] > 0 | i in index_set(start)], + ) + endif + elseif positive_durations /\ is_fixed(capacity) then + gecode_cumulatives_flex( + start, + duration, + end, + usage, + [0 | i in index_set(start)], + [fix(capacity)], + true, + ) + elseif latest_end - earliest_start <= int_limit /\ sum (ri in usage) (ub(ri)) <= int_limit then + forall (i in index_set(start)) ( + duration[i] > 0 -> usage[i] <= capacity + ) /\ + % Put zero-duration tasks on a separate machine. A task spanning the + % horizon with usage -capacity turns the variable bound into a fixed zero bound. + % The second bound is immaterial: only empty tasks use that machine. + % The usage-sum guard keeps the native integer profile representable. + gecode_cumulatives_flex( + start ++ [earliest_start], + duration ++ [latest_end - earliest_start], + end ++ [latest_end], + usage ++ [-capacity], + [bool2int(duration[i] = 0) | i in index_set(start)] ++ [0], + [0, max([ub(ri) | ri in usage])], + true, + ) + else + % Avoid an unrepresentable spanning duration or resource profile. + % With nonnegative usage the maximum load occurs at a task start. + % The number of constraints depends only on task count. + forall (j in index_set(start)) ( + sum (i in index_set(start)) ( + bool2int(start[i] <= start[j] /\ start[j] < end[i]) * usage[i] + ) <= capacity + ) + endif + endif; + +predicate gecode_schedule_unary( + array[int] of var int: s, + array[int] of int: d, +); +predicate gecode_schedule_cumulative_optional( + array[int] of var int: s, + array[int] of int: d, + array[int] of int: r, + array[int] of var bool: present, + var int: b, +); + +% Retained for compatibility with existing FlatZinc and MiniZinc models. +predicate gecode_cumulatives( + array[int] of var int: s, + array[int] of var int: d, + array[int] of var int: r, + var int: b, +); diff --git a/gecode/flatzinc/mznlib/fzn_cumulatives.mzn b/gecode/flatzinc/mznlib/fzn_cumulatives.mzn index cdc91f4e77..c909fe8e9d 100644 --- a/gecode/flatzinc/mznlib/fzn_cumulatives.mzn +++ b/gecode/flatzinc/mznlib/fzn_cumulatives.mzn @@ -1,22 +1,48 @@ include "fzn_cumulatives_decomp.mzn"; -predicate fzn_cumulatives(array[int] of var int: s, - array[int] of var int: d, - array[int] of var int: r, - array[int] of var int: m, - array[int] of var int: b, - bool: upper, - int: min_m) = +predicate fzn_cumulatives( + array[int] of var int: s, + array[int] of var int: d, + array[int] of var int: r, + array[int] of var int: m, + array[int] of var int: b, + bool: upper, + int: min_m, +) = if is_fixed(b) then % Propagator only supports fixed bounds - gecode_cumulatives(s, d, r, [m_i - min_m | m_i in m], fix(b), upper) + let { + % Match the implicit integer bounds used by the legacy registry binding. + array[int] of var -2147483646 .. 2147483646: end = [s[i] + d[i] | i in index_set(s)]; + } in + gecode_cumulatives_flex( + s, + d, + end, + r, + [m_i - min_m | m_i in m], + fix(b), + upper, + ) else fzn_cumulatives_decomp(s, d, r, m, b, upper) endif; -predicate gecode_cumulatives(array[int] of var int: s, - array[int] of var int: d, - array[int] of var int: r, - array[int] of var int: m, - array[int] of int: b, - bool: upper); +predicate gecode_cumulatives( + array[int] of var int: s, + array[int] of var int: d, + array[int] of var int: r, + array[int] of var int: m, + array[int] of int: b, + bool: upper, +); + +predicate gecode_cumulatives_flex( + array[int] of var int: s, + array[int] of var int: d, + array[int] of var int: e, + array[int] of var int: r, + array[int] of var int: m, + array[int] of int: b, + bool: upper, +); diff --git a/gecode/flatzinc/mznlib/gecode_fzn.mzn b/gecode/flatzinc/mznlib/gecode_fzn.mzn index e8c7d1b1d3..f77d66569a 100644 --- a/gecode/flatzinc/mznlib/gecode_fzn.mzn +++ b/gecode/flatzinc/mznlib/gecode_fzn.mzn @@ -166,9 +166,62 @@ predicate gecode_regular_nfa_int_fzn( set of int: final, ); -% Constrain tasks whose present entry is true not to overlap. Durations are -% nonnegative. The arrays have equal lengths. The caller must also constrain -% start[i] + duration[i] = end[i] for each present task. +/** @group gecode.constraints + Schedule tasks with explicit start, duration, and end variables on a unary + resource. Durations are nonnegative. A zero-duration task cannot occur + strictly inside another task. The arrays must have equal lengths. + The caller must also constrain start[i] + duration[i] = end[i]. + Reification is not supported. +*/ +predicate gecode_unary_flex( + array[int] of var int: start, + array[int] of var int: duration, + array[int] of var int: end, +); + +/** @group gecode.constraints + Schedule tasks with explicit start, duration, and end variables on a + cumulative resource. Durations, usage, and capacity are nonnegative. + The arrays must have equal lengths. The caller must also constrain + start[i] + duration[i] = end[i]. At each task start, its usage plus the usage + of tasks strictly spanning that start must fit capacity, even for a + zero-duration task. Use cumulative for MiniZinc's empty-task semantics. + Reification is not supported. +*/ +predicate gecode_cumulative_flex( + array[int] of var int: start, + array[int] of var int: duration, + array[int] of var int: end, + array[int] of int: usage, + var int: capacity, +); + +/** @group gecode.constraints + Schedule tasks on machines numbered 0..length(capacity)-1 with explicit + start, duration, and end variables. Usage may be negative. If upper is true, + capacity bounds usage from above, otherwise from below. The bound applies + at times when at least one task executes on the machine. + Task arrays must have equal lengths. The caller must constrain + start[i] + duration[i] = end[i], nonnegative durations, and machine domains. + Reification is not supported. Only value propagation is available. +*/ +predicate gecode_cumulatives_flex( + array[int] of var int: start, + array[int] of var int: duration, + array[int] of var int: end, + array[int] of var int: usage, + array[int] of var int: machine, + array[int] of int: capacity, + bool: upper, +); + +/** @group gecode.constraints + Schedule the tasks whose present entry is true on a unary resource. + Durations are nonnegative. Zero-duration tasks have the same semantics as + gecode_unary_flex. The arrays must have equal lengths. The caller must + constrain start[i] + duration[i] = end[i] for each present task. + Reification is not supported. +*/ predicate gecode_unary_flex_optional( array[int] of var int: start, array[int] of var int: duration, @@ -176,10 +229,13 @@ predicate gecode_unary_flex_optional( array[int] of var bool: present, ); -% Constrain the total usage of tasks whose present entry is true not to -% exceed capacity. Durations, usage, and capacity are nonnegative. -% The arrays have equal lengths. The caller must also constrain -% start[i] + duration[i] = end[i] for each present task. +/** @group gecode.constraints + Schedule the tasks whose present entry is true on a cumulative resource. + Durations, usage, and capacity are nonnegative. Zero-duration tasks have + the same semantics as gecode_cumulative_flex. The arrays must have equal + lengths. The caller must constrain start[i] + duration[i] = end[i] for each + present task. Reification is not supported. +*/ predicate gecode_cumulative_flex_optional( array[int] of var int: start, array[int] of var int: duration, diff --git a/gecode/flatzinc/registry.cpp b/gecode/flatzinc/registry.cpp index 97dd20b6e4..7c870fbd7e 100755 --- a/gecode/flatzinc/registry.cpp +++ b/gecode/flatzinc/registry.cpp @@ -1366,25 +1366,31 @@ namespace Gecode { namespace FlatZinc { void p_cumulatives(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { - if (ce.size() == 6) { - // Full cumulatives call + if (ce.size() == 6 || ce.size() == 7) { + // The seven-argument interface supplies end variables explicitly. + int offset = ce.size() == 7 ? 1 : 0; IntVarArgs start = s.arg2intvarargs(ce[0]); IntVarArgs duration = s.arg2intvarargs(ce[1]); - IntVarArgs resources = s.arg2intvarargs(ce[2]); - IntVarArgs machine = s.arg2intvarargs(ce[3]); - IntArgs bound = s.arg2intargs(ce[4]); - bool upper = ce[5]->getBool(); + IntVarArgs resources = s.arg2intvarargs(ce[2+offset]); + IntVarArgs machine = s.arg2intvarargs(ce[3+offset]); + IntArgs bound = s.arg2intargs(ce[4+offset]); + bool upper = ce[5+offset]->getBool(); int n = start.size(); + IntVarArgs end; + if (offset) { + end = s.arg2intvarargs(ce[2]); + } else { + end = IntVarArgs(n); + for (int i=n; i--;) + end[i] = expr(s, start[i] + duration[i]); + } + if (duration.assigned()) { IntArgs durationI(n); for (int i = n; (i--) != 0;) { durationI[i] = duration[i].val(); } - IntVarArgs end(n); - for (int i = n; (i--) != 0;) { - end[i] = expr(s, start[i] + durationI[i]); - } if (machine.assigned()) { IntArgs machineI(n); for (int i = n; (i--) != 0;) { @@ -1409,10 +1415,6 @@ namespace Gecode { namespace FlatZinc { cumulatives(s, machine, start, durationI, end, resources, bound, upper, s.ann2ipl(ann)); } } else { - IntVarArgs end(n); - for (int i = n; (i--) != 0;) { - end[i] = expr(s, start[i] + duration[i]); - } if (machine.assigned()) { IntArgs machineI(n); for (int i = n; (i--) != 0;) { @@ -2075,6 +2077,21 @@ fvar, ce[3]->getBool(), s.ann2ipl(ann)); } + void p_unary_flex(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + IntVarArgs start = s.arg2intvarargs(ce[0]); + unshare(s, start); + unary(s, start, s.arg2intvarargs(ce[1]), s.arg2intvarargs(ce[2]), + s.ann2ipl(ann)); + } + + void p_cumulative_flex(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { + IntVarArgs start = s.arg2intvarargs(ce[0]); + unshare(s, start); + cumulative(s, s.arg2IntVar(ce[4]), start, + s.arg2intvarargs(ce[1]), s.arg2intvarargs(ce[2]), + s.arg2intargs(ce[3]), s.ann2ipl(ann)); + } + void p_unary_flex_optional(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs start = s.arg2intvarargs(ce[0]); unshare(s, start); @@ -2282,6 +2299,9 @@ fvar, registry().add("member_bool",&p_member_bool); registry().add("gecode_member_bool_reif",&p_member_bool_reif); + registry().add("gecode_unary_flex", &p_unary_flex); + registry().add("gecode_cumulative_flex", &p_cumulative_flex); + registry().add("gecode_cumulatives_flex", &p_cumulatives); registry().add("gecode_unary_flex_optional", &p_unary_flex_optional); registry().add("gecode_cumulative_flex_optional", &p_cumulative_flex_optional); registry().add("gecode_array_int_ne", &p_array_int_ne); diff --git a/gecode/int/cumulatives/val.hpp b/gecode/int/cumulatives/val.hpp index 177bf8f5e6..f3c48f4487 100755 --- a/gecode/int/cumulatives/val.hpp +++ b/gecode/int/cumulatives/val.hpp @@ -138,15 +138,9 @@ namespace Gecode { namespace Int { namespace Cumulatives { int date; /// The quantity changed by this event (if any) int inc; - /** If the type is EVENT_PROF and it is the first of the pair, - * this value is true. Added to handle contribution-values - * correctly for both at_most and at_least. - */ - bool first_prof; - /// Simple constructor - Event(ev_t _e, int _task, int _date, int _inc = 0, bool _first_prof = false) - : e(_e), task(_task), date(_date), inc(_inc), first_prof(_first_prof) + Event(ev_t _e, int _task, int _date, int _inc = 0) + : e(_e), task(_task), date(_date), inc(_inc) {} // Default constructor for region-allocated memory @@ -305,7 +299,7 @@ namespace Gecode { namespace Int { namespace Cumulatives { ? u[t].min() > 0 : u[t].max() < 0) { GECODE_PUSH_EVENTS(Event(EVENT_PROF, t, s[t].max(), - at_most ? u[t].min() : u[t].max(), true)); + at_most ? u[t].min() : u[t].max())); GECODE_PUSH_EVENTS(Event(EVENT_PROF, t, e[t].min(), at_most ? -u[t].min() : -u[t].max())); } @@ -316,7 +310,7 @@ namespace Gecode { namespace Int { namespace Cumulatives { ? u[t].min() < 0 : u[t].max() > 0) { GECODE_PUSH_EVENTS(Event(EVENT_PROF, t, s[t].min(), - at_most ? u[t].min() : u[t].max(), true)); + at_most ? u[t].min() : u[t].max())); GECODE_PUSH_EVENTS(Event(EVENT_PROF, t, e[t].max(), at_most ? -u[t].min() : -u[t].max())); } @@ -361,10 +355,7 @@ namespace Gecode { namespace Int { namespace Cumulatives { ntask += events[ei].inc; } else /* if (events[ei].e == EVENT_PROF) */ { su += events[ei].inc; - if(events[ei].first_prof) - contribution[events[ei].task] = at_most - ? std::max(contribution[events[ei].task], events[ei].inc) - : std::min(contribution[events[ei].task], events[ei].inc); + contribution[events[ei].task] += events[ei].inc; } } else /* if (events[ei].e == EVENT_PRUN) */ { assert(prune_tasks_size