Fix bin packing assertion failures when using empty array arguments

Resolves #865

changes.rst

@@ -29,6 +29,8 @@ Bug fixes:
 -  Fix evaluation of ``dom_array`` on par arrays (:bugref:`851`).
 -  Fix flattening of array slices inside tuples and records (:bugref:`859`).
 -  Fix defines_var annotation for cyclic definitions (:bugref:`863`).
+-  Fix assertion failures when using arrays as argument to bin packing constraints
+   (:bugref:`865`).
 
 .. _v2.8.7:
 
@@ -67,7 +69,7 @@ Changes:
 -  Enforce strict enum type correctness for set operations (:bugref:`828`).
 -  Add ``par opt`` overloads of ``min`` / ``max`` and return enum values instead
    of coercing to integers.
--  Use half-reification only when there isn't a reification that is a more 
+-  Use half-reification only when there isn't a reification that is a more
    specific match.
 -  Add multidimensional overloads for the ``++`` array concatenation operator.
 
@@ -146,7 +148,7 @@ Bug fixes:
 -  Fix bug in computation of common type of incompatible record types.
 -  Fix crash when type checking nested arrays of tuples or records.
 -  Fix incorrect unification of flattened tuple/record fields with paths
-   enabled. 
+   enabled.
 
 Changes:
 ^^^^^^^^
@@ -225,7 +227,7 @@ Bug fixes:
    (:bugref:`798`).
 -  Fix crash when resolving type aliases for function parameters with ``$T``
    array dimensions (:bugref:`806`).
--  Fix ``default`` operator for ``par opt set`` parameters (:bugref:`809`). 
+-  Fix ``default`` operator for ``par opt set`` parameters (:bugref:`809`).
 -  Fix output of ``par opt set`` enumerated types.
 -  Fix pretty printing of records when using the document printer.
 -  Fix internal error when binding numeric literals to declarations with

share/minizinc/std/bin_packing.mzn

@@ -2,8 +2,8 @@ include "fzn_bin_packing.mzn";
 include "fzn_bin_packing_reif.mzn";
 
 /**  @group globals.packing
-  Requires that each item \p i with weight \a w[\p i], be put into \a bin[\p i] such 
-  that the sum of the weights of the items in each bin does not exceed the 
+  Requires that each item \p i with weight \a w[\p i], be put into \a bin[\p i] such
+  that the sum of the weights of the items in each bin does not exceed the
   capacity \a c.
 
   Assumptions:
@@ -17,7 +17,7 @@ predicate bin_packing(int: c,
                       array[int] of int: w) =
     assert(index_set(bin) == index_set(w),
         "bin_packing: the bin and weight arrays must have identical index sets",
-    assert(lb_array(w) >= 0,
+    assert(length(w) == 0 \/ lb_array(w) >= 0,
         "bin_packing: the weights must be non-negative",
     assert(c >= 0, "bin_packing: capacity must be non-negative",
         fzn_bin_packing(c, bin, w)

share/minizinc/std/bin_packing_capa.mzn

@@ -2,8 +2,8 @@ include "fzn_bin_packing_capa.mzn";
 include "fzn_bin_packing_capa_reif.mzn";
 
 /**  @group globals.packing
-  Requires that each item \p i with weight \a w[\p i], be put into \a bin[\p i] such 
-  that the sum of the weights of the items in each bin \p b does not exceed the 
+  Requires that each item \p i with weight \a w[\p i], be put into \a bin[\p i] such
+  that the sum of the weights of the items in each bin \p b does not exceed the
   capacity \a c[\p b].
 
   Assumptions:
@@ -16,11 +16,11 @@ predicate bin_packing_capa(array[int] of int: c,
                            array[int] of int: w) =
     assert(index_set(bin) = index_set(w),
         "bin_packing_capa: the bin and weight arrays must have identical index sets",
-    assert(lb_array(w) >= 0,
+    assert(length(w) == 0 \/ lb_array(w) >= 0,
         "bin_packing_capa: the weights must be non-negative",
-    assert(lb_array(c) >= 0,
+    assert(length(c) == 0 \/ lb_array(c) >= 0,
         "bin_packing_capa: the capacities must be non-negative",
-        fzn_bin_packing_capa(c, bin, w)    
+        fzn_bin_packing_capa(c, bin, w)
     )));
 
 %-----------------------------------------------------------------------------%

share/minizinc/std/bin_packing_load.mzn

@@ -4,7 +4,7 @@ include "fzn_bin_packing_load.mzn";
 include "fzn_bin_packing_load_reif.mzn";
 
 /**  @group globals.packing
-  Requires that each item \p i with weight \a w[\p i], be put into \a bin[\p i] such 
+  Requires that each item \p i with weight \a w[\p i], be put into \a bin[\p i] such
   that the sum of the weights of the items in each bin \p b is equal to
   \a load[\p b].
 
@@ -18,7 +18,7 @@ predicate bin_packing_load(array[int] of var int: load,
                            array[int] of int: w) =
     assert(index_set(bin) == index_set(w),
         "bin_packing_load: the bin and weight arrays must have identical index sets",
-    assert(lb_array(w) >= 0,
+    assert(length(w) == 0 \/ lb_array(w) >= 0,
         "bin_packing_load: the weights must be non-negative",
         fzn_bin_packing_load(load, bin, w)
     ));

share/minizinc/std/bin_packing_load_fn.mzn

@@ -2,18 +2,24 @@ include "fzn_bin_packing_load.mzn";
 
 /**  @group globals.packing
   Returns the load of each bin resulting from packing each item \p i with
-  weight \a w[\p i] into \a bin[\p i], where the load is defined as 
+  weight \a w[\p i] into \a bin[\p i], where the load is defined as
   the sum of the weights of the items in each bin.
 
   Assumptions:
 
   - forall \p i, \a w[\p i] >=0
 */
