Expose explicit-end MiniZinc scheduling and avoid horizon expansion

.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

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,
+);

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,
+);

gecode/flatzinc/mznlib/gecode_fzn.mzn

@@ -166,20 +166,76 @@ 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,
   array[int] of var int: end,
   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,