Generated on Sat Feb 7 2015 02:01:19 for Gecode by doxygen 1.8.9.1
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  * Last modified:
10  * $Date: 2013-02-14 16:29:11 +0100 (Thu, 14 Feb 2013) $ by $Author: schulte $
11  * $Revision: 13292 $
12  *
13  * This file is part of Gecode, the generic constraint
14  * development environment:
15  * http://www.gecode.org
16  *
17  * Permission is hereby granted, free of charge, to any person obtaining
18  * a copy of this software and associated documentation files (the
19  * "Software"), to deal in the Software without restriction, including
20  * without limitation the rights to use, copy, modify, merge, publish,
21  * distribute, sublicense, and/or sell copies of the Software, and to
22  * permit persons to whom the Software is furnished to do so, subject to
23  * the following conditions:
24  *
25  * The above copyright notice and this permission notice shall be
26  * included in all copies or substantial portions of the Software.
27  *
28  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
29  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
30  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
31  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
32  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
33  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
34  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
35  *
36  */
37 
38 #include <gecode/int/linear.hh>
39 
40 namespace Gecode { namespace Int { namespace Arithmetic {
41 
42  /*
43  * Positive bounds consistent division
44  *
45  */
46 
47  template<class VA, class VB, class VC>
49  DivPlusBnd<VA,VB,VC>::DivPlusBnd(Home home, VA x0, VB x1, VC x2)
51  (home,x0,x1,x2) {}
52 
53  template<class VA, class VB, class VC>
58  (home,share,p) {}
59 
60  template<class VA, class VB, class VC>
61  Actor*
62  DivPlusBnd<VA,VB,VC>::copy(Space& home, bool share) {
63  return new (home) DivPlusBnd<VA,VB,VC>(home,share,*this);
64  }
65 
66  template<class VA, class VB, class VC>
69  assert(pos(x0) && pos(x1) && !neg(x2));
70  bool mod;
71  do {
72  mod = false;
73  GECODE_ME_CHECK_MODIFIED(mod,x2.lq(home,
74  floor_div_pp(x0.max(),x1.min())));
75  GECODE_ME_CHECK_MODIFIED(mod,x2.gq(home,
76  floor_div_px(x0.min(),x1.max())));
77  GECODE_ME_CHECK_MODIFIED(mod,x0.le(home,mll(x1.max(),ill(x2.max()))));
78  GECODE_ME_CHECK_MODIFIED(mod,x0.gq(home,mll(x1.min(),x2.min())));
79  if (x2.min() > 0) {
81  x1.lq(home,floor_div_pp(x0.max(),x2.min())));
82  }
83  GECODE_ME_CHECK_MODIFIED(mod,x1.gq(home,ceil_div_pp(ll(x0.min()),
84  ill(x2.max()))));
85  } while (mod);
86  return x0.assigned() && x1.assigned() ?
87  home.ES_SUBSUMED(*this) : ES_FIX;
88  }
89 
90  template<class VA, class VB, class VC>
92  DivPlusBnd<VA,VB,VC>::post(Home home, VA x0, VB x1, VC x2) {
93  GECODE_ME_CHECK(x0.gr(home,0));
94  GECODE_ME_CHECK(x1.gr(home,0));
95  GECODE_ME_CHECK(x2.gq(home,floor_div_pp(x0.min(),x1.max())));
96  (void) new (home) DivPlusBnd<VA,VB,VC>(home,x0,x1,x2);
97  return ES_OK;
98  }
99 
100 
101  /*
102  * Bounds consistent division
103  *
104  */
105  template<class View>
107  DivBnd<View>::DivBnd(Home home, View x0, View x1, View x2)
108  : TernaryPropagator<View,PC_INT_BND>(home,x0,x1,x2) {}
109 
110  template<class View>
113  : TernaryPropagator<View,PC_INT_BND>(home,share,p) {}
114 
115  template<class View>
116  Actor*
117  DivBnd<View>::copy(Space& home, bool share) {
118  return new (home) DivBnd<View>(home,share,*this);
119  }
120 
121  template<class View>
122  ExecStatus
124  if (pos(x1)) {
125  if (pos(x2) || pos(x0)) goto rewrite_ppp;
126  if (neg(x2) || neg(x0)) goto rewrite_npn;
127  goto prop_xpx;
128  }
129  if (neg(x1)) {
130  if (neg(x2) || pos(x0)) goto rewrite_pnn;
131  if (pos(x2) || neg(x0)) goto rewrite_nnp;
132  goto prop_xnx;
133  }
134  if (pos(x2)) {
135  if (pos(x0)) goto rewrite_ppp;
136  if (neg(x0)) goto rewrite_nnp;
137  goto prop_xxp;
138  }
139  if (neg(x2)) {
140  if (pos(x0)) goto rewrite_pnn;
141  if (neg(x0)) goto rewrite_npn;
142  goto prop_xxn;
143  }
144  assert(any(x1) && any(x2));
145  GECODE_ME_CHECK(x0.lq(home,std::max(mll(x1.max(),ill(x2.max()))-1,
146  mll(x1.min(),dll(x2.min()))-1)));
147  GECODE_ME_CHECK(x0.gq(home,std::min(mll(x1.min(),ill(x2.max())),
148  mll(x1.max(),dll(x2.min())))));
149  return ES_NOFIX;
150 
151  prop_xxp:
152  assert(any(x0) && any(x1) && pos(x2));
153 
154  GECODE_ME_CHECK(x0.le(home, mll(x1.max(),ill(x2.max()))));
155  GECODE_ME_CHECK(x0.gq(home, mll(x1.min(),ill(x2.max()))));
156 
157  if (pos(x0)) goto rewrite_ppp;
158  if (neg(x0)) goto rewrite_nnp;
159 
160  GECODE_ME_CHECK(x1.lq(home,floor_div_pp(x0.max(),x2.min())));
161  GECODE_ME_CHECK(x1.gq(home,ceil_div_xp(x0.min(),x2.min())));
162 
163  if (x0.assigned() && x1.assigned())
164  goto subsumed;
165  return ES_NOFIX;
166 
167  prop_xpx:
168  assert(any(x0) && pos(x1) && any(x2));
169 
170  GECODE_ME_CHECK(x0.le(home, mll(x1.max(),ill(x2.max()))));
171  GECODE_ME_CHECK(x0.gq(home, mll(x1.max(),dll(x2.min()))));
172 
173  if (pos(x0)) goto rewrite_ppp;
174  if (neg(x0)) goto rewrite_npn;
175 
176  GECODE_ME_CHECK(x2.lq(home,floor_div_xp(x0.max(),x1.min())));
177  GECODE_ME_CHECK(x2.gq(home,floor_div_xp(x0.min(),x1.min())));
178 
179  if (x0.assigned() && x1.assigned())
180  goto subsumed;
181  return ES_NOFIX;
182 
183  prop_xxn:
184  assert(any(x0) && any(x1) && neg(x2));
185 
186  GECODE_ME_CHECK(x0.lq(home, mll(x1.min(),dll(x2.min()))));
187  GECODE_ME_CHECK(x0.gq(home, mll(x1.max(),dll(x2.min()))));
188 
189  if (pos(x0)) goto rewrite_pnn;
190  if (neg(x0)) goto rewrite_npn;
191 
192  if (x2.max() != -1)
193  GECODE_ME_CHECK(x1.lq(home,ceil_div_xx(ll(x0.min()),ill(x2.max()))));
194  if (x2.max() != -1)
195  GECODE_ME_CHECK(x1.gq(home,ceil_div_xx(ll(x0.max()),ill(x2.max()))));
196 
197  if (x0.assigned() && x1.assigned())
198  goto subsumed;
199  return ES_NOFIX;
200 
201  prop_xnx:
202  assert(any(x0) && neg(x1) && any(x2));
203 
204  GECODE_ME_CHECK(x0.lq(home, mll(x1.min(),dll(x2.min()))));
205  GECODE_ME_CHECK(x0.gq(home, mll(x1.min(),ill(x2.max()))));
206 
207  if (pos(x0)) goto rewrite_pnn;
208  if (neg(x0)) goto rewrite_nnp;
209 
210  GECODE_ME_CHECK(x2.lq(home,floor_div_xx(x0.min(),x1.max())));
211  GECODE_ME_CHECK(x2.gq(home,floor_div_xx(x0.max(),x1.max())));
212 
213  if (x0.assigned() && x1.assigned())
214  goto subsumed;
215  return ES_NOFIX;
216 
217  rewrite_ppp:
219  ::post(home(*this),x0,x1,x2)));
220  rewrite_nnp:
222  ::post(home(*this),MinusView(x0),MinusView(x1),x2)));
223  rewrite_pnn:
225  ::post(home(*this),x0,MinusView(x1),MinusView(x2))));
226  rewrite_npn:
228  ::post(home(*this),MinusView(x0),x1,MinusView(x2))));
229  subsumed:
230  assert(x0.assigned() && x1.assigned());
231  int result = std::abs(x0.val()) / std::abs(x1.val());
232  if (x0.val()/x1.val() < 0)
233  result = -result;
234  GECODE_ME_CHECK(x2.eq(home,result));
235  return home.ES_SUBSUMED(*this);
236  }
237 
238  template<class View>
239  ExecStatus
240  DivBnd<View>::post(Home home, View x0, View x1, View x2) {
241  GECODE_ME_CHECK(x1.nq(home, 0));
242  if (pos(x0)) {
243  if (pos(x1) || pos(x2)) goto post_ppp;
244  if (neg(x1) || neg(x2)) goto post_pnn;
245  } else if (neg(x0)) {
246  if (neg(x1) || pos(x2)) goto post_nnp;
247  if (pos(x1) || neg(x2)) goto post_npn;
248  } else if (pos(x1)) {
249  if (pos(x2)) goto post_ppp;
250  if (neg(x2)) goto post_npn;
251  } else if (neg(x1)) {
252  if (pos(x2)) goto post_nnp;
253  if (neg(x2)) goto post_pnn;
254  }
255  (void) new (home) DivBnd<View>(home,x0,x1,x2);
256  return ES_OK;
257 
258  post_ppp:
260  ::post(home,x0,x1,x2);
261  post_nnp:
263  ::post(home,MinusView(x0),MinusView(x1),x2);
264  post_pnn:
266  ::post(home,x0,MinusView(x1),MinusView(x2));
267  post_npn:
269  ::post(home,MinusView(x0),x1,MinusView(x2));
270  }
271 
272 
273  /*
274  * Propagator for x0 != 0 /\ (x1 != 0 => x0*x1>0) /\ abs(x1)<abs(x0)
275  *
276  */
277 
278  template<class View>
280  DivMod<View>::DivMod(Home home, View x0, View x1, View x2)
281  : TernaryPropagator<View,PC_INT_BND>(home,x0,x1,x2) {}
282 
283  template<class View>
285  DivMod<View>::post(Home home, View x0, View x1, View x2) {
286  GECODE_ME_CHECK(x1.nq(home,0));
287  (void) new (home) DivMod<View>(home,x0,x1,x2);
288  return ES_OK;
289  }
290 
291  template<class View>
294  : TernaryPropagator<View,PC_INT_BND>(home,share,p) {}
295 
296  template<class View>
297  Actor*
298  DivMod<View>::copy(Space& home, bool share) {
299  return new (home) DivMod<View>(home,share,*this);
300  }
301 
302  template<class View>
303  ExecStatus
305  bool signIsSame;
306  do {
307  signIsSame = true;
308  // The sign of x0 and x2 is the same
309  if (x0.min() >= 0) {
310  GECODE_ME_CHECK(x2.gq(home, 0));
311  } else if (x0.max() <= 0) {
312  GECODE_ME_CHECK(x2.lq(home, 0));
313  } else if (x2.min() > 0) {
314  GECODE_ME_CHECK(x0.gq(home, 0));
315  } else if (x2.max() < 0) {
316  GECODE_ME_CHECK(x0.lq(home, 0));
317  } else {
318  signIsSame = false;
319  }
320 
321  // abs(x2) is less than abs(x1)
322  int x1max = std::max(x1.max(),std::max(-x1.max(),
323  std::max(x1.min(),-x1.min())));
324  GECODE_ME_CHECK(x2.le(home, x1max));
325  GECODE_ME_CHECK(x2.gr(home, -x1max));
326 
327  int x2absmin = any(x2) ? 0 : (pos(x2) ? x2.min() : -x2.max());
328  Iter::Ranges::Singleton sr(-x2absmin,x2absmin);
329  GECODE_ME_CHECK(x1.minus_r(home,sr,false));
330  } while (!signIsSame &&
331  (x0.min() > 0 || x0.max() < 0 || x2.min() > 0 || x2.max() < 0));
332 
333  if (signIsSame) {
334  int x2max = std::max(x2.max(),std::max(-x2.max(),
335  std::max(x2.min(),-x2.min())));
336  int x1absmin = any(x1) ? 0 : (pos(x1) ? x1.min() : -x1.max());
337  if (x2max < x1absmin)
338  return home.ES_SUBSUMED(*this);
339  }
340  return ES_FIX;
341  }
342 
343 }}}
344 
345 // STATISTICS: int-prop
IntType ceil_div_pp(IntType x, IntType y)
Compute where x and y are non-negative.
Definition: div.hpp:42
#define GECODE_REWRITE(prop, post)
Rewrite propagator by executing post function.
Definition: macros.hpp:109
Bounds consistent positive division propagator.
Definition: arithmetic.hh:779
Integer division/modulo propagator.
Definition: arithmetic.hh:836
bool any(const View &x)
Test whether x is neither positive nor negative.
Definition: mult.hpp:86
void mod(Home home, IntVar x0, IntVar x1, IntVar x2, IntConLevel icl)
Post propagator for .
Definition: arithmetic.cpp:213
Range iterator for singleton range.
void post(Home home, Term *t, int n, FloatRelType frt, FloatVal c)
Post propagator for linear constraint over floats.
Definition: post.cpp:228
ExecStatus ES_SUBSUMED(Propagator &p)
Definition: core.hpp:2973
const FloatNum max
Largest allowed float value.
Definition: float.hh:831
DivPlusBnd(Home home, VA x0, VB x1, VC x2)
Constructor for posting.
Definition: divmod.hpp:49
long long int ll(int x)
Cast x into a long long int.
Definition: mult.hpp:57
void abs(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition: arithmetic.cpp:49
long long int mll(long long int x, long long int y)
Multiply x and .
Definition: mult.hpp:52
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: divmod.hpp:62
IntType floor_div_xx(IntType x, IntType y)
Compute .
Definition: div.hpp:91
Propagation has computed fixpoint.
Definition: core.hpp:528
DivBnd(Space &home, bool share, DivBnd< View > &p)
Constructor for cloning p.
Definition: divmod.hpp:112
Computation spaces.
Definition: core.hpp:1362
#define GECODE_ME_CHECK_MODIFIED(modified, me)
Check whether me is failed or modified, and forward failure.
Definition: macros.hpp:57
Base-class for both propagators and branchers.
Definition: core.hpp:666
long long int ill(int x)
Increment x by one.
Definition: mult.hpp:62
int p
Number of positive literals for node type.
Definition: bool-expr.cpp:236
const FloatNum min
Smallest allowed float value.
Definition: float.hh:833
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: divmod.hpp:68
Mixed ternary propagator.
Definition: propagator.hpp:235
const Gecode::PropCond PC_INT_BND
Propagate when minimum or maximum of a view changes.
Definition: var-type.hpp:91
IntType floor_div_pp(IntType x, IntType y)
Compute where x and y are non-negative.
Definition: div.hpp:53
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: divmod.hpp:117
DivMod(Space &home, bool share, DivMod< View > &p)
Constructor for cloning p.
Definition: divmod.hpp:293
Ternary propagator.
Definition: propagator.hpp:115
IntType floor_div_xp(IntType x, IntType y)
Compute where y is non-negative.
Definition: div.hpp:79
IntType ceil_div_xp(IntType x, IntType y)
Compute where y is non-negative.
Definition: div.hpp:73
IntType ceil_div_xx(IntType x, IntType y)
Compute .
Definition: div.hpp:86
#define GECODE_ME_CHECK(me)
Check whether modification event me is failed, and forward failure.
Definition: macros.hpp:45
Bounds consistent division propagator.
Definition: arithmetic.hh:806
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: divmod.hpp:298
ExecStatus subsumed(Space &home, Propagator &p, TaskArray< Task > &t)
Check tasks t for subsumption.
Definition: subsumption.hpp:42
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: divmod.hpp:304
IntType floor_div_px(IntType x, IntType y)
Compute where x is non-negative.
Definition: div.hpp:66
ExecStatus
Definition: core.hpp:523
Minus integer view.
Definition: view.hpp:276
#define forceinline
Definition: config.hpp:132
bool pos(const View &x)
Test whether x is postive.
Definition: mult.hpp:74
long long int dll(int x)
Decrement x by one.
Definition: mult.hpp:67
static ExecStatus post(Home home, View x0, View x1, View x2)
Post propagator (rounding towards 0)
Definition: divmod.hpp:240
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: divmod.hpp:123
Execution is okay.
Definition: core.hpp:527
Propagation has not computed fixpoint.
Definition: core.hpp:526
static ExecStatus post(Home home, View x0, View x1, View x2)
Post propagator .
Definition: divmod.hpp:285
Gecode toplevel namespace
int ModEventDelta
Modification event deltas.
Definition: core.hpp:173
static ExecStatus post(Home home, VA x0, VB x1, VC x2)
Post propagator (rounding towards 0)
Definition: divmod.hpp:92
Home class for posting propagators
Definition: core.hpp:717
bool neg(const View &x)
Test whether x is negative.
Definition: mult.hpp:80