Generated on Fri Aug 31 2012 16:21:18 for Gecode by doxygen 1.8.1.2
bool-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  * Tias Guns <tias.guns@cs.kuleuven.be>
6  *
7  * Copyright:
8  * Christian Schulte, 2002
9  * Tias Guns, 2009
10  *
11  * Last modified:
12  * $Date: 2010-03-04 03:40:32 +1100 (Thu, 04 Mar 2010) $ by $Author: schulte $
13  * $Revision: 10365 $
14  *
15  * This file is part of Gecode, the generic constraint
16  * development environment:
17  * http://www.gecode.org
18  *
19  * Permission is hereby granted, free of charge, to any person obtaining
20  * a copy of this software and associated documentation files (the
21  * "Software"), to deal in the Software without restriction, including
22  * without limitation the rights to use, copy, modify, merge, publish,
23  * distribute, sublicense, and/or sell copies of the Software, and to
24  * permit persons to whom the Software is furnished to do so, subject to
25  * the following conditions:
26  *
27  * The above copyright notice and this permission notice shall be
28  * included in all copies or substantial portions of the Software.
29  *
30  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
31  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
32  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
33  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
34  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
35  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
36  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
37  *
38  */
39 
40 #include <gecode/int/linear.hh>
41 
42 namespace Gecode { namespace Int { namespace Linear {
43 
45  inline IntRelType
46  inverse(const IntRelType r) {
47  switch (r) {
48  case IRT_EQ: return IRT_NQ; break;
49  case IRT_NQ: return IRT_EQ; break;
50  case IRT_GQ: return IRT_LE; break;
51  case IRT_LQ: return IRT_GR; break;
52  case IRT_LE: return IRT_GQ; break;
53  case IRT_GR: return IRT_LQ; break;
54  default: GECODE_NEVER;
55  }
56  throw UnknownRelation("Int::linear");
57  }
58 
60  inline void
61  eliminate(Term<BoolView>* t, int &n, double& d) {
62  for (int i=n; i--; )
63  if (t[i].x.one()) {
64  d -= t[i].a; t[i]=t[--n];
65  } else if (t[i].x.zero()) {
66  t[i]=t[--n];
67  }
68 
69  Limits::check(d,"Int::linear");
70  }
71 
73  inline void
74  rewrite(IntRelType &r, double &d) {
75  switch (r) {
76  case IRT_EQ: case IRT_NQ: case IRT_LQ: case IRT_GQ:
77  break;
78  case IRT_LE:
79  d--; r = IRT_LQ; break;
80  case IRT_GR:
81  d++; r = IRT_GQ; break;
82  default:
83  throw UnknownRelation("Int::linear");
84  }
85  }
86 
87  void
89  Term<BoolView>* t_p, int n_p,
90  IntRelType r, IntView y, int c) {
91  switch (r) {
92  case IRT_EQ:
93  {
94  ViewArray<BoolView> x(home,n_p);
95  for (int i=n_p; i--; )
96  x[i]=t_p[i].x;
98  ::post(home,x,y,c)));
99  }
100  break;
101  case IRT_NQ:
102  {
103  ViewArray<BoolView> x(home,n_p);
104  for (int i=n_p; i--; )
105  x[i]=t_p[i].x;
107  ::post(home,x,y,c)));
108  }
109  break;
110  case IRT_GQ:
111  {
112  ViewArray<BoolView> x(home,n_p);
113  for (int i=n_p; i--; )
114  x[i]=t_p[i].x;
116  ::post(home,x,y,c)));
117  }
118  break;
119  case IRT_LQ:
120  {
121  ViewArray<NegBoolView> x(home,n_p);
122  for (int i=n_p; i--; )
123  x[i]=NegBoolView(t_p[i].x);
124  MinusView z(y);
126  ::post(home,x,z,n_p-c)));
127  }
128  break;
129  default: GECODE_NEVER;
130  }
131  }
132 
133  void
135  Term<BoolView>* t_p, int n_p,
136  IntRelType r, ZeroIntView, int c) {
137  switch (r) {
138  case IRT_EQ:
139  {
140  ViewArray<BoolView> x(home,n_p);
141  for (int i=n_p; i--; )
142  x[i]=t_p[i].x;
144  }
145  break;
146  case IRT_NQ:
147  {
148  ViewArray<BoolView> x(home,n_p);
149  for (int i=n_p; i--; )
150  x[i]=t_p[i].x;
152  }
153  break;
154  case IRT_GQ:
155  {
156  ViewArray<BoolView> x(home,n_p);
157  for (int i=n_p; i--; )
158  x[i]=t_p[i].x;
160  }
161  break;
162  case IRT_LQ:
163  {
164  ViewArray<NegBoolView> x(home,n_p);
165  for (int i=n_p; i--; )
166  x[i]=NegBoolView(t_p[i].x);
168  }
169  break;
170  default: GECODE_NEVER;
171  }
172  }
173 
174  void
176  Term<BoolView>* t_p, int n_p,
177  IntRelType r, int c, BoolView b,
178  IntConLevel) {
179  switch (r) {
180  case IRT_EQ:
181  {
182  ViewArray<BoolView> x(home,n_p);
183  for (int i=n_p; i--; )
184  x[i]=t_p[i].x;
186  }
187  break;
188  case IRT_NQ:
189  {
190  ViewArray<BoolView> x(home,n_p);
191  for (int i=n_p; i--; )
192  x[i]=t_p[i].x;
193  NegBoolView nb(b);
195  }
196  break;
197  case IRT_GQ:
198  {
199  ViewArray<BoolView> x(home,n_p);
200  for (int i=n_p; i--; )
201  x[i]=t_p[i].x;
203  }
204  break;
205  case IRT_LQ:
206  {
207  ViewArray<NegBoolView> x(home,n_p);
208  for (int i=n_p; i--; )
209  x[i]=NegBoolView(t_p[i].x);
211  }
212  break;
213  default: GECODE_NEVER;
214  }
215  }
216 
217  void
219  Term<BoolView>* t_n, int n_n,
220  IntRelType r, IntView y, int c) {
221  switch (r) {
222  case IRT_EQ:
223  {
224  ViewArray<BoolView> x(home,n_n);
225  for (int i=n_n; i--; )
226  x[i]=t_n[i].x;
227  MinusView z(y);
229  ::post(home,x,z,-c)));
230  }
231  break;
232  case IRT_NQ:
233  {
234  ViewArray<BoolView> x(home,n_n);
235  for (int i=n_n; i--; )
236  x[i]=t_n[i].x;
237  MinusView z(y);
239  ::post(home,x,z,-c)));
240  }
241  break;
242  case IRT_GQ:
243  {
244  ViewArray<NegBoolView> x(home,n_n);
245  for (int i=n_n; i--; )
246  x[i]=NegBoolView(t_n[i].x);
248  ::post(home,x,y,n_n+c)));
249  }
250  break;
251  case IRT_LQ:
252  {
253  ViewArray<BoolView> x(home,n_n);
254  for (int i=n_n; i--; )
255  x[i]=t_n[i].x;
256  MinusView z(y);
258  ::post(home,x,z,-c)));
259  }
260  break;
261  default: GECODE_NEVER;
262  }
263  }
264 
265  void
267  Term<BoolView>* t_n, int n_n,
268  IntRelType r, ZeroIntView, int c) {
269  switch (r) {
270  case IRT_EQ:
271  {
272  ViewArray<BoolView> x(home,n_n);
273  for (int i=n_n; i--; )
274  x[i]=t_n[i].x;
276  }
277  break;
278  case IRT_NQ:
279  {
280  ViewArray<BoolView> x(home,n_n);
281  for (int i=n_n; i--; )
282  x[i]=t_n[i].x;
284  }
285  break;
286  case IRT_GQ:
287  {
288  ViewArray<NegBoolView> x(home,n_n);
289  for (int i=n_n; i--; )
290  x[i]=NegBoolView(t_n[i].x);
292  }
293  break;
294  case IRT_LQ:
295  {
296  ViewArray<BoolView> x(home,n_n);
297  for (int i=n_n; i--; )
298  x[i]=t_n[i].x;
300  }
301  break;
302  default: GECODE_NEVER;
303  }
304  }
305 
306  void
308  Term<BoolView>* t_n, int n_n,
309  IntRelType r, int c, BoolView b,
310  IntConLevel) {
311  switch (r) {
312  case IRT_EQ:
313  {
314  ViewArray<BoolView> x(home,n_n);
315  for (int i=n_n; i--; )
316  x[i]=t_n[i].x;
318  }
319  break;
320  case IRT_NQ:
321  {
322  ViewArray<BoolView> x(home,n_n);
323  for (int i=n_n; i--; )
324  x[i]=t_n[i].x;
325  NegBoolView nb(b);
327  }
328  break;
329  case IRT_GQ:
330  {
331  ViewArray<NegBoolView> x(home,n_n);
332  for (int i=n_n; i--; )
333  x[i]=NegBoolView(t_n[i].x);
335  }
336  break;
337  case IRT_LQ:
338  {
339  ViewArray<BoolView> x(home,n_n);
340  for (int i=n_n; i--; )
341  x[i]=t_n[i].x;
343  }
344  break;
345  default: GECODE_NEVER;
346  }
347  }
348 
349  void
351  Term<BoolView>* t_p, int n_p,
352  Term<BoolView>* t_n, int n_n,
353  IntRelType r, IntView y, int c) {
354  ScaleBoolArray b_p(home,n_p);
355  {
356  ScaleBool* f=b_p.fst();
357  for (int i=n_p; i--; ) {
358  f[i].x=t_p[i].x; f[i].a=t_p[i].a;
359  }
360  }
361  ScaleBoolArray b_n(home,n_n);
362  {
363  ScaleBool* f=b_n.fst();
364  for (int i=n_n; i--; ) {
365  f[i].x=t_n[i].x; f[i].a=t_n[i].a;
366  }
367  }
368  switch (r) {
369  case IRT_EQ:
372  ::post(home,b_p,b_n,y,c)));
373  break;
374  case IRT_NQ:
377  ::post(home,b_p,b_n,y,c)));
378  break;
379  case IRT_LQ:
382  ::post(home,b_p,b_n,y,c)));
383  break;
384  case IRT_GQ:
385  {
386  MinusView m(y);
389  ::post(home,b_n,b_p,m,-c)));
390  }
391  break;
392  default:
393  GECODE_NEVER;
394  }
395  }
396 
397 
398  void
400  Term<BoolView>* t_p, int n_p,
401  Term<BoolView>* t_n, int n_n,
402  IntRelType r, ZeroIntView y, int c) {
403  ScaleBoolArray b_p(home,n_p);
404  {
405  ScaleBool* f=b_p.fst();
406  for (int i=n_p; i--; ) {
407  f[i].x=t_p[i].x; f[i].a=t_p[i].a;
408  }
409  }
410  ScaleBoolArray b_n(home,n_n);
411  {
412  ScaleBool* f=b_n.fst();
413  for (int i=n_n; i--; ) {
414  f[i].x=t_n[i].x; f[i].a=t_n[i].a;
415  }
416  }
417  switch (r) {
418  case IRT_EQ:
421  ::post(home,b_p,b_n,y,c)));
422  break;
423  case IRT_NQ:
426  ::post(home,b_p,b_n,y,c)));
427  break;
428  case IRT_LQ:
431  ::post(home,b_p,b_n,y,c)));
432  break;
433  case IRT_GQ:
436  ::post(home,b_n,b_p,y,-c)));
437  break;
438  default:
439  GECODE_NEVER;
440  }
441  }
442 
443  template<class View>
444  forceinline void
446  Term<BoolView>* t, int n,
447  IntRelType r, View x, int c) {
448 
449  Limits::check(c,"Int::linear");
450 
451  double d = c;
452 
453  eliminate(t,n,d);
454 
455  rewrite(r,d);
456 
457  c = static_cast<int>(d);
458 
459  Term<BoolView> *t_p, *t_n;
460  int n_p, n_n;
461  bool unit = normalize<BoolView>(t,n,t_p,n_p,t_n,n_n);
462 
463  if (n == 0) {
464  switch (r) {
465  case IRT_EQ: GECODE_ME_FAIL(x.eq(home,-c)); break;
466  case IRT_NQ: GECODE_ME_FAIL(x.nq(home,-c)); break;
467  case IRT_GQ: GECODE_ME_FAIL(x.lq(home,-c)); break;
468  case IRT_LQ: GECODE_ME_FAIL(x.gq(home,-c)); break;
469  default: GECODE_NEVER;
470  }
471  return;
472  }
473 
474  // Check for overflow
475  {
476  double sl = x.max()+c;
477  double su = x.min()+c;
478  for (int i=n_p; i--; )
479  su -= t_p[i].a;
480  for (int i=n_n; i--; )
481  sl += t_n[i].a;
482  Limits::check(sl,"Int::linear");
483  Limits::check(su,"Int::linear");
484  }
485 
486  if (unit && (n_n == 0)) {
488  post_pos_unit(home,t_p,n_p,r,x,c);
489  } else if (unit && (n_p == 0)) {
490  // All coefficients are -1
491  post_neg_unit(home,t_n,n_n,r,x,c);
492  } else {
493  // Mixed coefficients
494  post_mixed(home,t_p,n_p,t_n,n_n,r,x,c);
495  }
496  }
497 
498 
499  void
500  post(Home home,
501  Term<BoolView>* t, int n, IntRelType r, IntView x, int c,
502  IntConLevel) {
503  post_all(home,t,n,r,x,c);
504  }
505 
506  void
507  post(Home home,
508  Term<BoolView>* t, int n, IntRelType r, int c,
509  IntConLevel) {
510  ZeroIntView x;
511  post_all(home,t,n,r,x,c);
512  }
513 
514  void
515  post(Home home,
516  Term<BoolView>* t, int n, IntRelType r, IntView x, BoolView b,
517  IntConLevel icl) {
518  int l, u;
519  estimate(t,n,0,l,u);
520  IntVar z(home,l,u); IntView zv(z);
521  post_all(home,t,n,IRT_EQ,zv,0);
522  rel(home,z,r,x,b,icl);
523  }
524 
525  void
526  post(Home home,
527  Term<BoolView>* t, int n, IntRelType r, int c, BoolView b,
528  IntConLevel icl) {
529 
530  if (b.one())
531  return post(home,t,n,r,c,icl);
532  if (b.zero())
533  return post(home,t,n,inverse(r),c,icl);
534 
535  Limits::check(c,"Int::linear");
536 
537  double d = c;
538 
539  eliminate(t,n,d);
540 
541  rewrite(r,d);
542 
543  c = static_cast<int>(d);
544 
545  if (n == 0) {
546  bool fail = false;
547  switch (r) {
548  case IRT_EQ: fail = (0 != c); break;
549  case IRT_NQ: fail = (0 == c); break;
550  case IRT_GQ: fail = (0 < c); break;
551  case IRT_LQ: fail = (0 > c); break;
552  default: GECODE_NEVER;
553  }
554  if ((fail ? b.zero(home) : b.one(home)) == ME_INT_FAILED)
555  home.fail();
556  return;
557  }
558 
559  Term<BoolView> *t_p, *t_n;
560  int n_p, n_n;
561  bool unit = normalize<BoolView>(t,n,t_p,n_p,t_n,n_n);
562 
563  // Check for overflow
564  {
565  double sl = c;
566  double su = c;
567  for (int i=n_p; i--; )
568  su -= t_p[i].a;
569  for (int i=n_n; i--; )
570  sl += t_n[i].a;
571  Limits::check(sl,"Int::linear");
572  Limits::check(su,"Int::linear");
573  }
574 
575  if (unit && (n_n == 0)) {
577  post_pos_unit(home,t_p,n_p,r,c,b,icl);
578  } else if (unit && (n_p == 0)) {
579  // All coefficients are -1
580  post_neg_unit(home,t_n,n_n,r,c,b,icl);
581  } else {
582  // Mixed coefficients
583  /*
584  * Denormalize: Make all t_n coefficients negative again
585  * (t_p and t_n are shared in t)
586  */
587  for (int i=n_n; i--; )
588  t_n[i].a = -t_n[i].a;
589 
590  // Note: still slow implementation
591  int l, u;
592  estimate(t,n,0,l,u);
593  IntVar z(home,l,u); IntView zv(z);
594  post_all(home,t,n,IRT_EQ,zv,0);
595  rel(home,z,r,c,b,icl);
596  }
597  }
598 
599 }}}
600 
601 // STATISTICS: int-post
602