Generated on Thu Jan 16 2025 00:00:00 for Gecode by doxygen 1.14.0
divmod.hpp
Go to the documentation of this file.
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>
48
49 template<class VA, class VB, class VC>
54
55 template<class VA, class VB, class VC>
56 Actor*
58 return new (home) DivPlusBnd<VA,VB,VC>(home,*this);
59 }
60
61 template<class VA, class VB, class VC>
64 assert(pos(x0) && pos(x1) && !neg(x2));
65 bool mod;
66 do {
67 mod = false;
69 floor_div_pp(x0.max(),x1.min())));
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) {
76 x1.lq(home,floor_div_pp(x0.max(),x2.min())));
77 }
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>
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>
104
105 template<class View>
109
110 template<class View>
111 Actor*
113 return new (home) DivBnd<View>(home,*this);
114 }
115
116 template<class View>
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:
214 ::post(home(*this),x0,x1,x2)));
215 rewrite_nnp:
217 ::post(home(*this),MinusView(x0),MinusView(x1),x2)));
218 rewrite_pnn:
220 ::post(home(*this),x0,MinusView(x1),MinusView(x2))));
221 rewrite_npn:
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>
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:
255 ::post(home,x0,x1,x2);
256 post_nnp:
259 post_pnn:
262 post_npn:
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>
277
278 template<class View>
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>
290
291 template<class View>
292 Actor*
294 return new (home) DivMod<View>(home,*this);
295 }
296
297 template<class View>
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
Base-class for both propagators and branchers.
Definition core.hpp:628
Home class for posting propagators
Definition core.hpp:856
virtual Actor * copy(Space &home)
Copy propagator during cloning.
Definition divmod.hpp:112
DivBnd(Space &home, DivBnd< View > &p)
Constructor for cloning p.
Definition divmod.hpp:107
static ExecStatus post(Home home, View x0, View x1, View x2)
Post propagator (rounding towards 0)
Definition divmod.hpp:235
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition divmod.hpp:118
static ExecStatus post(Home home, View x0, View x1, View x2)
Post propagator .
Definition divmod.hpp:280
virtual Actor * copy(Space &home)
Copy propagator during cloning.
Definition divmod.hpp:293
DivMod(Space &home, DivMod< View > &p)
Constructor for cloning p.
Definition divmod.hpp:288
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition divmod.hpp:299
Bounds consistent positive division propagator.
static ExecStatus post(Home home, VA x0, VB x1, VC x2)
Post propagator (rounding towards 0)
Definition divmod.hpp:87
virtual Actor * copy(Space &home)
Copy propagator during cloning.
Definition divmod.hpp:57
DivPlusBnd(Home home, VA x0, VB x1, VC x2)
Constructor for posting.
Definition divmod.hpp:45
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition divmod.hpp:63
Minus integer view.
Definition view.hpp:282
Range iterator for singleton range.
friend class Space
Definition core.hpp:1068
TernaryPropagator(Space &home, TernaryPropagator &p)
ExecStatus ES_SUBSUMED(Propagator &p)
Propagator p is subsumed
Definition core.hpp:3570
int ModEventDelta
Modification event deltas.
Definition core.hpp:89
#define GECODE_ME_CHECK(me)
Check whether modification event me is failed, and forward failure.
Definition macros.hpp:52
#define GECODE_REWRITE(prop, post)
Rewrite propagator by executing post function.
Definition macros.hpp:116
#define GECODE_ME_CHECK_MODIFIED(modified, me)
Check whether me is failed or modified, and forward failure.
Definition macros.hpp:64
Numerical (arithmetic) propagators.
long long int dll(int x)
Decrement x by one.
Definition mult.hpp:63
bool pos(const View &x)
Test whether x is postive.
Definition mult.hpp:70
bool any(const View &x)
Test whether x is neither positive nor negative.
Definition mult.hpp:82
long long int mll(long long int x, long long int y)
Multiply x and \y.
Definition mult.hpp:48
long long int ill(int x)
Increment x by one.
Definition mult.hpp:58
bool neg(const View &x)
Test whether x is negative.
Definition mult.hpp:76
long long int ll(int x)
Cast x into a long long int.
Definition mult.hpp:53
Finite domain integers.
IntType ceil_div_pp(IntType x, IntType y)
Compute where x and y are non-negative.
Definition div.hpp:38
const Gecode::PropCond PC_INT_BND
Propagate when minimum or maximum of a view changes.
Definition var-type.hpp:91
IntType ceil_div_xp(IntType x, IntType y)
Compute where y is non-negative.
Definition div.hpp:69
IntType floor_div_xp(IntType x, IntType y)
Compute where y is non-negative.
Definition div.hpp:75
IntType floor_div_xx(IntType x, IntType y)
Compute .
Definition div.hpp:87
IntType floor_div_pp(IntType x, IntType y)
Compute where x and y are non-negative.
Definition div.hpp:49
IntType ceil_div_xx(IntType x, IntType y)
Compute .
Definition div.hpp:82
IntType floor_div_px(IntType x, IntType y)
Compute where x is non-negative.
Definition div.hpp:62
Gecode toplevel namespace
void mod(Home home, IntVar x0, IntVar x1, IntVar x2, IntPropLevel ipl=IPL_DEF)
Post propagator for .
ExecStatus
Definition core.hpp:472
@ ES_OK
Execution is okay.
Definition core.hpp:476
@ ES_FIX
Propagation has computed fixpoint.
Definition core.hpp:477
@ ES_NOFIX
Propagation has not computed fixpoint.
Definition core.hpp:475
#define forceinline
Definition config.hpp:194