Generated on Mon Feb 8 2021 00:00:00 for Gecode by doxygen 1.8.20
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  * This file is part of Gecode, the generic constraint
10  * development environment:
11  * http://www.gecode.org
12  *
13  * Permission is hereby granted, free of charge, to any person obtaining
14  * a copy of this software and associated documentation files (the
15  * "Software"), to deal in the Software without restriction, including
16  * without limitation the rights to use, copy, modify, merge, publish,
17  * distribute, sublicense, and/or sell copies of the Software, and to
18  * permit persons to whom the Software is furnished to do so, subject to
19  * the following conditions:
20  *
21  * The above copyright notice and this permission notice shall be
22  * included in all copies or substantial portions of the Software.
23  *
24  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
25  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
26  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
27  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
28  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
29  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
30  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
31  *
32  */
33 
34 #include <algorithm>
35 
36 #include <gecode/int/rel.hh>
37 #include <gecode/int/linear.hh>
38 #include <gecode/int/div.hh>
39 
40 namespace Gecode { namespace Int { namespace Linear {
41 
43  forceinline void
44  eliminate(Term<IntView>* t, int &n, long long int& d) {
45  for (int i=n; i--; )
46  if (t[i].x.assigned()) {
47  long long int ax = t[i].a * static_cast<long long int>(t[i].x.val());
48  if (Limits::overflow_sub(d,ax))
49  throw OutOfLimits("Int::linear");
50  d=d-ax; t[i]=t[--n];
51  }
52  }
53 
55  forceinline void
56  rewrite(IntRelType &irt, long long int &d,
57  Term<IntView>* &t_p, int &n_p,
58  Term<IntView>* &t_n, int &n_n) {
59  switch (irt) {
60  case IRT_EQ: case IRT_NQ: case IRT_LQ:
61  break;
62  case IRT_LE:
63  d--; irt = IRT_LQ;
64  break;
65  case IRT_GR:
66  d++;
67  /* fall through */
68  case IRT_GQ:
69  irt = IRT_LQ;
70  std::swap(n_p,n_n); std::swap(t_p,t_n); d = -d;
71  break;
72  default:
73  throw UnknownRelation("Int::linear");
74  }
75  }
76 
78  forceinline bool
79  precision(Term<IntView>* t_p, int n_p,
80  Term<IntView>* t_n, int n_n,
81  long long int d) {
82  long long int sl = 0;
83  long long int su = 0;
84 
85  for (int i=0; i<n_p; i++) {
86  long long int axmin =
87  t_p[i].a * static_cast<long long int>(t_p[i].x.min());
88  if (Limits::overflow_add(sl,axmin))
89  throw OutOfLimits("Int::linear");
90  sl = sl + axmin;
91  long long int axmax =
92  t_p[i].a * static_cast<long long int>(t_p[i].x.max());
93  if (Limits::overflow_add(sl,axmax))
94  throw OutOfLimits("Int::linear");
95  su = su + axmax;
96  }
97  for (int i=0; i<n_n; i++) {
98  long long int axmax =
99  t_n[i].a * static_cast<long long int>(t_n[i].x.max());
100  if (Limits::overflow_sub(sl,axmax))
101  throw OutOfLimits("Int::linear");
102  sl = sl - axmax;
103  long long int axmin =
104  t_n[i].a * static_cast<long long int>(t_n[i].x.min());
105  if (Limits::overflow_sub(su,axmin))
106  throw OutOfLimits("Int::linear");
107  su = su - axmin;
108  }
109 
110  bool is_ip = (sl >= Limits::min) && (su <= Limits::max);
111 
112  if (Limits::overflow_sub(sl,d))
113  throw OutOfLimits("Int::linear");
114  sl = sl - d;
115  if (Limits::overflow_sub(su,d))
116  throw OutOfLimits("Int::linear");
117  su = su - d;
118 
119  is_ip = is_ip && (sl >= Limits::min) && (su <= Limits::max);
120 
121  for (int i=0; i<n_p; i++) {
122  long long int axmin =
123  t_p[i].a * static_cast<long long int>(t_p[i].x.min());
124  if (Limits::overflow_sub(sl,axmin))
125  throw OutOfLimits("Int::linear");
126  if (sl - axmin < Limits::min)
127  is_ip = false;
128  long long int axmax =
129  t_p[i].a * static_cast<long long int>(t_p[i].x.max());
130  if (Limits::overflow_sub(su,axmax))
131  throw OutOfLimits("Int::linear");
132  if (su - axmax > Limits::max)
133  is_ip = false;
134  }
135  for (int i=0; i<n_n; i++) {
136  long long int axmin =
137  t_n[i].a * static_cast<long long int>(t_n[i].x.min());
138  if (Limits::overflow_add(sl,axmin))
139  throw OutOfLimits("Int::linear");
140  if (sl + axmin < Limits::min)
141  is_ip = false;
142  long long int axmax =
143  t_n[i].a * static_cast<long long int>(t_n[i].x.max());
144  if (Limits::overflow_add(su,axmax))
145  throw OutOfLimits("Int::linear");
146  if (su + axmax > Limits::max)
147  is_ip = false;
148  }
149  return is_ip;
150  }
151 
156  template<class Val, class View>
157  forceinline void
160  switch (irt) {
161  case IRT_EQ:
163  break;
164  case IRT_NQ:
166  break;
167  case IRT_LQ:
169  break;
170  default: GECODE_NEVER;
171  }
172  }
173 
174 
176 #define GECODE_INT_PL_BIN(CLASS) \
177  switch (n_p) { \
178  case 2: \
179  GECODE_ES_FAIL((CLASS<int,IntView,IntView>::post \
180  (home,t_p[0].x,t_p[1].x,c))); \
181  break; \
182  case 1: \
183  GECODE_ES_FAIL((CLASS<int,IntView,MinusView>::post \
184  (home,t_p[0].x,MinusView(t_n[0].x),c))); \
185  break; \
186  case 0: \
187  GECODE_ES_FAIL((CLASS<int,MinusView,MinusView>::post \
188  (home,MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
189  break; \
190  default: GECODE_NEVER; \
191  }
192 
194 #define GECODE_INT_PL_TER(CLASS) \
195  switch (n_p) { \
196  case 3: \
197  GECODE_ES_FAIL((CLASS<int,IntView,IntView,IntView>::post \
198  (home,t_p[0].x,t_p[1].x,t_p[2].x,c))); \
199  break; \
200  case 2: \
201  GECODE_ES_FAIL((CLASS<int,IntView,IntView,MinusView>::post \
202  (home,t_p[0].x,t_p[1].x, \
203  MinusView(t_n[0].x),c))); \
204  break; \
205  case 1: \
206  GECODE_ES_FAIL((CLASS<int,IntView,MinusView,MinusView>::post \
207  (home,t_p[0].x, \
208  MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
209  break; \
210  case 0: \
211  GECODE_ES_FAIL((CLASS<int,MinusView,MinusView,MinusView>::post \
212  (home,MinusView(t_n[0].x), \
213  MinusView(t_n[1].x),MinusView(t_n[2].x),c))); \
214  break; \
215  default: GECODE_NEVER; \
216  }
217 
218  void
219  post(Home home, Term<IntView>* t, int n, IntRelType irt, int c,
220  IntPropLevel ipl) {
221 
222  Limits::check(c,"Int::linear");
223 
224  long long int d = c;
225 
226  eliminate(t,n,d);
227 
228  Term<IntView> *t_p, *t_n;
229  int n_p, n_n, gcd=1;
230  bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n,gcd);
231 
232  rewrite(irt,d,t_p,n_p,t_n,n_n);
233 
234  // Divide by gcd
235  if (gcd > 1) {
236  switch (irt) {
237  case IRT_EQ:
238  if ((d % gcd) != 0) {
239  home.fail();
240  return;
241  }
242  d /= gcd;
243  break;
244  case IRT_NQ:
245  if ((d % gcd) != 0)
246  return;
247  d /= gcd;
248  break;
249  case IRT_LQ:
250  d = floor_div_xp(d,static_cast<long long int>(gcd));
251  break;
252  default: GECODE_NEVER;
253  }
254  }
255 
256  if (n == 0) {
257  switch (irt) {
258  case IRT_EQ: if (d != 0) home.fail(); break;
259  case IRT_NQ: if (d == 0) home.fail(); break;
260  case IRT_LQ: if (d < 0) home.fail(); break;
261  default: GECODE_NEVER;
262  }
263  return;
264  }
265 
266  if (n == 1) {
267  if (n_p == 1) {
268  LLongScaleView y(t_p[0].a,t_p[0].x);
269  switch (irt) {
270  case IRT_EQ: GECODE_ME_FAIL(y.eq(home,d)); break;
271  case IRT_NQ: GECODE_ME_FAIL(y.nq(home,d)); break;
272  case IRT_LQ: GECODE_ME_FAIL(y.lq(home,d)); break;
273  default: GECODE_NEVER;
274  }
275  } else {
276  LLongScaleView y(t_n[0].a,t_n[0].x);
277  switch (irt) {
278  case IRT_EQ: GECODE_ME_FAIL(y.eq(home,-d)); break;
279  case IRT_NQ: GECODE_ME_FAIL(y.nq(home,-d)); break;
280  case IRT_LQ: GECODE_ME_FAIL(y.gq(home,-d)); break;
281  default: GECODE_NEVER;
282  }
283  }
284  return;
285  }
286 
287  // Check this special case here, as there can be no overflow
288  if ((n == 2) && is_unit &&
289  ((vbd(ipl) == IPL_DOM) || (vbd(ipl) == IPL_DEF)) &&
290  (irt == IRT_EQ) && (d == 0)) {
291  switch (n_p) {
292  case 2: {
293  IntView x(t_p[0].x);
294  MinusView y(t_p[1].x);
296  break;
297  }
298  case 1: {
299  IntView x(t_p[0].x);
300  IntView y(t_n[0].x);
302  break;
303  }
304  case 0: {
305  IntView x(t_n[0].x);
306  MinusView y(t_n[1].x);
308  break;
309  }
310  default:
311  GECODE_NEVER;
312  }
313  return;
314  }
315 
316  bool is_ip = precision(t_p,n_p,t_n,n_n,d);
317 
318  if (is_unit && is_ip &&
319  (vbd(ipl) != IPL_DOM) && (vbd(ipl) != IPL_DEF)) {
320  // Unit coefficients with integer precision
321  c = static_cast<int>(d);
322  if (n == 2) {
323  switch (irt) {
324  case IRT_EQ: GECODE_INT_PL_BIN(EqBin); break;
325  case IRT_NQ: GECODE_INT_PL_BIN(NqBin); break;
326  case IRT_LQ: GECODE_INT_PL_BIN(LqBin); break;
327  default: GECODE_NEVER;
328  }
329  } else if (n == 3) {
330  switch (irt) {
331  case IRT_EQ: GECODE_INT_PL_TER(EqTer); break;
332  case IRT_NQ: GECODE_INT_PL_TER(NqTer); break;
333  case IRT_LQ: GECODE_INT_PL_TER(LqTer); break;
334  default: GECODE_NEVER;
335  }
336  } else {
337  ViewArray<IntView> x(home,n_p);
338  for (int i=0; i<n_p; i++)
339  x[i] = t_p[i].x;
340  ViewArray<IntView> y(home,n_n);
341  for (int i=0; i<n_n; i++)
342  y[i] = t_n[i].x;
343  post_nary<int,IntView>(home,x,y,irt,c);
344  }
345  } else if (is_ip) {
346  if ((n==2) && is_unit &&
347  ((vbd(ipl) == IPL_DOM) || (vbd(ipl) == IPL_DEF)) &&
348  (irt == IRT_EQ)) {
349  // Binary domain-consistent equality
350  c = static_cast<int>(d);
351  assert(c != 0);
352  switch (n_p) {
353  case 2: {
354  MinusView x(t_p[0].x);
355  OffsetView y(t_p[1].x, -c);
357  break;
358  }
359  case 1: {
360  IntView x(t_p[0].x);
361  OffsetView y(t_n[0].x, c);
363  break;
364  }
365  case 0: {
366  MinusView x(t_n[0].x);
367  OffsetView y(t_n[1].x, c);
369  break;
370  }
371  default:
372  GECODE_NEVER;
373  }
374  } else {
375  // Arbitrary coefficients with integer precision
376  c = static_cast<int>(d);
377  ViewArray<IntScaleView> x(home,n_p);
378  for (int i=0; i<n_p; i++)
379  x[i] = IntScaleView(t_p[i].a,t_p[i].x);
380  ViewArray<IntScaleView> y(home,n_n);
381  for (int i=0; i<n_n; i++)
382  y[i] = IntScaleView(t_n[i].a,t_n[i].x);
383  if ((vbd(ipl) == IPL_DOM) && (irt == IRT_EQ)) {
385  } else {
386  post_nary<int,IntScaleView>(home,x,y,irt,c);
387  }
388  }
389  } else {
390  // Arbitrary coefficients with long long precision
391  ViewArray<LLongScaleView> x(home,n_p);
392  for (int i=0; i<n_p; i++)
393  x[i] = LLongScaleView(t_p[i].a,t_p[i].x);
394  ViewArray<LLongScaleView> y(home,n_n);
395  for (int i=0; i<n_n; i++)
396  y[i] = LLongScaleView(t_n[i].a,t_n[i].x);
397  if ((vbd(ipl) == IPL_DOM) && (irt == IRT_EQ)) {
399  ::post(home,x,y,d)));
400  } else {
401  post_nary<long long int,LLongScaleView>(home,x,y,irt,d);
402  }
403  }
404  }
405 
406 #undef GECODE_INT_PL_BIN
407 #undef GECODE_INT_PL_TER
408 
409 
414  template<class Val, class View>
415  forceinline void
418  IntRelType irt, Val c, Reify r) {
419  switch (irt) {
420  case IRT_EQ:
421  switch (r.mode()) {
422  case RM_EQV:
424  post(home,x,y,c,r.var())));
425  break;
426  case RM_IMP:
428  post(home,x,y,c,r.var())));
429  break;
430  case RM_PMI:
432  post(home,x,y,c,r.var())));
433  break;
434  default: GECODE_NEVER;
435  }
436  break;
437  case IRT_NQ:
438  {
439  NegBoolView n(r.var());
440  switch (r.mode()) {
441  case RM_EQV:
443  post(home,x,y,c,n)));
444  break;
445  case RM_IMP:
447  post(home,x,y,c,n)));
448  break;
449  case RM_PMI:
451  post(home,x,y,c,n)));
452  break;
453  default: GECODE_NEVER;
454  }
455  }
456  break;
457  case IRT_LQ:
458  switch (r.mode()) {
459  case RM_EQV:
461  post(home,x,y,c,r.var())));
462  break;
463  case RM_IMP:
465  post(home,x,y,c,r.var())));
466  break;
467  case RM_PMI:
469  post(home,x,y,c,r.var())));
470  break;
471  default: GECODE_NEVER;
472  }
473  break;
474  default: GECODE_NEVER;
475  }
476  }
477 
478  template<class CtrlView>
479  forceinline void
480  posteqint(Home home, IntView& x, int c, CtrlView b, ReifyMode rm,
481  IntPropLevel ipl) {
482  if ((vbd(ipl) == IPL_DOM) || (vbd(ipl) == IPL_DEF)) {
483  switch (rm) {
484  case RM_EQV:
486  post(home,x,c,b)));
487  break;
488  case RM_IMP:
490  post(home,x,c,b)));
491  break;
492  case RM_PMI:
494  post(home,x,c,b)));
495  break;
496  default: GECODE_NEVER;
497  }
498  } else {
499  switch (rm) {
500  case RM_EQV:
502  post(home,x,c,b)));
503  break;
504  case RM_IMP:
506  post(home,x,c,b)));
507  break;
508  case RM_PMI:
510  post(home,x,c,b)));
511  break;
512  default: GECODE_NEVER;
513  }
514  }
515  }
516 
517  void
518  post(Home home,
519  Term<IntView>* t, int n, IntRelType irt, int c, Reify r,
520  IntPropLevel ipl) {
521  Limits::check(c,"Int::linear");
522  long long int d = c;
523 
524  eliminate(t,n,d);
525 
526  Term<IntView> *t_p, *t_n;
527  int n_p, n_n, gcd=1;
528  bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n,gcd);
529 
530  rewrite(irt,d,t_p,n_p,t_n,n_n);
531 
532  // Divide by gcd
533  if (gcd > 1) {
534  switch (irt) {
535  case IRT_EQ:
536  if ((d % gcd) != 0) {
537  if (r.mode() != RM_PMI)
538  GECODE_ME_FAIL(BoolView(r.var()).zero(home));
539  return;
540  }
541  d /= gcd;
542  break;
543  case IRT_NQ:
544  if ((d % gcd) != 0) {
545  if (r.mode() != RM_IMP)
546  GECODE_ME_FAIL(BoolView(r.var()).one(home));
547  return;
548  }
549  d /= gcd;
550  break;
551  case IRT_LQ:
552  d = floor_div_xp(d,static_cast<long long int>(gcd));
553  break;
554  default: GECODE_NEVER;
555  }
556  }
557 
558  if (n == 0) {
559  bool fail = false;
560  switch (irt) {
561  case IRT_EQ: fail = (d != 0); break;
562  case IRT_NQ: fail = (d == 0); break;
563  case IRT_LQ: fail = (0 > d); break;
564  default: GECODE_NEVER;
565  }
566  if (fail) {
567  if (r.mode() != RM_PMI)
568  GECODE_ME_FAIL(BoolView(r.var()).zero(home));
569  } else {
570  if (r.mode() != RM_IMP)
571  GECODE_ME_FAIL(BoolView(r.var()).one(home));
572  }
573  return;
574  }
575 
576  bool is_ip = precision(t_p,n_p,t_n,n_n,d);
577 
578  if (is_unit && is_ip) {
579  c = static_cast<int>(d);
580  if (n == 1) {
581  switch (irt) {
582  case IRT_EQ:
583  if (n_p == 1) {
584  posteqint<BoolView>(home,t_p[0].x,c,r.var(),r.mode(),ipl);
585  } else {
586  posteqint<BoolView>(home,t_p[0].x,-c,r.var(),r.mode(),ipl);
587  }
588  break;
589  case IRT_NQ:
590  {
591  NegBoolView nb(r.var());
592  ReifyMode rm = r.mode();
593  switch (rm) {
594  case RM_IMP: rm = RM_PMI; break;
595  case RM_PMI: rm = RM_IMP; break;
596  default: ;
597  }
598  if (n_p == 1) {
599  posteqint<NegBoolView>(home,t_p[0].x,c,nb,rm,ipl);
600  } else {
601  posteqint<NegBoolView>(home,t_p[0].x,-c,nb,rm,ipl);
602  }
603  }
604  break;
605  case IRT_LQ:
606  if (n_p == 1) {
607  switch (r.mode()) {
608  case RM_EQV:
610  post(home,t_p[0].x,c,r.var())));
611  break;
612  case RM_IMP:
614  post(home,t_p[0].x,c,r.var())));
615  break;
616  case RM_PMI:
618  post(home,t_p[0].x,c,r.var())));
619  break;
620  default: GECODE_NEVER;
621  }
622  } else {
623  NegBoolView nb(r.var());
624  switch (r.mode()) {
625  case RM_EQV:
627  post(home,t_n[0].x,-c-1,nb)));
628  break;
629  case RM_IMP:
631  post(home,t_n[0].x,-c-1,nb)));
632  break;
633  case RM_PMI:
635  post(home,t_n[0].x,-c-1,nb)));
636  break;
637  default: GECODE_NEVER;
638  }
639  }
640  break;
641  default: GECODE_NEVER;
642  }
643  } else if (n == 2) {
644  switch (irt) {
645  case IRT_EQ:
646  switch (n_p) {
647  case 2:
648  switch (r.mode()) {
649  case RM_EQV:
651  post(home,t_p[0].x,t_p[1].x,c,r.var())));
652  break;
653  case RM_IMP:
655  post(home,t_p[0].x,t_p[1].x,c,r.var())));
656  break;
657  case RM_PMI:
659  post(home,t_p[0].x,t_p[1].x,c,r.var())));
660  break;
661  default: GECODE_NEVER;
662  }
663  break;
664  case 1:
665  switch (r.mode()) {
666  case RM_EQV:
668  post(home,t_p[0].x,MinusView(t_n[0].x),c,
669  r.var())));
670  break;
671  case RM_IMP:
673  post(home,t_p[0].x,MinusView(t_n[0].x),c,
674  r.var())));
675  break;
676  case RM_PMI:
678  post(home,t_p[0].x,MinusView(t_n[0].x),c,
679  r.var())));
680  break;
681  default: GECODE_NEVER;
682  }
683  break;
684  case 0:
685  switch (r.mode()) {
686  case RM_EQV:
688  post(home,t_n[0].x,t_n[1].x,-c,r.var())));
689  break;
690  case RM_IMP:
692  post(home,t_n[0].x,t_n[1].x,-c,r.var())));
693  break;
694  case RM_PMI:
696  post(home,t_n[0].x,t_n[1].x,-c,r.var())));
697  break;
698  default: GECODE_NEVER;
699  }
700  break;
701  default: GECODE_NEVER;
702  }
703  break;
704  case IRT_NQ:
705  {
706  NegBoolView nb(r.var());
707  switch (n_p) {
708  case 2:
709  switch (r.mode()) {
710  case RM_EQV:
712  post(home,t_p[0].x,t_p[1].x,c,nb)));
713  break;
714  case RM_IMP:
716  post(home,t_p[0].x,t_p[1].x,c,nb)));
717  break;
718  case RM_PMI:
720  post(home,t_p[0].x,t_p[1].x,c,nb)));
721  break;
722  default: GECODE_NEVER;
723  }
724  break;
725  case 1:
726  switch (r.mode()) {
727  case RM_EQV:
729  post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
730  break;
731  case RM_IMP:
733  post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
734  break;
735  case RM_PMI:
737  post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
738  break;
739  default: GECODE_NEVER;
740  }
741  break;
742  case 0:
743  switch (r.mode()) {
744  case RM_EQV:
746  post(home,t_p[0].x,t_p[1].x,-c,nb)));
747  break;
748  case RM_IMP:
750  post(home,t_p[0].x,t_p[1].x,-c,nb)));
751  break;
752  case RM_PMI:
754  post(home,t_p[0].x,t_p[1].x,-c,nb)));
755  break;
756  default: GECODE_NEVER;
757  }
758  break;
759  default: GECODE_NEVER;
760  }
761  }
762  break;
763  case IRT_LQ:
764  switch (n_p) {
765  case 2:
766  switch (r.mode()) {
767  case RM_EQV:
769  post(home,t_p[0].x,t_p[1].x,c,r.var())));
770  break;
771  case RM_IMP:
773  post(home,t_p[0].x,t_p[1].x,c,r.var())));
774  break;
775  case RM_PMI:
777  post(home,t_p[0].x,t_p[1].x,c,r.var())));
778  break;
779  default: GECODE_NEVER;
780  }
781  break;
782  case 1:
783  switch (r.mode()) {
784  case RM_EQV:
786  post(home,t_p[0].x,MinusView(t_n[0].x),c,
787  r.var())));
788  break;
789  case RM_IMP:
791  post(home,t_p[0].x,MinusView(t_n[0].x),c,
792  r.var())));
793  break;
794  case RM_PMI:
796  post(home,t_p[0].x,MinusView(t_n[0].x),c,
797  r.var())));
798  break;
799  default: GECODE_NEVER;
800  }
801  break;
802  case 0:
803  switch (r.mode()) {
804  case RM_EQV:
806  post(home,MinusView(t_n[0].x),
807  MinusView(t_n[1].x),c,r.var())));
808  break;
809  case RM_IMP:
811  post(home,MinusView(t_n[0].x),
812  MinusView(t_n[1].x),c,r.var())));
813  break;
814  case RM_PMI:
816  post(home,MinusView(t_n[0].x),
817  MinusView(t_n[1].x),c,r.var())));
818  break;
819  default: GECODE_NEVER;
820  }
821  break;
822  default: GECODE_NEVER;
823  }
824  break;
825  default: GECODE_NEVER;
826  }
827  } else {
828  ViewArray<IntView> x(home,n_p);
829  for (int i=0; i<n_p; i++)
830  x[i] = t_p[i].x;
831  ViewArray<IntView> y(home,n_n);
832  for (int i=0; i<n_n; i++)
833  y[i] = t_n[i].x;
834  post_nary<int,IntView>(home,x,y,irt,c,r);
835  }
836  } else if (is_ip) {
837  // Arbitrary coefficients with integer precision
838  c = static_cast<int>(d);
839  ViewArray<IntScaleView> x(home,n_p);
840  for (int i=0; i<n_p; i++)
841  x[i] = IntScaleView(t_p[i].a,t_p[i].x);
842  ViewArray<IntScaleView> y(home,n_n);
843  for (int i=0; i<n_n; i++)
844  y[i] = IntScaleView(t_n[i].a,t_n[i].x);
845  post_nary<int,IntScaleView>(home,x,y,irt,c,r);
846  } else {
847  // Arbitrary coefficients with long long precision
848  ViewArray<LLongScaleView> x(home,n_p);
849  for (int i=0; i<n_p; i++)
850  x[i] = LLongScaleView(t_p[i].a,t_p[i].x);
851  ViewArray<LLongScaleView> y(home,n_n);
852  for (int i=0; i<n_n; i++)
853  y[i] = LLongScaleView(t_n[i].a,t_n[i].x);
854  post_nary<long long int,LLongScaleView>(home,x,y,irt,d,r);
855  }
856  }
857 
858 }}}
859 
860 // STATISTICS: int-post
Negated Boolean view.
Definition: view.hpp:1574
void rewrite(IntRelType &r, long long int &d)
Rewrite non-strict relations.
Definition: bool-post.cpp:55
Propagator for bounds consistent binary linear less or equal
Definition: linear.hh:237
Post propagator for SetVar x
Definition: set.hh:767
IntRelType
Relation types for integers.
Definition: int.hh:925
bool zero(void) const
Test whether view is assigned to be zero.
Definition: bool.hpp:220
Post propagator for SetVar SetOpType SetVar y
Definition: set.hh:767
@ RM_PMI
Inverse implication for reification.
Definition: int.hh:869
#define GECODE_ES_FAIL(es)
Check whether execution status es is failed, and fail space home.
Definition: macros.hpp:103
Class for describing linear term .
Definition: linear.hh:1336
View x
View.
Definition: linear.hh:1341
Reified less or equal with integer propagator.
Definition: rel.hh:575
@ IRT_GQ
Greater or equal ( )
Definition: int.hh:930
Reified domain consistent equality with integer propagator.
Definition: rel.hh:398
@ IRT_LE
Less ( )
Definition: int.hh:929
Propagator for bounds consistent n-ary linear less or equal
Definition: linear.hh:716
bool overflow_sub(int n, int m)
Check whether subtracting m from n would overflow.
Definition: limits.hpp:93
Minus integer view.
Definition: view.hpp:282
@ RM_IMP
Implication for reification.
Definition: int.hh:862
bool one(void) const
Test whether view is assigned to be one.
Definition: bool.hpp:224
bool overflow_add(int n, int m)
Check whether adding n and m would overflow.
Definition: limits.hpp:79
NodeType t
Type of node.
Definition: bool-expr.cpp:230
void check(int n, const char *l)
Check whether n is in range, otherwise throw out of limits with information l.
Definition: limits.hpp:46
IntPropLevel
Propagation levels for integer propagators.
Definition: int.hh:974
IntType floor_div_xp(IntType x, IntType y)
Compute where y is non-negative.
Definition: div.hpp:75
bool assigned(void) const
Test whether view is assigned.
Definition: var.hpp:111
void post_nary(Home home, ViewArray< View > &x, ViewArray< View > &y, IntRelType irt, Val c)
Posting n-ary propagators.
Definition: int-post.cpp:158
void eliminate(Term< BoolView > *t, int &n, long long int &d)
Eliminate assigned views.
Definition: bool-post.cpp:43
Propagator for bounds consistent ternary linear disquality
Definition: linear.hh:419
Boolean view for Boolean variables.
Definition: view.hpp:1380
Gecode toplevel namespace
Propagator for bounds consistent n-ary linear equality
Definition: linear.hh:577
int gcd(int a, int b)
Compute the greatest common divisor of a and b.
Definition: post.hpp:89
IntPropLevel vbd(IntPropLevel ipl)
Extract value, bounds, or domain propagation from propagation level.
Definition: ipl.hpp:37
Binary domain consistent equality propagator.
Definition: rel.hh:68
Reification specification.
Definition: int.hh:876
@ RM_EQV
Equivalence for reification (default)
Definition: int.hh:855
Propagator for bounds consistent n-ary linear disequality
Definition: linear.hh:683
Home class for posting propagators
Definition: core.hpp:856
Post propagator for SetVar SetOpType SetVar SetRelType r
Definition: set.hh:767
@ IPL_DOM
Domain propagation Options: basic versus advanced propagation.
Definition: int.hh:979
IntRelType swap(IntRelType irt)
Return swapped relation type of irt.
Definition: irt.hpp:37
Propagator for reified bounds consistent n-ary linear less or equal
Definition: linear.hh:749
bool one(const Gecode::FloatValArgs &a)
Check whether has only one coefficients.
Definition: linear.cpp:46
struct Gecode::@602::NNF::@65::@66 b
For binary nodes (and, or, eqv)
const int max
Largest allowed integer value.
Definition: int.hh:116
Propagator for bounds consistent binary linear disequality
Definition: linear.hh:201
Propagator for reified bounds consistent binary linear equality
Definition: linear.hh:168
Propagator for domain consistent n-ary linear equality
Definition: linear.hh:609
Offset integer view.
Definition: view.hpp:443
#define GECODE_INT_PL_TER(CLASS)
Macro for posting ternary special cases for linear constraints.
Definition: int-post.cpp:194
#define GECODE_NEVER
Assert that this command is never executed.
Definition: macros.hpp:56
struct Gecode::@602::NNF::@65::@67 a
For atomic nodes.
Propagator for bounds consistent ternary linear equality
Definition: linear.hh:384
void fail(void)
Mark space as failed.
Definition: core.hpp:4039
@ IPL_DEF
Simple propagation levels.
Definition: int.hh:976
Gecode::IntSet d(v, 7)
ReifyMode
Mode for reification.
Definition: int.hh:848
void posteqint(Home home, IntView &x, int c, CtrlView b, ReifyMode rm, IntPropLevel ipl)
Definition: int-post.cpp:480
#define GECODE_INT_PL_BIN(CLASS)
Macro for posting binary special cases for linear constraints.
Definition: int-post.cpp:176
Integer view for integer variables.
Definition: view.hpp:129
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:79
Reified bounds consistent equality with integer propagator.
Definition: rel.hh:425
Propagator for reified bounds consistent n-ary linear equality
Definition: linear.hh:649
#define GECODE_ME_FAIL(me)
Check whether modification event me is failed, and fail space home.
Definition: macros.hpp:77
Propagator for bounds consistent ternary linear less or equal
Definition: linear.hh:454
int a
Coefficient.
Definition: linear.hh:1339
Propagator for reified bounds consistent binary linear less or equal
Definition: linear.hh:305
const int min
Smallest allowed integer value.
Definition: int.hh:118
#define forceinline
Definition: config.hpp:192
@ IRT_EQ
Equality ( )
Definition: int.hh:926
Exception: Unknown relation passed as argument
Definition: exception.hpp:87
Propagator for bounds consistent binary linear equality
Definition: linear.hh:134
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:589
@ IRT_NQ
Disequality ( )
Definition: int.hh:927
Exception: Value out of limits
Definition: exception.hpp:44
Gecode::FloatVal c(-8, 8)
View arrays.
Definition: array.hpp:253
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:234
@ IRT_GR
Greater ( )
Definition: int.hh:931
Gecode::IntArgs i({1, 2, 3, 4})
@ IRT_LQ
Less or equal ( )
Definition: int.hh:928