-function array[int] of var int: bin_packing_load(array[int] of var int: bin,
-                                                 array[int] of int: w) :: promise_total =
-   assert(index_set(bin) == index_set(w),
-        "bin_packing_load: the bin and weight arrays must have identical index sets",
-   let { array[dom_bounds_array(bin)] of var 0..sum(w): load ::is_defined_var;
-         constraint fzn_bin_packing_load(load,bin,w) ::defines_var(load); }
-   in load
-   );
+function array[int] of var int: bin_packing_load(
+	array[int] of var int: bin,
+	array[int] of int: w
+) :: promise_total =
+	assert(
+		index_set(bin) == index_set(w),
+		"bin_packing_load: the bin and weight arrays must have identical index sets",
+  	if length(bin) > 0 then
+			let {
+				array[dom_bounds_array(bin)] of var 0..sum(w): load ::is_defined_var;
+				constraint fzn_bin_packing_load(load,bin,w) ::defines_var(load);
+			} in load
+		endif
+	);

share/minizinc/std/fzn_bin_packing.mzn

@@ -1,12 +1,15 @@
-predicate fzn_bin_packing(int: c,
-                      array[int] of var int: bin,
-                      array[int] of int: w) =
-    let {
-        int: all_weight = sum(w)
-    } in forall( b in lb_array(bin)..ub_array(bin) ) (
-        sum(i in index_set(bin)) (
-            w[i] * (bin[i] != b)
-        ) >= (all_weight - c)
-    );
+predicate fzn_bin_packing(
+	int: c,
+  array[int] of var int: bin,
+  array[int] of int: w
+) = if length(bin) > 0 then
+  let {
+    int: all_weight = sum(w)
+  } in forall( b in lb_array(bin)..ub_array(bin) ) (
+    sum(i in index_set(bin)) (
+      w[i] * (bin[i] != b)
+    ) >= (all_weight - c)
+  )
+endif;
 
 %-----------------------------------------------------------------------------%

share/minizinc/std/fzn_bin_packing_reif.mzn

@@ -1,11 +1,15 @@
-predicate fzn_bin_packing_reif(int: c,
-                      array[int] of var int: bin,
-                      array[int] of int: w,
-                      var bool: b) =
-        b <-> forall( assigned_bin in lb_array(bin)..ub_array(bin) ) (
-            c >= sum ( i in index_set(bin) ) (
-                w[i] * ( bin[i] == assigned_bin )
-            )
-        );
+predicate fzn_bin_packing_reif(
+	int: c,
+  array[int] of var int: bin,
+  array[int] of int: w,
+  var bool: b
+) =
+	b <-> if length(bin) > 0 then
+		forall(assigned_bin in lb_array(bin)..ub_array(bin)) (
+      sum (i in index_set(bin))(
+        w[i] * (bin[i] == assigned_bin)
+      ) <= c
+    )
+  endif;
 
 %-----------------------------------------------------------------------------%

tests/spec/unit/regression/github_865.mzn

@@ -0,0 +1,19 @@
+/***
+!Test
+solvers: [gecode]
+options:
+  -G: std
+expected: !Result
+  solution: !Solution
+***/
+
+include "bin_packing.mzn";
+include "bin_packing_capa.mzn";
+include "bin_packing_load.mzn";
+include "bin_packing_load_fn.mzn";
+
+constraint bin_packing(0, [], []);
+constraint bin_packing_capa([], [], []);
+constraint bin_packing_load([], [], []);
+constraint bin_packing_load([0], [], []);
+constraint bin_packing_load([], []) == [];