Skip to content

Commit 06f9b4a

Browse files
guidotackguidotack
committed
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
1 parent 62727e8 commit 06f9b4a

File tree

10 files changed

+140
-13
lines changed

10 files changed

+140
-13
lines changed

‎changelog.in

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,14 @@ Date: ???
7272
[DESCRIPTION]
7373
Minor release.
7474

75+
[ENTRY]
76+
Module: flatzinc
77+
What: bug
78+
Rank: minor
79+
[DESCRIPTION]
80+
Some FlatZinc constraints were not guarded with assertions, which could make
81+
Gecode crash on incorrect models.
82+
7583
[ENTRY]
7684
Module: float
7785
What: bug

‎gecode/flatzinc/mznlib/bin_packing.mzn

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,13 @@ include "bin_packing_capa.mzn";
3939
predicate bin_packing(int: c,
4040
array[int] of var int: bin,
4141
array[int] of int: w) =
42+
assert(index_set(bin) == index_set(w),
43+
"bin_packing: the bin and weight arrays must have identical index sets",
44+
assert(lb_array(w) >= 0,
45+
"bin_packing: the weights must be non-negative",
46+
assert(c >= 0, "bin_packing: capacity must be non-negative",
4247
let {
4348
set of int: idx = lb_array(bin)..ub_array(bin),
4449
array[idx] of int: capa = array1d(idx, [c|i in idx])
4550
} in
46-
bin_packing_capa(capa,bin,w);
51+
bin_packing_capa(capa,bin,w))));

‎gecode/flatzinc/mznlib/bin_packing_capa.mzn

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,9 +39,15 @@ include "bin_packing_load.mzn";
3939
predicate bin_packing_capa(array[int] of int: c,
4040
array[int] of var int: bin,
4141
array[int] of int: w) =
42+
assert(index_set(bin) = index_set(w),
43+
"bin_packing_capa: the bin and weight arrays must have identical index sets",
44+
assert(lb_array(w) >= 0,
45+
"bin_packing_capa: the weights must be non-negative",
46+
assert(lb_array(c) >= 0,
47+
"bin_packing_capa: the capacities must be non-negative",
4248
let {
4349
array[min(index_set(c))..max(index_set(c))] of var 0..ub_array(c): l
4450
} in (
4551
forall( i in index_set(l) ) ( l[i] <= c[i] )
4652
/\ bin_packing_load(l,bin,w)
47-
);
53+
))));

‎gecode/flatzinc/mznlib/bin_packing_load.mzn

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,4 +42,8 @@ predicate gecode_bin_packing_load(array[int] of var int: l,
4242
predicate bin_packing_load(array[int] of var int: l,
4343
array[int] of var int: bin,
4444
array[int] of int: w) =
45-
gecode_bin_packing_load(l,bin,w,min(index_set(l)));
45+
assert(index_set(bin) == index_set(w),
46+
"bin_packing_load: the bin and weight arrays must have identical index sets",
47+
assert(lb_array(w) >= 0,
48+
"bin_packing_load: the weights must be non-negative",
49+
gecode_bin_packing_load(l,bin,w,min(index_set(l)))));

‎gecode/flatzinc/mznlib/diffn.mzn

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,4 +41,9 @@ predicate diffn(array[int] of var int: x,
4141
array[int] of var int: y,
4242
array[int] of var int: dx,
4343
array[int] of var int: dy) =
44-
gecode_nooverlap(x,dx,y,dy);
44+
assert(
45+
index_set(x) = index_set(y) /\
46+
index_set(x) = index_set(dx) /\
47+
index_set(x) = index_set(dy),
48+
"diffn: index set mismatch",
49+
gecode_nooverlap(x,dx,y,dy));

‎gecode/flatzinc/mznlib/global_cardinality.mzn

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,10 +34,17 @@
3434
%
3535
%
3636

37+
predicate gecode_global_cardinality(array[int] of var int: x,
38+
array[int] of int: cover,
39+
array[int] of var int: counts);
40+
3741
predicate global_cardinality(array[int] of var int: x,
3842
array[int] of int: cover,
39-
array[int] of var int: counts);
43+
array[int] of var int: counts) =
44+
assert(index_set(cover) = index_set(counts),
45+
"global_cardinality: cover and counts must have identical index sets",
46+
gecode_global_cardinality(x,cover,counts));
4047

4148
predicate global_cardinality_old(array[int] of var int: x,
4249
array[int] of var int: c) =
43-
global_cardinality(x,[i|i in index_set(c)],c);
50+
global_cardinality(x,[i|i in index_set(c)],c));

‎gecode/flatzinc/mznlib/global_cardinality_closed.mzn

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,14 @@
3434
%
3535
%
3636

