this repo has no description
dekker.one
1%-----------------------------------------------------------------------------%
2% A table constraint table(x, t) represents the constraint x in t where we
3% consider each row in t to be a tuple and t as a set of tuples.
4%-----------------------------------------------------------------------------%
5
6%-----------------------------------------------------------------------------%
7% Reified version
8%
9% We only support special cases of a few variables.
10%
11% The approach is to add the Boolean variable to the list of variables and
12% create an extended table. The extended table covers all combinations of
13% assignments to the original variables, and every entry in it is padded with a
14% value that depends on whether that entry occurs in the original table.
15%
16% For example, the original table constraint
17%
18% x y
19% ---
20% 2 3
21% 5 8
22% 4 1
23%
24% reified with a Boolean b is turned into a table constraint of the form
25%
26% x y b
27% ---------
28% 2 3 true
29% 5 8 true
30% 4 1 true
31% ... false
32% ... false % for all other pairs (x,y)
33% ... false
34%
35
36predicate fzn_table_int_reif(array[int] of var int: x,
37 array[int, int] of int: t,
38 var bool: b) =
39
40 let { int: n_vars = length(x) }
41 in
42
43 assert(n_vars in 1..5,
44 "'table' constraints in a reified context " ++
45 "are only supported for 1..5 variables.",
46
47 if n_vars = 1 then
48
49 x[1] in { t[it,1] | it in index_set_1of2(t) } <-> b
50
51 else
52
53 let { set of int: ix = index_set(x),
54 set of int: full_size = 1..product(i in ix)( dom_size(x[i]) ),
55 array[full_size, 1..n_vars + 1] of int: t_b =
56 array2d(full_size, 1..n_vars + 1,
57
58 if n_vars = 2 then
59
60 [ let { array[ix] of int: tpl = [i1,i2] } in
61 (tpl ++ [bool2int(aux_is_in_table(tpl,t))])[p]
62 | i1 in dom(x[1]),
63 i2 in dom(x[2]),
64 p in 1..n_vars + 1 ]
65
66 else if n_vars = 3 then
67
68 [ let { array[ix] of int: tpl = [i1,i2,i3] } in
69 (tpl ++ [bool2int(aux_is_in_table(tpl,t))])[p]
70 | i1 in dom(x[1]),
71 i2 in dom(x[2]),
72 i3 in dom(x[3]),
73 p in 1..n_vars + 1 ]
74
75 else if n_vars = 4 then
76
77 [ let { array[ix] of int: tpl = [i1,i2,i3,i4] }
78 in
79 (tpl ++ [bool2int(aux_is_in_table(tpl,t))])[p]
80 | i1 in dom(x[1]),
81 i2 in dom(x[2]),
82 i3 in dom(x[3]),
83 i4 in dom(x[4]),
84 p in 1..n_vars + 1 ]
85
86 else % if n_vars = 5 then
87
88 [ let { array[ix] of int: tpl = [i1,i2,i3,i4,i5] } in
89 (tpl ++ [bool2int(aux_is_in_table(tpl,t))])[p]
90 | i1 in dom(x[1]),
91 i2 in dom(x[2]),
92 i3 in dom(x[3]),
93 i4 in dom(x[4]),
94 i5 in dom(x[5]),
95 p in 1..n_vars + 1 ]
96
97 endif endif endif ) }
98 in
99 fzn_table_int(x ++ [bool2int(b)], t_b)
100
101 endif
102 );
103
104test aux_is_in_table(array[int] of int: e, array[int, int] of int: t) =
105 exists(i in index_set_1of2(t))(
106 forall(j in index_set(e))( t[i,j] = e[j] )
107 );
108
109%-----------------------------------------------------------------------------%