this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Guido Tack <tack@gecode.org>
5 *
6 * Copyright:
7 * Guido Tack, 2008
8 *
9 * This file is part of Gecode, the generic constraint
10 * development environment:
11 * http://www.gecode.org
12 *
13 * Permission is hereby granted, free of charge, to any person obtaining
14 * a copy of this software and associated documentation files (the
15 * "Software"), to deal in the Software without restriction, including
16 * without limitation the rights to use, copy, modify, merge, publish,
17 * distribute, sublicense, and/or sell copies of the Software, and to
18 * permit persons to whom the Software is furnished to do so, subject to
19 * the following conditions:
20 *
21 * The above copyright notice and this permission notice shall be
22 * included in all copies or substantial portions of the Software.
23 *
24 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
25 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
26 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
27 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
28 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
29 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
30 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
31 *
32 */
33
34#include <gecode/int/linear.hh>
35
36namespace Gecode { namespace Int { namespace Arithmetic {
37
38 /*
39 * Positive bounds consistent division
40 *
41 */
42
43 template<class VA, class VB, class VC>
44 forceinline
45 DivPlusBnd<VA,VB,VC>::DivPlusBnd(Home home, VA x0, VB x1, VC x2)
46 : MixTernaryPropagator<VA,PC_INT_BND,VB,PC_INT_BND,VC,PC_INT_BND>
47 (home,x0,x1,x2) {}
48
49 template<class VA, class VB, class VC>
50 forceinline
51 DivPlusBnd<VA,VB,VC>::DivPlusBnd(Space& home, DivPlusBnd<VA,VB,VC>& p)
52 : MixTernaryPropagator<VA,PC_INT_BND,VB,PC_INT_BND,VC,PC_INT_BND>
53 (home,p) {}
54
55 template<class VA, class VB, class VC>
56 Actor*
57 DivPlusBnd<VA,VB,VC>::copy(Space& home) {
58 return new (home) DivPlusBnd<VA,VB,VC>(home,*this);
59 }
60
61 template<class VA, class VB, class VC>
62 ExecStatus
63 DivPlusBnd<VA,VB,VC>::propagate(Space& home, const ModEventDelta&) {
64 assert(pos(x0) && pos(x1) && !neg(x2));
65 bool mod;
66 do {
67 mod = false;
68 GECODE_ME_CHECK_MODIFIED(mod,x2.lq(home,
69 floor_div_pp(x0.max(),x1.min())));
70 GECODE_ME_CHECK_MODIFIED(mod,x2.gq(home,
71 floor_div_px(x0.min(),x1.max())));
72 GECODE_ME_CHECK_MODIFIED(mod,x0.le(home,mll(x1.max(),ill(x2.max()))));
73 GECODE_ME_CHECK_MODIFIED(mod,x0.gq(home,mll(x1.min(),x2.min())));
74 if (x2.min() > 0) {
75 GECODE_ME_CHECK_MODIFIED(mod,
76 x1.lq(home,floor_div_pp(x0.max(),x2.min())));
77 }
78 GECODE_ME_CHECK_MODIFIED(mod,x1.gq(home,ceil_div_pp(ll(x0.min()),
79 ill(x2.max()))));
80 } while (mod);
81 return x0.assigned() && x1.assigned() ?
82 home.ES_SUBSUMED(*this) : ES_FIX;
83 }
84
85 template<class VA, class VB, class VC>
86 forceinline ExecStatus
87 DivPlusBnd<VA,VB,VC>::post(Home home, VA x0, VB x1, VC x2) {
88 GECODE_ME_CHECK(x0.gr(home,0));
89 GECODE_ME_CHECK(x1.gr(home,0));
90 GECODE_ME_CHECK(x2.gq(home,floor_div_pp(x0.min(),x1.max())));
91 (void) new (home) DivPlusBnd<VA,VB,VC>(home,x0,x1,x2);
92 return ES_OK;
93 }
94
95
96 /*
97 * Bounds consistent division
98 *
99 */
100 template<class View>
101 forceinline
102 DivBnd<View>::DivBnd(Home home, View x0, View x1, View x2)
103 : TernaryPropagator<View,PC_INT_BND>(home,x0,x1,x2) {}
104
105 template<class View>
106 forceinline
107 DivBnd<View>::DivBnd(Space& home, DivBnd<View>& p)
108 : TernaryPropagator<View,PC_INT_BND>(home,p) {}
109
110 template<class View>
111 Actor*
112 DivBnd<View>::copy(Space& home) {
113 return new (home) DivBnd<View>(home,*this);
114 }
115
116 template<class View>
117 ExecStatus
118 DivBnd<View>::propagate(Space& home, const ModEventDelta&) {
119 if (pos(x1)) {
120 if (pos(x2) || pos(x0)) goto rewrite_ppp;
121 if (neg(x2) || neg(x0)) goto rewrite_npn;
122 goto prop_xpx;
123 }
124 if (neg(x1)) {
125 if (neg(x2) || pos(x0)) goto rewrite_pnn;
126 if (pos(x2) || neg(x0)) goto rewrite_nnp;
127 goto prop_xnx;
128 }
129 if (pos(x2)) {
130 if (pos(x0)) goto rewrite_ppp;
131 if (neg(x0)) goto rewrite_nnp;
132 goto prop_xxp;
133 }
134 if (neg(x2)) {
135 if (pos(x0)) goto rewrite_pnn;
136 if (neg(x0)) goto rewrite_npn;
137 goto prop_xxn;
138 }
139 assert(any(x1) && any(x2));
140 GECODE_ME_CHECK(x0.lq(home,std::max(mll(x1.max(),ill(x2.max()))-1,
141 mll(x1.min(),dll(x2.min()))-1)));
142 GECODE_ME_CHECK(x0.gq(home,std::min(mll(x1.min(),ill(x2.max())),
143 mll(x1.max(),dll(x2.min())))));
144 return ES_NOFIX;
145
146 prop_xxp:
147 assert(any(x0) && any(x1) && pos(x2));
148
149 GECODE_ME_CHECK(x0.le(home, mll(x1.max(),ill(x2.max()))));
150 GECODE_ME_CHECK(x0.gq(home, mll(x1.min(),ill(x2.max()))));
151
152 if (pos(x0)) goto rewrite_ppp;
153 if (neg(x0)) goto rewrite_nnp;
154
155 GECODE_ME_CHECK(x1.lq(home,floor_div_pp(x0.max(),x2.min())));
156 GECODE_ME_CHECK(x1.gq(home,ceil_div_xp(x0.min(),x2.min())));
157
158 if (x0.assigned() && x1.assigned())
159 goto subsumed;
160 return ES_NOFIX;
161
162 prop_xpx:
163 assert(any(x0) && pos(x1) && any(x2));
164
165 GECODE_ME_CHECK(x0.le(home, mll(x1.max(),ill(x2.max()))));
166 GECODE_ME_CHECK(x0.gq(home, mll(x1.max(),dll(x2.min()))));
167
168 if (pos(x0)) goto rewrite_ppp;
169 if (neg(x0)) goto rewrite_npn;
170
171 GECODE_ME_CHECK(x2.lq(home,floor_div_xp(x0.max(),x1.min())));
172 GECODE_ME_CHECK(x2.gq(home,floor_div_xp(x0.min(),x1.min())));
173
174 if (x0.assigned() && x1.assigned())
175 goto subsumed;
176 return ES_NOFIX;
177
178 prop_xxn:
179 assert(any(x0) && any(x1) && neg(x2));
180
181 GECODE_ME_CHECK(x0.lq(home, mll(x1.min(),dll(x2.min()))));
182 GECODE_ME_CHECK(x0.gq(home, mll(x1.max(),dll(x2.min()))));
183
184 if (pos(x0)) goto rewrite_pnn;
185 if (neg(x0)) goto rewrite_npn;
186
187 if (x2.max() != -1)
188 GECODE_ME_CHECK(x1.lq(home,ceil_div_xx(ll(x0.min()),ill(x2.max()))));
189 if (x2.max() != -1)
190 GECODE_ME_CHECK(x1.gq(home,ceil_div_xx(ll(x0.max()),ill(x2.max()))));
191
192 if (x0.assigned() && x1.assigned())
193 goto subsumed;
194 return ES_NOFIX;
195
196 prop_xnx:
197 assert(any(x0) && neg(x1) && any(x2));
198
199 GECODE_ME_CHECK(x0.lq(home, mll(x1.min(),dll(x2.min()))));
200 GECODE_ME_CHECK(x0.gq(home, mll(x1.min(),ill(x2.max()))));
201
202 if (pos(x0)) goto rewrite_pnn;
203 if (neg(x0)) goto rewrite_nnp;
204
205 GECODE_ME_CHECK(x2.lq(home,floor_div_xx(x0.min(),x1.max())));
206 GECODE_ME_CHECK(x2.gq(home,floor_div_xx(x0.max(),x1.max())));
207
208 if (x0.assigned() && x1.assigned())
209 goto subsumed;
210 return ES_NOFIX;
211
212 rewrite_ppp:
213 GECODE_REWRITE(*this,(DivPlusBnd<IntView,IntView,IntView>
214 ::post(home(*this),x0,x1,x2)));
215 rewrite_nnp:
216 GECODE_REWRITE(*this,(DivPlusBnd<MinusView,MinusView,IntView>
217 ::post(home(*this),MinusView(x0),MinusView(x1),x2)));
218 rewrite_pnn:
219 GECODE_REWRITE(*this,(DivPlusBnd<IntView,MinusView,MinusView>
220 ::post(home(*this),x0,MinusView(x1),MinusView(x2))));
221 rewrite_npn:
222 GECODE_REWRITE(*this,(DivPlusBnd<MinusView,IntView,MinusView>
223 ::post(home(*this),MinusView(x0),x1,MinusView(x2))));
224 subsumed:
225 assert(x0.assigned() && x1.assigned());
226 int result = std::abs(x0.val()) / std::abs(x1.val());
227 if (x0.val()/x1.val() < 0)
228 result = -result;
229 GECODE_ME_CHECK(x2.eq(home,result));
230 return home.ES_SUBSUMED(*this);
231 }
232
233 template<class View>
234 ExecStatus
235 DivBnd<View>::post(Home home, View x0, View x1, View x2) {
236 GECODE_ME_CHECK(x1.nq(home, 0));
237 if (pos(x0)) {
238 if (pos(x1) || pos(x2)) goto post_ppp;
239 if (neg(x1) || neg(x2)) goto post_pnn;
240 } else if (neg(x0)) {
241 if (neg(x1) || pos(x2)) goto post_nnp;
242 if (pos(x1) || neg(x2)) goto post_npn;
243 } else if (pos(x1)) {
244 if (pos(x2)) goto post_ppp;
245 if (neg(x2)) goto post_npn;
246 } else if (neg(x1)) {
247 if (pos(x2)) goto post_nnp;
248 if (neg(x2)) goto post_pnn;
249 }
250 (void) new (home) DivBnd<View>(home,x0,x1,x2);
251 return ES_OK;
252
253 post_ppp:
254 return DivPlusBnd<IntView,IntView,IntView>
255 ::post(home,x0,x1,x2);
256 post_nnp:
257 return DivPlusBnd<MinusView,MinusView,IntView>
258 ::post(home,MinusView(x0),MinusView(x1),x2);
259 post_pnn:
260 return DivPlusBnd<IntView,MinusView,MinusView>
261 ::post(home,x0,MinusView(x1),MinusView(x2));
262 post_npn:
263 return DivPlusBnd<MinusView,IntView,MinusView>
264 ::post(home,MinusView(x0),x1,MinusView(x2));
265 }
266
267
268 /*
269 * Propagator for x0 != 0 /\ (x1 != 0 => x0*x1>0) /\ abs(x1)<abs(x0)
270 *
271 */
272
273 template<class View>
274 forceinline
275 DivMod<View>::DivMod(Home home, View x0, View x1, View x2)
276 : TernaryPropagator<View,PC_INT_BND>(home,x0,x1,x2) {}
277
278 template<class View>
279 forceinline ExecStatus
280 DivMod<View>::post(Home home, View x0, View x1, View x2) {
281 GECODE_ME_CHECK(x1.nq(home,0));
282 (void) new (home) DivMod<View>(home,x0,x1,x2);
283 return ES_OK;
284 }
285
286 template<class View>
287 forceinline
288 DivMod<View>::DivMod(Space& home, DivMod<View>& p)
289 : TernaryPropagator<View,PC_INT_BND>(home,p) {}
290
291 template<class View>
292 Actor*
293 DivMod<View>::copy(Space& home) {
294 return new (home) DivMod<View>(home,*this);
295 }
296
297 template<class View>
298 ExecStatus
299 DivMod<View>::propagate(Space& home, const ModEventDelta&) {
300 bool signIsSame;
301 do {
302 signIsSame = true;
303 // The sign of x0 and x2 is the same
304 if (x0.min() >= 0) {
305 GECODE_ME_CHECK(x2.gq(home, 0));
306 } else if (x0.max() <= 0) {
307 GECODE_ME_CHECK(x2.lq(home, 0));
308 } else if (x2.min() > 0) {
309 GECODE_ME_CHECK(x0.gq(home, 0));
310 } else if (x2.max() < 0) {
311 GECODE_ME_CHECK(x0.lq(home, 0));
312 } else {
313 signIsSame = false;
314 }
315
316 // abs(x2) is less than abs(x1)
317 int x1max = std::max(x1.max(),std::max(-x1.max(),
318 std::max(x1.min(),-x1.min())));
319 GECODE_ME_CHECK(x2.le(home, x1max));
320 GECODE_ME_CHECK(x2.gr(home, -x1max));
321
322 int x2absmin = any(x2) ? 0 : (pos(x2) ? x2.min() : -x2.max());
323 Iter::Ranges::Singleton sr(-x2absmin,x2absmin);
324 GECODE_ME_CHECK(x1.minus_r(home,sr,false));
325 } while (!signIsSame &&
326 (x0.min() > 0 || x0.max() < 0 || x2.min() > 0 || x2.max() < 0));
327
328 if (signIsSame) {
329 int x2max = std::max(x2.max(),std::max(-x2.max(),
330 std::max(x2.min(),-x2.min())));
331 int x1absmin = any(x1) ? 0 : (pos(x1) ? x1.min() : -x1.max());
332 if (x2max < x1absmin)
333 return home.ES_SUBSUMED(*this);
334 }
335 return ES_FIX;
336 }
337
338}}}
339
340// STATISTICS: int-prop