Generated on Tue Feb 11 2025 17:33:26 for Gecode by doxygen 1.12.0
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
40namespace 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:
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:
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
392 for (int i=0; i<n_p; i++)
393 x[i] = LLongScaleView(t_p[i].a,t_p[i].x);
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 {
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
849 for (int i=0; i<n_p; i++)
850 x[i] = LLongScaleView(t_p[i].a,t_p[i].x);
852 for (int i=0; i<n_n; i++)
853 y[i] = LLongScaleView(t_n[i].a,t_n[i].x);
855 }
856 }
857
858}}}
859
860// STATISTICS: int-post
struct Gecode::@603::NNF::@65::@66 b
For binary nodes (and, or, eqv)
NodeType t
Type of node.
int n
Number of negative literals for node type.
struct Gecode::@603::NNF::@65::@67 a
For atomic nodes.
Home class for posting propagators
Definition core.hpp:856
void fail(void)
Mark space as failed.
Definition core.hpp:4039
Boolean view for Boolean variables.
Definition view.hpp:1380
bool zero(void) const
Test whether view is assigned to be zero.
Definition bool.hpp:220
bool one(void) const
Test whether view is assigned to be one.
Definition bool.hpp:224
Integer view for integer variables.
Definition view.hpp:129
Propagator for domain consistent n-ary linear equality
Definition linear.hh:609
Propagator for bounds consistent binary linear equality
Definition linear.hh:134
Propagator for bounds consistent ternary linear equality
Definition linear.hh:384
Propagator for bounds consistent n-ary linear equality
Definition linear.hh:577
Propagator for bounds consistent binary linear less or equal
Definition linear.hh:237
Propagator for bounds consistent ternary linear less or equal
Definition linear.hh:454
Propagator for bounds consistent n-ary linear less or equal
Definition linear.hh:716
Propagator for bounds consistent binary linear disequality
Definition linear.hh:201
Propagator for bounds consistent ternary linear disquality
Definition linear.hh:419
Propagator for bounds consistent n-ary linear disequality
Definition linear.hh:683
Propagator for reified bounds consistent binary linear equality
Definition linear.hh:168
Propagator for reified bounds consistent n-ary linear equality
Definition linear.hh:649
Propagator for reified bounds consistent binary linear less or equal
Definition linear.hh:305
Propagator for reified bounds consistent n-ary linear less or equal
Definition linear.hh:749
Class for describing linear term .
Definition linear.hh:1336
int a
Coefficient.
Definition linear.hh:1339
Minus integer view.
Definition view.hpp:282
Negated Boolean view.
Definition view.hpp:1574
Offset integer view.
Definition view.hpp:443
Exception: Value out of limits
Definition exception.hpp:44
Binary domain consistent equality propagator.
Definition rel.hh:68
Reified bounds consistent equality with integer propagator.
Definition rel.hh:425
Reified domain consistent equality with integer propagator.
Definition rel.hh:398
Reified less or equal with integer propagator.
Definition rel.hh:575
Exception: Unknown relation passed as argument
Definition exception.hpp:87
Reification specification.
Definition int.hh:876
bool assigned(void) const
Test whether view is assigned.
Definition var.hpp:111
View arrays.
Definition array.hpp:253
void post(Home home, Term< IntView > *t, int n, IntRelType irt, int c, IntPropLevel=IPL_DEF)
Post propagator for linear constraint over integers.
Definition int-post.cpp:219
#define GECODE_ES_FAIL(es)
Check whether execution status es is failed, and fail space home.
Definition macros.hpp:103
#define GECODE_ME_FAIL(me)
Check whether modification event me is failed, and fail space home.
Definition macros.hpp:77
IntRelType
Relation types for integers.
Definition int.hh:925
ReifyMode
Mode for reification.
Definition int.hh:848
IntPropLevel
Propagation levels for integer propagators.
Definition int.hh:974
@ IRT_EQ
Equality ( )
Definition int.hh:926
@ IRT_NQ
Disequality ( )
Definition int.hh:927
@ IRT_GQ
Greater or equal ( )
Definition int.hh:930
@ IRT_LE
Less ( )
Definition int.hh:929
@ IRT_GR
Greater ( )
Definition int.hh:931
@ IRT_LQ
Less or equal ( )
Definition int.hh:928
@ RM_IMP
Implication for reification.
Definition int.hh:862
@ RM_PMI
Inverse implication for reification.
Definition int.hh:869
@ RM_EQV
Equivalence for reification (default)
Definition int.hh:855
@ IPL_DOM
Domain propagation Options: basic versus advanced propagation.
Definition int.hh:979
@ IPL_DEF
Simple propagation levels.
Definition int.hh:976
#define GECODE_INT_PL_TER(CLASS)
Macro for posting ternary special cases for linear constraints.
Definition int-post.cpp:194
#define GECODE_INT_PL_BIN(CLASS)
Macro for posting binary special cases for linear constraints.
Definition int-post.cpp:176
bool overflow_add(int n, int m)
Check whether adding n and m would overflow.
Definition limits.hpp:79
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
const int min
Smallest allowed integer value.
Definition int.hh:118
const int max
Largest allowed integer value.
Definition int.hh:116
bool overflow_sub(int n, int m)
Check whether subtracting m from n would overflow.
Definition limits.hpp:93
void eliminate(Term< BoolView > *t, int &n, long long int &d)
Eliminate assigned views.
Definition bool-post.cpp:43
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
void posteqint(Home home, IntView &x, int c, CtrlView b, ReifyMode rm, IntPropLevel ipl)
Definition int-post.cpp:480
void rewrite(IntRelType &r, long long int &d)
Rewrite non-strict relations.
Definition bool-post.cpp:55
int gcd(int a, int b)
Compute the greatest common divisor of a and b.
Definition post.hpp:89
bool normalize(Term< View > *t, int &n, Term< View > *&t_p, int &n_p, Term< View > *&t_n, int &n_n, int &g)
Normalize linear integer constraints.
Definition post.hpp:126
void post_nary(Home home, ViewArray< View > &x, ViewArray< View > &y, IntRelType irt, Val c)
Posting n-ary propagators.
Definition int-post.cpp:158
IntType floor_div_xp(IntType x, IntType y)
Compute where y is non-negative.
Definition div.hpp:75
Gecode toplevel namespace
Post propagator for SetVar SetOpType SetVar SetRelType r
Definition set.hh:767
IntPropLevel vbd(IntPropLevel ipl)
Extract value, bounds, or domain propagation from propagation level.
Definition ipl.hpp:37
Post propagator for SetVar SetOpType SetVar y
Definition set.hh:767
Post propagator for SetVar x
Definition set.hh:767
#define forceinline
Definition config.hpp:187
#define GECODE_NEVER
Assert that this command is never executed.
Definition macros.hpp:56