Generated on Thu Apr 5 2018 19:44:19 for Gecode by doxygen 1.8.13
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$ by $Author$
11  * $Revision$
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>
57  (home,p) {}
58 
59  template<class VA, class VB, class VC>
60  Actor*
62  return new (home) DivPlusBnd<VA,VB,VC>(home,*this);
63  }
64 
65  template<class VA, class VB, class VC>
68  assert(pos(x0) && pos(x1) && !neg(x2));
69  bool mod;
70  do {
71  mod = false;
72  GECODE_ME_CHECK_MODIFIED(mod,x2.lq(home,
73  floor_div_pp(x0.max(),x1.min())));
74  GECODE_ME_CHECK_MODIFIED(mod,x2.gq(home,
75  floor_div_px(x0.min(),x1.max())));
76  GECODE_ME_CHECK_MODIFIED(mod,x0.le(home,mll(x1.max(),ill(x2.max()))));
77  GECODE_ME_CHECK_MODIFIED(mod,x0.gq(home,mll(x1.min(),x2.min())));
78  if (x2.min() > 0) {
80  x1.lq(home,floor_div_pp(x0.max(),x2.min())));
81  }
82  GECODE_ME_CHECK_MODIFIED(mod,x1.gq(home,ceil_div_pp(ll(x0.min()),
83  ill(x2.max()))));
84  } while (mod);
85  return x0.assigned() && x1.assigned() ?
86  home.ES_SUBSUMED(*this) : ES_FIX;
87  }
88 
89  template<class VA, class VB, class VC>
91  DivPlusBnd<VA,VB,VC>::post(Home home, VA x0, VB x1, VC x2) {
92  GECODE_ME_CHECK(x0.gr(home,0));
93  GECODE_ME_CHECK(x1.gr(home,0));
94  GECODE_ME_CHECK(x2.gq(home,floor_div_pp(x0.min(),x1.max())));
95  (void) new (home) DivPlusBnd<VA,VB,VC>(home,x0,x1,x2);
96  return ES_OK;
97  }
98 
99 
100  /*
101  * Bounds consistent division
102  *
103  */
104  template<class View>
106  DivBnd<View>::DivBnd(Home home, View x0, View x1, View x2)
107  : TernaryPropagator<View,PC_INT_BND>(home,x0,x1,x2) {}
108 
109  template<class View>
112  : TernaryPropagator<View,PC_INT_BND>(home,p) {}
113 
114  template<class View>
115  Actor*
117  return new (home) DivBnd<View>(home,*this);
118  }
119 
120  template<class View>
121  ExecStatus
123  if (pos(x1)) {
124  if (pos(x2) || pos(x0)) goto rewrite_ppp;
125  if (neg(x2) || neg(x0)) goto rewrite_npn;
126  goto prop_xpx;
127  }
128  if (neg(x1)) {
129  if (neg(x2) || pos(x0)) goto rewrite_pnn;
130  if (pos(x2) || neg(x0)) goto rewrite_nnp;
131  goto prop_xnx;
132  }
133  if (pos(x2)) {
134  if (pos(x0)) goto rewrite_ppp;
135  if (neg(x0)) goto rewrite_nnp;
136  goto prop_xxp;
137  }
138  if (neg(x2)) {
139  if (pos(x0)) goto rewrite_pnn;
140  if (neg(x0)) goto rewrite_npn;
141  goto prop_xxn;
142  }
143  assert(any(x1) && any(x2));
144  GECODE_ME_CHECK(x0.lq(home,std::max(mll(x1.max(),ill(x2.max()))-1,
145  mll(x1.min(),dll(x2.min()))-1)));
146  GECODE_ME_CHECK(x0.gq(home,std::min(mll(x1.min(),ill(x2.max())),
147  mll(x1.max(),dll(x2.min())))));
148  return ES_NOFIX;
149 
150  prop_xxp:
151  assert(any(x0) && any(x1) && pos(x2));
152 
153  GECODE_ME_CHECK(x0.le(home, mll(x1.max(),ill(x2.max()))));
154  GECODE_ME_CHECK(x0.gq(home, mll(x1.min(),ill(x2.max()))));
155 
156  if (pos(x0)) goto rewrite_ppp;
157  if (neg(x0)) goto rewrite_nnp;
158 
159  GECODE_ME_CHECK(x1.lq(home,floor_div_pp(x0.max(),x2.min())));
160  GECODE_ME_CHECK(x1.gq(home,ceil_div_xp(x0.min(),x2.min())));
161 
162  if (x0.assigned() && x1.assigned())
163  goto subsumed;
164  return ES_NOFIX;
165 
166  prop_xpx:
167  assert(any(x0) && pos(x1) && any(x2));
168 
169  GECODE_ME_CHECK(x0.le(home, mll(x1.max(),ill(x2.max()))));
170  GECODE_ME_CHECK(x0.gq(home, mll(x1.max(),dll(x2.min()))));
171 
172  if (pos(x0)) goto rewrite_ppp;
173  if (neg(x0)) goto rewrite_npn;
174 
175  GECODE_ME_CHECK(x2.lq(home,floor_div_xp(x0.max(),x1.min())));
176  GECODE_ME_CHECK(x2.gq(home,floor_div_xp(x0.min(),x1.min())));
177 
178  if (x0.assigned() && x1.assigned())
179  goto subsumed;
180  return ES_NOFIX;
181 
182  prop_xxn:
183  assert(any(x0) && any(x1) && neg(x2));
184 
185  GECODE_ME_CHECK(x0.lq(home, mll(x1.min(),dll(x2.min()))));
186  GECODE_ME_CHECK(x0.gq(home, mll(x1.max(),dll(x2.min()))));
187 
188  if (pos(x0)) goto rewrite_pnn;
189  if (neg(x0)) goto rewrite_npn;
190 
191  if (x2.max() != -1)
192  GECODE_ME_CHECK(x1.lq(home,ceil_div_xx(ll(x0.min()),ill(x2.max()))));
193  if (x2.max() != -1)
194  GECODE_ME_CHECK(x1.gq(home,ceil_div_xx(ll(x0.max()),ill(x2.max()))));
195 
196  if (x0.assigned() && x1.assigned())
197  goto subsumed;
198  return ES_NOFIX;
199 
200  prop_xnx:
201  assert(any(x0) && neg(x1) && any(x2));
202 
203  GECODE_ME_CHECK(x0.lq(home, mll(x1.min(),dll(x2.min()))));
204  GECODE_ME_CHECK(x0.gq(home, mll(x1.min(),ill(x2.max()))));
205 
206  if (pos(x0)) goto rewrite_pnn;
207  if (neg(x0)) goto rewrite_nnp;
208 
209  GECODE_ME_CHECK(x2.lq(home,floor_div_xx(x0.min(),x1.max())));
210  GECODE_ME_CHECK(x2.gq(home,floor_div_xx(x0.max(),x1.max())));
211 
212  if (x0.assigned() && x1.assigned())
213  goto subsumed;
214  return ES_NOFIX;
215 
216  rewrite_ppp:
218  ::post(home(*this),x0,x1,x2)));
219  rewrite_nnp:
221  ::post(home(*this),MinusView(x0),MinusView(x1),x2)));
222  rewrite_pnn:
224  ::post(home(*this),x0,MinusView(x1),MinusView(x2))));
225  rewrite_npn:
227  ::post(home(*this),MinusView(x0),x1,MinusView(x2))));
228  subsumed:
229  assert(x0.assigned() && x1.assigned());
230  int result = std::abs(x0.val()) / std::abs(x1.val());
231  if (x0.val()/x1.val() < 0)
232  result = -result;
233  GECODE_ME_CHECK(x2.eq(home,result));
234  return home.ES_SUBSUMED(*this);
235  }
236 
237  template<class View>
238  ExecStatus
239  DivBnd<View>::post(Home home, View x0, View x1, View x2) {
240  GECODE_ME_CHECK(x1.nq(home, 0));
241  if (pos(x0)) {
242  if (pos(x1) || pos(x2)) goto post_ppp;
243  if (neg(x1) || neg(x2)) goto post_pnn;
244  } else if (neg(x0)) {
245  if (neg(x1) || pos(x2)) goto post_nnp;
246  if (pos(x1) || neg(x2)) goto post_npn;
247  } else if (pos(x1)) {
248  if (pos(x2)) goto post_ppp;
249  if (neg(x2)) goto post_npn;
250  } else if (neg(x1)) {
251  if (pos(x2)) goto post_nnp;
252  if (neg(x2)) goto post_pnn;
253  }
254  (void) new (home) DivBnd<View>(home,x0,x1,x2);
255  return ES_OK;
256 
257  post_ppp:
259  ::post(home,x0,x1,x2);
260  post_nnp:
262  ::post(home,MinusView(x0),MinusView(x1),x2);
263  post_pnn:
265  ::post(home,x0,MinusView(x1),MinusView(x2));
266  post_npn:
268  ::post(home,MinusView(x0),x1,MinusView(x2));
269  }
270 
271 
272  /*
273  * Propagator for x0 != 0 /\ (x1 != 0 => x0*x1>0) /\ abs(x1)<abs(x0)
274  *
275  */
276 
277  template<class View>
279  DivMod<View>::DivMod(Home home, View x0, View x1, View x2)
280  : TernaryPropagator<View,PC_INT_BND>(home,x0,x1,x2) {}
281 
282  template<class View>
284  DivMod<View>::post(Home home, View x0, View x1, View x2) {
285  GECODE_ME_CHECK(x1.nq(home,0));
286  (void) new (home) DivMod<View>(home,x0,x1,x2);
287  return ES_OK;
288  }
289 
290  template<class View>
293  : TernaryPropagator<View,PC_INT_BND>(home,p) {}
294 
295  template<class View>
296  Actor*
298  return new (home) DivMod<View>(home,*this);
299  }
300 
301  template<class View>
302  ExecStatus
304  bool signIsSame;
305  do {
306  signIsSame = true;
307  // The sign of x0 and x2 is the same
308  if (x0.min() >= 0) {
309  GECODE_ME_CHECK(x2.gq(home, 0));
310  } else if (x0.max() <= 0) {
311  GECODE_ME_CHECK(x2.lq(home, 0));
312  } else if (x2.min() > 0) {
313  GECODE_ME_CHECK(x0.gq(home, 0));
314  } else if (x2.max() < 0) {
315  GECODE_ME_CHECK(x0.lq(home, 0));
316  } else {
317  signIsSame = false;
318  }
319 
320  // abs(x2) is less than abs(x1)
321  int x1max = std::max(x1.max(),std::max(-x1.max(),
322  std::max(x1.min(),-x1.min())));
323  GECODE_ME_CHECK(x2.le(home, x1max));
324  GECODE_ME_CHECK(x2.gr(home, -x1max));
325 
326  int x2absmin = any(x2) ? 0 : (pos(x2) ? x2.min() : -x2.max());
327  Iter::Ranges::Singleton sr(-x2absmin,x2absmin);
328  GECODE_ME_CHECK(x1.minus_r(home,sr,false));
329  } while (!signIsSame &&
330  (x0.min() > 0 || x0.max() < 0 || x2.min() > 0 || x2.max() < 0));
331 
332  if (signIsSame) {
333  int x2max = std::max(x2.max(),std::max(-x2.max(),
334  std::max(x2.min(),-x2.min())));
335  int x1absmin = any(x1) ? 0 : (pos(x1) ? x1.min() : -x1.max());
336  if (x2max < x1absmin)
337  return home.ES_SUBSUMED(*this);
338  }
339  return ES_FIX;
340  }
341 
342 }}}
343 
344 // STATISTICS: int-prop
IntType ceil_div_pp(IntType x, IntType y)
Compute where x and y are non-negative.
Definition: div.hpp:42
void mod(Home home, IntVar x0, IntVar x1, IntVar x2, IntPropLevel ipl)
Post propagator for .
Definition: arithmetic.cpp:267
#define GECODE_REWRITE(prop, post)
Rewrite propagator by executing post function.
Definition: macros.hpp:120
Bounds consistent positive division propagator.
Definition: arithmetic.hh:781
Integer division/modulo propagator.
Definition: arithmetic.hh:838
bool any(const View &x)
Test whether x is neither positive nor negative.
Definition: mult.hpp:86
Range iterator for singleton range.
ExecStatus ES_SUBSUMED(Propagator &p)
Definition: core.hpp:3433
const FloatNum max
Largest allowed float value.
Definition: float.hh:848
ExecStatus subsumed(Space &home, Propagator &p, int c, TaskArray< Task > &t)
Check for subsumption (all tasks must be assigned)
Definition: subsumption.hpp:42
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:45
virtual Actor * copy(Space &home)
Copy propagator during cloning.
Definition: divmod.hpp:116
long long int mll(long long int x, long long int y)
Multiply x and .
Definition: mult.hpp:52
IntType floor_div_xx(IntType x, IntType y)
Compute .
Definition: div.hpp:91
virtual Actor * copy(Space &home)
Copy propagator during cloning.
Definition: divmod.hpp:297
#define forceinline
Definition: config.hpp:182
Propagation has computed fixpoint.
Definition: core.hpp:469
Computation spaces.
Definition: core.hpp:1668
#define GECODE_ME_CHECK_MODIFIED(modified, me)
Check whether me is failed or modified, and forward failure.
Definition: macros.hpp:68
Base-class for both propagators and branchers.
Definition: core.hpp:620
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:850
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: divmod.hpp:67
Mixed ternary propagator.
Definition: pattern.hpp:241
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
DivBnd(Space &home, DivBnd< View > &p)
Constructor for cloning p.
Definition: divmod.hpp:111
Ternary propagator.
Definition: pattern.hpp:117
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:56
Bounds consistent division propagator.
Definition: arithmetic.hh:808
DivMod(Space &home, DivMod< View > &p)
Constructor for cloning p.
Definition: divmod.hpp:292
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: divmod.hpp:303
IntType floor_div_px(IntType x, IntType y)
Compute where x is non-negative.
Definition: div.hpp:66
ExecStatus
Definition: core.hpp:464
Minus integer view.
Definition: view.hpp:278
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:239
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: divmod.hpp:122
Execution is okay.
Definition: core.hpp:468
Propagation has not computed fixpoint.
Definition: core.hpp:467
static ExecStatus post(Home home, View x0, View x1, View x2)
Post propagator .
Definition: divmod.hpp:284
Gecode toplevel namespace
int ModEventDelta
Modification event deltas.
Definition: core.hpp:91
static ExecStatus post(Home home, VA x0, VB x1, VC x2)
Post propagator (rounding towards 0)
Definition: divmod.hpp:91
Home class for posting propagators
Definition: core.hpp:846
virtual Actor * copy(Space &home)
Copy propagator during cloning.
Definition: divmod.hpp:61
bool neg(const View &x)
Test whether x is negative.
Definition: mult.hpp:80