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 *
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 <gecode/int/bool.hh>
35#include <gecode/int/rel.hh>
36
37namespace Gecode {
38
39 void
40 rel(Home home, BoolVar x0, IntRelType irt, BoolVar x1, IntPropLevel) {
41 using namespace Int;
42 GECODE_POST;
43 switch (irt) {
44 case IRT_EQ:
45 GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>
46 ::post(home,x0,x1)));
47 break;
48 case IRT_NQ:
49 {
50 NegBoolView n1(x1);
51 GECODE_ES_FAIL((Bool::Eq<BoolView,NegBoolView>
52 ::post(home,x0,n1)));
53 }
54 break;
55 case IRT_GQ:
56 GECODE_ES_FAIL(Bool::Lq<BoolView>::post(home,x1,x0));
57 break;
58 case IRT_LQ:
59 GECODE_ES_FAIL(Bool::Lq<BoolView>::post(home,x0,x1));
60 break;
61 case IRT_GR:
62 GECODE_ES_FAIL(Bool::Le<BoolView>::post(home,x1,x0));
63 break;
64 case IRT_LE:
65 GECODE_ES_FAIL(Bool::Le<BoolView>::post(home,x0,x1));
66 break;
67 default:
68 throw UnknownRelation("Int::rel");
69 }
70 }
71
72 void
73 rel(Home home, BoolVar x0, IntRelType irt, int n, IntPropLevel) {
74 using namespace Int;
75 GECODE_POST;
76 BoolView x(x0);
77 if (n == 0) {
78 switch (irt) {
79 case IRT_LQ:
80 case IRT_EQ:
81 GECODE_ME_FAIL(x.zero(home)); break;
82 case IRT_NQ:
83 case IRT_GR:
84 GECODE_ME_FAIL(x.one(home)); break;
85 case IRT_LE:
86 home.fail(); break;
87 case IRT_GQ:
88 break;
89 default:
90 throw UnknownRelation("Int::rel");
91 }
92 } else if (n == 1) {
93 switch (irt) {
94 case IRT_GQ:
95 case IRT_EQ:
96 GECODE_ME_FAIL(x.one(home)); break;
97 case IRT_NQ:
98 case IRT_LE:
99 GECODE_ME_FAIL(x.zero(home)); break;
100 case IRT_GR:
101 home.fail(); break;
102 case IRT_LQ:
103 break;
104 default:
105 throw UnknownRelation("Int::rel");
106 }
107 } else {
108 throw NotZeroOne("Int::rel");
109 }
110 }
111
112 void
113 rel(Home home, BoolVar x0, IntRelType irt, BoolVar x1, Reify r,
114 IntPropLevel) {
115 using namespace Int;
116 GECODE_POST;
117 switch (irt) {
118 case IRT_EQ:
119 switch (r.mode()) {
120 case RM_EQV:
121 GECODE_ES_FAIL((Bool::Eqv<BoolView,BoolView,BoolView>
122 ::post(home,x0,x1,r.var())));
123 break;
124 case RM_IMP:
125 GECODE_ES_FAIL((Rel::ReEqBnd<BoolView,BoolView,RM_IMP>
126 ::post(home,x0,x1,r.var())));
127 break;
128 case RM_PMI:
129 GECODE_ES_FAIL((Rel::ReEqBnd<BoolView,BoolView,RM_PMI>
130 ::post(home,x0,x1,r.var())));
131 break;
132 default: throw UnknownReifyMode("Int::rel");
133 }
134 break;
135 case IRT_NQ:
136 {
137 NegBoolView nr(r.var());
138 switch (r.mode()) {
139 case RM_EQV:
140 GECODE_ES_FAIL((Bool::Eqv<BoolView,BoolView,NegBoolView>
141 ::post(home,x0,x1,nr)));
142 break;
143 case RM_IMP:
144 GECODE_ES_FAIL((Rel::ReEqBnd<BoolView,NegBoolView,RM_PMI>
145 ::post(home,x0,x1,nr)));
146 break;
147 case RM_PMI:
148 GECODE_ES_FAIL((Rel::ReEqBnd<BoolView,NegBoolView,RM_IMP>
149 ::post(home,x0,x1,nr)));
150 break;
151 default: throw UnknownReifyMode("Int::rel");
152 }
153 }
154 break;
155 case IRT_GQ:
156 std::swap(x0,x1); // Fall through
157 case IRT_LQ:
158 switch (r.mode()) {
159 case RM_EQV:
160 {
161 NegBoolView n0(x0);
162 GECODE_ES_FAIL((Bool::Or<NegBoolView,BoolView,BoolView>
163 ::post(home,n0,x1,r.var())));
164 }
165 break;
166 case RM_IMP:
167 GECODE_ES_FAIL((Rel::ReLq<BoolView,BoolView,RM_IMP>
168 ::post(home,x0,x1,r.var())));
169 break;
170 case RM_PMI:
171 GECODE_ES_FAIL((Rel::ReLq<BoolView,BoolView,RM_PMI>
172 ::post(home,x0,x1,r.var())));
173 break;
174 default: throw UnknownReifyMode("Int::rel");
175 }
176 break;
177 case IRT_LE:
178 std::swap(x0,x1); // Fall through
179 case IRT_GR:
180 {
181 NegBoolView nr(r.var());
182 switch (r.mode()) {
183 case RM_EQV:
184 {
185 NegBoolView n0(x0);
186 GECODE_ES_FAIL((Bool::Or<NegBoolView,BoolView,NegBoolView>
187 ::post(home,n0,x1,nr)));
188 }
189 break;
190 case RM_IMP:
191 GECODE_ES_FAIL((Rel::ReLq<BoolView,NegBoolView,RM_PMI>
192 ::post(home,x0,x1,nr)));
193 break;
194 case RM_PMI:
195 GECODE_ES_FAIL((Rel::ReLq<BoolView,NegBoolView,RM_IMP>
196 ::post(home,x0,x1,nr)));
197 break;
198 default: throw UnknownReifyMode("Int::rel");
199 }
200 }
201 break;
202 default:
203 throw UnknownRelation("Int::rel");
204 }
205 }
206
207 void
208 rel(Home home, BoolVar x0, IntRelType irt, int n, Reify r,
209 IntPropLevel) {
210 using namespace Int;
211 GECODE_POST;
212 BoolView x(x0);
213 BoolView y(r.var());
214 if (n == 0) {
215 switch (irt) {
216 case IRT_LQ:
217 case IRT_EQ:
218 switch (r.mode()) {
219 case RM_EQV:
220 {
221 NegBoolView ny(y);
222 GECODE_ES_FAIL((Bool::Eq<BoolView,NegBoolView>
223 ::post(home,x,ny)));
224 }
225 break;
226 case RM_IMP:
227 {
228 NegBoolView nx(x); NegBoolView ny(y);
229 GECODE_ES_FAIL((Bool::BinOrTrue<NegBoolView,NegBoolView>
230 ::post(home,nx,ny)));
231 }
232 break;
233 case RM_PMI:
234 GECODE_ES_FAIL((Bool::BinOrTrue<BoolView,BoolView>
235 ::post(home,x,y)));
236 break;
237 default: throw UnknownReifyMode("Int::rel");
238 }
239 break;
240 case IRT_NQ:
241 case IRT_GR:
242 switch (r.mode()) {
243 case RM_EQV:
244 GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>
245 ::post(home,x,y)));
246 break;
247 case RM_IMP:
248 {
249 NegBoolView ny(y);
250 GECODE_ES_FAIL((Bool::BinOrTrue<BoolView,NegBoolView>
251 ::post(home,x,ny)));
252 }
253 break;
254 case RM_PMI:
255 {
256 NegBoolView nx(x);
257 GECODE_ES_FAIL((Bool::BinOrTrue<NegBoolView,BoolView>
258 ::post(home,nx,y)));
259 }
260 break;
261 default: throw UnknownReifyMode("Int::rel");
262 }
263 break;
264 case IRT_LE:
265 switch (r.mode()) {
266 case RM_EQV:
267 case RM_IMP:
268 GECODE_ME_FAIL(y.zero(home));
269 break;
270 case RM_PMI:
271 break;
272 default: throw UnknownReifyMode("Int::rel");
273 }
274 break;
275 case IRT_GQ:
276 switch (r.mode()) {
277 case RM_EQV:
278 case RM_PMI:
279 GECODE_ME_FAIL(y.one(home));
280 break;
281 case RM_IMP:
282 break;
283 default: throw UnknownReifyMode("Int::rel");
284 }
285 break;
286 default:
287 throw UnknownRelation("Int::rel");
288 }
289 } else if (n == 1) {
290 switch (irt) {
291 case IRT_NQ:
292 case IRT_LE:
293 switch (r.mode()) {
294 case RM_EQV:
295 {
296 NegBoolView ny(y);
297 GECODE_ES_FAIL((Bool::Eq<BoolView,NegBoolView>
298 ::post(home,x,ny)));
299 }
300 break;
301 case RM_IMP:
302 {
303 NegBoolView nx(x); NegBoolView ny(y);
304 GECODE_ES_FAIL((Bool::BinOrTrue<NegBoolView,NegBoolView>
305 ::post(home,nx,ny)));
306 }
307 break;
308 case RM_PMI:
309 GECODE_ES_FAIL((Bool::BinOrTrue<BoolView,BoolView>
310 ::post(home,x,y)));
311 break;
312 default: throw UnknownReifyMode("Int::rel");
313 }
314 break;
315 case IRT_EQ:
316 case IRT_GQ:
317 switch (r.mode()) {
318 case RM_EQV:
319 GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>
320 ::post(home,x,y)));
321 break;
322 case RM_IMP:
323 {
324 NegBoolView ny(y);
325 GECODE_ES_FAIL((Bool::BinOrTrue<BoolView,NegBoolView>
326 ::post(home,x,ny)));
327 }
328 break;
329 case RM_PMI:
330 {
331 NegBoolView nx(x);
332 GECODE_ES_FAIL((Bool::BinOrTrue<NegBoolView,BoolView>
333 ::post(home,nx,y)));
334 }
335 break;
336 default: throw UnknownReifyMode("Int::rel");
337 }
338 break;
339 case IRT_GR:
340 switch (r.mode()) {
341 case RM_EQV:
342 case RM_IMP:
343 GECODE_ME_FAIL(y.zero(home));
344 break;
345 case RM_PMI:
346 break;
347 default: throw UnknownReifyMode("Int::rel");
348 }
349 break;
350 case IRT_LQ:
351 switch (r.mode()) {
352 case RM_EQV:
353 case RM_PMI:
354 GECODE_ME_FAIL(y.one(home));
355 break;
356 case RM_IMP:
357 break;
358 default: throw UnknownReifyMode("Int::rel");
359 }
360 break;
361 default:
362 throw UnknownRelation("Int::rel");
363 }
364 } else {
365 throw NotZeroOne("Int::rel");
366 }
367 }
368
369 void
370 rel(Home home, const BoolVarArgs& x, IntRelType irt, BoolVar y,
371 IntPropLevel) {
372 using namespace Int;
373 GECODE_POST;
374 switch (irt) {
375 case IRT_EQ:
376 for (int i=0; i<x.size(); i++) {
377 GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>
378 ::post(home,x[i],y)));
379 }
380 break;
381 case IRT_NQ:
382 {
383 NegBoolView n(y);
384 for (int i=0; i<x.size(); i++) {
385 GECODE_ES_FAIL((Bool::Eq<BoolView,NegBoolView>
386 ::post(home,x[i],n)));
387 }
388 }
389 break;
390 case IRT_GQ:
391 for (int i=0; i<x.size(); i++) {
392 GECODE_ES_FAIL(Bool::Lq<BoolView>::post(home,y,x[i]));
393 }
394 break;
395 case IRT_LQ:
396 for (int i=0; i<x.size(); i++) {
397 GECODE_ES_FAIL(Bool::Lq<BoolView>::post(home,x[i],y));
398 }
399 break;
400 case IRT_GR:
401 for (int i=0; i<x.size(); i++) {
402 GECODE_ES_FAIL(Bool::Le<BoolView>::post(home,y,x[i]));
403 }
404 break;
405 case IRT_LE:
406 for (int i=0; i<x.size(); i++) {
407 GECODE_ES_FAIL(Bool::Le<BoolView>::post(home,x[i],y));
408 }
409 break;
410 default:
411 throw UnknownRelation("Int::rel");
412 }
413 }
414
415 void
416 rel(Home home, const BoolVarArgs& x, IntRelType irt, int n,
417 IntPropLevel) {
418 using namespace Int;
419 GECODE_POST;
420 if (n == 0) {
421 switch (irt) {
422 case IRT_LQ:
423 case IRT_EQ:
424 for (int i=0; i<x.size(); i++) {
425 BoolView xi(x[i]); GECODE_ME_FAIL(xi.zero(home));
426 }
427 break;
428 case IRT_NQ:
429 case IRT_GR:
430 for (int i=0; i<x.size(); i++) {
431 BoolView xi(x[i]); GECODE_ME_FAIL(xi.one(home));
432 }
433 break;
434 case IRT_LE:
435 home.fail(); break;
436 case IRT_GQ:
437 break;
438 default:
439 throw UnknownRelation("Int::rel");
440 }
441 } else if (n == 1) {
442 switch (irt) {
443 case IRT_GQ:
444 case IRT_EQ:
445 for (int i=0; i<x.size(); i++) {
446 BoolView xi(x[i]); GECODE_ME_FAIL(xi.one(home));
447 }
448 break;
449 case IRT_NQ:
450 case IRT_LE:
451 for (int i=0; i<x.size(); i++) {
452 BoolView xi(x[i]); GECODE_ME_FAIL(xi.zero(home));
453 }
454 break;
455 case IRT_GR:
456 home.fail(); break;
457 case IRT_LQ:
458 break;
459 default:
460 throw UnknownRelation("Int::rel");
461 }
462 } else {
463 throw NotZeroOne("Int::rel");
464 }
465 }
466
467 void
468 rel(Home home, const BoolVarArgs& x, IntRelType irt, IntPropLevel) {
469 using namespace Int;
470 GECODE_POST;
471 if ((irt != IRT_NQ) && (x.size() < 2))
472 return;
473
474 switch (irt) {
475 case IRT_EQ:
476 {
477 ViewArray<BoolView> y(home,x);
478 GECODE_ES_FAIL(Bool::NaryEq<BoolView>::post(home,y));
479 }
480 break;
481 case IRT_NQ:
482 {
483 ViewArray<BoolView> y(home,x);
484 GECODE_ES_FAIL((Rel::NaryNq<BoolView>::post(home,y)));
485 }
486 break;
487 case IRT_LE:
488 if (x.size() == 2) {
489 GECODE_ES_FAIL(Bool::Le<BoolView>::post(home,x[0],x[1]));
490 } else {
491 home.fail();
492 }
493 break;
494 case IRT_LQ:
495 {
496 ViewArray<BoolView> y(home,x);
497 GECODE_ES_FAIL(Bool::NaryLq<BoolView>::post(home,y));
498 }
499 break;
500 case IRT_GR:
501 if (x.size() == 2) {
502 GECODE_ES_FAIL(Bool::Le<BoolView>::post(home,x[1],x[0]));
503 } else {
504 home.fail();
505 }
506 break;
507 case IRT_GQ:
508 {
509 ViewArray<BoolView> y(home,x.size());
510 for (int i=0; i<x.size(); i++)
511 y[i] = x[x.size()-1-i];
512 GECODE_ES_FAIL(Bool::NaryLq<BoolView>::post(home,y));
513 }
514 break;
515 default:
516 throw UnknownRelation("Int::rel");
517 }
518 }
519
520 void
521 rel(Home home, const BoolVarArgs& x, IntRelType irt, const BoolVarArgs& y,
522 IntPropLevel) {
523 using namespace Int;
524 GECODE_POST;
525
526 switch (irt) {
527 case IRT_GR:
528 {
529 ViewArray<BoolView> xv(home,x), yv(home,y);
530 GECODE_ES_FAIL((Rel::LexLqLe<BoolView,BoolView>
531 ::post(home,yv,xv,true)));
532 }
533 break;
534 case IRT_LE:
535 {
536 ViewArray<BoolView> xv(home,x), yv(home,y);
537 GECODE_ES_FAIL((Rel::LexLqLe<BoolView,BoolView>
538 ::post(home,xv,yv,true)));
539 }
540 break;
541 case IRT_GQ:
542 {
543 ViewArray<BoolView> xv(home,x), yv(home,y);
544 GECODE_ES_FAIL((Rel::LexLqLe<BoolView,BoolView>
545 ::post(home,yv,xv,false)));
546 }
547 break;
548 case IRT_LQ:
549 {
550 ViewArray<BoolView> xv(home,x), yv(home,y);
551 GECODE_ES_FAIL((Rel::LexLqLe<BoolView,BoolView>
552 ::post(home,xv,yv,false)));
553 }
554 break;
555 case IRT_EQ:
556 for (int i=0; i<x.size(); i++) {
557 GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>
558 ::post(home,x[i],y[i])));
559 }
560 break;
561 case IRT_NQ:
562 {
563 ViewArray<BoolView> xv(home,x), yv(home,y);
564 GECODE_ES_FAIL((Rel::LexNq<BoolView,BoolView>
565 ::post(home,xv,yv)));
566 }
567 break;
568 default:
569 throw UnknownRelation("Int::rel");
570 }
571 }
572
573 namespace {
574
575 /// Return view array
576 ViewArray<Int::ConstIntView>
577 viewarray(Space& home, const IntArgs& x) {
578 ViewArray<Int::ConstIntView> xv(home, x.size());
579 for (int i=0; i<x.size(); i++) {
580 if ((x[i] != 0) && (x[i] != 1))
581 throw Int::NotZeroOne("Int::rel");
582 xv[i] = Int::ConstIntView(x[i]);
583 }
584 return xv;
585 }
586
587 }
588
589 void
590 rel(Home home, const BoolVarArgs& x, IntRelType irt, const IntArgs& y,
591 IntPropLevel) {
592 using namespace Int;
593 GECODE_POST;
594
595 switch (irt) {
596 case IRT_GR:
597 {
598 ViewArray<BoolView> xv(home,x);
599 ViewArray<ConstIntView> yv(viewarray(home,y));
600 GECODE_ES_FAIL((Rel::LexLqLe<ConstIntView,BoolView>
601 ::post(home,yv,xv,true)));
602 }
603 break;
604 case IRT_LE:
605 {
606 ViewArray<BoolView> xv(home,x);
607 ViewArray<ConstIntView> yv(viewarray(home,y));
608 GECODE_ES_FAIL((Rel::LexLqLe<BoolView,ConstIntView>
609 ::post(home,xv,yv,true)));
610 }
611 break;
612 case IRT_GQ:
613 {
614 ViewArray<BoolView> xv(home,x);
615 ViewArray<ConstIntView> yv(viewarray(home,y));
616 GECODE_ES_FAIL((Rel::LexLqLe<ConstIntView,BoolView>
617 ::post(home,yv,xv,false)));
618 }
619 break;
620 case IRT_LQ:
621 {
622 ViewArray<BoolView> xv(home,x);
623 ViewArray<ConstIntView> yv(viewarray(home,y));
624 GECODE_ES_FAIL((Rel::LexLqLe<BoolView,ConstIntView>
625 ::post(home,xv,yv,false)));
626 }
627 break;
628 case IRT_EQ:
629 if (x.size() != y.size()) {
630 home.fail();
631 } else {
632 for (int i=0; i<x.size(); i++)
633 GECODE_ME_FAIL(BoolView(x[i]).eq(home,y[i]));
634 }
635 break;
636 case IRT_NQ:
637 {
638 ViewArray<BoolView> xv(home,x);
639 ViewArray<ConstIntView> yv(viewarray(home,y));
640 GECODE_ES_FAIL((Rel::LexNq<BoolView,ConstIntView>
641 ::post(home,xv,yv)));
642 }
643 break;
644 default:
645 throw UnknownRelation("Int::rel");
646 }
647 }
648
649 void
650 rel(Home home, const IntArgs& x, IntRelType irt, const BoolVarArgs& y,
651 IntPropLevel ipl) {
652 rel(home,y,irt,x,ipl);
653 }
654
655 void
656 rel(Home home, BoolVar x0, BoolOpType o, BoolVar x1, BoolVar x2,
657 IntPropLevel) {
658 using namespace Int;
659 GECODE_POST;
660 switch (o) {
661 case BOT_AND:
662 {
663 NegBoolView n0(x0); NegBoolView n1(x1); NegBoolView n2(x2);
664 GECODE_ES_FAIL((Bool::Or<NegBoolView,NegBoolView,NegBoolView>
665 ::post(home,n0,n1,n2)));
666 }
667 break;
668 case BOT_OR:
669 GECODE_ES_FAIL((Bool::Or<BoolView,BoolView,BoolView>
670 ::post(home,x0,x1,x2)));
671 break;
672 case BOT_IMP:
673 {
674 NegBoolView n0(x0);
675 GECODE_ES_FAIL((Bool::Or<NegBoolView,BoolView,BoolView>
676 ::post(home,n0,x1,x2)));
677 }
678 break;
679 case BOT_EQV:
680 GECODE_ES_FAIL((Bool::Eqv<BoolView,BoolView,BoolView>
681 ::post(home,x0,x1,x2)));
682 break;
683 case BOT_XOR:
684 {
685 NegBoolView n2(x2);
686 GECODE_ES_FAIL((Bool::Eqv<BoolView,BoolView,NegBoolView>
687 ::post(home,x0,x1,n2)));
688 }
689 break;
690 default:
691 throw UnknownOperation("Int::rel");
692 }
693 }
694
695 void
696 rel(Home home, BoolVar x0, BoolOpType o, BoolVar x1, int n,
697 IntPropLevel) {
698 using namespace Int;
699 GECODE_POST;
700 if (n == 0) {
701 switch (o) {
702 case BOT_AND:
703 {
704 NegBoolView n0(x0); NegBoolView n1(x1);
705 GECODE_ES_FAIL((Bool::BinOrTrue<NegBoolView,NegBoolView>
706 ::post(home,n0,n1)));
707 }
708 break;
709 case BOT_OR:
710 {
711 BoolView b0(x0); BoolView b1(x1);
712 GECODE_ME_FAIL(b0.zero(home));
713 GECODE_ME_FAIL(b1.zero(home));
714 }
715 break;
716 case BOT_IMP:
717 {
718 BoolView b0(x0); BoolView b1(x1);
719 GECODE_ME_FAIL(b0.one(home));
720 GECODE_ME_FAIL(b1.zero(home));
721 }
722 break;
723 case BOT_EQV:
724 {
725 NegBoolView n0(x0);
726 GECODE_ES_FAIL((Bool::Eq<NegBoolView,BoolView>::post(home,n0,x1)));
727 }
728 break;
729 case BOT_XOR:
730 GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>::post(home,x0,x1)));
731 break;
732 default:
733 throw UnknownOperation("Int::rel");
734 }
735 } else if (n == 1) {
736 switch (o) {
737 case BOT_AND:
738 {
739 BoolView b0(x0); BoolView b1(x1);
740 GECODE_ME_FAIL(b0.one(home));
741 GECODE_ME_FAIL(b1.one(home));
742 }
743 break;
744 case BOT_OR:
745 GECODE_ES_FAIL((Bool::BinOrTrue<BoolView,BoolView>::post(home,x0,x1)));
746 break;
747 case BOT_IMP:
748 {
749 NegBoolView n0(x0);
750 GECODE_ES_FAIL((Bool::BinOrTrue<NegBoolView,BoolView>
751 ::post(home,n0,x1)));
752 }
753 break;
754 case BOT_EQV:
755 GECODE_ES_FAIL((Bool::Eq<BoolView,BoolView>::post(home,x0,x1)));
756 break;
757 case BOT_XOR:
758 {
759 NegBoolView n0(x0);
760 GECODE_ES_FAIL((Bool::Eq<NegBoolView,BoolView>::post(home,n0,x1)));
761 }
762 break;
763 default:
764 throw UnknownOperation("Int::rel");
765 }
766 } else {
767 throw NotZeroOne("Int::rel");
768 }
769 }
770
771 void
772 rel(Home home, BoolOpType o, const BoolVarArgs& x, BoolVar y,
773 IntPropLevel) {
774 using namespace Int;
775 GECODE_POST;
776 int m = x.size();
777 Region r;
778 switch (o) {
779 case BOT_AND:
780 {
781 ViewArray<NegBoolView> b(home,m);
782 for (int i=0; i<m; i++) {
783 NegBoolView nb(x[i]); b[i]=nb;
784 }
785 NegBoolView ny(y);
786 b.unique();
787 GECODE_ES_FAIL((Bool::NaryOr<NegBoolView,NegBoolView>
788 ::post(home,b,ny)));
789 }
790 break;
791 case BOT_OR:
792 {
793 ViewArray<BoolView> b(home,x);
794 b.unique();
795 GECODE_ES_FAIL((Bool::NaryOr<BoolView,BoolView>::post(home,b,y)));
796 }
797 break;
798 case BOT_IMP:
799 if (m < 2) {
800 throw TooFewArguments("Int::rel");
801 } else {
802 ViewArray<NegBoolView> a(home,x.size()-1);
803 for (int i=x.size()-1; i--; )
804 a[i]=NegBoolView(x[i]);
805 ViewArray<BoolView> b(home,1);
806 b[0]=x[x.size()-1];
807 GECODE_ES_FAIL((Bool::Clause<BoolView,NegBoolView>
808 ::post(home,b,a,y)));
809 }
810 break;
811 case BOT_EQV:
812 {
813 ViewArray<BoolView> xy(home, x.size() + 1);
814 for (int i=0; i<x.size(); i++)
815 xy[i] = x[i];
816 xy[x.size()] = y;
817 GECODE_ES_FAIL(Bool::NaryEqv::post(home,xy,0));
818 }
819 break;
820 case BOT_XOR:
821 {
822 ViewArray<BoolView> xy(home, x.size() + 1);
823 for (int i=0; i<x.size(); i++)
824 xy[i] = x[i];
825 xy[x.size()] = y;
826 GECODE_ES_FAIL(Bool::NaryEqv::post(home,xy,1));
827 }
828 break;
829 default:
830 throw UnknownOperation("Int::rel");
831 }
832 }
833
834 void
835 rel(Home home, BoolOpType o, const BoolVarArgs& x, int n,
836 IntPropLevel) {
837 using namespace Int;
838 if ((n < 0) || (n > 1))
839 throw NotZeroOne("Int::rel");
840 GECODE_POST;
841 int m = x.size();
842 Region r;
843 switch (o) {
844 case BOT_AND:
845 if (n == 0) {
846 ViewArray<NegBoolView> b(home,m);
847 for (int i=0; i<m; i++) {
848 NegBoolView nb(x[i]); b[i]=nb;
849 }
850 b.unique();
851 GECODE_ES_FAIL(Bool::NaryOrTrue<NegBoolView>::post(home,b));
852 } else {
853 for (int i=0; i<m; i++) {
854 BoolView b(x[i]); GECODE_ME_FAIL(b.one(home));
855 }
856 }
857 break;
858 case BOT_OR:
859 if (n == 0) {
860 for (int i=0; i<m; i++) {
861 BoolView b(x[i]); GECODE_ME_FAIL(b.zero(home));
862 }
863 } else {
864 ViewArray<BoolView> b(home,x);
865 b.unique();
866 GECODE_ES_FAIL(Bool::NaryOrTrue<BoolView>::post(home,b));
867 }
868 break;
869 case BOT_IMP:
870 if (m < 2) {
871 throw TooFewArguments("Int::rel");
872 } else if (n == 0) {
873 for (int i=m-1; i--; )
874 GECODE_ME_FAIL(BoolView(x[i]).one(home));
875 GECODE_ME_FAIL(BoolView(x[m-1]).zero(home));
876 } else {
877 ViewArray<NegBoolView> a(home,x.size()-1);
878 for (int i=x.size()-1; i--; )
879 a[i]=NegBoolView(x[i]);
880 ViewArray<BoolView> b(home,1);
881 b[0]=x[x.size()-1];
882 GECODE_ES_FAIL((Bool::ClauseTrue<BoolView,NegBoolView>
883 ::post(home,b,a)));
884 }
885 break;
886 case BOT_EQV:
887 {
888 ViewArray<BoolView> b(home,x);
889 GECODE_ES_FAIL(Bool::NaryEqv::post(home,b,n));
890 }
891 break;
892 case BOT_XOR:
893 {
894 ViewArray<BoolView> b(home,x);
895 GECODE_ES_FAIL(Bool::NaryEqv::post(home,b,1^n));
896 }
897 break;
898 default:
899 throw UnknownOperation("Int::rel");
900 }
901 }
902
903 void
904 clause(Home home, BoolOpType o, const BoolVarArgs& x, const BoolVarArgs& y,
905 int n, IntPropLevel) {
906 using namespace Int;
907 if ((n < 0) || (n > 1))
908 throw NotZeroOne("Int::rel");
909 GECODE_POST;
910 switch (o) {
911 case BOT_AND:
912 if (n == 0) {
913 ViewArray<NegBoolView> xv(home,x.size());
914 for (int i=0; i<x.size(); i++) {
915 NegBoolView nxi(x[i]); xv[i]=nxi;
916 }
917 ViewArray<BoolView> yv(home,y);
918 xv.unique(); yv.unique();
919 GECODE_ES_FAIL((Bool::ClauseTrue<NegBoolView,BoolView>
920 ::post(home,xv,yv)));
921 } else {
922 for (int i=0; i<x.size(); i++) {
923 BoolView b(x[i]); GECODE_ME_FAIL(b.one(home));
924 }
925 for (int i=0; i<y.size(); i++) {
926 BoolView b(y[i]); GECODE_ME_FAIL(b.zero(home));
927 }
928 }
929 break;
930 case BOT_OR:
931 if (n == 0) {
932 for (int i=0; i<x.size(); i++) {
933 BoolView b(x[i]); GECODE_ME_FAIL(b.zero(home));
934 }
935 for (int i=0; i<y.size(); i++) {
936 BoolView b(y[i]); GECODE_ME_FAIL(b.one(home));
937 }
938 } else {
939 ViewArray<BoolView> xv(home,x);
940 ViewArray<NegBoolView> yv(home,y.size());
941 for (int i=0; i<y.size(); i++) {
942 NegBoolView nyi(y[i]); yv[i]=nyi;
943 }
944 xv.unique(); yv.unique();
945 GECODE_ES_FAIL((Bool::ClauseTrue<BoolView,NegBoolView>
946 ::post(home,xv,yv)));
947 }
948 break;
949 default:
950 throw IllegalOperation("Int::clause");
951 }
952 }
953
954 void
955 clause(Home home, BoolOpType o, const BoolVarArgs& x, const BoolVarArgs& y,
956 BoolVar z, IntPropLevel) {
957 using namespace Int;
958 GECODE_POST;
959 switch (o) {
960 case BOT_AND:
961 {
962 ViewArray<NegBoolView> xv(home,x.size());
963 for (int i=0; i<x.size(); i++) {
964 NegBoolView n(x[i]); xv[i]=n;
965 }
966 ViewArray<BoolView> yv(home,y);
967 xv.unique(); yv.unique();
968 NegBoolView nz(z);
969 GECODE_ES_FAIL((Bool::Clause<NegBoolView,BoolView>
970 ::post(home,xv,yv,nz)));
971 }
972 break;
973 case BOT_OR:
974 {
975 ViewArray<BoolView> xv(home,x);
976 ViewArray<NegBoolView> yv(home,y.size());
977 for (int i=0; i<y.size(); i++) {
978 NegBoolView n(y[i]); yv[i]=n;
979 }
980 xv.unique(); yv.unique();
981 GECODE_ES_FAIL((Bool::Clause<BoolView,NegBoolView>
982 ::post(home,xv,yv,z)));
983 }
984 break;
985 default:
986 throw IllegalOperation("Int::clause");
987 }
988 }
989
990 void
991 ite(Home home, BoolVar b, IntVar x, IntVar y, IntVar z,
992 IntPropLevel ipl) {
993 using namespace Int;
994 GECODE_POST;
995 if (vbd(ipl) == IPL_BND) {
996 GECODE_ES_FAIL((Bool::IteBnd<IntView,IntView,IntView>
997 ::post(home,b,x,y,z)));
998 } else {
999 GECODE_ES_FAIL((Bool::IteDom<IntView,IntView,IntView>
1000 ::post(home,b,x,y,z)));
1001 }
1002 }
1003
1004 void
1005 ite(Home home, BoolVar b, BoolVar x, BoolVar y, BoolVar z,
1006 IntPropLevel) {
1007 using namespace Int;
1008 GECODE_POST;
1009 GECODE_ES_FAIL((Bool::IteBnd<BoolView,BoolView,BoolView>
1010 ::post(home,b,x,y,z)));
1011 }
1012
1013}
1014
1015// STATISTICS: int-post