this repo has no description
dekker.one
1include "redefs_lin_halfreifs.mzn";
2include "redefs_lin_reifs.mzn";
3
4%% var, var
5predicate int_le_imp(var int: x, var int: y, var bool: b) =
6 if is_fixed(b) then
7 if fix(b) then x<=y else true endif
8 elseif ub(x)<=lb(y) then true
9 elseif lb(x)>ub(y) then (not b)
10 % elseif fPostprocessDomains /\ fPostproDom_DIFF then
11 % % TODO MIPDomains
12 else
13 aux_int_le_if_1(x, y, b)
14 endif;
15
16%% var, var
17predicate int_lt_imp(var int: x, var int: y, var bool: b) =
18 if is_fixed(x) then
19 int_le_imp(x + 1, y, b)
20 else
21 int_le_imp(x, y - 1, b)
22 endif;
23
24%% var, var
25predicate int_eq_imp(var int: x, var int: y, var bool: b) =
26 if is_fixed(b) then
27 if fix(b) then (x = y) else true endif
28 elseif card( dom(x) intersect dom(y) ) > 0 then
29 if is_fixed(x) then
30 if is_fixed(y) then
31 b -> (fix(x) = fix(y))
32 else
33 int_eq_imp(y, fix(x), b)
34 endif
35 elseif is_fixed(y) then
36 int_eq_imp(x, fix(y), b)
37 % elseif fPostprocessDomains /\ fPostproDom_DIFF then
38 % % TODO MIPDomains
39 else
40 aux_int_eq_if_1(x, y, b)
41 endif
42 else
43 not b
44 endif;
45
46%% var, const
47predicate int_eq_imp(var int: x, int: y, var bool: b) =
48 if is_fixed(b) then
49 if fix(b) then (x = y) else true endif
50 elseif y in dom(x) then
51 if is_fixed(x) then
52 b -> (y = fix(x))
53 % elseif fPostprocessDomains then
54 % % TODO MIPDomains
55 elseif card(dom(x)) < nMZN__UnaryLenMax_eq then % TODO: Use eq_encode in imp ??
56 let {
57 array[int] of var int: p = eq_encode(x);
58 } in b <= p[y]
59 else
60 aux_int_eq_if_1(x, y, b)
61 endif
62 else
63 not b
64 endif;
65
66%% var, var
67predicate int_ne_imp(var int: x, var int: y, var bool: b) =
68 if is_fixed(b) then
69 if fix(b) then (x != y) else true endif
70 elseif (ub(x) < lb(y)) \/ (lb(x) > ub(y)) then
71 true
72 else
73 if is_fixed(x) then
74 if is_fixed(y) then
75 b -> (fix(x) != fix(y))
76 else
77 int_ne_imp(y, fix(x), b)
78 endif
79 elseif is_fixed(y) then
80 int_ne_imp(x, fix(y), b)
81 % elseif fPostprocessDomains /\ fPostproDom_DIFF then
82 % % TODO MIPDomains
83 else
84 aux_int_ne_if_1(x, y, b)
85 endif
86 endif;
87
88%% var, const
89predicate int_ne_imp(var int: x, int: y, var bool: b) =
90 if is_fixed(b) then
91 if fix(b) then (x != y) else true endif
92 elseif (ub(x) < lb(y)) \/ (lb(x) > ub(y)) then
93 true
94 else
95 if is_fixed(x) then
96 b -> (y != fix(x))
97 % elseif fPostprocessDomains then
98 % % TODO MIPDomains
99 elseif card(dom(x)) < nMZN__UnaryLenMax_eq then
100 let {
101 array[int] of var int: p = eq_encode(x);
102 } in b <= (1 - p[y])
103 else
104 aux_int_ne_if_1(x, y, b)
105 endif
106 endif;
107
108%-----------------------------------------------------------------------------%
109
110%% lin_expr, const
111predicate int_lin_le_imp(array[int] of int: c, array[int] of var int: x,
112 int: d, var bool: b) =
113 if (d = 0) /\ (length(c) = 2) /\ (abs(c[1]) = 1) /\ (c[1] = -1 * c[2]) then
114 if (c[1] < 0) then
115 int_le_imp(x[2], x[1], b)
116 else
117 int_le_imp(x[1], x[2], b)
118 endif
119 elseif fPostprocessDomains /\ fPostproDom_DIFF then
120 int_le_imp(sum(i in index_set(x))(c[i] * x[i]), d, b)
121 elseif fAvoidNI then
122 aux_float_le_if_1(sum2float(c, x), d, b)
123 else
124 aux_int_le_if_1(sum(i in index_set(x))(c[i] * x[i]), d, b)
125 endif;
126
127predicate int_lin_lt_imp(array[int] of int: c, array[int] of var int: x,
128 int: d, var bool: b) =
129 if true then
130 abort("int_lin_lt_imp not supposed to be called")
131 else
132 int_lin_le_imp(c, x, d - 1, b)
133 endif;
134
135%% lin_expr, const
136predicate int_lin_eq_imp(array[int] of int: c, array[int] of var int: x,
137 int: d, var bool: b) =
138 if (d = 0) /\ (length(c) = 2) /\ (abs(c[1]) = 1) /\ (c[1] = -1 * c[2]) then
139 int_ne_imp(x[1], x[2], b)
140 elseif fPostprocessDomains /\ fPostproDom_DIFF then
141 int_eq_imp(sum(i in index_set(x))(c[i] * x[i]), d, b)
142 elseif fAvoidNI then
143 aux_float_eq_if_1(sum2float(c, x), d, b)
144 else
145 aux_int_eq_if_1(sum(i in index_set(x))(c[i] * x[i]), d, b)
146 endif;
147
148%% lin_expr, const
149predicate int_lin_ne_imp(array[int] of int: c, array[int] of var int: x,
150 int: d, var bool: b) =
151 if (d = 0) /\ (length(c) = 2) /\ (abs(c[1]) = 1) /\ (c[1] = -1 * c[2]) then
152 int_ne_imp(x[1], x[2], b)
153 elseif fPostprocessDomains /\ fPostproDom_DIFF then
154 int_ne_imp(sum(i in index_set(x))(c[i] * x[i]), d, b)
155 elseif fAvoidNI then
156 aux_float_ne_if_1(sum2float(c, x), d, b)
157 else
158 aux_int_ne_if_1(sum(i in index_set(x))(c[i] * x[i]), d, b)
159 endif;
160
161%-----------------------------------------------------------------------------%
162
163%% var float, var float
164predicate float_le_imp(var float: x, var float: y, var bool: b) =
165 if is_fixed(b) then
166 if fix(b) then x <= y else true endif
167 elseif ub(x) <= lb(y) then true
168 elseif lb(x) > ub(y) then (not b)
169 % elseif fPostprocessDomains /\ fPostproDom_DIFF then
170 % % TODO MIPDomains
171 else
172 aux_float_le_if_1(x, y, b)
173 endif;
174
175%% var float, var float
176predicate float_lt_imp(var float: x, var float: y, var bool: b) =
177 if is_fixed(b) then
178 if fix(b) then (x < y) else true endif
179 % elseif fPostprocessDomains /\ fPostproDom_DIFF then
180 % % TODO MIPDomains
181 else
182 aux_float_lt_if_1(x, y, b)
183 endif;
184
185%% var float, var float
186predicate float_eq_imp(var float: x, var float: y, var bool: b) =
187 if is_fixed(b) then
188 if fix(b) then (x = y) else true endif
189 elseif (ub(x) < lb(y)) \/ (lb(x) > ub(y)) then
190 not b
191 elseif is_fixed(x) /\ is_fixed(y) then
192 b -> (fix(x) == fix(y))
193 % elseif fPostprocessDomains /\ fPostproDom_DIFF then
194 % % TODO MIPDomains
195 else
196 aux_float_eq_if_1(x, y, b)
197 endif;
198
199%% var float, var float
200predicate float_ne_imp(var float: x, var float: y, var bool: b) =
201 if is_fixed(b) then
202 if fix(b) then (x != y) else true endif
203 elseif (ub(x) < lb(y)) \/ (lb(x) > ub(y)) then
204 true
205 elseif is_fixed(x) /\ is_fixed(y) then
206 b -> (fix(x) != fix(y))
207 % elseif fPostprocessDomains /\ fPostproDom_DIFF then
208 % % TODO MIPDomains
209 else
210 aux_float_ne_if_1(x, y, b)
211 endif;
212
213%-----------------------------------------------------------------------------%
214
215predicate float_lin_eq_imp(array[int] of float: c, array[int] of var float: x,
216 float: d, var bool: b) =
217 if (d = 0.0) /\ (length(c) = 2) /\ (abs(c[1]) = 1.0) /\ (c[1] = -1.0 * c[2]) then
218 float_eq_imp(x[1], x[2], b)
219 elseif fPostprocessDomains /\ fPostproDom_DIFF then
220 float_eq_imp(sum(i in index_set(x))(c[i] * x[i]), d, b)
221 else
222 aux_float_eq_if_1(sum(i in index_set(x))(c[i] * x[i]), d, b)
223 endif;
224
225predicate float_lin_ne_imp(array[int] of float: c, array[int] of var float: x,
226 float: d, var bool: b) =
227 if (d = 0.0) /\ (length(c) = 2) /\ (abs(c[1]) = 1.0) /\ (c[1] = -1.0 * c[2]) then
228 float_ne_imp(x[1], x[2], b)
229 elseif fPostprocessDomains /\ fPostproDom_DIFF then
230 float_ne_imp(sum(i in index_set(x))(c[i] * x[i]), d, not b)
231 else
232 aux_float_ne_if_1(sum(i in index_set(x))(c[i] * x[i]), d, b)
233 endif;
234
235predicate float_lin_le_imp(array[int] of float: c, array[int] of var float: x,
236 float: d, var bool: b) =
237 if (d = 0.0) /\ (length(c) = 2) /\ (abs(c[1]) = 1.0) /\ (c[1] = -1.0 * c[2]) then
238 if (c[1] < 0.0) then
239 float_le_imp(x[2], x[1], b)
240 else
241 float_le_imp(x[1], x[2], b)
242 endif
243 elseif fPostprocessDomains /\ fPostproDom_DIFF then
244 float_le_imp(sum(i in index_set(x))(c[i] * x[i]), d, b)
245 else
246 aux_float_le_if_1(sum(i in index_set(x))(c[i] * x[i]), d, b)
247 endif;
248
249predicate float_lin_lt_imp(array[int] of float: c, array[int] of var float: x,
250 float: d, var bool: b) =
251 if (d = 0.0) /\ (length(c) = 2) /\ (abs(c[1]) = 1.0) /\ (c[1] = -1.0 * c[2]) then
252 if (c[1] < 0.0) then
253 float_lt_imp(x[2], x[1], b)
254 else
255 float_lt_imp(x[1], x[2], b)
256 endif
257 elseif fPostprocessDomains /\ fPostproDom_DIFF then
258 float_lt_imp(sum(i in index_set(x))(c[i] * x[i]), d, b)
259 else
260 aux_float_lt_if_1(sum(i in index_set(x))(c[i] * x[i]), d, b)
261 endif;