Generated on Fri Aug 31 2012 16:21:20 for Gecode by doxygen 1.8.1.2
int-post.cpp
Go to the documentation of this file.
1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2 /*
3  * Main authors:
4  * Christian Schulte <schulte@gecode.org>
5  *
6  * Copyright:
7  * Christian Schulte, 2002
8  *
9  * Last modified:
10  * $Date: 2011-09-02 19:52:00 +1000 (Fri, 02 Sep 2011) $ by $Author: tack $
11  * $Revision: 12388 $
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 <cfloat>
39 #include <algorithm>
40 
41 #include <gecode/int/rel.hh>
42 #include <gecode/int/linear.hh>
43 
44 namespace Gecode { namespace Int { namespace Linear {
45 
47  inline void
48  eliminate(Term<IntView>* t, int &n, double& d) {
49  for (int i=n; i--; )
50  if (t[i].x.assigned()) {
51  d -= t[i].a * static_cast<double>(t[i].x.val());
52  t[i]=t[--n];
53  }
54  if ((d < Limits::double_min) || (d > Limits::double_max))
55  throw OutOfLimits("Int::linear");
56  }
57 
59  inline void
60  rewrite(IntRelType &r, double &d,
61  Term<IntView>* &t_p, int &n_p,
62  Term<IntView>* &t_n, int &n_n) {
63  switch (r) {
64  case IRT_EQ: case IRT_NQ: case IRT_LQ:
65  break;
66  case IRT_LE:
67  d--; r = IRT_LQ; break;
68  case IRT_GR:
69  d++; /* fall through */
70  case IRT_GQ:
71  r = IRT_LQ;
72  std::swap(n_p,n_n); std::swap(t_p,t_n); d = -d;
73  break;
74  default:
75  throw UnknownRelation("Int::linear");
76  }
77  }
78 
80  inline bool
81  precision(Term<IntView>* t_p, int n_p,
82  Term<IntView>* t_n, int n_n,
83  double d) {
84  double sl = 0.0;
85  double su = 0.0;
86 
87  for (int i = n_p; i--; ) {
88  sl += t_p[i].a * static_cast<double>(t_p[i].x.min());
89  su += t_p[i].a * static_cast<double>(t_p[i].x.max());
90  if ((sl < Limits::double_min) || (su > Limits::double_max))
91  throw OutOfLimits("Int::linear");
92  }
93  for (int i = n_n; i--; ) {
94  sl -= t_n[i].a * static_cast<double>(t_n[i].x.max());
95  su -= t_n[i].a * static_cast<double>(t_n[i].x.min());
96  if ((sl < Limits::double_min) || (su > Limits::double_max))
97  throw OutOfLimits("Int::linear");
98  }
99 
100  bool is_ip = (sl >= Limits::min) && (su <= Limits::max);
101 
102  sl -= d;
103  su -= d;
104  if ((sl < Limits::double_min) || (su > Limits::double_max))
105  throw OutOfLimits("Int::linear");
106 
107  is_ip = is_ip && (sl >= Limits::min) && (su <= Limits::max);
108 
109  for (int i = n_p; i--; ) {
110  if (sl - t_p[i].a * static_cast<double>(t_p[i].x.min())
112  throw OutOfLimits("Int::linear");
113  if (sl - t_p[i].a * static_cast<double>(t_p[i].x.min()) < Limits::min)
114  is_ip = false;
115  if (su - t_p[i].a * static_cast<double>(t_p[i].x.max())
117  throw OutOfLimits("Int::linear");
118  if (su - t_p[i].a * static_cast<double>(t_p[i].x.max()) > Limits::max)
119  is_ip = false;
120  }
121  for (int i = n_n; i--; ) {
122  if (sl + t_n[i].a * static_cast<double>(t_n[i].x.min())
124  throw OutOfLimits("Int::linear");
125  if (sl + t_n[i].a * static_cast<double>(t_n[i].x.min()) < Limits::min)
126  is_ip = false;
127  if (su + t_n[i].a * static_cast<double>(t_n[i].x.max())
129  throw OutOfLimits("Int::linear");
130  if (su + t_n[i].a * static_cast<double>(t_n[i].x.max()) > Limits::max)
131  is_ip = false;
132  }
133  return is_ip;
134  }
135 
140  template<class Val, class View>
141  forceinline void
144  switch (r) {
145  case IRT_EQ:
147  break;
148  case IRT_NQ:
150  break;
151  case IRT_LQ:
153  break;
154  default: GECODE_NEVER;
155  }
156  }
157 
158 
160 #define GECODE_INT_PL_BIN(CLASS) \
161  switch (n_p) { \
162  case 2: \
163  GECODE_ES_FAIL((CLASS<int,IntView,IntView>::post \
164  (home,t_p[0].x,t_p[1].x,c))); \
165  break; \
166  case 1: \
167  GECODE_ES_FAIL((CLASS<int,IntView,MinusView>::post \
168  (home,t_p[0].x,MinusView(t_n[0].x),c))); \
169  break; \
170  case 0: \
171  GECODE_ES_FAIL((CLASS<int,MinusView,MinusView>::post \
172  (home,MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
173  break; \
174  default: GECODE_NEVER; \
175  }
176 
178 #define GECODE_INT_PL_TER(CLASS) \
179  switch (n_p) { \
180  case 3: \
181  GECODE_ES_FAIL((CLASS<int,IntView,IntView,IntView>::post \
182  (home,t_p[0].x,t_p[1].x,t_p[2].x,c))); \
183  break; \
184  case 2: \
185  GECODE_ES_FAIL((CLASS<int,IntView,IntView,MinusView>::post \
186  (home,t_p[0].x,t_p[1].x, \
187  MinusView(t_n[0].x),c))); \
188  break; \
189  case 1: \
190  GECODE_ES_FAIL((CLASS<int,IntView,MinusView,MinusView>::post \
191  (home,t_p[0].x, \
192  MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
193  break; \
194  case 0: \
195  GECODE_ES_FAIL((CLASS<int,MinusView,MinusView,MinusView>::post \
196  (home,MinusView(t_n[0].x), \
197  MinusView(t_n[1].x),MinusView(t_n[2].x),c))); \
198  break; \
199  default: GECODE_NEVER; \
200  }
201 
202  void
203  post(Home home, Term<IntView>* t, int n, IntRelType r, int c,
204  IntConLevel icl) {
205 
206  Limits::check(c,"Int::linear");
207 
208  double d = c;
209 
210  eliminate(t,n,d);
211 
212  Term<IntView> *t_p, *t_n;
213  int n_p, n_n;
214  bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n);
215 
216  rewrite(r,d,t_p,n_p,t_n,n_n);
217 
218  if (n == 0) {
219  switch (r) {
220  case IRT_EQ: if (d != 0.0) home.fail(); break;
221  case IRT_NQ: if (d == 0.0) home.fail(); break;
222  case IRT_LQ: if (d < 0.0) home.fail(); break;
223  default: GECODE_NEVER;
224  }
225  return;
226  }
227 
228  if (n == 1) {
229  if (n_p == 1) {
230  DoubleScaleView y(t_p[0].a,t_p[0].x);
231  switch (r) {
232  case IRT_EQ: GECODE_ME_FAIL(y.eq(home,d)); break;
233  case IRT_NQ: GECODE_ME_FAIL(y.nq(home,d)); break;
234  case IRT_LQ: GECODE_ME_FAIL(y.lq(home,d)); break;
235  default: GECODE_NEVER;
236  }
237  } else {
238  DoubleScaleView y(t_n[0].a,t_n[0].x);
239  switch (r) {
240  case IRT_EQ: GECODE_ME_FAIL(y.eq(home,-d)); break;
241  case IRT_NQ: GECODE_ME_FAIL(y.nq(home,-d)); break;
242  case IRT_LQ: GECODE_ME_FAIL(y.gq(home,-d)); break;
243  default: GECODE_NEVER;
244  }
245  }
246  return;
247  }
248 
249  bool is_ip = precision(t_p,n_p,t_n,n_n,d);
250 
251  if (is_unit && is_ip && (icl != ICL_DOM)) {
252  // Unit coefficients with integer precision
253  c = static_cast<int>(d);
254  if (n == 2) {
255  switch (r) {
256  case IRT_EQ: GECODE_INT_PL_BIN(EqBin); break;
257  case IRT_NQ: GECODE_INT_PL_BIN(NqBin); break;
258  case IRT_LQ: GECODE_INT_PL_BIN(LqBin); break;
259  default: GECODE_NEVER;
260  }
261  } else if (n == 3) {
262  switch (r) {
263  case IRT_EQ: GECODE_INT_PL_TER(EqTer); break;
264  case IRT_NQ: GECODE_INT_PL_TER(NqTer); break;
265  case IRT_LQ: GECODE_INT_PL_TER(LqTer); break;
266  default: GECODE_NEVER;
267  }
268  } else {
269  ViewArray<IntView> x(home,n_p);
270  for (int i = n_p; i--; )
271  x[i] = t_p[i].x;
272  ViewArray<IntView> y(home,n_n);
273  for (int i = n_n; i--; )
274  y[i] = t_n[i].x;
275  post_nary<int,IntView>(home,x,y,r,c);
276  }
277  } else if (is_ip) {
278  if (n==2 && is_unit && icl == ICL_DOM && r == IRT_EQ) {
279  // Binary domain-consistent equality
280  c = static_cast<int>(d);
281  if (c==0) {
282  switch (n_p) {
283  case 2: {
284  IntView x(t_p[0].x);
285  MinusView y(t_p[1].x);
288  break;
289  }
290  case 1: {
291  IntView x(t_p[0].x);
292  IntView y(t_n[0].x);
295  break;
296  }
297  case 0: {
298  IntView x(t_n[0].x);
299  MinusView y(t_n[1].x);
302  break;
303  }
304  default:
305  GECODE_NEVER;
306  }
307  } else {
308  switch (n_p) {
309  case 2: {
310  MinusView x(t_p[0].x);
311  OffsetView y(t_p[1].x, -c);
314  break;
315  }
316  case 1: {
317  IntView x(t_p[0].x);
318  OffsetView y(t_n[0].x, c);
321  break;
322  }
323  case 0: {
324  MinusView x(t_n[0].x);
325  OffsetView y(t_n[1].x, c);
328  break;
329  }
330  default:
331  GECODE_NEVER;
332  }
333  }
334  } else {
335  // Arbitrary coefficients with integer precision
336  c = static_cast<int>(d);
337  ViewArray<IntScaleView> x(home,n_p);
338  for (int i = n_p; i--; )
339  x[i] = IntScaleView(t_p[i].a,t_p[i].x);
340  ViewArray<IntScaleView> y(home,n_n);
341  for (int i = n_n; i--; )
342  y[i] = IntScaleView(t_n[i].a,t_n[i].x);
343  if ((icl == ICL_DOM) && (r == IRT_EQ)) {
345  } else {
346  post_nary<int,IntScaleView>(home,x,y,r,c);
347  }
348  }
349  } else {
350  // Arbitrary coefficients with double precision
351  ViewArray<DoubleScaleView> x(home,n_p);
352  for (int i = n_p; i--; )
353  x[i] = DoubleScaleView(t_p[i].a,t_p[i].x);
354  ViewArray<DoubleScaleView> y(home,n_n);
355  for (int i = n_n; i--; )
356  y[i] = DoubleScaleView(t_n[i].a,t_n[i].x);
357  if ((icl == ICL_DOM) && (r == IRT_EQ)) {
359  } else {
360  post_nary<double,DoubleScaleView>(home,x,y,r,d);
361  }
362  }
363  }
364 
365 #undef GECODE_INT_PL_BIN
366 #undef GECODE_INT_PL_TER
367 
368 
373  template<class Val, class View>
374  forceinline void
377  IntRelType r, Val c, BoolView b) {
378  switch (r) {
379  case IRT_EQ:
381  break;
382  case IRT_NQ:
383  {
384  NegBoolView n(b);
386  (home,x,y,c,n)));
387  }
388  break;
389  case IRT_LQ:
390  GECODE_ES_FAIL((ReLq<Val,View,View>::post(home,x,y,c,b)));
391  break;
392  default: GECODE_NEVER;
393  }
394  }
395 
396  void
397  post(Home home,
398  Term<IntView>* t, int n, IntRelType r, int c, BoolView b,
399  IntConLevel) {
400 
401  Limits::check(c,"Int::linear");
402 
403  double d = c;
404 
405  eliminate(t,n,d);
406 
407  Term<IntView> *t_p, *t_n;
408  int n_p, n_n;
409  bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n);
410 
411  rewrite(r,d,t_p,n_p,t_n,n_n);
412 
413  if (n == 0) {
414  bool fail = false;
415  switch (r) {
416  case IRT_EQ: fail = (d != 0.0); break;
417  case IRT_NQ: fail = (d == 0.0); break;
418  case IRT_LQ: fail = (0.0 > d); break;
419  default: GECODE_NEVER;
420  }
421  if ((fail ? b.zero(home) : b.one(home)) == ME_INT_FAILED)
422  home.fail();
423  return;
424  }
425 
426  bool is_ip = precision(t_p,n_p,t_n,n_n,d);
427 
428  if (is_unit && is_ip) {
429  c = static_cast<int>(d);
430  if (n == 1) {
431  switch (r) {
432  case IRT_EQ:
433  if (n_p == 1) {
435  (home,t_p[0].x,c,b)));
436  } else {
438  (home,t_n[0].x,-c,b)));
439  }
440  break;
441  case IRT_NQ:
442  {
443  NegBoolView nb(b);
444  if (n_p == 1) {
446  (home,t_p[0].x,c,nb)));
447  } else {
449  (home,t_n[0].x,-c,nb)));
450  }
451  }
452  break;
453  case IRT_LQ:
454  if (n_p == 1) {
456  (home,t_p[0].x,c,b)));
457  } else {
458  NegBoolView nb(b);
460  (home,t_n[0].x,-c-1,nb)));
461  }
462  break;
463  default: GECODE_NEVER;
464  }
465  } else if (n == 2) {
466  switch (r) {
467  case IRT_EQ:
468  switch (n_p) {
469  case 2:
471  (home,t_p[0].x,t_p[1].x,c,b)));
472  break;
473  case 1:
475  (home,t_p[0].x,MinusView(t_n[0].x),c,b)));
476  break;
477  case 0:
479  (home,t_n[0].x,t_n[1].x,-c,b)));
480  break;
481  default: GECODE_NEVER;
482  }
483  break;
484  case IRT_NQ:
485  {
486  NegBoolView nb(b);
487  switch (n_p) {
488  case 2:
491  (home,t_p[0].x,t_p[1].x,c,nb)));
492  break;
493  case 1:
496  (home,t_p[0].x,MinusView(t_n[0].x),c,
497  NegBoolView(b))));
498  break;
499  case 0:
502  (home,t_p[0].x,t_p[1].x,-c,NegBoolView(b))));
503  break;
504  default: GECODE_NEVER;
505  }
506  }
507  break;
508  case IRT_LQ:
509  switch (n_p) {
510  case 2:
512  (home,t_p[0].x,t_p[1].x,c,b)));
513  break;
514  case 1:
516  (home,t_p[0].x,MinusView(t_n[0].x),c,b)));
517  break;
518  case 0:
520  (home,MinusView(t_n[0].x),
521  MinusView(t_n[1].x),c,b)));
522  break;
523  default: GECODE_NEVER;
524  }
525  break;
526  default: GECODE_NEVER;
527  }
528  } else {
529  ViewArray<IntView> x(home,n_p);
530  for (int i = n_p; i--; )
531  x[i] = t_p[i].x;
532  ViewArray<IntView> y(home,n_n);
533  for (int i = n_n; i--; )
534  y[i] = t_n[i].x;
535  post_nary<int,IntView>(home,x,y,r,c,b);
536  }
537  } else if (is_ip) {
538  // Arbitrary coefficients with integer precision
539  c = static_cast<int>(d);
540  ViewArray<IntScaleView> x(home,n_p);
541  for (int i = n_p; i--; )
542  x[i] = IntScaleView(t_p[i].a,t_p[i].x);
543  ViewArray<IntScaleView> y(home,n_n);
544  for (int i = n_n; i--; )
545  y[i] = IntScaleView(t_n[i].a,t_n[i].x);
546  post_nary<int,IntScaleView>(home,x,y,r,c,b);
547  } else {
548  // Arbitrary coefficients with double precision
549  ViewArray<DoubleScaleView> x(home,n_p);
550  for (int i = n_p; i--; )
551  x[i] = DoubleScaleView(t_p[i].a,t_p[i].x);
552  ViewArray<DoubleScaleView> y(home,n_n);
553  for (int i = n_n; i--; )
554  y[i] = DoubleScaleView(t_n[i].a,t_n[i].x);
555  post_nary<double,DoubleScaleView>(home,x,y,r,d,b);
556  }
557  }
558 
559 }}}
560 
561 // STATISTICS: int-post