From 670d77a0d1557b864db609fc4768b8660315c10d Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 12 Nov 2024 15:22:41 +1100 Subject: [PATCH] Fix bin packing assertion failures when using empty array arguments Resolves #865 --- changes.rst | 8 ++++--- share/minizinc/std/bin_packing.mzn | 6 +++--- share/minizinc/std/bin_packing_capa.mzn | 10 ++++----- share/minizinc/std/bin_packing_load.mzn | 4 ++-- share/minizinc/std/bin_packing_load_fn.mzn | 24 +++++++++++++-------- share/minizinc/std/fzn_bin_packing.mzn | 23 +++++++++++--------- share/minizinc/std/fzn_bin_packing_reif.mzn | 22 +++++++++++-------- tests/spec/unit/regression/github_865.mzn | 19 ++++++++++++++++ 8 files changed, 75 insertions(+), 41 deletions(-) create mode 100644 tests/spec/unit/regression/github_865.mzn diff --git a/changes.rst b/changes.rst index 08c1078d3..2f011e85d 100644 --- a/changes.rst +++ b/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 diff --git a/share/minizinc/std/bin_packing.mzn b/share/minizinc/std/bin_packing.mzn index b6d177433..158ba4910 100644 --- a/share/minizinc/std/bin_packing.mzn +++ b/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) diff --git a/share/minizinc/std/bin_packing_capa.mzn b/share/minizinc/std/bin_packing_capa.mzn index 9adc3e34d..da2b8f93b 100644 --- a/share/minizinc/std/bin_packing_capa.mzn +++ b/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) ))); %-----------------------------------------------------------------------------% diff --git a/share/minizinc/std/bin_packing_load.mzn b/share/minizinc/std/bin_packing_load.mzn index 10b2c6b50..cd5946ad3 100644 --- a/share/minizinc/std/bin_packing_load.mzn +++ b/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) )); diff --git a/share/minizinc/std/bin_packing_load_fn.mzn b/share/minizinc/std/bin_packing_load_fn.mzn index be841ea6b..4c9cf96d2 100644 --- a/share/minizinc/std/bin_packing_load_fn.mzn +++ b/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 + ); diff --git a/share/minizinc/std/fzn_bin_packing.mzn b/share/minizinc/std/fzn_bin_packing.mzn index a615379db..1821c79e7 100644 --- a/share/minizinc/std/fzn_bin_packing.mzn +++ b/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; %-----------------------------------------------------------------------------% diff --git a/share/minizinc/std/fzn_bin_packing_reif.mzn b/share/minizinc/std/fzn_bin_packing_reif.mzn index 2437908de..46557b829 100644 --- a/share/minizinc/std/fzn_bin_packing_reif.mzn +++ b/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; %-----------------------------------------------------------------------------% diff --git a/tests/spec/unit/regression/github_865.mzn b/tests/spec/unit/regression/github_865.mzn new file mode 100644 index 000000000..e06a83d19 --- /dev/null +++ b/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([], []) == [];