Add assertions to several FlatZinc globals

git-svn-id: svn+ssh://svn.gecode.org/srv/gecode/svn/gecode/trunk@15636 64335634-5103-0410-b293-fc3d331e086d

Author: guidotack

changelog.in

@@ -72,6 +72,14 @@ Date: ???
 [DESCRIPTION]
 Minor release.
 
+[ENTRY]
+Module: flatzinc
+What:   bug
+Rank:   minor
+[DESCRIPTION]
+Some FlatZinc constraints were not guarded with assertions, which could make
+Gecode crash on incorrect models.
+
 [ENTRY]
 Module: float
 What:   bug

gecode/flatzinc/mznlib/bin_packing.mzn

@@ -39,8 +39,13 @@ include "bin_packing_capa.mzn";
 predicate bin_packing(int: c,
                       array[int] of var int: bin,
                       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,
+        "bin_packing: the weights must be non-negative",
+    assert(c >= 0, "bin_packing: capacity must be non-negative",
     let {
         set of int: idx = lb_array(bin)..ub_array(bin),
         array[idx] of int: capa = array1d(idx, [c|i in idx])
     } in
-    bin_packing_capa(capa,bin,w);
+    bin_packing_capa(capa,bin,w))));

gecode/flatzinc/mznlib/bin_packing_capa.mzn

@@ -39,9 +39,15 @@ include "bin_packing_load.mzn";
 predicate bin_packing_capa(array[int] of int: c,
                            array[int] of var int: bin,
                            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,
+        "bin_packing_capa: the weights must be non-negative",
+    assert(lb_array(c) >= 0,
+        "bin_packing_capa: the capacities must be non-negative",
     let {
         array[min(index_set(c))..max(index_set(c))] of var 0..ub_array(c): l
     } in (
         forall( i in index_set(l) ) ( l[i] <= c[i] )
     /\  bin_packing_load(l,bin,w)
-    );
+    ))));

gecode/flatzinc/mznlib/bin_packing_load.mzn

@@ -42,4 +42,8 @@ predicate gecode_bin_packing_load(array[int] of var int: l,
 predicate bin_packing_load(array[int] of var int: l,
                            array[int] of var int: bin,
                            array[int] of int: w) =
-    gecode_bin_packing_load(l,bin,w,min(index_set(l)));
+    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",
+    gecode_bin_packing_load(l,bin,w,min(index_set(l)))));

gecode/flatzinc/mznlib/diffn.mzn

@@ -41,4 +41,9 @@ predicate diffn(array[int] of var int: x,
                 array[int] of var int: y,
                 array[int] of var int: dx,
                 array[int] of var int: dy) =
-    gecode_nooverlap(x,dx,y,dy);
+    assert(
+        index_set(x) = index_set(y)  /\
+        index_set(x) = index_set(dx) /\
+        index_set(x) = index_set(dy),
+        "diffn: index set mismatch",
+    gecode_nooverlap(x,dx,y,dy));

gecode/flatzinc/mznlib/global_cardinality.mzn

@@ -34,10 +34,17 @@
 %
 %
 
+predicate gecode_global_cardinality(array[int] of var int: x,
+                                    array[int] of int: cover,
+                                    array[int] of var int: counts);
+
 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",
+        gecode_global_cardinality(x,cover,counts));
 
 predicate global_cardinality_old(array[int] of var int: x,
                              array[int] of var int: c) =
-    global_cardinality(x,[i|i in index_set(c)],c);
+    global_cardinality(x,[i|i in index_set(c)],c));

gecode/flatzinc/mznlib/global_cardinality_closed.mzn

@@ -34,6 +34,14 @@
 %
 %
 
+predicate gecode_global_cardinality_closed(array[int] of var int: x,
+                                           array[int] of int: cover,
+                                           array[int] of var int: counts);
+
 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) =
