From 3e38ad09aa76a8e2dcb0f9b2edfb4cdf670e5520 Mon Sep 17 00:00:00 2001 From: Mikael Zayenz Lagerkvist Date: Thu, 22 Oct 2026 21:33:27 +0200 Subject: [PATCH 1/5] Expose explicit-end scheduling bindings to MiniZinc --- gecode/flatzinc/mznlib/gecode_fzn.mzn | 70 ++++++++++++++++++++++++--- gecode/flatzinc/registry.cpp | 46 ++++++++++++------ test/flatzinc/native-registry.cpp | 19 ++++++++ 3 files changed, 114 insertions(+), 21 deletions(-) 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..080a10365c 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,19 @@ 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) { + cumulative(s, s.arg2IntVar(ce[4]), s.arg2intvarargs(ce[0]), + 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 +2297,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/test/flatzinc/native-registry.cpp b/test/flatzinc/native-registry.cpp index c2c587ad45..0b733e1cc5 100644 --- a/test/flatzinc/native-registry.cpp +++ b/test/flatzinc/native-registry.cpp @@ -97,6 +97,25 @@ namespace Test { namespace FlatZinc { Create(void) { const std::string sat = "----------\n"; const std::string unsat = "=====UNSATISFIABLE=====\n"; + // Explicit ends retain native scheduling semantics, including shared + // starts, empty tasks, and negative resource usage. + (void) new FlatZincTest(TestTags::check(), + "NativeRegistry::UnaryFlexSharedStart", + "var 0..1:s; var 1..2:e; " + "constraint int_plus(s,1,e); " + "constraint gecode_unary_flex([s,s],[1,1],[e,e]); solve satisfy;", unsat); + (void) new FlatZincTest(TestTags::check(), + "NativeRegistry::CumulativeFlexZeroDuration", + "constraint gecode_cumulative_flex([0,1],[2,0],[2,1],[1,1],1); " + "solve satisfy;", unsat); + (void) new FlatZincTest(TestTags::check(), + "NativeRegistry::CumulativesFlexNegativeUsage", + "constraint gecode_cumulatives_flex([0,0],[2,2],[2,2]," + "[3,-2],[0,0],[1],true); solve satisfy;", sat); + (void) new FlatZincTest(TestTags::check(), + "NativeRegistry::CumulativesFlexLowerBound", + "constraint gecode_cumulatives_flex([0,0],[2,2],[2,2]," + "[3,-2],[0,0],[2],false); solve satisfy;", unsat); (void) new FlatZincTest(TestTags::check(), "NativeRegistry::CumulativeSingletonZeroDuration", "var 0..1:s; var 2..3:r; " From 8eccc46ef57d33dff24db4393579b5a86ba2a21f Mon Sep 17 00:00:00 2001 From: Mikael Zayenz Lagerkvist Date: Thu, 22 Oct 2026 21:33:27 +0200 Subject: [PATCH 2/5] Dispatch cumulative scheduling constraints in MiniZinc --- gecode/flatzinc/mznlib/fzn_cumulative.mzn | 76 +++++++++++++++++++++- gecode/flatzinc/mznlib/fzn_cumulatives.mzn | 10 ++- 2 files changed, 82 insertions(+), 4 deletions(-) diff --git a/gecode/flatzinc/mznlib/fzn_cumulative.mzn b/gecode/flatzinc/mznlib/fzn_cumulative.mzn index 71e5f50bd5..4e3dfff664 100644 --- a/gecode/flatzinc/mznlib/fzn_cumulative.mzn +++ b/gecode/flatzinc/mznlib/fzn_cumulative.mzn @@ -32,11 +32,81 @@ % % +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 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); + 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 { + array[int] of var int: start = array1d(s); + array[int] of var int: duration = array1d(d); + array[int] of var int: usage = array1d(r); + array[int] of var int: end = [start[i] + duration[i] | i in index_set(start)]; + bool: positive = forall(di in d)(lb(di) > 0); + array[int] of int: heights = sort([lb(ri) | ri in r]); + bool: disjunctive = positive /\ + (heights[1] > ub(b) div 2 \/ + (heights[2] > ub(b) div 2 /\ heights[1] + heights[2] > ub(b))); + } in + if disjunctive then + forall(ri in r)(ri <= b) /\ + if is_fixed(d) then + gecode_schedule_unary(start, fix(duration)) + else + gecode_unary_flex(start, duration, end) + endif + elseif is_fixed(r) then + if positive then + if is_fixed(d) then + gecode_schedule_cumulative_optional(start, fix(duration), + fix(usage), [true | i in index_set(start)], b) + else + gecode_cumulative_flex(start, duration, end, fix(usage), b) + endif + else + % MiniZinc's zero-duration tasks consume no capacity. + gecode_cumulative_flex_optional(start, duration, end, fix(usage), b, + [duration[i] > 0 | i in index_set(start)]) + endif + elseif positive /\ is_fixed(b) then + gecode_cumulatives_flex(start, duration, end, usage, + [0 | i in index_set(start)], [fix(b)], true) + else + % With nonnegative usage the maximum load occurs at a task start. + % Unlike a time-point decomposition, size does not depend on the horizon. + forall(j in index_set(start)) ( + sum(i in index_set(start)) ( + bool2int(start[i] <= start[j] /\ start[j] < end[i]) * usage[i] + ) <= b + ) + 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); + 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..d8873550cc 100644 --- a/gecode/flatzinc/mznlib/fzn_cumulatives.mzn +++ b/gecode/flatzinc/mznlib/fzn_cumulatives.mzn @@ -9,7 +9,9 @@ predicate fzn_cumulatives(array[int] of var int: s, 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) + gecode_cumulatives_flex(s, d, + [s[i] + d[i] | i in index_set(s)], r, + [m_i - min_m | m_i in m], fix(b), upper) else fzn_cumulatives_decomp(s, d, r, m, b, upper) endif; @@ -20,3 +22,9 @@ predicate gecode_cumulatives(array[int] of var int: s, 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); From 149951b813fe20808ae821245b37c4d180a72d74 Mon Sep 17 00:00:00 2001 From: Mikael Zayenz Lagerkvist Date: Thu, 22 Oct 2026 21:33:27 +0200 Subject: [PATCH 3/5] Encode zero-duration cumulative tasks with alternate machines --- .github/ci/flatzinc-tools-smoke.sh | 28 +++++++++++++++++++++++ gecode/flatzinc/mznlib/fzn_cumulative.mzn | 13 ++++++++++- 2 files changed, 40 insertions(+), 1 deletion(-) diff --git a/.github/ci/flatzinc-tools-smoke.sh b/.github/ci/flatzinc-tools-smoke.sh index 22b8667eb8..975e2da508 100644 --- a/.github/ci/flatzinc-tools-smoke.sh +++ b/.github/ci/flatzinc-tools-smoke.sh @@ -17,4 +17,32 @@ 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"; +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); +solve minimize b + zero_b; +output ["capacity=",show(b)," empty-capacity=",show(zero_b),"\n"]; +MZN + ) + [[ "$result" == *"capacity=3 empty-capacity=1"* ]] + fi diff --git a/gecode/flatzinc/mznlib/fzn_cumulative.mzn b/gecode/flatzinc/mznlib/fzn_cumulative.mzn index 4e3dfff664..615eeb0ccc 100644 --- a/gecode/flatzinc/mznlib/fzn_cumulative.mzn +++ b/gecode/flatzinc/mznlib/fzn_cumulative.mzn @@ -62,6 +62,8 @@ predicate fzn_cumulative(array[int] of var int: s, array[int] of var int: usage = array1d(r); array[int] of var int: end = [start[i] + duration[i] | i in index_set(start)]; bool: positive = forall(di in d)(lb(di) > 0); + int: early = min([lb(si) | si in start]); + int: late = max([ub(start[i]) + ub(duration[i]) | i in index_set(start)]); array[int] of int: heights = sort([lb(ri) | ri in r]); bool: disjunctive = positive /\ (heights[1] > ub(b) div 2 \/ @@ -90,8 +92,17 @@ predicate fzn_cumulative(array[int] of var int: s, elseif positive /\ is_fixed(b) then gecode_cumulatives_flex(start, duration, end, usage, [0 | i in index_set(start)], [fix(b)], true) + elseif late - early <= 2147483646 then + % Put zero-duration tasks on a separate machine. A task spanning the + % horizon with usage -b turns the variable bound into a fixed zero bound. + % The second bound is immaterial: only empty tasks use that machine. + gecode_cumulatives_flex(start ++ [early], + duration ++ [late - early], end ++ [late], usage ++ [-b], + [bool2int(duration[i] = 0) | i in index_set(start)] ++ [0], + [0, max([ub(ri) | ri in usage])], true) else - % With nonnegative usage the maximum load occurs at a task start. + % Avoid an unrepresentable spanning duration. With nonnegative usage + % the maximum load occurs at a task start. % Unlike a time-point decomposition, size does not depend on the horizon. forall(j in index_set(start)) ( sum(i in index_set(start)) ( From c7cb91cb9741a6a95cc912a08efaf394edcd3135 Mon Sep 17 00:00:00 2001 From: Mikael Zayenz Lagerkvist Date: Thu, 22 Oct 2026 21:57:45 +0200 Subject: [PATCH 4/5] Fix scheduling bounds, shared starts, and resource overflow --- .github/ci/flatzinc-tools-smoke.sh | 26 ++- gecode/flatzinc/mznlib/fzn_cumulative.mzn | 177 ++++++++++++++------- gecode/flatzinc/mznlib/fzn_cumulatives.mzn | 60 ++++--- gecode/flatzinc/registry.cpp | 4 +- test/flatzinc/native-registry.cpp | 6 + 5 files changed, 190 insertions(+), 83 deletions(-) diff --git a/.github/ci/flatzinc-tools-smoke.sh b/.github/ci/flatzinc-tools-smoke.sh index 975e2da508..1e1b9bb4d5 100644 --- a/.github/ci/flatzinc-tools-smoke.sh +++ b/.github/ci/flatzinc-tools-smoke.sh @@ -23,6 +23,7 @@ MZN 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; @@ -39,10 +40,29 @@ 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); -solve minimize b + zero_b; -output ["capacity=",show(b)," empty-capacity=",show(zero_b),"\n"]; +% 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"* ]] + [[ "$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 615eeb0ccc..bcccb341c9 100644 --- a/gecode/flatzinc/mznlib/fzn_cumulative.mzn +++ b/gecode/flatzinc/mznlib/fzn_cumulative.mzn @@ -32,22 +32,42 @@ % % -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_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 fzn_cumulative(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 @@ -57,67 +77,108 @@ predicate fzn_cumulative(array[int] of var int: s, gecode_cumulatives(s, d, r, b) else let { - array[int] of var int: start = array1d(s); - array[int] of var int: duration = array1d(d); - array[int] of var int: usage = array1d(r); - array[int] of var int: end = [start[i] + duration[i] | i in index_set(start)]; - bool: positive = forall(di in d)(lb(di) > 0); - int: early = min([lb(si) | si in start]); - int: late = max([ub(start[i]) + ub(duration[i]) | i in index_set(start)]); - array[int] of int: heights = sort([lb(ri) | ri in r]); - bool: disjunctive = positive /\ - (heights[1] > ub(b) div 2 \/ - (heights[2] > ub(b) div 2 /\ heights[1] + heights[2] > ub(b))); + % 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 disjunctive then - forall(ri in r)(ri <= b) /\ - if is_fixed(d) then + 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(r) then - if positive then - if is_fixed(d) then - gecode_schedule_cumulative_optional(start, fix(duration), - fix(usage), [true | i in index_set(start)], b) + 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), b) + 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), b, - [duration[i] > 0 | i in index_set(start)]) + gecode_cumulative_flex_optional( + start, + duration, + end, + fix(usage), + capacity, + [duration[i] > 0 | i in index_set(start)], + ) endif - elseif positive /\ is_fixed(b) then - gecode_cumulatives_flex(start, duration, end, usage, - [0 | i in index_set(start)], [fix(b)], true) - elseif late - early <= 2147483646 then + 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 % Put zero-duration tasks on a separate machine. A task spanning the - % horizon with usage -b turns the variable bound into a fixed zero bound. + % horizon with usage -capacity turns the variable bound into a fixed zero bound. % The second bound is immaterial: only empty tasks use that machine. - gecode_cumulatives_flex(start ++ [early], - duration ++ [late - early], end ++ [late], usage ++ [-b], + % 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) + [0, max([ub(ri) | ri in usage])], + true, + ) else - % Avoid an unrepresentable spanning duration. With nonnegative usage - % the maximum load occurs at a task start. - % Unlike a time-point decomposition, size does not depend on the horizon. - forall(j in index_set(start)) ( - sum(i in index_set(start)) ( + % 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] - ) <= b + ) <= 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); +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); +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 d8873550cc..c909fe8e9d 100644 --- a/gecode/flatzinc/mznlib/fzn_cumulatives.mzn +++ b/gecode/flatzinc/mznlib/fzn_cumulatives.mzn @@ -1,30 +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_flex(s, d, - [s[i] + d[i] | i in index_set(s)], 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); +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/registry.cpp b/gecode/flatzinc/registry.cpp index 080a10365c..7c870fbd7e 100755 --- a/gecode/flatzinc/registry.cpp +++ b/gecode/flatzinc/registry.cpp @@ -2085,7 +2085,9 @@ fvar, } void p_cumulative_flex(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { - cumulative(s, s.arg2IntVar(ce[4]), s.arg2intvarargs(ce[0]), + 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)); } diff --git a/test/flatzinc/native-registry.cpp b/test/flatzinc/native-registry.cpp index 0b733e1cc5..2dc6dd1b51 100644 --- a/test/flatzinc/native-registry.cpp +++ b/test/flatzinc/native-registry.cpp @@ -104,6 +104,12 @@ namespace Test { namespace FlatZinc { "var 0..1:s; var 1..2:e; " "constraint int_plus(s,1,e); " "constraint gecode_unary_flex([s,s],[1,1],[e,e]); solve satisfy;", unsat); + (void) new FlatZincTest(TestTags::check(), + "NativeRegistry::CumulativeFlexSharedStart", + "var 0..1:s; var 1..2:e; " + "constraint int_plus(s,1,e); " + "constraint gecode_cumulative_flex([s,s],[1,1],[e,e],[1,1],1); " + "solve satisfy;", unsat); (void) new FlatZincTest(TestTags::check(), "NativeRegistry::CumulativeFlexZeroDuration", "constraint gecode_cumulative_flex([0,1],[2,0],[2,1],[1,1],1); " From 417ee02efed0014cf53d9b5e9d06d1083ba96629 Mon Sep 17 00:00:00 2001 From: Mikael Zayenz Lagerkvist Date: Fri, 23 Oct 2026 06:51:56 +0200 Subject: [PATCH 5/5] Fix signed cumulatives profile propagation Track each task's active signed profile contribution at both endpoints, including cancellation of empty profiles. This restores producer bounds for upper and lower resource limits. Strengthen the MiniZinc alternate cumulative encoding with each positive- duration task's resource bound, preserving zero-duration semantics. Add focused propagation and empty-profile regressions. --- gecode/flatzinc/mznlib/fzn_cumulative.mzn | 3 ++ gecode/int/cumulatives/val.hpp | 19 +++------ test/int/cumulatives.cpp | 52 +++++++++++++++++++++++ 3 files changed, 60 insertions(+), 14 deletions(-) diff --git a/gecode/flatzinc/mznlib/fzn_cumulative.mzn b/gecode/flatzinc/mznlib/fzn_cumulative.mzn index bcccb341c9..91b3bb585c 100644 --- a/gecode/flatzinc/mznlib/fzn_cumulative.mzn +++ b/gecode/flatzinc/mznlib/fzn_cumulative.mzn @@ -138,6 +138,9 @@ predicate fzn_cumulative( 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. 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