Revised definitions of global constraints

informarte · Oct 31, 2018 · 3dea2d9 · 3dea2d9
1 parent 3940c2b
commit 3dea2d9
Show file tree

Hide file tree

Showing 11 changed files with 46 additions and 107 deletions.
diff --git a/resources/mzn/lib/yuck/bin_packing.mzn b/resources/mzn/lib/yuck/bin_packing.mzn
@@ -1,10 +1,9 @@
 include "cumulative.mzn";
 
-predicate safe_bin_packing(
+predicate bin_packing(
     int: c,
     array[int] of var int: bin,
-    array[int] of int: w,
-    var bool: continuation) =
+    array[int] of int: w) =
     assert(
         index_set(bin) == index_set(w),
         "bin_packing: the bin and weight arrays must have identical index sets",
@@ -14,10 +13,4 @@ predicate safe_bin_packing(
             assert(
                 c >= 0,
                 "bin_packing: capacity must be non-negative",
-                continuation)));
-
-predicate bin_packing(
-    int: c,
-    array[int] of var int: bin,
-    array[int] of int: w) =
-    safe_bin_packing(c, bin, w, cumulative(bin, [1 | i in index_set(bin)], w, c));
+                cumulative(bin, [1 | i in index_set(bin)], w, c))));
diff --git a/resources/mzn/lib/yuck/bin_packing_capa.mzn b/resources/mzn/lib/yuck/bin_packing_capa.mzn
@@ -1,10 +1,9 @@
 include "cumulative.mzn";
 
-predicate safe_bin_packing_capa(
+predicate bin_packing_capa(
     array[int] of int: c,
     array[int] of var int: bin,
-    array[int] of int: w,
-    var bool: continuation) =
+    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",
@@ -14,22 +13,15 @@ predicate safe_bin_packing_capa(
             assert(
                 lb_array(c) >= 0,
                 "bin_packing_capa: the capacities must be non-negative",
-                continuation)));
+                forall (i in index_set(bin)) (
+                    min(index_set(c)) <= bin[i] /\ bin[i] <= max(index_set(c))
+                )
+                /\
+                let {int: cMax = max(c),
+                     array[int] of int: fixed = [i | i in index_set(c) where c[i] < cMax]} in
+                cumulative(
+                    bin ++ fixed,
+                    [1 | i in bin ++ fixed],
+                    w ++ [cMax - c[i] | i in fixed],
+                    cMax))));
 
-predicate bin_packing_capa(
-    array[int] of int: c,
-    array[int] of var int: bin,
-    array[int] of int: w) =
-    safe_bin_packing_capa(
-        c, bin, w,
-        forall (i in index_set(bin)) (
-           min(index_set(c)) <= bin[i] /\ bin[i] <= max(index_set(c))
-        )
-        /\
-        let {int: cMax = max(c),
-            array[int] of int: fixed = [i | i in index_set(c) where c[i] < cMax]} in
-        cumulative(
-            bin ++ fixed,
-            [1 | i in bin ++ fixed],
-            w ++ [cMax - c[i] | i in fixed],
-            cMax));
diff --git a/resources/mzn/lib/yuck/bin_packing_load.mzn b/resources/mzn/lib/yuck/bin_packing_load.mzn
@@ -4,26 +4,17 @@ predicate yuck_bin_packing(
     array[int] of int: w,
     int: minLoadIndex);
 
-predicate safe_bin_packing_load(
+predicate bin_packing_load(
     array[int] of var int: load,
     array[int] of var int: bin,
-    array[int] of int: w,
-    var bool: continuation) =
+    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,
-           "bin_packing_load: the weights must be non-negative",
-           continuation));
-
-predicate bin_packing_load(
-    array[int] of var int: load,
-    array[int] of var int: bin,
-    array[int] of int: w) =
-    safe_bin_packing_load(
-        load, bin, w,
-        forall (i in index_set(bin)) (
-            min(index_set(load)) <= bin[i] /\ bin[i] <= max(index_set(load))
-        ) /\
-        yuck_bin_packing(load, bin, w, min(index_set(load))));
+            lb_array(w) >= 0,
+            "bin_packing_load: the weights must be non-negative",
+            forall (i in index_set(bin)) (
+                min(index_set(load)) <= bin[i] /\ bin[i] <= max(index_set(load))
+            ) /\
+            yuck_bin_packing(load, bin, w, min(index_set(load)))));
diff --git a/resources/mzn/lib/yuck/cumulative.mzn b/resources/mzn/lib/yuck/cumulative.mzn
@@ -6,33 +6,24 @@ predicate yuck_cumulative(
     array[int] of var int: r,
     var int: b);
 
-predicate safe_cumulative(
+predicate cumulative(
     array[int] of var int: s,
     array[int] of var int: d,
     array[int] of var int: r,
-    var bool: continuation) =
+    var int: b) =
     assert(
         index_set(s) == index_set(d) /\ index_set(s) == index_set(r),
         "cumulative: the array arguments must have identical index sets",
         assert(
             lb_array(d) >= 0 /\ lb_array(r) >= 0,
             "cumulative: durations and resource usages must be non-negative",
-            continuation));
-
-predicate cumulative(
-    array[int] of var int: s,
-    array[int] of var int: d,
-    array[int] of var int: r,
-    var int: b) =
-    safe_cumulative(
-        s, d, r,
-        if forall(i in index_set(r))(is_fixed(r[i]) /\ fix(r[i]) == 1) /\ is_fixed(b) /\ fix(b) == 1 then
-            if forall(i in index_set(d))(is_fixed(d[i]) /\ fix(d[i]) == 1) then
-                alldifferent(s)
+            if forall(i in index_set(r))(is_fixed(r[i]) /\ fix(r[i]) == 1) /\ is_fixed(b) /\ fix(b) == 1 then
+               if forall(i in index_set(d))(is_fixed(d[i]) /\ fix(d[i]) == 1) then
+                   alldifferent(s)
+               else
+                   % disjunctive case
+                   yuck_cumulative(s, d, r, b)
+               endif
             else
-                % disjunctive case
-                yuck_cumulative(s, d, r, b)
-            endif
-        else
-            yuck_cumulative(s, d, r, b)
-        endif);
+               yuck_cumulative(s, d, r, b)
+            endif));
diff --git a/resources/mzn/lib/yuck/disjunctive.mzn b/resources/mzn/lib/yuck/disjunctive.mzn
@@ -1,18 +1,10 @@
 include "cumulative.mzn";
 