+  assert(index_set(cover) = index_set(counts),
+      "global_cardinality_closed: " ++
+      "cover and counts must have identical index sets",
+    gecode_global_cardinality_closed(x,cover,counts);

gecode/flatzinc/mznlib/table_bool.mzn

@@ -34,4 +34,10 @@
 %
 %
 
-predicate table_bool(array[int] of var bool: x, array[int, int] of bool: t);
+predicate gecode_table_bool(array[int] of var bool: x, array[int, int] of bool: t);
+
+predicate table_bool(array[int] of var bool: x, array[int, int] of bool: 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",
+        gecode_table_bool(x,t);

gecode/flatzinc/mznlib/table_int.mzn

@@ -34,4 +34,82 @@
 %
 %
 
-predicate table_int(array[int] of var int: x, array[int, int] of int: t);
+predicate gecode_table_int(array[int] of var int: x, array[int, int] of int: t);
+
+predicate table_int(array[int] of var int: x, 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",
+        gecode_table_int(x,t);
+
+predicate table_int_reif(array[int] of var int: x, array[int, int] of int: t,
+                         var bool: b) =
+
+    let { int: n_vars = length(x) }
+    in
+
+    assert(n_vars in 1..5,
+        "'table' constraints in a reified context " ++
+        "are only supported for 1..5 variables.",
+
+    if n_vars = 1 then
+
+        x[1] in { t[it,1] | it in index_set_1of2(t) } <-> b
+
+    else
+
+        let { set of int: ix  = index_set(x),
+              set of int: full_size = 1..product(i in ix)( dom_size(x[i]) ),
+              array[full_size, 1..n_vars + 1] of int: t_b =
+                    array2d(full_size, 1..n_vars + 1,
+
+                    if n_vars = 2 then
+
+                        [ let { array[ix] of int: tpl = [i1,i2] } in
+                            (tpl ++ [bool2int(aux_is_in_table(tpl,t))])[p]
+                          | i1 in dom(x[1]),
+                            i2 in dom(x[2]),
+                            p in 1..n_vars + 1 ]
+
+                    else if n_vars = 3 then
+
+                        [ let { array[ix] of int: tpl = [i1,i2,i3] } in
+                            (tpl ++ [bool2int(aux_is_in_table(tpl,t))])[p]
+                          | i1 in dom(x[1]),
+                            i2 in dom(x[2]),
+                            i3 in dom(x[3]),
+                            p in 1..n_vars + 1 ]
+
+                    else if n_vars = 4 then
+
+                        [ let { array[ix] of int: tpl = [i1,i2,i3,i4] }
+                          in
+                            (tpl ++ [bool2int(aux_is_in_table(tpl,t))])[p]
+                          | i1 in dom(x[1]),
+                            i2 in dom(x[2]),
+                            i3 in dom(x[3]),
+                            i4 in dom(x[4]),
+                            p in 1..n_vars + 1 ]
+
+                    else % if n_vars = 5 then
+
+                        [ let { array[ix] of int: tpl = [i1,i2,i3,i4,i5] } in
+                            (tpl ++ [bool2int(aux_is_in_table(tpl,t))])[p]
+                          | i1 in dom(x[1]),
+                            i2 in dom(x[2]),
+                            i3 in dom(x[3]),
+                            i4 in dom(x[4]),
+                            i5 in dom(x[5]),
+                            p in 1..n_vars + 1 ]
+
+                    endif endif endif ) }
+        in
+        table_int(x ++ [bool2int(b)], t_b)
+
+    endif
+    );
+
+test aux_is_in_table(array[int] of int: e, array[int, int] of int: t) =
+    exists(i in index_set_1of2(t))(
+        forall(j in index_set(e))( t[i,j] = e[j] )
+    );

gecode/flatzinc/registry.cpp

@@ -1520,8 +1520,8 @@ namespace Gecode { namespace FlatZinc {
         registry().add("at_least_int", &p_at_least);
         registry().add("at_most_int", &p_at_most);
         registry().add("gecode_bin_packing_load", &p_bin_packing_load);
-        registry().add("global_cardinality", &p_global_cardinality);
-        registry().add("global_cardinality_closed",
+        registry().add("gecode_global_cardinality", &p_global_cardinality);
+        registry().add("gecode_global_cardinality_closed",
           &p_global_cardinality_closed);
         registry().add("global_cardinality_low_up",
           &p_global_cardinality_low_up);
@@ -1539,8 +1539,8 @@ namespace Gecode { namespace FlatZinc {
         registry().add("increasing_bool", &p_increasing_bool);
         registry().add("decreasing_int", &p_decreasing_int);
         registry().add("decreasing_bool", &p_decreasing_bool);
-        registry().add("table_int", &p_table_int);
-        registry().add("table_bool", &p_table_bool);
+        registry().add("gecode_table_int", &p_table_int);
+        registry().add("gecode_table_bool", &p_table_bool);
         registry().add("cumulatives", &p_cumulatives);
         registry().add("gecode_among_seq_int", &p_among_seq_int);
         registry().add("gecode_among_seq_bool", &p_among_seq_bool);