Generated on Wed Jan 24 2018 21:22:26 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: 2017-03-14 11:10:06 +0100 (Tue, 14 Mar 2017) $ by $Author: schulte $
11  * $Revision: 15576 $
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  bool is_ip = precision(t_p,n_p,t_n,n_n,d);
292 
293  if (is_unit && is_ip &&
294  (vbd(ipl) != IPL_DOM) && (vbd(ipl) != IPL_DEF)) {
295  // Unit coefficients with integer precision
296  c = static_cast<int>(d);
297  if (n == 2) {
298  switch (irt) {
299  case IRT_EQ: GECODE_INT_PL_BIN(EqBin); break;
300  case IRT_NQ: GECODE_INT_PL_BIN(NqBin); break;
301  case IRT_LQ: GECODE_INT_PL_BIN(LqBin); break;
302  default: GECODE_NEVER;
303  }
304  } else if (n == 3) {
305  switch (irt) {
306  case IRT_EQ: GECODE_INT_PL_TER(EqTer); break;
307  case IRT_NQ: GECODE_INT_PL_TER(NqTer); break;
308  case IRT_LQ: GECODE_INT_PL_TER(LqTer); break;
309  default: GECODE_NEVER;
310  }
311  } else {
312  ViewArray<IntView> x(home,n_p);
313  for (int i = n_p; i--; )
314  x[i] = t_p[i].x;
315  ViewArray<IntView> y(home,n_n);
316  for (int i = n_n; i--; )
317  y[i] = t_n[i].x;
318  post_nary<int,IntView>(home,x,y,irt,c);
319  }
320  } else if (is_ip) {
321  if ((n==2) && is_unit &&
322  ((vbd(ipl) == IPL_DOM) || (vbd(ipl) == IPL_DEF)) &&
323  (irt == IRT_EQ)) {
324  // Binary domain-consistent equality
325  c = static_cast<int>(d);
326  if (c == 0) {
327  switch (n_p) {
328  case 2: {
329  IntView x(t_p[0].x);
330  MinusView y(t_p[1].x);
333  break;
334  }
335  case 1: {
336  IntView x(t_p[0].x);
337  IntView y(t_n[0].x);
340  break;
341  }
342  case 0: {
343  IntView x(t_n[0].x);
344  MinusView y(t_n[1].x);
347  break;
348  }
349  default:
350  GECODE_NEVER;
351  }
352  } else {
353  switch (n_p) {
354  case 2: {
355  MinusView x(t_p[0].x);
356  OffsetView y(t_p[1].x, -c);
359  break;
360  }
361  case 1: {
362  IntView x(t_p[0].x);
363  OffsetView y(t_n[0].x, c);
366  break;
367  }
368  case 0: {
369  MinusView x(t_n[0].x);
370  OffsetView y(t_n[1].x, c);
373  break;
374  }
375  default:
376  GECODE_NEVER;
377  }
378  }
379  } else {
380  // Arbitrary coefficients with integer precision
381  c = static_cast<int>(d);
382  ViewArray<IntScaleView> x(home,n_p);
383  for (int i = n_p; i--; )
384  x[i] = IntScaleView(t_p[i].a,t_p[i].x);
385  ViewArray<IntScaleView> y(home,n_n);
386  for (int i = n_n; i--; )
387  y[i] = IntScaleView(t_n[i].a,t_n[i].x);
388  if ((vbd(ipl) == IPL_DOM) && (irt == IRT_EQ)) {
390  } else {
391  post_nary<int,IntScaleView>(home,x,y,irt,c);
392  }
393  }
394  } else {
395  // Arbitrary coefficients with long long precision
396  ViewArray<LLongScaleView> x(home,n_p);
397  for (int i = n_p; i--; )
398  x[i] = LLongScaleView(t_p[i].a,t_p[i].x);
399  ViewArray<LLongScaleView> y(home,n_n);
400  for (int i = n_n; i--; )
401  y[i] = LLongScaleView(t_n[i].a,t_n[i].x);
402  if ((vbd(ipl) == IPL_DOM) && (irt == IRT_EQ)) {
404  ::post(home,x,y,d)));
405  } else {
406  post_nary<long long int,LLongScaleView>(home,x,y,irt,d);
407  }
408  }
409  }
410 
411 #undef GECODE_INT_PL_BIN
412 #undef GECODE_INT_PL_TER
413 
414 
419  template<class Val, class View>
420  forceinline void
423  IntRelType irt, Val c, Reify r) {
424  switch (irt) {
425  case IRT_EQ:
426  switch (r.mode()) {
427  case RM_EQV:
429  post(home,x,y,c,r.var())));
430  break;
431  case RM_IMP:
433  post(home,x,y,c,r.var())));
434  break;
435  case RM_PMI:
437  post(home,x,y,c,r.var())));
438  break;
439  default: GECODE_NEVER;
440  }
441  break;
442  case IRT_NQ:
443  {
444  NegBoolView n(r.var());
445  switch (r.mode()) {
446  case RM_EQV:
448  post(home,x,y,c,n)));
449  break;
450  case RM_IMP:
452  post(home,x,y,c,n)));
453  break;
454  case RM_PMI:
456  post(home,x,y,c,n)));
457  break;
458  default: GECODE_NEVER;
459  }
460  }
461  break;
462  case IRT_LQ:
463  switch (r.mode()) {
464  case RM_EQV:
466  post(home,x,y,c,r.var())));
467  break;
468  case RM_IMP:
470  post(home,x,y,c,r.var())));
471  break;
472  case RM_PMI:
474  post(home,x,y,c,r.var())));
475  break;
476  default: GECODE_NEVER;
477  }
478  break;
479  default: GECODE_NEVER;
480  }
481  }
482 
483  template<class CtrlView>
484  forceinline void
485  posteqint(Home home, IntView& x, int c, CtrlView b, ReifyMode rm,
486  IntPropLevel ipl) {
487  if ((vbd(ipl) == IPL_DOM) || (vbd(ipl) == IPL_DEF)) {
488  switch (rm) {
489  case RM_EQV:
491  post(home,x,c,b)));
492  break;
493  case RM_IMP:
495  post(home,x,c,b)));
496  break;
497  case RM_PMI:
499  post(home,x,c,b)));
500  break;
501  default: GECODE_NEVER;
502  }
503  } else {
504  switch (rm) {
505  case RM_EQV:
507  post(home,x,c,b)));
508  break;
509  case RM_IMP:
511  post(home,x,c,b)));
512  break;
513  case RM_PMI:
515  post(home,x,c,b)));
516  break;
517  default: GECODE_NEVER;
518  }
519  }
520  }
521 
522  void
523  post(Home home,
524  Term<IntView>* t, int n, IntRelType irt, int c, Reify r,
525  IntPropLevel ipl) {
526  Limits::check(c,"Int::linear");
527  long long int d = c;
528 
529  eliminate(t,n,d);
530 
531  Term<IntView> *t_p, *t_n;
532  int n_p, n_n, gcd=1;
533  bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n,gcd);
534 
535  rewrite(irt,d,t_p,n_p,t_n,n_n);
536 
537  // Divide by gcd
538  if (gcd > 1) {
539  switch (irt) {
540  case IRT_EQ:
541  if ((d % gcd) != 0) {
542  if (r.mode() != RM_PMI)
543  GECODE_ME_FAIL(BoolView(r.var()).zero(home));
544  return;
545  }
546  d /= gcd;
547  break;
548  case IRT_NQ:
549  if ((d % gcd) != 0) {
550  if (r.mode() != RM_IMP)
551  GECODE_ME_FAIL(BoolView(r.var()).one(home));
552  return;
553  }
554  d /= gcd;
555  break;
556  case IRT_LQ:
557  d = floor_div_xp(d,static_cast<long long int>(gcd));
558  break;
559  default: GECODE_NEVER;
560  }
561  }
562 
563  if (n == 0) {
564  bool fail = false;
565  switch (irt) {
566  case IRT_EQ: fail = (d != 0); break;
567  case IRT_NQ: fail = (d == 0); break;
568  case IRT_LQ: fail = (0 > d); break;
569  default: GECODE_NEVER;
570  }
571  if (fail) {
572  if (r.mode() != RM_PMI)
573  GECODE_ME_FAIL(BoolView(r.var()).zero(home));
574  } else {
575  if (r.mode() != RM_IMP)
576  GECODE_ME_FAIL(BoolView(r.var()).one(home));
577  }
578  return;
579  }
580 
581  bool is_ip = precision(t_p,n_p,t_n,n_n,d);
582 
583  if (is_unit && is_ip) {
584  c = static_cast<int>(d);
585  if (n == 1) {
586  switch (irt) {
587  case IRT_EQ:
588  if (n_p == 1) {
589  posteqint<BoolView>(home,t_p[0].x,c,r.var(),r.mode(),ipl);
590  } else {
591  posteqint<BoolView>(home,t_p[0].x,-c,r.var(),r.mode(),ipl);
592  }
593  break;
594  case IRT_NQ:
595  {
596  NegBoolView nb(r.var());
597  ReifyMode rm = r.mode();
598  switch (rm) {
599  case RM_IMP: rm = RM_PMI; break;
600  case RM_PMI: rm = RM_IMP; break;
601  default: ;
602  }
603  if (n_p == 1) {
604  posteqint<NegBoolView>(home,t_p[0].x,c,nb,rm,ipl);
605  } else {
606  posteqint<NegBoolView>(home,t_p[0].x,-c,nb,rm,ipl);
607  }
608  }
609  break;
610  case IRT_LQ:
611  if (n_p == 1) {
612  switch (r.mode()) {
613  case RM_EQV:
615  post(home,t_p[0].x,c,r.var())));
616  break;
617  case RM_IMP:
619  post(home,t_p[0].x,c,r.var())));
620  break;
621  case RM_PMI:
623  post(home,t_p[0].x,c,r.var())));
624  break;
625  default: GECODE_NEVER;
626  }
627  } else {
628  NegBoolView nb(r.var());
629  switch (r.mode()) {
630  case RM_EQV:
632  post(home,t_n[0].x,-c-1,nb)));
633  break;
634  case RM_IMP:
636  post(home,t_n[0].x,-c-1,nb)));
637  break;
638  case RM_PMI:
640  post(home,t_n[0].x,-c-1,nb)));
641  break;
642  default: GECODE_NEVER;
643  }
644  }
645  break;
646  default: GECODE_NEVER;
647  }
648  } else if (n == 2) {
649  switch (irt) {
650  case IRT_EQ:
651  switch (n_p) {
652  case 2:
653  switch (r.mode()) {
654  case RM_EQV:
656  post(home,t_p[0].x,t_p[1].x,c,r.var())));
657  break;
658  case RM_IMP:
660  post(home,t_p[0].x,t_p[1].x,c,r.var())));
661  break;
662  case RM_PMI:
664  post(home,t_p[0].x,t_p[1].x,c,r.var())));
665  break;
666  default: GECODE_NEVER;
667  }
668  break;
669  case 1:
670  switch (r.mode()) {
671  case RM_EQV:
673  post(home,t_p[0].x,MinusView(t_n[0].x),c,
674  r.var())));
675  break;
676  case RM_IMP:
678  post(home,t_p[0].x,MinusView(t_n[0].x),c,
679  r.var())));
680  break;
681  case RM_PMI:
683  post(home,t_p[0].x,MinusView(t_n[0].x),c,
684  r.var())));
685  break;
686  default: GECODE_NEVER;
687  }
688  break;
689  case 0:
690  switch (r.mode()) {
691  case RM_EQV:
693  post(home,t_n[0].x,t_n[1].x,-c,r.var())));
694  break;
695  case RM_IMP:
697  post(home,t_n[0].x,t_n[1].x,-c,r.var())));
698  break;
699  case RM_PMI:
701  post(home,t_n[0].x,t_n[1].x,-c,r.var())));
702  break;
703  default: GECODE_NEVER;
704  }
705  break;
706  default: GECODE_NEVER;
707  }
708  break;
709  case IRT_NQ:
710  {
711  NegBoolView nb(r.var());
712  switch (n_p) {
713  case 2:
714  switch (r.mode()) {
715  case RM_EQV:
717  post(home,t_p[0].x,t_p[1].x,c,nb)));
718  break;
719  case RM_IMP:
721  post(home,t_p[0].x,t_p[1].x,c,nb)));
722  break;
723  case RM_PMI:
725  post(home,t_p[0].x,t_p[1].x,c,nb)));
726  break;
727  default: GECODE_NEVER;
728  }
729  break;
730  case 1:
731  switch (r.mode()) {
732  case RM_EQV:
734  post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
735  break;
736  case RM_IMP:
738  post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
739  break;
740  case RM_PMI:
742  post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
743  break;
744  default: GECODE_NEVER;
745  }
746  break;
747  case 0:
748  switch (r.mode()) {
749  case RM_EQV:
751  post(home,t_p[0].x,t_p[1].x,-c,nb)));
752  break;
753  case RM_IMP:
755  post(home,t_p[0].x,t_p[1].x,-c,nb)));
756  break;
757  case RM_PMI:
759  post(home,t_p[0].x,t_p[1].x,-c,nb)));
760  break;
761  default: GECODE_NEVER;
762  }
763  break;
764  default: GECODE_NEVER;
765  }
766  }
767  break;
768  case IRT_LQ:
769  switch (n_p) {
770  case 2:
771  switch (r.mode()) {
772  case RM_EQV:
774  post(home,t_p[0].x,t_p[1].x,c,r.var())));
775  break;
776  case RM_IMP:
778  post(home,t_p[0].x,t_p[1].x,c,r.var())));
779  break;
780  case RM_PMI:
782  post(home,t_p[0].x,t_p[1].x,c,r.var())));
783  break;
784  default: GECODE_NEVER;
785  }
786  break;
787  case 1:
788  switch (r.mode()) {
789  case RM_EQV:
791  post(home,t_p[0].x,MinusView(t_n[0].x),c,
792  r.var())));
793  break;
794  case RM_IMP:
796  post(home,t_p[0].x,MinusView(t_n[0].x),c,
797  r.var())));
798  break;
799  case RM_PMI:
801  post(home,t_p[0].x,MinusView(t_n[0].x),c,
802  r.var())));
803  break;
804  default: GECODE_NEVER;
805  }
806  break;
807  case 0:
808  switch (r.mode()) {
809  case RM_EQV:
811  post(home,MinusView(t_n[0].x),
812  MinusView(t_n[1].x),c,r.var())));
813  break;
814  case RM_IMP:
816  post(home,MinusView(t_n[0].x),
817  MinusView(t_n[1].x),c,r.var())));
818  break;
819  case RM_PMI:
821  post(home,MinusView(t_n[0].x),
822  MinusView(t_n[1].x),c,r.var())));
823  break;
824  default: GECODE_NEVER;
825  }
826  break;
827  default: GECODE_NEVER;
828  }
829  break;
830  default: GECODE_NEVER;
831  }
832  } else {
833  ViewArray<IntView> x(home,n_p);
834  for (int i = n_p; i--; )
835  x[i] = t_p[i].x;
836  ViewArray<IntView> y(home,n_n);
837  for (int i = n_n; i--; )
838  y[i] = t_n[i].x;
839  post_nary<int,IntView>(home,x,y,irt,c,r);
840  }
841  } else if (is_ip) {
842  // Arbitrary coefficients with integer precision
843  c = static_cast<int>(d);
844  ViewArray<IntScaleView> x(home,n_p);
845  for (int i = n_p; i--; )
846  x[i] = IntScaleView(t_p[i].a,t_p[i].x);
847  ViewArray<IntScaleView> y(home,n_n);
848  for (int i = n_n; i--; )
849  y[i] = IntScaleView(t_n[i].a,t_n[i].x);
850  post_nary<int,IntScaleView>(home,x,y,irt,c,r);
851  } else {
852  // Arbitrary coefficients with long long precision
853  ViewArray<LLongScaleView> x(home,n_p);
854  for (int i = n_p; i--; )
855  x[i] = LLongScaleView(t_p[i].a,t_p[i].x);
856  ViewArray<LLongScaleView> y(home,n_n);
857  for (int i = n_n; i--; )
858  y[i] = LLongScaleView(t_n[i].a,t_n[i].x);
859  post_nary<long long int,LLongScaleView>(home,x,y,irt,d,r);
860  }
861  }
862 
863 }}}
864 
865 // STATISTICS: int-post
Scale integer view (template)
Definition: view.hpp:671
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:850
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:1503
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:909
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:912
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:911
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
struct Gecode::@579::NNF::@61::@63 a
For atomic nodes.
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:907
IntRelType
Relation types for integers.
Definition: int.hh:906
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:957
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:857
struct Gecode::@579::NNF::@61::@62 b
For binary nodes (and, or, eqv)
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:910
Offset integer view.
Definition: view.hpp:422
View arrays.
Definition: array.hpp:234
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:784
Reified bounds consistent equality with integer propagator.
Definition: rel.hh:429
IntPropLevel
Propagation levels for integer propagators.
Definition: int.hh:955
Integer view for integer variables.
Definition: view.hpp:129
Post propagator for SetVar SetOpType SetVar y
Definition: set.hh:784
bool overflow_sub(int n, int m)
Check whether subtracting m from n would overflow.
Definition: limits.hpp:97
ScaleView< int, unsigned int > IntScaleView
Integer-precision integer scale view.
Definition: view.hpp:759
Minus integer view.
Definition: view.hpp:276
#define forceinline
Definition: config.hpp:173
#define GECODE_INT_PL_TER(CLASS)
Macro for posting ternary special cases for linear constraints.
Definition: int-post.cpp:198
Domain propagation Preferences: prefer speed or memory.
Definition: int.hh:960
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:784
#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:4090
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:485
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:843
Disequality ( )
Definition: int.hh:908
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:765
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:922
#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:829
#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:836
IntRelType swap(IntRelType irt)
Return swapped relation type of irt.
Definition: irt.hpp:41
Boolean view for Boolean variables.
Definition: view.hpp:1315