-predicate safe_disjunctive(
+predicate disjunctive(
     array[int] of var int: s,
-    array[int] of var int: d,
-    var bool: continuation) =
+    array[int] of var int: d) =
     assert(
         index_set(s) == index_set(d),
         "disjunctive: the array arguments must have identical index sets",
-        continuation);
-
-predicate disjunctive(
-    array[int] of var int: s,
-    array[int] of var int: d) =
-    safe_disjunctive(
-        s, d,
         forall (i in index_set(d)) (d[i] >= 0) /\
         cumulative(s, d, [1 | i in index_set(s)], 1));
diff --git a/resources/mzn/lib/yuck/global_cardinality.mzn b/resources/mzn/lib/yuck/global_cardinality.mzn
@@ -6,8 +6,7 @@ predicate yuck_global_cardinality(
 predicate global_cardinality(
     array[int] of var int: x,
     array[int] of int: cover,
-    array[int] of var int: counts)
-=
+    array[int] of var int: counts) =
     assert(
         index_set(cover) = index_set(counts),
         "global_cardinality: cover and counts must have identical index sets",

diff --git a/resources/mzn/lib/yuck/global_cardinality_closed.mzn b/resources/mzn/lib/yuck/global_cardinality_closed.mzn
@@ -3,8 +3,7 @@ include "global_cardinality.mzn";
 predicate global_cardinality_closed(
     array[int] of var int: x,
     array[int] of int: cover,
-    array[int] of var int: counts)
-=
+    array[int] of var int: counts) =
     forall (i in index_set(x)) (x[i] in array2set(cover))
     /\
     global_cardinality(x, cover, counts);
diff --git a/resources/mzn/lib/yuck/global_cardinality_low_up.mzn b/resources/mzn/lib/yuck/global_cardinality_low_up.mzn
@@ -4,8 +4,7 @@ predicate global_cardinality_low_up(
     array[int] of var int: x,
     array[int] of int: cover,
     array[int] of int: lbound,
-    array[int] of int: ubound)
-=
+    array[int] of int: ubound) =
     assert(
         index_set(cover) = index_set(lbound) /\ index_set(lbound) = index_set(ubound),
         "global_cardinality_low_up: cover, lbound, and ubound must have identical index sets",

diff --git a/resources/mzn/lib/yuck/global_cardinality_low_up_closed.mzn b/resources/mzn/lib/yuck/global_cardinality_low_up_closed.mzn
@@ -4,8 +4,7 @@ predicate global_cardinality_low_up_closed(
     array[int] of var int: x,
     array[int] of int: cover,
     array[int] of int: lbound,
-    array[int] of int: ubound)
-=
+    array[int] of int: ubound) =
     forall (i in index_set(x)) (x[i] in array2set(cover))
     /\
     global_cardinality_low_up(x, cover, lbound, ubound);
diff --git a/resources/mzn/lib/yuck/regular.mzn b/resources/mzn/lib/yuck/regular.mzn
@@ -4,10 +4,9 @@ predicate yuck_regular(
     array[int] of var int: x, int: Q, int: S,
     array[int] of int: d, int: q0, set of int: F);
 
-predicate safe_regular(
+predicate regular(
     array[int] of var int: x, int: Q, int: S,
-    array[int, int] of int: d, int: q0, set of int: F,
-    var bool: continuation) =
+    array[int, int] of int: d, int: q0, set of int: F) =
     assert(
         Q > 0,
         "regular: 'Q' must be greater than zero",
@@ -28,11 +27,4 @@ predicate safe_regular(
                         assert(
                             F subset 1..Q,
                             "regular: final states in 'F' contain states outside 1..Q",
-                            continuation))))));
-
-predicate regular(
-    array[int] of var int: x, int: Q, int: S,
-    array[int, int] of int: d, int: q0, set of int: F) =
-    safe_regular(
-        x, Q, S, d, q0, F,
-        yuck_regular(x, Q, S, [d[i, j] | i in index_set_1of2(d), j in index_set_2of2(d)], q0, F));
+                            yuck_regular(x, Q, S, [d[i, j] | i in index_set_1of2(d), j in index_set_2of2(d)], q0, F)))))));
diff --git a/resources/mzn/lib/yuck/table_int.mzn b/resources/mzn/lib/yuck/table_int.mzn
@@ -11,18 +11,10 @@ predicate yuck_table_int(
     array[int] of var int: x,
     array[int] of int: t);
 
-predicate safe_table_int(
+predicate table_int(
     array[int] of var int: x,
-    array[int, int] of int: t,
-    var bool: continuation) =
+    array[int, int] of int: t) =
     assert(
         index_set_2of2(t) == index_set(x),
         "The second dimension of the table must equal the number of variables in the first argument",
-        continuation);
-
-predicate table_int(
-    array[int] of var int: x,
-    array[int, int] of int: t) =
-    safe_table_int(
-        x, t,
         yuck_table_int(x, [t[i, j] | i in index_set_1of2(t), j in index_set_2of2(t)]));