-
Notifications
You must be signed in to change notification settings - Fork 78
/
table_int.mzn
133 lines (112 loc) · 4.68 KB
/
table_int.mzn
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
%-----------------------------------------------------------------------------%
% A table constraint table(x, t) represents the constraint x in t where we
% consider each row in t to be a tuple and t as a set of tuples.
%-----------------------------------------------------------------------------%
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",
let { int: l = min(index_set(x)),
int: u = max(index_set(x)),
int: lt = min(index_set_1of2(t)),
int: ut = max(index_set_1of2(t)),
var lt..ut: i,
array[l..u, lt..ut] of int: t_transposed =
array2d(l..u, lt..ut, [ t[i,j] | j in l..u, i in lt..ut ]) }
in
forall(j in l..u) (
% Having the variable index component at the left position
% means that the nD-to-1D array translation during Mzn-to-Fzn
% will generate at most an offset constraint, instead of a
% scaling + offset constraint.
%
t_transposed[j,i] = x[j]
%
% t[i,j] = x[j]
)
);
%-----------------------------------------------------------------------------%
% Reified version
%
% We only support special cases of a few variables.
%
% The approach is to add the Boolean variable to the list of variables and
% create an extended table. The extended table covers all combinations of
% assignments to the original variables, and every entry in it is padded with a
% value that depends on whether that entry occurs in the original table.
%
% For example, the original table constraint
%
% x y
% ---
% 2 3
% 5 8
% 4 1
%
% reified with a Boolean b is turned into a table constraint of the form
%
% x y b
% ---------
% 2 3 true
% 5 8 true
% 4 1 true
% ... false
% ... false % for all other pairs (x,y)
% ... false
%
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] )
);
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%