this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Christian Schulte <schulte@gecode.org>
5 * Tias Guns <tias.guns@cs.kuleuven.be>
6 *
7 * Copyright:
8 * Christian Schulte, 2002
9 * Tias Guns, 2009
10 *
11 * This file is part of Gecode, the generic constraint
12 * development environment:
13 * http://www.gecode.org
14 *
15 * Permission is hereby granted, free of charge, to any person obtaining
16 * a copy of this software and associated documentation files (the
17 * "Software"), to deal in the Software without restriction, including
18 * without limitation the rights to use, copy, modify, merge, publish,
19 * distribute, sublicense, and/or sell copies of the Software, and to
20 * permit persons to whom the Software is furnished to do so, subject to
21 * the following conditions:
22 *
23 * The above copyright notice and this permission notice shall be
24 * included in all copies or substantial portions of the Software.
25 *
26 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
27 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
28 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
29 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
30 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
31 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
32 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
33 *
34 */
35
36#include <gecode/int/linear.hh>
37#include <gecode/int/div.hh>
38
39namespace Gecode { namespace Int { namespace Linear {
40
41 /// Eliminate assigned views
42 forceinline void
43 eliminate(Term<BoolView>* t, int &n, long long int& d) {
44 for (int i=n; i--; )
45 if (t[i].x.one()) {
46 d -= t[i].a; t[i]=t[--n];
47 } else if (t[i].x.zero()) {
48 t[i]=t[--n];
49 }
50 Limits::check(d,"Int::linear");
51 }
52
53 /// Rewrite non-strict relations
54 forceinline void
55 rewrite(IntRelType &r, long long int &d) {
56 switch (r) {
57 case IRT_EQ: case IRT_NQ: case IRT_LQ: case IRT_GQ:
58 break;
59 case IRT_LE:
60 d--; r = IRT_LQ; break;
61 case IRT_GR:
62 d++; r = IRT_GQ; break;
63 default:
64 throw UnknownRelation("Int::linear");
65 }
66 }
67
68 forceinline void
69 post_pos_unit(Home home,
70 Term<BoolView>* t_p, int n_p,
71 IntRelType irt, IntView y, int c) {
72 switch (irt) {
73 case IRT_EQ:
74 {
75 ViewArray<BoolView> x(home,n_p);
76 for (int i=0; i<n_p; i++)
77 x[i]=t_p[i].x;
78 GECODE_ES_FAIL((EqBoolView<BoolView,IntView>
79 ::post(home,x,y,c)));
80 }
81 break;
82 case IRT_NQ:
83 {
84 ViewArray<BoolView> x(home,n_p);
85 for (int i=0; i<n_p; i++)
86 x[i]=t_p[i].x;
87 GECODE_ES_FAIL((NqBoolView<BoolView,IntView>
88 ::post(home,x,y,c)));
89 }
90 break;
91 case IRT_GQ:
92 {
93 ViewArray<BoolView> x(home,n_p);
94 for (int i=0; i<n_p; i++)
95 x[i]=t_p[i].x;
96 GECODE_ES_FAIL((GqBoolView<BoolView,IntView>
97 ::post(home,x,y,c)));
98 }
99 break;
100 case IRT_LQ:
101 {
102 ViewArray<NegBoolView> x(home,n_p);
103 for (int i=0; i<n_p; i++)
104 x[i]=NegBoolView(t_p[i].x);
105 MinusView z(y);
106 GECODE_ES_FAIL((GqBoolView<NegBoolView,MinusView>
107 ::post(home,x,z,n_p-c)));
108 }
109 break;
110 default: GECODE_NEVER;
111 }
112 }
113
114 forceinline void
115 post_pos_unit(Home home,
116 Term<BoolView>* t_p, int n_p,
117 IntRelType irt, ZeroIntView, int c) {
118 switch (irt) {
119 case IRT_EQ:
120 {
121 ViewArray<BoolView> x(home,n_p);
122 for (int i=0; i<n_p; i++)
123 x[i]=t_p[i].x;
124 GECODE_ES_FAIL((EqBoolInt<BoolView>::post(home,x,c)));
125 }
126 break;
127 case IRT_NQ:
128 {
129 ViewArray<BoolView> x(home,n_p);
130 for (int i=0; i<n_p; i++)
131 x[i]=t_p[i].x;
132 GECODE_ES_FAIL((NqBoolInt<BoolView>::post(home,x,c)));
133 }
134 break;
135 case IRT_GQ:
136 {
137 ViewArray<BoolView> x(home,n_p);
138 for (int i=0; i<n_p; i++)
139 x[i]=t_p[i].x;
140 GECODE_ES_FAIL((GqBoolInt<BoolView>::post(home,x,c)));
141 }
142 break;
143 case IRT_LQ:
144 {
145 ViewArray<NegBoolView> x(home,n_p);
146 for (int i=0; i<n_p; i++)
147 x[i]=NegBoolView(t_p[i].x);
148 GECODE_ES_FAIL((GqBoolInt<NegBoolView>::post(home,x,n_p-c)));
149 }
150 break;
151 default: GECODE_NEVER;
152 }
153 }
154
155 forceinline void
156 post_pos_unit(Home home,
157 Term<BoolView>* t_p, int n_p,
158 IntRelType irt, int c, Reify r,
159 IntPropLevel) {
160 switch (irt) {
161 case IRT_EQ:
162 {
163 ViewArray<BoolView> x(home,n_p);
164 for (int i=0; i<n_p; i++)
165 x[i]=t_p[i].x;
166 switch (r.mode()) {
167 case RM_EQV:
168 GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView,RM_EQV>::
169 post(home,x,c,r.var())));
170 break;
171 case RM_IMP:
172 GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView,RM_IMP>::
173 post(home,x,c,r.var())));
174 break;
175 case RM_PMI:
176 GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView,RM_PMI>::
177 post(home,x,c,r.var())));
178 break;
179 default: GECODE_NEVER;
180 }
181 }
182 break;
183 case IRT_NQ:
184 {
185 ViewArray<BoolView> x(home,n_p);
186 for (int i=0; i<n_p; i++)
187 x[i]=t_p[i].x;
188 NegBoolView nb(r.var());
189 switch (r.mode()) {
190 case RM_EQV:
191 GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView,RM_EQV>::
192 post(home,x,c,nb)));
193 break;
194 case RM_IMP:
195 GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView,RM_PMI>::
196 post(home,x,c,nb)));
197 break;
198 case RM_PMI:
199 GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView,RM_IMP>::
200 post(home,x,c,nb)));
201 break;
202 default: GECODE_NEVER;
203 }
204 }
205 break;
206 case IRT_GQ:
207 {
208 ViewArray<BoolView> x(home,n_p);
209 for (int i=0; i<n_p; i++)
210 x[i]=t_p[i].x;
211 switch (r.mode()) {
212 case RM_EQV:
213 GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView,RM_EQV>::
214 post(home,x,c,r.var())));
215 break;
216 case RM_IMP:
217 GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView,RM_IMP>::
218 post(home,x,c,r.var())));
219 break;
220 case RM_PMI:
221 GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView,RM_PMI>::
222 post(home,x,c,r.var())));
223 break;
224 default: GECODE_NEVER;
225 }
226 }
227 break;
228 case IRT_LQ:
229 {
230 ViewArray<NegBoolView> x(home,n_p);
231 for (int i=0; i<n_p; i++)
232 x[i]=NegBoolView(t_p[i].x);
233 switch (r.mode()) {
234 case RM_EQV:
235 GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView,RM_EQV>::
236 post(home,x,n_p-c,r.var())));
237 break;
238 case RM_IMP:
239 GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView,RM_IMP>::
240 post(home,x,n_p-c,r.var())));
241 break;
242 case RM_PMI:
243 GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView,RM_PMI>::
244 post(home,x,n_p-c,r.var())));
245 break;
246 default: GECODE_NEVER;
247 }
248 }
249 break;
250 default: GECODE_NEVER;
251 }
252 }
253
254 forceinline void
255 post_neg_unit(Home home,
256 Term<BoolView>* t_n, int n_n,
257 IntRelType irt, IntView y, int c) {
258 switch (irt) {
259 case IRT_EQ:
260 {
261 ViewArray<BoolView> x(home,n_n);
262 for (int i=0; i<n_n; i++)
263 x[i]=t_n[i].x;
264 MinusView z(y);
265 GECODE_ES_FAIL((EqBoolView<BoolView,MinusView>
266 ::post(home,x,z,-c)));
267 }
268 break;
269 case IRT_NQ:
270 {
271 ViewArray<BoolView> x(home,n_n);
272 for (int i=0; i<n_n; i++)
273 x[i]=t_n[i].x;
274 MinusView z(y);
275 GECODE_ES_FAIL((NqBoolView<BoolView,MinusView>
276 ::post(home,x,z,-c)));
277 }
278 break;
279 case IRT_GQ:
280 {
281 ViewArray<NegBoolView> x(home,n_n);
282 for (int i=0; i<n_n; i++)
283 x[i]=NegBoolView(t_n[i].x);
284 GECODE_ES_FAIL((GqBoolView<NegBoolView,IntView>
285 ::post(home,x,y,n_n+c)));
286 }
287 break;
288 case IRT_LQ:
289 {
290 ViewArray<BoolView> x(home,n_n);
291 for (int i=0; i<n_n; i++)
292 x[i]=t_n[i].x;
293 MinusView z(y);
294 GECODE_ES_FAIL((GqBoolView<BoolView,MinusView>
295 ::post(home,x,z,-c)));
296 }
297 break;
298 default: GECODE_NEVER;
299 }
300 }
301
302 forceinline void
303 post_neg_unit(Home home,
304 Term<BoolView>* t_n, int n_n,
305 IntRelType irt, ZeroIntView, int c) {
306 switch (irt) {
307 case IRT_EQ:
308 {
309 ViewArray<BoolView> x(home,n_n);
310 for (int i=0; i<n_n; i++)
311 x[i]=t_n[i].x;
312 GECODE_ES_FAIL((EqBoolInt<BoolView>::post(home,x,-c)));
313 }
314 break;
315 case IRT_NQ:
316 {
317 ViewArray<BoolView> x(home,n_n);
318 for (int i=0; i<n_n; i++)
319 x[i]=t_n[i].x;
320 GECODE_ES_FAIL((NqBoolInt<BoolView>::post(home,x,-c)));
321 }
322 break;
323 case IRT_GQ:
324 {
325 ViewArray<NegBoolView> x(home,n_n);
326 for (int i=0; i<n_n; i++)
327 x[i]=NegBoolView(t_n[i].x);
328 GECODE_ES_FAIL((GqBoolInt<NegBoolView>::post(home,x,n_n+c)));
329 }
330 break;
331 case IRT_LQ:
332 {
333 ViewArray<BoolView> x(home,n_n);
334 for (int i=0; i<n_n; i++)
335 x[i]=t_n[i].x;
336 GECODE_ES_FAIL((GqBoolInt<BoolView>::post(home,x,-c)));
337 }
338 break;
339 default: GECODE_NEVER;
340 }
341 }
342
343 forceinline void
344 post_neg_unit(Home home,
345 Term<BoolView>* t_n, int n_n,
346 IntRelType irt, int c, Reify r,
347 IntPropLevel) {
348 switch (irt) {
349 case IRT_EQ:
350 {
351 ViewArray<BoolView> x(home,n_n);
352 for (int i=0; i<n_n; i++)
353 x[i]=t_n[i].x;
354 switch (r.mode()) {
355 case RM_EQV:
356 GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView,RM_EQV>::
357 post(home,x,-c,r.var())));
358 break;
359 case RM_IMP:
360 GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView,RM_IMP>::
361 post(home,x,-c,r.var())));
362 break;
363 case RM_PMI:
364 GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView,RM_PMI>::
365 post(home,x,-c,r.var())));
366 break;
367 default: GECODE_NEVER;
368 }
369 }
370 break;
371 case IRT_NQ:
372 {
373 ViewArray<BoolView> x(home,n_n);
374 for (int i=0; i<n_n; i++)
375 x[i]=t_n[i].x;
376 NegBoolView nb(r.var());
377 switch (r.mode()) {
378 case RM_EQV:
379 GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView,RM_EQV>::
380 post(home,x,-c,nb)));
381 break;
382 case RM_IMP:
383 GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView,RM_PMI>::
384 post(home,x,-c,nb)));
385 break;
386 case RM_PMI:
387 GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView,RM_IMP>::
388 post(home,x,-c,nb)));
389 break;
390 default: GECODE_NEVER;
391 }
392 }
393 break;
394 case IRT_GQ:
395 {
396 ViewArray<NegBoolView> x(home,n_n);
397 for (int i=0; i<n_n; i++)
398 x[i]=NegBoolView(t_n[i].x);
399 switch (r.mode()) {
400 case RM_EQV:
401 GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView,RM_EQV>::
402 post(home,x,n_n+c,r.var())));
403 break;
404 case RM_IMP:
405 GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView,RM_IMP>::
406 post(home,x,n_n+c,r.var())));
407 break;
408 case RM_PMI:
409 GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView,RM_PMI>::
410 post(home,x,n_n+c,r.var())));
411 break;
412 default: GECODE_NEVER;
413 }
414 }
415 break;
416 case IRT_LQ:
417 {
418 ViewArray<BoolView> x(home,n_n);
419 for (int i=0; i<n_n; i++)
420 x[i]=t_n[i].x;
421 switch (r.mode()) {
422 case RM_EQV:
423 GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView,RM_EQV>::
424 post(home,x,-c,r.var())));
425 break;
426 case RM_IMP:
427 GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView,RM_IMP>::
428 post(home,x,-c,r.var())));
429 break;
430 case RM_PMI:
431 GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView,RM_PMI>::
432 post(home,x,-c,r.var())));
433 break;
434 default: GECODE_NEVER;
435 }
436 }
437 break;
438 default: GECODE_NEVER;
439 }
440 }
441
442 forceinline void
443 post_mixed(Home home,
444 Term<BoolView>* t_p, int n_p,
445 Term<BoolView>* t_n, int n_n,
446 IntRelType irt, IntView y, int c) {
447 ScaleBoolArray b_p(home,n_p);
448 {
449 ScaleBool* f=b_p.fst();
450 for (int i=0; i<n_p; i++) {
451 f[i].x=t_p[i].x; f[i].a=t_p[i].a;
452 }
453 }
454 ScaleBoolArray b_n(home,n_n);
455 {
456 ScaleBool* f=b_n.fst();
457 for (int i=0; i<n_n; i++) {
458 f[i].x=t_n[i].x; f[i].a=t_n[i].a;
459 }
460 }
461 switch (irt) {
462 case IRT_EQ:
463 GECODE_ES_FAIL((EqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView>
464 ::post(home,b_p,b_n,y,c)));
465 break;
466 case IRT_NQ:
467 GECODE_ES_FAIL((NqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView>
468 ::post(home,b_p,b_n,y,c)));
469 break;
470 case IRT_LQ:
471 GECODE_ES_FAIL((LqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView>
472 ::post(home,b_p,b_n,y,c)));
473 break;
474 case IRT_GQ:
475 {
476 MinusView m(y);
477 GECODE_ES_FAIL((LqBoolScale<ScaleBoolArray,ScaleBoolArray,MinusView>
478 ::post(home,b_n,b_p,m,-c)));
479 }
480 break;
481 default:
482 GECODE_NEVER;
483 }
484 }
485
486
487 forceinline void
488 post_mixed(Home home,
489 Term<BoolView>* t_p, int n_p,
490 Term<BoolView>* t_n, int n_n,
491 IntRelType irt, ZeroIntView y, int c) {
492 ScaleBoolArray b_p(home,n_p);
493 {
494 ScaleBool* f=b_p.fst();
495 for (int i=0; i<n_p; i++) {
496 f[i].x=t_p[i].x; f[i].a=t_p[i].a;
497 }
498 }
499 ScaleBoolArray b_n(home,n_n);
500 {
501 ScaleBool* f=b_n.fst();
502 for (int i=0; i<n_n; i++) {
503 f[i].x=t_n[i].x; f[i].a=t_n[i].a;
504 }
505 }
506 switch (irt) {
507 case IRT_EQ:
508 GECODE_ES_FAIL(
509 (EqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
510 ::post(home,b_p,b_n,y,c)));
511 break;
512 case IRT_NQ:
513 GECODE_ES_FAIL(
514 (NqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
515 ::post(home,b_p,b_n,y,c)));
516 break;
517 case IRT_LQ:
518 GECODE_ES_FAIL(
519 (LqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
520 ::post(home,b_p,b_n,y,c)));
521 break;
522 case IRT_GQ:
523 GECODE_ES_FAIL(
524 (LqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
525 ::post(home,b_n,b_p,y,-c)));
526 break;
527 default:
528 GECODE_NEVER;
529 }
530 }
531
532 template<class View>
533 forceinline void
534 post_all(Home home,
535 Term<BoolView>* t, int n,
536 IntRelType irt, View x, int c) {
537
538 Limits::check(c,"Int::linear");
539
540 long long int d = c;
541
542 eliminate(t,n,d);
543
544 Term<BoolView> *t_p, *t_n;
545 int n_p, n_n, gcd=0;
546 bool unit = normalize<BoolView>(t,n,t_p,n_p,t_n,n_n,gcd);
547
548 rewrite(irt,d);
549
550 c = static_cast<int>(d);
551
552 if (n == 0) {
553 switch (irt) {
554 case IRT_EQ: GECODE_ME_FAIL(x.eq(home,-c)); break;
555 case IRT_NQ: GECODE_ME_FAIL(x.nq(home,-c)); break;
556 case IRT_GQ: GECODE_ME_FAIL(x.lq(home,-c)); break;
557 case IRT_LQ: GECODE_ME_FAIL(x.gq(home,-c)); break;
558 default: GECODE_NEVER;
559 }
560 return;
561 }
562
563 // Check for overflow
564 {
565 long long int sl = static_cast<long long int>(x.max())+c;
566 long long int su = static_cast<long long int>(x.min())+c;
567 for (int i=0; i<n_p; i++)
568 su -= t_p[i].a;
569 for (int i=0; i<n_n; i++)
570 sl += t_n[i].a;
571 Limits::check(sl,"Int::linear");
572 Limits::check(su,"Int::linear");
573 }
574
575 if (unit && (n_n == 0)) {
576 /// All coefficients are 1
577 post_pos_unit(home,t_p,n_p,irt,x,c);
578 } else if (unit && (n_p == 0)) {
579 // All coefficients are -1
580 post_neg_unit(home,t_n,n_n,irt,x,c);
581 } else {
582 // Mixed coefficients
583 post_mixed(home,t_p,n_p,t_n,n_n,irt,x,c);
584 }
585 }
586
587
588 void
589 post(Home home,
590 Term<BoolView>* t, int n, IntRelType irt, IntView x, int c,
591 IntPropLevel) {
592 post_all(home,t,n,irt,x,c);
593 }
594
595 void
596 post(Home home,
597 Term<BoolView>* t, int n, IntRelType irt, int c,
598 IntPropLevel) {
599 ZeroIntView x;
600 post_all(home,t,n,irt,x,c);
601 }
602
603 void
604 post(Home home,
605 Term<BoolView>* t, int n, IntRelType irt, IntView x, Reify r,
606 IntPropLevel ipl) {
607 int l, u;
608 estimate(t,n,0,l,u);
609 IntVar z(home,l,u); IntView zv(z);
610 post_all(home,t,n,IRT_EQ,zv,0);
611 rel(home,z,irt,x,r,ipl);
612 }
613
614 void
615 post(Home home,
616 Term<BoolView>* t, int n, IntRelType irt, int c, Reify r,
617 IntPropLevel ipl) {
618
619 if (r.var().one()) {
620 if (r.mode() != RM_PMI)
621 post(home,t,n,irt,c,ipl);
622 return;
623 }
624 if (r.var().zero()) {
625 if (r.mode() != RM_IMP)
626 post(home,t,n,neg(irt),c,ipl);
627 return;
628 }
629
630 Limits::check(c,"Int::linear");
631
632 long long int d = c;
633
634 eliminate(t,n,d);
635
636 Term<BoolView> *t_p, *t_n;
637 int n_p, n_n, gcd=1;
638 bool unit = normalize<BoolView>(t,n,t_p,n_p,t_n,n_n,gcd);
639
640 rewrite(irt,d);
641
642 // Divide by gcd
643 if (gcd > 1) {
644 switch (irt) {
645 case IRT_EQ:
646 if ((d % gcd) != 0) {
647 if (r.mode() != RM_PMI)
648 GECODE_ME_FAIL(BoolView(r.var()).zero(home));
649 return;
650 }
651 d /= gcd;
652 break;
653 case IRT_NQ:
654 if ((d % gcd) == 0) {
655 if (r.mode() != RM_IMP)
656 GECODE_ME_FAIL(BoolView(r.var()).one(home));
657 return;
658 }
659 d /= gcd;
660 break;
661 case IRT_LQ:
662 d = floor_div_xp(d,static_cast<long long int>(gcd));
663 break;
664 case IRT_GQ:
665 d = ceil_div_xp(d,static_cast<long long int>(gcd));
666 break;
667 default: GECODE_NEVER;
668 }
669 }
670
671 c = static_cast<int>(d);
672
673 if (n == 0) {
674 bool fail = false;
675 switch (irt) {
676 case IRT_EQ: fail = (0 != c); break;
677 case IRT_NQ: fail = (0 == c); break;
678 case IRT_GQ: fail = (0 < c); break;
679 case IRT_LQ: fail = (0 > c); break;
680 default: GECODE_NEVER;
681 }
682 if (fail) {
683 if (r.mode() != RM_PMI)
684 GECODE_ME_FAIL(BoolView(r.var()).zero(home));
685 } else {
686 if (r.mode() != RM_IMP)
687 GECODE_ME_FAIL(BoolView(r.var()).one(home));
688 }
689 return;
690 }
691
692 // Check for overflow
693 {
694 long long int sl = c;
695 long long int su = c;
696 for (int i=0; i<n_p; i++)
697 su -= t_p[i].a;
698 for (int i=0; i<n_n; i++)
699 sl += t_n[i].a;
700 Limits::check(sl,"Int::linear");
701 Limits::check(su,"Int::linear");
702 }
703
704 if (unit && (n_n == 0)) {
705 /// All coefficients are 1
706 post_pos_unit(home,t_p,n_p,irt,c,r,ipl);
707 } else if (unit && (n_p == 0)) {
708 // All coefficients are -1
709 post_neg_unit(home,t_n,n_n,irt,c,r,ipl);
710 } else {
711 // Mixed coefficients
712 /*
713 * Denormalize: Make all t_n coefficients negative again
714 * (t_p and t_n are shared in t)
715 */
716 for (int i=0; i<n_n; i++)
717 t_n[i].a = -t_n[i].a;
718
719 // Note: still slow implementation
720 int l, u;
721 estimate(t,n,0,l,u);
722 IntVar z(home,l,u); IntView zv(z);
723 post_all(home,t,n,IRT_EQ,zv,0);
724 rel(home,z,irt,c,r,ipl);
725 }
726 }
727
728}}}
729
730// STATISTICS: int-post
731