Generated on Sat Feb 7 2015 02:01:24 for Gecode by doxygen 1.8.9.1
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: 2013-02-14 16:29:11 +0100 (Thu, 14 Feb 2013) $ by $Author: schulte $
11  * $Revision: 13292 $
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
163  ViewArray<View>& x, ViewArray<View>& y, IntRelType irt, Val c) {
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  IntConLevel icl) {
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 && (icl != ICL_DOM)) {
294  // Unit coefficients with integer precision
295  c = static_cast<int>(d);
296  if (n == 2) {
297  switch (irt) {
298  case IRT_EQ: GECODE_INT_PL_BIN(EqBin); break;
299  case IRT_NQ: GECODE_INT_PL_BIN(NqBin); break;
300  case IRT_LQ: GECODE_INT_PL_BIN(LqBin); break;
301  default: GECODE_NEVER;
302  }
303  } else if (n == 3) {
304  switch (irt) {
305  case IRT_EQ: GECODE_INT_PL_TER(EqTer); break;
306  case IRT_NQ: GECODE_INT_PL_TER(NqTer); break;
307  case IRT_LQ: GECODE_INT_PL_TER(LqTer); break;
308  default: GECODE_NEVER;
309  }
310  } else {
311  ViewArray<IntView> x(home,n_p);
312  for (int i = n_p; i--; )
313  x[i] = t_p[i].x;
314  ViewArray<IntView> y(home,n_n);
315  for (int i = n_n; i--; )
316  y[i] = t_n[i].x;
317  post_nary<int,IntView>(home,x,y,irt,c);
318  }
319  } else if (is_ip) {
320  if ((n==2) && is_unit && (icl == ICL_DOM) && (irt == IRT_EQ)) {
321  // Binary domain-consistent equality
322  c = static_cast<int>(d);
323  if (c == 0) {
324  switch (n_p) {
325  case 2: {
326  IntView x(t_p[0].x);
327  MinusView y(t_p[1].x);
330  break;
331  }
332  case 1: {
333  IntView x(t_p[0].x);
334  IntView y(t_n[0].x);
337  break;
338  }
339  case 0: {
340  IntView x(t_n[0].x);
341  MinusView y(t_n[1].x);
344  break;
345  }
346  default:
347  GECODE_NEVER;
348  }
349  } else {
350  switch (n_p) {
351  case 2: {
352  MinusView x(t_p[0].x);
353  OffsetView y(t_p[1].x, -c);
356  break;
357  }
358  case 1: {
359  IntView x(t_p[0].x);
360  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);
370  break;
371  }
372  default:
373  GECODE_NEVER;
374  }
375  }
376  } else {
377  // Arbitrary coefficients with integer precision
378  c = static_cast<int>(d);
379  ViewArray<IntScaleView> x(home,n_p);
380  for (int i = n_p; i--; )
381  x[i] = IntScaleView(t_p[i].a,t_p[i].x);
382  ViewArray<IntScaleView> y(home,n_n);
383  for (int i = n_n; i--; )
384  y[i] = IntScaleView(t_n[i].a,t_n[i].x);
385  if ((icl == ICL_DOM) && (irt == IRT_EQ)) {
387  } else {
388  post_nary<int,IntScaleView>(home,x,y,irt,c);
389  }
390  }
391  } else {
392  // Arbitrary coefficients with long long precision
393  ViewArray<LLongScaleView> x(home,n_p);
394  for (int i = n_p; i--; )
395  x[i] = LLongScaleView(t_p[i].a,t_p[i].x);
396  ViewArray<LLongScaleView> y(home,n_n);
397  for (int i = n_n; i--; )
398  y[i] = LLongScaleView(t_n[i].a,t_n[i].x);
399  if ((icl == ICL_DOM) && (irt == IRT_EQ)) {
401  ::post(home,x,y,d)));
402  } else {
403  post_nary<long long int,LLongScaleView>(home,x,y,irt,d);
404  }
405  }
406  }
407 
408 #undef GECODE_INT_PL_BIN
409 #undef GECODE_INT_PL_TER
410 
411 
416  template<class Val, class View>
417  forceinline void
420  IntRelType irt, Val c, Reify r) {
421  switch (irt) {
422  case IRT_EQ:
423  switch (r.mode()) {
424  case RM_EQV:
426  post(home,x,y,c,r.var())));
427  break;
428  case RM_IMP:
430  post(home,x,y,c,r.var())));
431  break;
432  case RM_PMI:
434  post(home,x,y,c,r.var())));
435  break;
436  default: GECODE_NEVER;
437  }
438  break;
439  case IRT_NQ:
440  {
441  NegBoolView n(r.var());
442  switch (r.mode()) {
443  case RM_EQV:
445  post(home,x,y,c,n)));
446  break;
447  case RM_IMP:
449  post(home,x,y,c,n)));
450  break;
451  case RM_PMI:
453  post(home,x,y,c,n)));
454  break;
455  default: GECODE_NEVER;
456  }
457  }
458  break;
459  case IRT_LQ:
460  switch (r.mode()) {
461  case RM_EQV:
463  post(home,x,y,c,r.var())));
464  break;
465  case RM_IMP:
467  post(home,x,y,c,r.var())));
468  break;
469  case RM_PMI:
471  post(home,x,y,c,r.var())));
472  break;
473  default: GECODE_NEVER;
474  }
475  break;
476  default: GECODE_NEVER;
477  }
478  }
479 
480  template<class CtrlView>
481  forceinline void
482  posteqint(Home home, IntView& x, int c, CtrlView b, ReifyMode rm,
483  IntConLevel icl) {
484  if (icl == ICL_DOM) {
485  switch (rm) {
486  case RM_EQV:
488  post(home,x,c,b)));
489  break;
490  case RM_IMP:
492  post(home,x,c,b)));
493  break;
494  case RM_PMI:
496  post(home,x,c,b)));
497  break;
498  default: GECODE_NEVER;
499  }
500  } else {
501  switch (rm) {
502  case RM_EQV:
504  post(home,x,c,b)));
505  break;
506  case RM_IMP:
508  post(home,x,c,b)));
509  break;
510  case RM_PMI:
512  post(home,x,c,b)));
513  break;
514  default: GECODE_NEVER;
515  }
516  }
517  }
518 
519  void
520  post(Home home,
521  Term<IntView>* t, int n, IntRelType irt, int c, Reify r,
522  IntConLevel icl) {
523  Limits::check(c,"Int::linear");
524  long long int d = c;
525 
526  eliminate(t,n,d);
527 
528  Term<IntView> *t_p, *t_n;
529  int n_p, n_n, gcd=1;
530  bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n,gcd);
531 
532  rewrite(irt,d,t_p,n_p,t_n,n_n);
533 
534  // Divide by gcd
535  if (gcd > 1) {
536  switch (irt) {
537  case IRT_EQ:
538  if ((d % gcd) != 0) {
539  if (r.mode() != RM_PMI)
540  GECODE_ME_FAIL(BoolView(r.var()).zero(home));
541  return;
542  }
543  d /= gcd;
544  break;
545  case IRT_NQ:
546  if ((d % gcd) != 0) {
547  if (r.mode() != RM_IMP)
548  GECODE_ME_FAIL(BoolView(r.var()).one(home));
549  return;
550  }
551  d /= gcd;
552  break;
553  case IRT_LQ:
554  d = floor_div_xp(d,static_cast<long long int>(gcd));
555  break;
556  default: GECODE_NEVER;
557  }
558  }
559 
560  if (n == 0) {
561  bool fail = false;
562  switch (irt) {
563  case IRT_EQ: fail = (d != 0); break;
564  case IRT_NQ: fail = (d == 0); break;
565  case IRT_LQ: fail = (0 > d); break;
566  default: GECODE_NEVER;
567  }
568  if (fail) {
569  if (r.mode() != RM_PMI)
570  GECODE_ME_FAIL(BoolView(r.var()).zero(home));
571  } else {
572  if (r.mode() != RM_IMP)
573  GECODE_ME_FAIL(BoolView(r.var()).one(home));
574  }
575  return;
576  }
577 
578  bool is_ip = precision(t_p,n_p,t_n,n_n,d);
579 
580  if (is_unit && is_ip) {
581  c = static_cast<int>(d);
582  if (n == 1) {
583  switch (irt) {
584  case IRT_EQ:
585  if (n_p == 1) {
586  posteqint<BoolView>(home,t_p[0].x,c,r.var(),r.mode(),icl);
587  } else {
588  posteqint<BoolView>(home,t_p[0].x,-c,r.var(),r.mode(),icl);
589  }
590  break;
591  case IRT_NQ:
592  {
593  NegBoolView nb(r.var());
594  ReifyMode rm = r.mode();
595  switch (rm) {
596  case RM_IMP: rm = RM_PMI; break;
597  case RM_PMI: rm = RM_IMP; break;
598  default: ;
599  }
600  if (n_p == 1) {
601  posteqint<NegBoolView>(home,t_p[0].x,c,nb,rm,icl);
602  } else {
603  posteqint<NegBoolView>(home,t_p[0].x,-c,nb,rm,icl);
604  }
605  }
606  break;
607  case IRT_LQ:
608  if (n_p == 1) {
609  switch (r.mode()) {
610  case RM_EQV:
612  post(home,t_p[0].x,c,r.var())));
613  break;
614  case RM_IMP:
616  post(home,t_p[0].x,c,r.var())));
617  break;
618  case RM_PMI:
620  post(home,t_p[0].x,c,r.var())));
621  break;
622  default: GECODE_NEVER;
623  }
624  } else {
625  NegBoolView nb(r.var());
626  switch (r.mode()) {
627  case RM_EQV:
629  post(home,t_n[0].x,-c-1,nb)));
630  break;
631  case RM_IMP:
633  post(home,t_n[0].x,-c-1,nb)));
634  break;
635  case RM_PMI:
637  post(home,t_n[0].x,-c-1,nb)));
638  break;
639  default: GECODE_NEVER;
640  }
641  }
642  break;
643  default: GECODE_NEVER;
644  }
645  } else if (n == 2) {
646  switch (irt) {
647  case IRT_EQ:
648  switch (n_p) {
649  case 2:
650  switch (r.mode()) {
651  case RM_EQV:
653  post(home,t_p[0].x,t_p[1].x,c,r.var())));
654  break;
655  case RM_IMP:
657  post(home,t_p[0].x,t_p[1].x,c,r.var())));
658  break;
659  case RM_PMI:
661  post(home,t_p[0].x,t_p[1].x,c,r.var())));
662  break;
663  default: GECODE_NEVER;
664  }
665  break;
666  case 1:
667  switch (r.mode()) {
668  case RM_EQV:
670  post(home,t_p[0].x,MinusView(t_n[0].x),c,
671  r.var())));
672  break;
673  case RM_IMP:
675  post(home,t_p[0].x,MinusView(t_n[0].x),c,
676  r.var())));
677  break;
678  case RM_PMI:
680  post(home,t_p[0].x,MinusView(t_n[0].x),c,
681  r.var())));
682  break;
683  default: GECODE_NEVER;
684  }
685  break;
686  case 0:
687  switch (r.mode()) {
688  case RM_EQV:
690  post(home,t_n[0].x,t_n[1].x,-c,r.var())));
691  break;
692  case RM_IMP:
694  post(home,t_n[0].x,t_n[1].x,-c,r.var())));
695  break;
696  case RM_PMI:
698  post(home,t_n[0].x,t_n[1].x,-c,r.var())));
699  break;
700  default: GECODE_NEVER;
701  }
702  break;
703  default: GECODE_NEVER;
704  }
705  break;
706  case IRT_NQ:
707  {
708  NegBoolView nb(r.var());
709  switch (n_p) {
710  case 2:
711  switch (r.mode()) {
712  case RM_EQV:
714  post(home,t_p[0].x,t_p[1].x,c,nb)));
715  break;
716  case RM_IMP:
718  post(home,t_p[0].x,t_p[1].x,c,nb)));
719  break;
720  case RM_PMI:
722  post(home,t_p[0].x,t_p[1].x,c,nb)));
723  break;
724  default: GECODE_NEVER;
725  }
726  break;
727  case 1:
728  switch (r.mode()) {
729  case RM_EQV:
731  post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
732  break;
733  case RM_IMP:
735  post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
736  break;
737  case RM_PMI:
739  post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
740  break;
741  default: GECODE_NEVER;
742  }
743  break;
744  case 0:
745  switch (r.mode()) {
746  case RM_EQV:
748  post(home,t_p[0].x,t_p[1].x,-c,nb)));
749  break;
750  case RM_IMP:
752  post(home,t_p[0].x,t_p[1].x,-c,nb)));
753  break;
754  case RM_PMI:
756  post(home,t_p[0].x,t_p[1].x,-c,nb)));
757  break;
758  default: GECODE_NEVER;
759  }
760  break;
761  default: GECODE_NEVER;
762  }
763  }
764  break;
765  case IRT_LQ:
766  switch (n_p) {
767  case 2:
768  switch (r.mode()) {
769  case RM_EQV:
771  post(home,t_p[0].x,t_p[1].x,c,r.var())));
772  break;
773  case RM_IMP:
775  post(home,t_p[0].x,t_p[1].x,c,r.var())));
776  break;
777  case RM_PMI:
779  post(home,t_p[0].x,t_p[1].x,c,r.var())));
780  break;
781  default: GECODE_NEVER;
782  }
783  break;
784  case 1:
785  switch (r.mode()) {
786  case RM_EQV:
788  post(home,t_p[0].x,MinusView(t_n[0].x),c,
789  r.var())));
790  break;
791  case RM_IMP:
793  post(home,t_p[0].x,MinusView(t_n[0].x),c,
794  r.var())));
795  break;
796  case RM_PMI:
798  post(home,t_p[0].x,MinusView(t_n[0].x),c,
799  r.var())));
800  break;
801  default: GECODE_NEVER;
802  }
803  break;
804  case 0:
805  switch (r.mode()) {
806  case RM_EQV:
808  post(home,MinusView(t_n[0].x),
809  MinusView(t_n[1].x),c,r.var())));
810  break;
811  case RM_IMP:
813  post(home,MinusView(t_n[0].x),
814  MinusView(t_n[1].x),c,r.var())));
815  break;
816  case RM_PMI:
818  post(home,MinusView(t_n[0].x),
819  MinusView(t_n[1].x),c,r.var())));
820  break;
821  default: GECODE_NEVER;
822  }
823  break;
824  default: GECODE_NEVER;
825  }
826  break;
827  default: GECODE_NEVER;
828  }
829  } else {
830  ViewArray<IntView> x(home,n_p);
831  for (int i = n_p; i--; )
832  x[i] = t_p[i].x;
833  ViewArray<IntView> y(home,n_n);
834  for (int i = n_n; i--; )
835  y[i] = t_n[i].x;
836  post_nary<int,IntView>(home,x,y,irt,c,r);
837  }
838  } else if (is_ip) {
839  // Arbitrary coefficients with integer precision
840  c = static_cast<int>(d);
841  ViewArray<IntScaleView> x(home,n_p);
842  for (int i = n_p; i--; )
843  x[i] = IntScaleView(t_p[i].a,t_p[i].x);
844  ViewArray<IntScaleView> y(home,n_n);
845  for (int i = n_n; i--; )
846  y[i] = IntScaleView(t_n[i].a,t_n[i].x);
847  post_nary<int,IntScaleView>(home,x,y,irt,c,r);
848  } else {
849  // Arbitrary coefficients with long long precision
850  ViewArray<LLongScaleView> x(home,n_p);
851  for (int i = n_p; i--; )
852  x[i] = LLongScaleView(t_p[i].a,t_p[i].x);
853  ViewArray<LLongScaleView> y(home,n_n);
854  for (int i = n_n; i--; )
855  y[i] = LLongScaleView(t_n[i].a,t_n[i].x);
856  post_nary<long long int,LLongScaleView>(home,x,y,irt,d,r);
857  }
858  }
859 
860 }}}
861 
862 // STATISTICS: int-post
Scale integer view (template)
Definition: view.hpp:671
Propagator for bounds consistent binary linear disequality
Definition: linear.hh:201
NodeType t
Type of node.
Definition: bool-expr.cpp:234
void posteqint(Home home, IntView &x, int c, CtrlView b, ReifyMode rm, IntConLevel icl)
Definition: int-post.cpp:482
Propagator for bounds consistent n-ary linear equality
Definition: linear.hh:569
IntConLevel
Consistency levels for integer propagators.
Definition: int.hh:937
Inverse implication for reification.
Definition: int.hh:847
ReifyMode mode(void) const
Return reification mode.
Definition: reify.hpp:60
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:62
Binary domain consistent equality propagator.
Definition: rel.hh:71
Propagator for reified bounds consistent n-ary linear less or equal
Definition: linear.hh:741
BoolVar var(void) const
Return Boolean control variable.
Definition: reify.hpp:52
Negated Boolean view.
Definition: view.hpp:1503
bool one(const Gecode::FloatValArgs &a)
Check whether has only one coefficients.
Definition: linear.cpp:50
void post(Home home, Term< BoolView > *t, int n, IntRelType irt, IntView x, int c, IntConLevel)
Post propagator for linear constraint over Booleans.
Definition: bool-post.cpp:608
int a
Coefficient.
Definition: linear.hh:1313
Propagator for bounds consistent n-ary linear disequality
Definition: linear.hh:675
Propagator for domain consistent n-ary linear equality
Definition: linear.hh:600
Less or equal ( )
Definition: int.hh:906
Propagator for bounds consistent ternary linear equality
Definition: linear.hh:382
Reified less or equal with integer propagator.
Definition: rel.hh:549
Greater ( )
Definition: int.hh:909
Propagator for bounds consistent binary linear equality
Definition: linear.hh:134
const int max
Largest allowed integer value.
Definition: int.hh:113
Greater or equal ( )
Definition: int.hh:908
const int min
Smallest allowed integer value.
Definition: int.hh:115
Gecode::IntSet d(v, 7)
Propagator for bounds consistent ternary linear less or equal
Definition: linear.hh:452
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:904
IntRelType
Relation types for integers.
Definition: int.hh:903
NNF * r
Right subtree.
Definition: bool-expr.cpp:246
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
Propagator for bounds consistent binary linear less or equal
Definition: linear.hh:237
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:854
void rewrite(IntRelType &r, long long int &d)
Rewrite non-strict relations.
Definition: bool-post.cpp:74
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:641
Less ( )
Definition: int.hh:907
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:305
#define GECODE_INT_PL_BIN(CLASS)
Macro for posting binary special cases for linear constraints.
Definition: int-post.cpp:180
Reified bounds consistent equality with integer propagator.
Definition: rel.hh:397
Integer view for integer variables.
Definition: view.hpp:129
bool overflow_sub(int n, int m)
Check whether subtracting m from n would overflow.
Definition: limits.hpp:97
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:253
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:132
#define GECODE_INT_PL_TER(CLASS)
Macro for posting ternary special cases for linear constraints.
Definition: int-post.cpp:198
Propagator for reified bounds consistent binary linear equality
Definition: linear.hh:168
#define GECODE_ME_FAIL(me)
Check whether modification event me is failed, and fail space home.
Definition: macros.hpp:70
void fail(void)
Mark space as failed.
Definition: core.hpp:3437
Class for describing linear term .
Definition: linear.hh:1310
struct Gecode::@518::NNF::@57::@58 b
For binary nodes (and, or, eqv)
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:708
Implication for reification.
Definition: int.hh:840
Disequality ( )
Definition: int.hh:905
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:417
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:370
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:717
#define GECODE_ES_FAIL(es)
Check whether execution status es is failed, and fail space home.
Definition: macros.hpp:96
ReifyMode
Mode for reification.
Definition: int.hh:826
#define GECODE_NEVER
Assert that this command is never executed.
Definition: macros.hpp:60
struct Gecode::@518::NNF::@57::@59 a
For atomic nodes.
Domain propagation or consistency.
Definition: int.hh:940
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:833
Boolean view for Boolean variables.
Definition: view.hpp:1315