37+
predicate gecode_global_cardinality_closed(array[int] of var int: x,
38+
array[int] of int: cover,
39+
array[int] of var int: counts);
40+
3741
predicate global_cardinality_closed(array[int] of var int: x,
3842
array[int] of int: cover,
39-
array[int] of var int: counts);
43+
array[int] of var int: counts) =
44+
assert(index_set(cover) = index_set(counts),
45+
"global_cardinality_closed: " ++
46+
"cover and counts must have identical index sets",
47+
gecode_global_cardinality_closed(x,cover,counts);

‎gecode/flatzinc/mznlib/table_bool.mzn

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,4 +34,10 @@
3434
%
3535
%
3636

37-
predicate table_bool(array[int] of var bool: x, array[int, int] of bool: t);
37+
predicate gecode_table_bool(array[int] of var bool: x, array[int, int] of bool: t);
38+
39+
predicate table_bool(array[int] of var bool: x, array[int, int] of bool: t) =
40+
assert (index_set_2of2(t) == index_set(x),
41+
"The second dimension of the table must equal the number of variables "
42+
++ "in the first argument",
43+
gecode_table_bool(x,t);

‎gecode/flatzinc/mznlib/table_int.mzn

Lines changed: 79 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,4 +34,82 @@
3434
%
3535
%
3636

37-
predicate table_int(array[int] of var int: x, array[int, int] of int: t);
37+
predicate gecode_table_int(array[int] of var int: x, array[int, int] of int: t);
38+
39+
predicate table_int(array[int] of var int: x, array[int, int] of int: t) =
40+
assert (index_set_2of2(t) == index_set(x),
41+
"The second dimension of the table must equal the number of variables "
42+
++ "in the first argument",
43+
gecode_table_int(x,t);
44+
45+
predicate table_int_reif(array[int] of var int: x, array[int, int] of int: t,
46+
var bool: b) =
47+
48+
let { int: n_vars = length(x) }
49+
in
50+
51+
assert(n_vars in 1..5,
52+
"'table' constraints in a reified context " ++
53+
"are only supported for 1..5 variables.",
54+
55+
if n_vars = 1 then
56+
57+
x[1] in { t[it,1] | it in index_set_1of2(t) } <-> b
58+
59+
else
60+
61+
let { set of int: ix = index_set(x),
62+
set of int: full_size = 1..product(i in ix)( dom_size(x[i]) ),
63+
array[full_size, 1..n_vars + 1] of int: t_b =
64+
array2d(full_size, 1..n_vars + 1,
65+
66+
if n_vars = 2 then
67+
68+
[ let { array[ix] of int: tpl = [i1,i2] } in
69+
(tpl ++ [bool2int(aux_is_in_table(tpl,t))])[p]
70+
| i1 in dom(x[1]),
71+
i2 in dom(x[2]),
72+
p in 1..n_vars + 1 ]
73+
74+
else if n_vars = 3 then
75+
76+
[ let { array[ix] of int: tpl = [i1,i2,i3] } in
77+
(tpl ++ [bool2int(aux_is_in_table(tpl,t))])[p]
78+
| i1 in dom(x[1]),
79+
i2 in dom(x[2]),
80+
i3 in dom(x[3]),
81+
p in 1..n_vars + 1 ]
82+
83+
else if n_vars = 4 then
84+
85+
[ let { array[ix] of int: tpl = [i1,i2,i3,i4] }
86+
in
87+
(tpl ++ [bool2int(aux_is_in_table(tpl,t))])[p]
88+
| i1 in dom(x[1]),
89+
i2 in dom(x[2]),
90+
i3 in dom(x[3]),
91+
i4 in dom(x[4]),
92+
p in 1..n_vars + 1 ]
93+
94+
else % if n_vars = 5 then
95+
96+
[ let { array[ix] of int: tpl = [i1,i2,i3,i4,i5] } in
97+
(tpl ++ [bool2int(aux_is_in_table(tpl,t))])[p]
98+
| i1 in dom(x[1]),
99+
i2 in dom(x[2]),
100+
i3 in dom(x[3]),
101+
i4 in dom(x[4]),
102+
i5 in dom(x[5]),
103+
p in 1..n_vars + 1 ]
104+
105+
endif endif endif ) }
106+
in
107+
table_int(x ++ [bool2int(b)], t_b)
108+
109+
endif
110+
);
111+
112+
test aux_is_in_table(array[int] of int: e, array[int, int] of int: t) =
113+
exists(i in index_set_1of2(t))(
114+
forall(j in index_set(e))( t[i,j] = e[j] )
115+
);

‎gecode/flatzinc/registry.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1520,8 +1520,8 @@ namespace Gecode { namespace FlatZinc {
15201520
registry().add("at_least_int", &p_at_least);
15211521
registry().add("at_most_int", &p_at_most);
15221522
registry().add("gecode_bin_packing_load", &p_bin_packing_load);
1523-
registry().add("global_cardinality", &p_global_cardinality);
1524-
registry().add("global_cardinality_closed",
1523+
registry().add("gecode_global_cardinality", &p_global_cardinality);
1524+
registry().add("gecode_global_cardinality_closed",
15251525
&p_global_cardinality_closed);
15261526
registry().add("global_cardinality_low_up",
15271527
&p_global_cardinality_low_up);
@@ -1539,8 +1539,8 @@ namespace Gecode { namespace FlatZinc {
15391539
registry().add("increasing_bool", &p_increasing_bool);
15401540
registry().add("decreasing_int", &p_decreasing_int);
15411541
registry().add("decreasing_bool", &p_decreasing_bool);
1542-
registry().add("table_int", &p_table_int);
1543-
registry().add("table_bool", &p_table_bool);
1542+
registry().add("gecode_table_int", &p_table_int);
1543+
registry().add("gecode_table_bool", &p_table_bool);
15441544
registry().add("cumulatives", &p_cumulatives);
15451545
registry().add("gecode_among_seq_int", &p_among_seq_int);
15461546
registry().add("gecode_among_seq_bool", &p_among_seq_bool);

0 commit comments

Comments
 (0)