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