Generated on Thu Apr 5 2018 19:44:19 for Gecode by doxygen 1.8.13
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$ 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 <algorithm>
39 
40 #include <gecode/int/rel.hh>
41 #include <gecode/int/linear.hh>
42 #include <gecode/int/div.hh>
43 
44 namespace Gecode { namespace Int { namespace Linear {
45 
47  forceinline void
48  eliminate(Term<IntView>* t, int &n, long long int& d) {
49  for (int i=n; i--; )
50  if (t[i].x.assigned()) {
51  long long int ax = t[i].a * static_cast<long long int>(t[i].x.val());
52  if (Limits::overflow_sub(d,ax))
53  throw OutOfLimits("Int::linear");
54  d=d-ax; t[i]=t[--n];
55  }
56  }
57 
59  forceinline void
60  rewrite(IntRelType &irt, long long int &d,
61  Term<IntView>* &t_p, int &n_p,
62  Term<IntView>* &t_n, int &n_n) {
63  switch (irt) {
64  case IRT_EQ: case IRT_NQ: case IRT_LQ:
65  break;
66  case IRT_LE:
67  d--; irt = IRT_LQ;
68  break;
69  case IRT_GR:
70  d++;
71  /* fall through */
72  case IRT_GQ:
73  irt = IRT_LQ;
74  std::swap(n_p,n_n); std::swap(t_p,t_n); d = -d;
75  break;
76  default:
77  throw UnknownRelation("Int::linear");
78  }
79  }
80 
82  forceinline bool
83  precision(Term<IntView>* t_p, int n_p,
84  Term<IntView>* t_n, int n_n,
85  long long int d) {
86  long long int sl = 0;
87  long long int su = 0;
88 
89  for (int i = n_p; i--; ) {
90  long long int axmin =
91  t_p[i].a * static_cast<long long int>(t_p[i].x.min());
92  if (Limits::overflow_add(sl,axmin))
93  throw OutOfLimits("Int::linear");
94  sl = sl + axmin;
95  long long int axmax =
96  t_p[i].a * static_cast<long long int>(t_p[i].x.max());
97  if (Limits::overflow_add(sl,axmax))
98  throw OutOfLimits("Int::linear");
99  su = su + axmax;
100  }
101  for (int i = n_n; i--; ) {
102  long long int axmax =
103  t_n[i].a * static_cast<long long int>(t_n[i].x.max());
104  if (Limits::overflow_sub(sl,axmax))
105  throw OutOfLimits("Int::linear");
106  sl = sl - axmax;
107  long long int axmin =
108  t_n[i].a * static_cast<long long int>(t_n[i].x.min());
109  if (Limits::overflow_sub(su,axmin))
110  throw OutOfLimits("Int::linear");
111  su = su - axmin;
112  }
113 
114  bool is_ip = (sl >= Limits::min) && (su <= Limits::max);
115 
116  if (Limits::overflow_sub(sl,d))
117  throw OutOfLimits("Int::linear");
118  sl = sl - d;
119  if (Limits::overflow_sub(su,d))
120  throw OutOfLimits("Int::linear");
121  su = su - d;
122 
123  is_ip = is_ip && (sl >= Limits::min) && (su <= Limits::max);
124 
125  for (int i = n_p; i--; ) {
126  long long int axmin =
127  t_p[i].a * static_cast<long long int>(t_p[i].x.min());
128  if (Limits::overflow_sub(sl,axmin))
129  throw OutOfLimits("Int::linear");
130  if (sl - axmin < Limits::min)
131  is_ip = false;
132  long long int axmax =
133  t_p[i].a * static_cast<long long int>(t_p[i].x.max());
134  if (Limits::overflow_sub(su,axmax))
135  throw OutOfLimits("Int::linear");
136  if (su - axmax > Limits::max)
137  is_ip = false;
138  }
139  for (int i = n_n; i--; ) {
140  long long int axmin =
141  t_n[i].a * static_cast<long long int>(t_n[i].x.min());
142  if (Limits::overflow_add(sl,axmin))
143  throw OutOfLimits("Int::linear");
144  if (sl + axmin < Limits::min)
145  is_ip = false;
146  long long int axmax =
147  t_n[i].a * static_cast<long long int>(t_n[i].x.max());
148  if (Limits::overflow_add(su,axmax))
149  throw OutOfLimits("Int::linear");
150  if (su + axmax > Limits::max)
151  is_ip = false;
152  }
153  return is_ip;
154  }
155 
160  template<class Val, class View>
161  forceinline void
164  switch (irt) {
165  case IRT_EQ:
167  break;
168  case IRT_NQ:
170  break;
171  case IRT_LQ:
173  break;
174  default: GECODE_NEVER;
175  }
176  }
177 
178 
180 #define GECODE_INT_PL_BIN(CLASS) \
181  switch (n_p) { \
182  case 2: \
183  GECODE_ES_FAIL((CLASS<int,IntView,IntView>::post \
184  (home,t_p[0].x,t_p[1].x,c))); \
185  break; \
186  case 1: \
187  GECODE_ES_FAIL((CLASS<int,IntView,MinusView>::post \
188  (home,t_p[0].x,MinusView(t_n[0].x),c))); \
189  break; \
190  case 0: \
191  GECODE_ES_FAIL((CLASS<int,MinusView,MinusView>::post \
192  (home,MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
193  break; \
194  default: GECODE_NEVER; \
195  }
196 
198 #define GECODE_INT_PL_TER(CLASS) \
199  switch (n_p) { \
200  case 3: \
201  GECODE_ES_FAIL((CLASS<int,IntView,IntView,IntView>::post \
202  (home,t_p[0].x,t_p[1].x,t_p[2].x,c))); \
203  break; \
204  case 2: \
205  GECODE_ES_FAIL((CLASS<int,IntView,IntView,MinusView>::post \
206  (home,t_p[0].x,t_p[1].x, \
207  MinusView(t_n[0].x),c))); \
208  break; \
209  case 1: \
210  GECODE_ES_FAIL((CLASS<int,IntView,MinusView,MinusView>::post \
211  (home,t_p[0].x, \
212  MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
213  break; \
214  case 0: \
215  GECODE_ES_FAIL((CLASS<int,MinusView,MinusView,MinusView>::post \
216  (home,MinusView(t_n[0].x), \
217  MinusView(t_n[1].x),MinusView(t_n[2].x),c))); \
218  break; \
219  default: GECODE_NEVER; \
220  }
221 
222  void
223  post(Home home, Term<IntView>* t, int n, IntRelType irt, int c,
224  IntPropLevel ipl) {
225 
226  Limits::check(c,"Int::linear");
227 
228  long long int d = c;
229 
230  eliminate(t,n,d);
231 
232  Term<IntView> *t_p, *t_n;
233  int n_p, n_n, gcd=1;
234  bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n,gcd);
235 
236  rewrite(irt,d,t_p,n_p,t_n,n_n);
237 
238  // Divide by gcd
239  if (gcd > 1) {
240  switch (irt) {
241  case IRT_EQ:
242  if ((d % gcd) != 0) {
243  home.fail();
244  return;
245  }
246  d /= gcd;
247  break;
248  case IRT_NQ:
249  if ((d % gcd) != 0)
250  return;
251  d /= gcd;
252  break;
253  case IRT_LQ:
254  d = floor_div_xp(d,static_cast<long long int>(gcd));
255  break;
256  default: GECODE_NEVER;
257  }
258  }
259 
260  if (n == 0) {
261  switch (irt) {
262  case IRT_EQ: if (d != 0) home.fail(); break;
263  case IRT_NQ: if (d == 0) home.fail(); break;
264  case IRT_LQ: if (d < 0) home.fail(); break;
265  default: GECODE_NEVER;
266  }
267  return;
268  }
269 
270  if (n == 1) {
271  if (n_p == 1) {
272  LLongScaleView y(t_p[0].a,t_p[0].x);
273  switch (irt) {
274  case IRT_EQ: GECODE_ME_FAIL(y.eq(home,d)); break;
275  case IRT_NQ: GECODE_ME_FAIL(y.nq(home,d)); break;
276  case IRT_LQ: GECODE_ME_FAIL(y.lq(home,d)); break;
277  default: GECODE_NEVER;
278  }
279  } else {
280  LLongScaleView y(t_n[0].a,t_n[0].x);
281  switch (irt) {
282  case IRT_EQ: GECODE_ME_FAIL(y.eq(home,-d)); break;
283  case IRT_NQ: GECODE_ME_FAIL(y.nq(home,-d)); break;
284  case IRT_LQ: GECODE_ME_FAIL(y.gq(home,-d)); break;
285  default: GECODE_NEVER;
286  }
287  }
288  return;
289  }
290 
291  // Check this special case here, as there can be no overflow
292  if ((n == 2) && is_unit &&
293  ((vbd(ipl) == IPL_DOM) || (vbd(ipl) == IPL_DEF)) &&
294  (irt == IRT_EQ) && (d == 0)) {
295  switch (n_p) {
296  case 2: {
297  IntView x(t_p[0].x);
298  MinusView y(t_p[1].x);
300  break;
301  }
302  case 1: {
303  IntView x(t_p[0].x);
304  IntView y(t_n[0].x);
306  break;
307  }
308  case 0: {
309  IntView x(t_n[0].x);
310  MinusView y(t_n[1].x);
312  break;
313  }
314  default:
315  GECODE_NEVER;
316  }
317  return;
318  }
319 
320  bool is_ip = precision(t_p,n_p,t_n,n_n,d);
321 
322  if (is_unit && is_ip &&
323  (vbd(ipl) != IPL_DOM) && (vbd(ipl) != IPL_DEF)) {
324  // Unit coefficients with integer precision
325  c = static_cast<int>(d);
326  if (n == 2) {
327  switch (irt) {
328  case IRT_EQ: GECODE_INT_PL_BIN(EqBin); break;
329  case IRT_NQ: GECODE_INT_PL_BIN(NqBin); break;
330  case IRT_LQ: GECODE_INT_PL_BIN(LqBin); break;
331  default: GECODE_NEVER;
332  }
333  } else if (n == 3) {
334  switch (irt) {
335  case IRT_EQ: GECODE_INT_PL_TER(EqTer); break;
336  case IRT_NQ: GECODE_INT_PL_TER(NqTer); break;
337  case IRT_LQ: GECODE_INT_PL_TER(LqTer); break;
338  default: GECODE_NEVER;
339  }
340  } else {
341  ViewArray<IntView> x(home,n_p);
342  for (int i = n_p; i--; )
343  x[i] = t_p[i].x;
344  ViewArray<IntView> y(home,n_n);
345  for (int i = n_n; i--; )
346  y[i] = t_n[i].x;
347  post_nary<int,IntView>(home,x,y,irt,c);
348  }
349  } else if (is_ip) {
350  if ((n==2) && is_unit &&
351  ((vbd(ipl) == IPL_DOM) || (vbd(ipl) == IPL_DEF)) &&
352  (irt == IRT_EQ)) {
353  // Binary domain-consistent equality
354  c = static_cast<int>(d);
355  assert(c != 0);
356  switch (n_p) {
357  case 2: {
358  MinusView x(t_p[0].x);
359  OffsetView y(t_p[1].x, -c);
361  break;
362  }
363  case 1: {
364  IntView x(t_p[0].x);
365  OffsetView y(t_n[0].x, c);
367  break;
368  }
369  case 0: {
370  MinusView x(t_n[0].x);
371  OffsetView y(t_n[1].x, c);
373  break;
374  }
375  default:
376  GECODE_NEVER;
377  }
378  } else {
379  // Arbitrary coefficients with integer precision
380  c = static_cast<int>(d);
381  ViewArray<IntScaleView> x(home,n_p);
382  for (int i = n_p; i--; )
383  x[i] = IntScaleView(t_p[i].a,t_p[i].x);
384  ViewArray<IntScaleView> y(home,n_n);
385  for (int i = n_n; i--; )
386  y[i] = IntScaleView(t_n[i].a,t_n[i].x);
387  if ((vbd(ipl) == IPL_DOM) && (irt == IRT_EQ)) {
389  } else {
390  post_nary<int,IntScaleView>(home,x,y,irt,c);
391  }
392  }
393  } else {
394  // Arbitrary coefficients with long long precision
395  ViewArray<LLongScaleView> x(home,n_p);
396  for (int i = n_p; i--; )
397  x[i] = LLongScaleView(t_p[i].a,t_p[i].x);
398  ViewArray<LLongScaleView> y(home,n_n);
399  for (int i = n_n; i--; )
400  y[i] = LLongScaleView(t_n[i].a,t_n[i].x);
401  if ((vbd(ipl) == IPL_DOM) && (irt == IRT_EQ)) {
403  ::post(home,x,y,d)));
404  } else {
405  post_nary<long long int,LLongScaleView>(home,x,y,irt,d);
406  }
407  }
408  }
409 
410 #undef GECODE_INT_PL_BIN
411 #undef GECODE_INT_PL_TER
412 
413 
418  template<class Val, class View>
419  forceinline void
422  IntRelType irt, Val c, Reify r) {
423  switch (irt) {
424  case IRT_EQ:
425  switch (r.mode()) {
426  case RM_EQV:
428  post(home,x,y,c,r.var())));
429  break;
430  case RM_IMP:
432  post(home,x,y,c,r.var())));
433  break;
434  case RM_PMI:
436  post(home,x,y,c,r.var())));
437  break;
438  default: GECODE_NEVER;
439  }
440  break;
441  case IRT_NQ:
442  {
443  NegBoolView n(r.var());
444  switch (r.mode()) {
445  case RM_EQV:
447  post(home,x,y,c,n)));
448  break;
449  case RM_IMP:
451  post(home,x,y,c,n)));
452  break;
453  case RM_PMI:
455  post(home,x,y,c,n)));
456  break;
457  default: GECODE_NEVER;
458  }
459  }
460  break;
461  case IRT_LQ:
462  switch (r.mode()) {
463  case RM_EQV:
465  post(home,x,y,c,r.var())));
466  break;
467  case RM_IMP:
469  post(home,x,y,c,r.var())));
470  break;
471  case RM_PMI:
473  post(home,x,y,c,r.var())));
474  break;
475  default: GECODE_NEVER;
476  }
477  break;
478  default: GECODE_NEVER;
479  }
480  }
481 
482  template<class CtrlView>
483  forceinline void
484  posteqint(Home home, IntView& x, int c, CtrlView b, ReifyMode rm,
485  IntPropLevel ipl) {
486  if ((vbd(ipl) == IPL_DOM) || (vbd(ipl) == IPL_DEF)) {
487  switch (rm) {
488  case RM_EQV:
490  post(home,x,c,b)));
491  break;
492  case RM_IMP:
494  post(home,x,c,b)));
495  break;
496  case RM_PMI:
498  post(home,x,c,b)));
499  break;
500  default: GECODE_NEVER;
501  }
502  } else {
503  switch (rm) {
504  case RM_EQV:
506  post(home,x,c,b)));
507  break;
508  case RM_IMP:
510  post(home,x,c,b)));
511  break;
512  case RM_PMI:
514  post(home,x,c,b)));
515  break;
516  default: GECODE_NEVER;
517  }
518  }
519  }
520 
521  void
522  post(Home home,
523  Term<IntView>* t, int n, IntRelType irt, int c, Reify r,
524  IntPropLevel ipl) {
525  Limits::check(c,"Int::linear");
526  long long int d = c;
527 
528  eliminate(t,n,d);
529 
530  Term<IntView> *t_p, *t_n;
531  int n_p, n_n, gcd=1;
532  bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n,gcd);
533 
534  rewrite(irt,d,t_p,n_p,t_n,n_n);
535 
536  // Divide by gcd
537  if (gcd > 1) {
538  switch (irt) {
539  case IRT_EQ:
540  if ((d % gcd) != 0) {
541  if (r.mode() != RM_PMI)
542  GECODE_ME_FAIL(BoolView(r.var()).zero(home));
543  return;
544  }
545  d /= gcd;
546  break;
547  case IRT_NQ:
548  if ((d % gcd) != 0) {
549  if (r.mode() != RM_IMP)
550  GECODE_ME_FAIL(BoolView(r.var()).one(home));
551  return;
552  }
553  d /= gcd;
554  break;
555  case IRT_LQ:
556  d = floor_div_xp(d,static_cast<long long int>(gcd));
557  break;
558  default: GECODE_NEVER;
559  }
560  }
561 
562  if (n == 0) {
563  bool fail = false;
564  switch (irt) {
565  case IRT_EQ: fail = (d != 0); break;
566  case IRT_NQ: fail = (d == 0); break;
567  case IRT_LQ: fail = (0 > d); break;
568  default: GECODE_NEVER;
569  }
570  if (fail) {
571  if (r.mode() != RM_PMI)
572  GECODE_ME_FAIL(BoolView(r.var()).zero(home));
573  } else {
574  if (r.mode() != RM_IMP)
575  GECODE_ME_FAIL(BoolView(r.var()).one(home));
576  }
577  return;
578  }
579 
580  bool is_ip = precision(t_p,n_p,t_n,n_n,d);
581 
582  if (is_unit && is_ip) {
583  c = static_cast<int>(d);
584  if (n == 1) {
585  switch (irt) {
586  case IRT_EQ:
587  if (n_p == 1) {
588  posteqint<BoolView>(home,t_p[0].x,c,r.var(),r.mode(),ipl);
589  } else {
590  posteqint<BoolView>(home,t_p[0].x,-c,r.var(),r.mode(),ipl);
591  }
592  break;
593  case IRT_NQ:
594  {
595  NegBoolView nb(r.var());
596  ReifyMode rm = r.mode();
597  switch (rm) {
598  case RM_IMP: rm = RM_PMI; break;
599  case RM_PMI: rm = RM_IMP; break;
600  default: ;
601  }
602  if (n_p == 1) {
603  posteqint<NegBoolView>(home,t_p[0].x,c,nb,rm,ipl);
604  } else {
605  posteqint<NegBoolView>(home,t_p[0].x,-c,nb,rm,ipl);
606  }
607  }
608  break;
609  case IRT_LQ:
610  if (n_p == 1) {
611  switch (r.mode()) {
612  case RM_EQV:
614  post(home,t_p[0].x,c,r.var())));
615  break;
616  case RM_IMP:
618  post(home,t_p[0].x,c,r.var())));
619  break;
620  case RM_PMI:
622  post(home,t_p[0].x,c,r.var())));
623  break;
624  default: GECODE_NEVER;
625  }
626  } else {
627  NegBoolView nb(r.var());
628  switch (r.mode()) {
629  case RM_EQV:
631  post(home,t_n[0].x,-c-1,nb)));
632  break;
633  case RM_IMP:
635  post(home,t_n[0].x,-c-1,nb)));
636  break;
637  case RM_PMI:
639  post(home,t_n[0].x,-c-1,nb)));
640  break;
641  default: GECODE_NEVER;
642  }
643  }
644  break;
645  default: GECODE_NEVER;
646  }
647  } else if (n == 2) {
648  switch (irt) {
649  case IRT_EQ:
650  switch (n_p) {
651  case 2:
652  switch (r.mode()) {
653  case RM_EQV:
655  post(home,t_p[0].x,t_p[1].x,c,r.var())));
656  break;
657  case RM_IMP:
659  post(home,t_p[0].x,t_p[1].x,c,r.var())));
660  break;
661  case RM_PMI:
663  post(home,t_p[0].x,t_p[1].x,c,r.var())));
664  break;
665  default: GECODE_NEVER;
666  }
667  break;
668  case 1:
669  switch (r.mode()) {
670  case RM_EQV:
672  post(home,t_p[0].x,MinusView(t_n[0].x),c,
673  r.var())));
674  break;
675  case RM_IMP:
677  post(home,t_p[0].x,MinusView(t_n[0].x),c,
678  r.var())));
679  break;
680  case RM_PMI:
682  post(home,t_p[0].x,MinusView(t_n[0].x),c,
683  r.var())));
684  break;
685  default: GECODE_NEVER;
686  }
687  break;
688  case 0:
689  switch (r.mode()) {
690  case RM_EQV:
692  post(home,t_n[0].x,t_n[1].x,-c,r.var())));
693  break;
694  case RM_IMP:
696  post(home,t_n[0].x,t_n[1].x,-c,r.var())));
697  break;
698  case RM_PMI:
700  post(home,t_n[0].x,t_n[1].x,-c,r.var())));
701  break;
702  default: GECODE_NEVER;
703  }
704  break;
705  default: GECODE_NEVER;
706  }
707  break;
708  case IRT_NQ:
709  {
710  NegBoolView nb(r.var());
711  switch (n_p) {
712  case 2:
713  switch (r.mode()) {
714  case RM_EQV:
716  post(home,t_p[0].x,t_p[1].x,c,nb)));
717  break;
718  case RM_IMP:
720  post(home,t_p[0].x,t_p[1].x,c,nb)));
721  break;
722  case RM_PMI:
724  post(home,t_p[0].x,t_p[1].x,c,nb)));
725  break;
726  default: GECODE_NEVER;
727  }
728  break;
729  case 1:
730  switch (r.mode()) {
731  case RM_EQV:
733  post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
734  break;
735  case RM_IMP:
737  post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
738  break;
739  case RM_PMI:
741  post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
742  break;
743  default: GECODE_NEVER;
744  }
745  break;
746  case 0:
747  switch (r.mode()) {
748  case RM_EQV:
750  post(home,t_p[0].x,t_p[1].x,-c,nb)));
751  break;
752  case RM_IMP:
754  post(home,t_p[0].x,t_p[1].x,-c,nb)));
755  break;
756  case RM_PMI:
758  post(home,t_p[0].x,t_p[1].x,-c,nb)));
759  break;
760  default: GECODE_NEVER;
761  }
762  break;
763  default: GECODE_NEVER;
764  }
765  }
766  break;
767  case IRT_LQ:
768  switch (n_p) {
769  case 2:
770  switch (r.mode()) {
771  case RM_EQV:
773  post(home,t_p[0].x,t_p[1].x,c,r.var())));
774  break;
775  case RM_IMP:
777  post(home,t_p[0].x,t_p[1].x,c,r.var())));
778  break;
779  case RM_PMI:
781  post(home,t_p[0].x,t_p[1].x,c,r.var())));
782  break;
783  default: GECODE_NEVER;
784  }
785  break;
786  case 1:
787  switch (r.mode()) {
788  case RM_EQV:
790  post(home,t_p[0].x,MinusView(t_n[0].x),c,
791  r.var())));
792  break;
793  case RM_IMP:
795  post(home,t_p[0].x,MinusView(t_n[0].x),c,
796  r.var())));
797  break;
798  case RM_PMI:
800  post(home,t_p[0].x,MinusView(t_n[0].x),c,
801  r.var())));
802  break;
803  default: GECODE_NEVER;
804  }
805  break;
806  case 0:
807  switch (r.mode()) {
808  case RM_EQV:
810  post(home,MinusView(t_n[0].x),
811  MinusView(t_n[1].x),c,r.var())));
812  break;
813  case RM_IMP:
815  post(home,MinusView(t_n[0].x),
816  MinusView(t_n[1].x),c,r.var())));
817  break;
818  case RM_PMI:
820  post(home,MinusView(t_n[0].x),
821  MinusView(t_n[1].x),c,r.var())));
822  break;
823  default: GECODE_NEVER;
824  }
825  break;
826  default: GECODE_NEVER;
827  }
828  break;
829  default: GECODE_NEVER;
830  }
831  } else {
832  ViewArray<IntView> x(home,n_p);
833  for (int i = n_p; i--; )
834  x[i] = t_p[i].x;
835  ViewArray<IntView> y(home,n_n);
836  for (int i = n_n; i--; )
837  y[i] = t_n[i].x;
838  post_nary<int,IntView>(home,x,y,irt,c,r);
839  }
840  } else if (is_ip) {
841  // Arbitrary coefficients with integer precision
842  c = static_cast<int>(d);
843  ViewArray<IntScaleView> x(home,n_p);
844  for (int i = n_p; i--; )
845  x[i] = IntScaleView(t_p[i].a,t_p[i].x);
846  ViewArray<IntScaleView> y(home,n_n);
847  for (int i = n_n; i--; )
848  y[i] = IntScaleView(t_n[i].a,t_n[i].x);
849  post_nary<int,IntScaleView>(home,x,y,irt,c,r);
850  } else {
851  // Arbitrary coefficients with long long precision
852  ViewArray<LLongScaleView> x(home,n_p);
853  for (int i = n_p; i--; )
854  x[i] = LLongScaleView(t_p[i].a,t_p[i].x);
855  ViewArray<LLongScaleView> y(home,n_n);
856  for (int i = n_n; i--; )
857  y[i] = LLongScaleView(t_n[i].a,t_n[i].x);
858  post_nary<long long int,LLongScaleView>(home,x,y,irt,d,r);
859  }
860  }
861 
862 }}}
863 
864 // STATISTICS: int-post
Scale integer view (template)
Definition: view.hpp:677
Propagator for bounds consistent binary linear disequality
Definition: linear.hh:205
IntPropLevel vbd(IntPropLevel ipl)
Extract value, bounds, or domain propagation from propagation level.
Definition: ipl.hpp:41
NodeType t
Type of node.
Definition: bool-expr.cpp:234
Propagator for bounds consistent n-ary linear equality
Definition: linear.hh:581
Inverse implication for reification.
Definition: int.hh:848
Exception: Value out of limits
Definition: exception.hpp:48
void eliminate(Term< BoolView > *t, int &n, long long int &d)
Eliminate assigned views.
Definition: bool-post.cpp:47
Binary domain consistent equality propagator.
Definition: rel.hh:71
Propagator for reified bounds consistent n-ary linear less or equal
Definition: linear.hh:753
ReifyMode mode(void) const
Return reification mode.
Definition: reify.hpp:60
Negated Boolean view.
Definition: view.hpp:1519
bool one(const Gecode::FloatValArgs &a)
Check whether has only one coefficients.
Definition: linear.cpp:50
int a
Coefficient.
Definition: linear.hh:1343
Propagator for bounds consistent n-ary linear disequality
Definition: linear.hh:687
Propagator for domain consistent n-ary linear equality
Definition: linear.hh:612
bool assigned(void) const
Test whether view is assigned.
Definition: var.hpp:123
Less or equal ( )
Definition: int.hh:907
Propagator for bounds consistent ternary linear equality
Definition: linear.hh:388
Reified less or equal with integer propagator.
Definition: rel.hh:583
Greater ( )
Definition: int.hh:910
#define forceinline
Definition: config.hpp:182
Propagator for bounds consistent binary linear equality
Definition: linear.hh:138
const int max
Largest allowed integer value.
Definition: int.hh:116
Greater or equal ( )
Definition: int.hh:909
const int min
Smallest allowed integer value.
Definition: int.hh:118
Gecode::IntSet d(v, 7)
Propagator for bounds consistent ternary linear less or equal
Definition: linear.hh:458
Gecode::FloatVal c(-8, 8)
Exception: Unknown relation passed as argument
Definition: exception.hpp:91
Gecode::IntArgs i(4, 1, 2, 3, 4)
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
Equality ( )
Definition: int.hh:905
IntRelType
Relation types for integers.
Definition: int.hh:904
int gcd(int a, int b)
Compute the greatest common divisor of a and b.
Definition: post.hpp:82
ModEvent lq(Space &home, Val n)
Restrict domain values to be less or equal than n.
Definition: scale.hpp:138
Simple propagation levels.
Definition: int.hh:955
Propagator for bounds consistent binary linear less or equal
Definition: linear.hh:241
bool precision(Term< IntView > *t_p, int n_p, Term< IntView > *t_n, int n_n, long long int d)
Decide the required precision and check for overflow.
Definition: int-post.cpp:83
Reification specification.
Definition: int.hh:855
void rewrite(IntRelType &r, long long int &d)
Rewrite non-strict relations.
Definition: bool-post.cpp:59
bool overflow_add(int n, int m)
Check whether adding n and m would overflow.
Definition: limits.hpp:83
IntType floor_div_xp(IntType x, IntType y)
Compute where y is non-negative.
Definition: div.hpp:79
Propagator for reified bounds consistent n-ary linear equality
Definition: linear.hh:653
Less ( )
Definition: int.hh:908
Offset integer view.
Definition: view.hpp:426
View arrays.
Definition: array.hpp:228
Propagator for reified bounds consistent binary linear less or equal
Definition: linear.hh:309
#define GECODE_INT_PL_BIN(CLASS)
Macro for posting binary special cases for linear constraints.
Definition: int-post.cpp:180
Post propagator for SetVar SetOpType SetVar SetRelType r
Definition: set.hh:769
Reified bounds consistent equality with integer propagator.
Definition: rel.hh:429
IntPropLevel
Propagation levels for integer propagators.
Definition: int.hh:953
struct Gecode::@585::NNF::@62::@63 b
For binary nodes (and, or, eqv)
Integer view for integer variables.
Definition: view.hpp:129
Post propagator for SetVar SetOpType SetVar y
Definition: set.hh:769
bool overflow_sub(int n, int m)
Check whether subtracting m from n would overflow.
Definition: limits.hpp:97
struct Gecode::@585::NNF::@62::@64 a
For atomic nodes.
ScaleView< int, unsigned int > IntScaleView
Integer-precision integer scale view.
Definition: view.hpp:767
Minus integer view.
Definition: view.hpp:278
#define GECODE_INT_PL_TER(CLASS)
Macro for posting ternary special cases for linear constraints.
Definition: int-post.cpp:198
Domain propagation Options: basic versus advanced propagation.
Definition: int.hh:958
Propagator for reified bounds consistent binary linear equality
Definition: linear.hh:172
BoolVar var(void) const
Return Boolean control variable.
Definition: reify.hpp:52
Post propagator for SetVar x
Definition: set.hh:769
#define GECODE_ME_FAIL(me)
Check whether modification event me is failed, and fail space home.
Definition: macros.hpp:81
void fail(void)
Mark space as failed.
Definition: core.hpp:3909
Class for describing linear term .
Definition: linear.hh:1340
void posteqint(Home home, IntView &x, int c, CtrlView b, ReifyMode rm, IntPropLevel ipl)
Definition: int-post.cpp:484
void post_nary(Home home, ViewArray< View > &x, ViewArray< View > &y, IntRelType irt, Val c)
Posting n-ary propagators.
Definition: int-post.cpp:162
Gecode toplevel namespace
Propagator for bounds consistent n-ary linear less or equal
Definition: linear.hh:720
Implication for reification.
Definition: int.hh:841
Disequality ( )
Definition: int.hh:906
void post(Home home, Term< BoolView > *t, int n, IntRelType irt, IntView x, int c, IntPropLevel)
Post propagator for linear constraint over Booleans.
Definition: bool-post.cpp:593
ScaleView< long long int, unsigned long long int > LLongScaleView
Long long-precision integer scale view.
Definition: view.hpp:773
Propagator for bounds consistent ternary linear disquality
Definition: linear.hh:423
ModEvent nq(Space &home, Val n)
Restrict domain values to be different from n.
Definition: scale.hpp:165
Reified domain consistent equality with integer propagator.
Definition: rel.hh:402
void check(int n, const char *l)
Check whether n is in range, otherwise throw out of limits with information l.
Definition: limits.hpp:50
Home class for posting propagators
Definition: core.hpp:846
#define GECODE_ES_FAIL(es)
Check whether execution status es is failed, and fail space home.
Definition: macros.hpp:107
ReifyMode
Mode for reification.
Definition: int.hh:827
#define GECODE_NEVER
Assert that this command is never executed.
Definition: macros.hpp:60
ModEvent eq(Space &home, Val n)
Restrict domain values to be equal to n.
Definition: scale.hpp:171
ModEvent gq(Space &home, Val n)
Restrict domain values to be greater or equal than n.
Definition: scale.hpp:152
Equivalence for reification (default)
Definition: int.hh:834
IntRelType swap(IntRelType irt)
Return swapped relation type of irt.
Definition: irt.hpp:41
Boolean view for Boolean variables.
Definition: view.hpp:1329