main page
modules
namespaces
classes
files
Gecode home
Generated on Sat Nov 9 2013 19:18:29 for Gecode by
doxygen
1.8.4
test
int.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
* Mikael Lagerkvist <lagerkvist@gecode.org>
6
*
7
* Copyright:
8
* Christian Schulte, 2005
9
* Mikael Lagerkvist, 2005
10
*
11
* Last modified:
12
* $Date: 2013-03-05 14:40:46 +0100 (Tue, 05 Mar 2013) $ by $Author: schulte $
13
* $Revision: 13435 $
14
*
15
* This file is part of Gecode, the generic constraint
16
* development environment:
17
* http://www.gecode.org
18
*
19
* Permission is hereby granted, free of charge, to any person obtaining
20
* a copy of this software and associated documentation files (the
21
* "Software"), to deal in the Software without restriction, including
22
* without limitation the rights to use, copy, modify, merge, publish,
23
* distribute, sublicense, and/or sell copies of the Software, and to
24
* permit persons to whom the Software is furnished to do so, subject to
25
* the following conditions:
26
*
27
* The above copyright notice and this permission notice shall be
28
* included in all copies or substantial portions of the Software.
29
*
30
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
31
* EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
32
* MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
33
* NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
34
* LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
35
* OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
36
* WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
37
*
38
*/
39
40
#include "
test/int.hh
"
41
42
#include <algorithm>
43
44
namespace
Test {
namespace
Int {
45
46
47
/*
48
* Complete assignments
49
*
50
*/
51
void
52
CpltAssignment::operator++
(
void
) {
53
int
i
=
n
-1;
54
while
(
true
) {
55
++
dsv
[
i
];
56
if
(
dsv
[i]() || (i == 0))
57
return
;
58
dsv
[i--].
init
(
d
);
59
}
60
}
61
62
/*
63
* Random assignments
64
*
65
*/
66
void
67
RandomAssignment::operator++
(
void
) {
68
for
(
int
i
=
n
;
i
--; )
69
vals
[
i
]=
randval
();
70
a
--;
71
}
72
73
void
74
RandomMixAssignment::operator++
(
void
) {
75
for
(
int
i
=
n
-
_n1
;
i
--; )
76
vals
[
i
] =
randval
(
d
);
77
for
(
int
i
=
_n1
;
i
--; )
78
vals
[
n
-
_n1
+
i
] =
randval
(
_d1
);
79
a
--;
80
}
81
82
}}
83
84
std::ostream&
85
operator<<
(std::ostream& os,
const
Test::Int::Assignment
&
a
) {
86
int
n
= a.
size
();
87
os <<
"{"
;
88
for
(
int
i
=0;
i
<
n
;
i
++)
89
os << a[
i
] << ((
i
!=n-1) ?
","
:
"}"
);
90
return
os;
91
}
92
93
namespace
Test {
namespace
Int {
94
95
TestSpace::TestSpace
(
int
n
,
Gecode::IntSet
& d0,
Test
*
t
)
96
:
d
(d0),
x
(*this,n,Gecode::Int::Limits::
min
,Gecode::Int::Limits::
max
),
97
test(t), reified(false) {
98
Gecode::IntVarArgs
_x(*
this
,n,
d
);
99
if
(
x
.
size
() == 1)
100
Gecode::dom
(*
this
,
x
[0],_x[0]);
101
else
102
Gecode::dom
(*
this
,
x
,_x);
103
Gecode::BoolVar
b
(*
this
,0,1);
104
r
=
Gecode::Reify
(b,
Gecode::RM_EQV
);
105
if
(
opt
.
log
)
106
olog
<<
ind
(2) <<
"Initial: x[]="
<<
x
107
<< std::endl;
108
}
109
110
TestSpace::TestSpace
(
int
n
,
Gecode::IntSet
& d0,
Test
*
t
,
111
Gecode::ReifyMode
rm)
112
:
d
(d0),
x
(*this,n,Gecode::Int::Limits::
min
,Gecode::Int::Limits::
max
),
113
test(t), reified(true) {
114
Gecode::IntVarArgs
_x(*
this
,n,
d
);
115
if
(
x
.
size
() == 1)
116
Gecode::dom
(*
this
,
x
[0],_x[0]);
117
else
118
Gecode::dom
(*
this
,
x
,_x);
119
Gecode::BoolVar
b
(*
this
,0,1);
120
r
=
Gecode::Reify
(b,rm);
121
if
(
opt
.
log
)
122
olog
<<
ind
(2) <<
"Initial: x[]="
<<
x
123
<<
" b="
<<
r
.
var
() << std::endl;
124
}
125
126
TestSpace::TestSpace
(
bool
share,
TestSpace
& s)
127
: Gecode::Space(share,s),
d
(s.
d
), test(s.test), reified(s.reified) {
128
x
.
update
(*
this
, share, s.
x
);
129
Gecode::BoolVar
b
;
130
Gecode::BoolVar
sr(s.
r
.
var
());
131
b.
update
(*
this
, share, sr);
132
r
.
var
(b);
r
.
mode
(s.
r
.
mode
());
133
}
134
135
Gecode::Space
*
136
TestSpace::copy
(
bool
share) {
137
return
new
TestSpace
(share,*
this
);
138
}
139
140
bool
141
TestSpace::assigned
(
void
)
const
{
142
for
(
int
i
=
x
.
size
();
i
--; )
143
if
(!
x
[
i
].
assigned
())
144
return
false
;
145
return
true
;
146
}
147
148
void
149
TestSpace::post
(
void
) {
150
if
(
reified
){
151
test
->
post
(*
this
,
x
,
r
);
152
if
(
opt
.
log
)
153
olog
<<
ind
(3) <<
"Posting reified propagator"
<< std::endl;
154
}
else
{
155
test
->
post
(*
this
,
x
);
156
if
(
opt
.
log
)
157
olog
<<
ind
(3) <<
"Posting propagator"
<< std::endl;
158
}
159
}
160
161
bool
162
TestSpace::failed
(
void
) {
163
if
(
opt
.
log
) {
164
olog
<<
ind
(3) <<
"Fixpoint: "
<<
x
;
165
bool
f=(
status
() ==
Gecode::SS_FAILED
);
166
olog
<< std::endl <<
ind
(3) <<
" --> "
<< x << std::endl;
167
return
f;
168
}
else
{
169
return
status
() ==
Gecode::SS_FAILED
;
170
}
171
}
172
173
void
174
TestSpace::rel
(
int
i
,
Gecode::IntRelType
irt,
int
n
) {
175
if
(
opt
.
log
) {
176
olog
<<
ind
(4) <<
"x["
<< i <<
"] "
;
177
switch
(irt) {
178
case
Gecode::IRT_EQ
:
olog
<<
"="
;
break
;
179
case
Gecode::IRT_NQ
:
olog
<<
"!="
;
break
;
180
case
Gecode::IRT_LQ
:
olog
<<
"<="
;
break
;
181
case
Gecode::IRT_LE
:
olog
<<
"<"
;
break
;
182
case
Gecode::IRT_GQ
:
olog
<<
">="
;
break
;
183
case
Gecode::IRT_GR
:
olog
<<
">"
;
break
;
184
}
185
olog
<<
" "
<< n << std::endl;
186
}
187
Gecode::rel
(*
this
,
x
[i], irt, n);
188
}
189
190
void
191
TestSpace::rel
(
bool
sol) {
192
int
n
= sol ? 1 : 0;
193
assert(
reified
);
194
if
(
opt
.
log
)
195
olog
<<
ind
(4) <<
"b = "
<< n << std::endl;
196
Gecode::rel
(*
this
,
r
.
var
(),
Gecode::IRT_EQ
,
n
);
197
}
198
199
void
200
TestSpace::assign
(
const
Assignment
&
a
,
bool
skip) {
201
using namespace
Gecode;
202
int
i
= skip ?
static_cast<
int
>
(
Base::rand
(a.
size
())) : -1;
203
for
(
int
j=a.
size
(); j--; )
204
if
(
i
!= j) {
205
rel
(j,
IRT_EQ
, a[j]);
206
if
(
Base::fixpoint
() &&
failed
())
207
return
;
208
}
209
}
210
211
void
212
TestSpace::bound
(
void
) {
213
using namespace
Gecode;
214
// Select variable to be assigned
215
int
i
=
Base::rand
(
x
.
size
());
216
while
(
x
[
i
].
assigned
()) {
217
i
= (
i
+1) %
x
.
size
();
218
}
219
bool
min
=
Base::rand
(2);
220
rel
(
i
,
IRT_EQ
,
min
?
x
[
i
].
min
() :
x
[
i
].
max
());
221
}
222
223
void
224
TestSpace::prune
(
int
i
,
bool
bounds_only) {
225
using namespace
Gecode;
226
// Prune values
227
if
(bounds_only) {
228
if
(
Base::rand
(2) && !
x
[i].
assigned
()) {
229
int
v
=
x
[
i
].min()+1+
Base::rand
(static_cast
230
<
unsigned
int
>(
x
[i].
max
()-
x
[i].
min
()));
231
assert((v >
x
[i].
min
()) && (v <=
x
[i].
max
()));
232
rel
(i,
Gecode::IRT_LE
, v);
233
}
234
if
(
Base::rand
(2) && !
x
[i].
assigned
()) {
235
int
v
=
x
[
i
].min()+
Base::rand
(static_cast
236
<
unsigned
int
>(
x
[i].
max
()-
x
[i].
min
()));
237
assert((v <
x
[i].
max
()) && (v >=
x
[i].
min
()));
238
rel
(i,
Gecode::IRT_GR
, v);
239
}
240
}
else
{
241
for
(
int
vals =
Base::rand
(
x
[i].
size
()-1)+1; vals--; ) {
242
int
v
;
243
Gecode::Int::ViewRanges<Gecode::Int::IntView>
it(
x
[i]);
244
unsigned
int
skip =
Base::rand
(
x
[i].
size
()-1);
245
while
(
true
) {
246
if
(it.
width
() > skip) {
247
v = it.
min
() + skip;
break
;
248
}
249
skip -= it.
width
(); ++it;
250
}
251
rel
(i,
IRT_NQ
, v);
252
}
253
}
254
}
255
256
void
257
TestSpace::prune
(
void
) {
258
using namespace
Gecode;
259
// Select variable to be pruned
260
int
i
=
Base::rand
(
x
.
size
());
261
while
(
x
[
i
].
assigned
()) {
262
i
= (
i
+1) %
x
.
size
();
263
}
264
prune
(
i
,
false
);
265
}
266
267
bool
268
TestSpace::prune
(
const
Assignment
&
a
,
bool
testfix) {
269
// Select variable to be pruned
270
int
i
=
Base::rand
(
x
.
size
());
271
while
(
x
[i].
assigned
())
272
i = (i+1) %
x
.
size
();
273
// Select mode for pruning
274
switch
(
Base::rand
(3)) {
275
case
0:
276
if
(a[i] <
x
[i].
max
()) {
277
int
v
=a[
i
]+1+
Base::rand
(static_cast
278
<
unsigned
int
>(
x
[i].
max
()-a[i]));
279
assert((v > a[i]) && (v <=
x
[i].
max
()));
280
rel
(i,
Gecode::IRT_LE
, v);
281
}
282
break
;
283
case
1:
284
if
(a[i] >
x
[i].
min
()) {
285
int
v
=
x
[
i
].min()+
Base::rand
(static_cast
286
<
unsigned
int
>(a[i]-
x
[i].
min
()));
287
assert((v < a[i]) && (v >=
x
[i].
min
()));
288
rel
(i,
Gecode::IRT_GR
, v);
289
}
290
break
;
291
default
:
292
{
293
int
v
;
294
Gecode::Int::ViewRanges<Gecode::Int::IntView>
it(
x
[i]);
295
unsigned
int
skip =
Base::rand
(
x
[i].
size
()-1);
296
while
(
true
) {
297
if
(it.
width
() > skip) {
298
v = it.
min
() + skip;
299
if
(v == a[i]) {
300
if
(it.
width
() == 1) {
301
++it; v = it.
min
();
302
}
else
if
(v < it.
max
()) {
303
++
v
;
304
}
else
{
305
--
v
;
306
}
307
}
308
break
;
309
}
310
skip -= it.
width
(); ++it;
311
}
312
rel
(i,
Gecode::IRT_NQ
, v);
313
break
;
314
}
315
}
316
if
(
Base::fixpoint
()) {
317
if
(
failed
() || !testfix)
318
return
true
;
319
TestSpace
*
c
=
static_cast<
TestSpace
*
>
(
clone
());
320
if
(
opt
.
log
)
321
olog
<<
ind
(3) <<
"Testing fixpoint on copy"
<< std::endl;
322
c->
post
();
323
if
(c->
failed
()) {
324
if
(
opt
.
log
)
325
olog
<<
ind
(4) <<
"Copy failed after posting"
<< std::endl;
326
delete
c
;
return
false
;
327
}
328
for
(
int
i=
x
.
size
(); i--; )
329
if
(
x
[i].
size
() != c->
x
[
i
].
size
()) {
330
if
(
opt
.
log
)
331
olog
<<
ind
(4) <<
"Different domain size"
<< std::endl;
332
delete
c
;
return
false
;
333
}
334
if
(
reified
&& (
r
.
var
().
size
() != c->
r
.
var
().
size
())) {
335
if
(
opt
.
log
)
336
olog
<<
ind
(4) <<
"Different control variable"
<< std::endl;
337
delete
c
;
return
false
;
338
}
339
if
(
opt
.
log
)
340
olog
<<
ind
(3) <<
"Finished testing fixpoint on copy"
<< std::endl;
341
delete
c
;
342
}
343
return
true
;
344
}
345
346
347
const
Gecode::IntConLevel
IntConLevels::icls[] =
348
{
Gecode::ICL_DOM
,
Gecode::ICL_BND
,
Gecode::ICL_VAL
};
349
350
const
Gecode::IntRelType
IntRelTypes::irts[] =
351
{
Gecode::IRT_EQ
,
Gecode::IRT_NQ
,
Gecode::IRT_LQ
,
352
Gecode::IRT_LE
,
Gecode::IRT_GQ
,
Gecode::IRT_GR
};
353
354
const
Gecode::BoolOpType
BoolOpTypes::bots[] =
355
{
Gecode::BOT_AND
,
Gecode::BOT_OR
,
Gecode::BOT_IMP
,
356
Gecode::BOT_EQV
,
Gecode::BOT_XOR
};
357
358
Assignment*
359
Test::assignment
(
void
)
const
{
360
return
new
CpltAssignment
(arity,
dom
);
361
}
362
363
365
#define CHECK_TEST(T,M) \
366
if (opt.log) \
367
olog << ind(3) << "Check: " << (M) << std::endl; \
368
if (!(T)) { \
369
problem = (M); delete s; goto failed; \
370
}
371
373
#define START_TEST(T) \
374
if (opt.log) { \
375
olog.str(""); \
376
olog << ind(2) << "Testing: " << (T) << std::endl; \
377
} \
378
test = (T);
379
380
bool
381
Test::ignore
(
const
Assignment
&)
const
{
382
return
false
;
383
}
384
385
void
386
Test::post
(
Gecode::Space
&,
Gecode::IntVarArray
&,
387
Gecode::Reify
) {}
388
389
bool
390
Test::run
(
void
) {
391
using namespace
Gecode;
392
const
char
*
test
=
"NONE"
;
393
const
char
* problem =
"NONE"
;
394
395
// Set up assignments
396
Assignment
* ap = assignment();
397
Assignment
&
a
= *ap;
398
399
// Set up space for all solution search
400
TestSpace
* search_s =
new
TestSpace
(arity,
dom
,
this
);
401
post
(*search_s,search_s->x);
402
branch
(*search_s,search_s->x,
INT_VAR_NONE
(),
INT_VAL_MIN
());
403
Search::Options
search_o;
404
search_o.
threads
= 1;
405
DFS<TestSpace>
e_s(search_s,search_o);
406
delete
search_s;
407
408
while
(
a
()) {
409
bool
sol = solution(
a
);
410
if
(
opt
.
log
) {
411
olog
<<
ind
(1) <<
"Assignment: "
<<
a
412
<< (sol ?
" (solution)"
:
" (no solution)"
)
413
<< std::endl;
414
}
415
416
START_TEST
(
"Assignment (after posting)"
);
417
{
418
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
);
419
TestSpace
* sc = NULL;
420
s->
post
();
421
switch
(
Base::rand
(3)) {
422
case
0:
423
if
(
opt
.
log
)
424
olog
<<
ind
(3) <<
"No copy"
<< std::endl;
425
sc = s;
426
s = NULL;
427
break
;
428
case
1:
429
if
(
opt
.
log
)
430
olog
<<
ind
(3) <<
"Unshared copy"
<< std::endl;
431
if
(s->
status
() !=
SS_FAILED
) {
432
sc =
static_cast<
TestSpace
*
>
(s->
clone
(
false
));
433
}
else
{
434
sc = s; s = NULL;
435
}
436
break
;
437
case
2:
438
if
(
opt
.
log
)
439
olog
<<
ind
(3) <<
"Shared copy"
<< std::endl;
440
if
(s->
status
() !=
SS_FAILED
) {
441
sc =
static_cast<
TestSpace
*
>
(s->
clone
(
true
));
442
}
else
{
443
sc = s; s = NULL;
444
}
445
break
;
446
default
: assert(
false
);
447
}
448
sc->
assign
(
a
);
449
if
(sol) {
450
CHECK_TEST
(!sc->
failed
(),
"Failed on solution"
);
451
CHECK_TEST
(sc->
propagators
()==0,
"No subsumption"
);
452
}
else
{
453
CHECK_TEST
(sc->
failed
(),
"Solved on non-solution"
);
454
}
455
delete
s;
delete
sc;
456
}
457
START_TEST
(
"Partial assignment (after posting)"
);
458
{
459
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
);
460
s->
post
();
461
s->
assign
(
a
,
true
);
462
(void) s->
failed
();
463
s->
assign
(
a
);
464
if
(sol) {
465
CHECK_TEST
(!s->
failed
(),
"Failed on solution"
);
466
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
467
}
else
{
468
CHECK_TEST
(s->
failed
(),
"Solved on non-solution"
);
469
}
470
delete
s;
471
}
472
START_TEST
(
"Assignment (before posting)"
);
473
{
474
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
);
475
s->
assign
(
a
);
476
s->
post
();
477
if
(sol) {
478
CHECK_TEST
(!s->
failed
(),
"Failed on solution"
);
479
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
480
}
else
{
481
CHECK_TEST
(s->
failed
(),
"Solved on non-solution"
);
482
}
483
delete
s;
484
}
485
START_TEST
(
"Partial assignment (before posting)"
);
486
{
487
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
);
488
s->
assign
(
a
,
true
);
489
s->
post
();
490
(void) s->
failed
();
491
s->
assign
(
a
);
492
if
(sol) {
493
CHECK_TEST
(!s->
failed
(),
"Failed on solution"
);
494
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
495
}
else
{
496
CHECK_TEST
(s->
failed
(),
"Solved on non-solution"
);
497
}
498
delete
s;
499
}
500
START_TEST
(
"Prune"
);
501
{
502
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
);
503
s->
post
();
504
while
(!s->
failed
() && !s->
assigned
())
505
if
(!s->
prune
(
a
,testfix)) {
506
problem =
"No fixpoint"
;
507
delete
s;
508
goto
failed
;
509
}
510
s->
assign
(
a
);
511
if
(sol) {
512
CHECK_TEST
(!s->
failed
(),
"Failed on solution"
);
513
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
514
}
else
{
515
CHECK_TEST
(s->
failed
(),
"Solved on non-solution"
);
516
}
517
delete
s;
518
}
519
520
if
(!
ignore
(
a
)) {
521
if
(
eqv
()) {
522
START_TEST
(
"Assignment reified (rewrite after post, <=>)"
);
523
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_EQV
);
524
s->
post
();
525
s->
rel
(sol);
526
s->
assign
(
a
);
527
CHECK_TEST
(!s->
failed
(),
"Failed"
);
528
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
529
delete
s;
530
}
531
if
(
imp
()) {
532
START_TEST
(
"Assignment reified (rewrite after post, =>)"
);
533
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_IMP
);
534
s->
post
();
535
s->
rel
(sol);
536
s->
assign
(
a
);
537
CHECK_TEST
(!s->
failed
(),
"Failed"
);
538
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
539
delete
s;
540
}
541
if
(
pmi
()) {
542
START_TEST
(
"Assignment reified (rewrite after post, <=)"
);
543
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_PMI
);
544
s->
post
();
545
s->
rel
(sol);
546
s->
assign
(
a
);
547
CHECK_TEST
(!s->
failed
(),
"Failed"
);
548
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
549
delete
s;
550
}
551
if
(
eqv
()) {
552
START_TEST
(
"Assignment reified (rewrite failure, <=>)"
);
553
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_EQV
);
554
s->
post
();
555
s->
rel
(!sol);
556
s->
assign
(
a
);
557
CHECK_TEST
(s->
failed
(),
"Not failed"
);
558
delete
s;
559
}
560
if
(
imp
()) {
561
START_TEST
(
"Assignment reified (rewrite failure, =>)"
);
562
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_IMP
);
563
s->
post
();
564
s->
rel
(!sol);
565
s->
assign
(
a
);
566
if
(sol) {
567
CHECK_TEST
(!s->
failed
(),
"Failed"
);
568
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
569
}
else
{
570
CHECK_TEST
(s->
failed
(),
"Not failed"
);
571
}
572
delete
s;
573
}
574
if
(
pmi
()) {
575
START_TEST
(
"Assignment reified (rewrite failure, <=)"
);
576
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_PMI
);
577
s->
post
();
578
s->
rel
(!sol);
579
s->
assign
(
a
);
580
if
(sol) {
581
CHECK_TEST
(s->
failed
(),
"Not failed"
);
582
}
else
{
583
CHECK_TEST
(!s->
failed
(),
"Failed"
);
584
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
585
}
586
delete
s;
587
}
588
if
(
eqv
()) {
589
START_TEST
(
"Assignment reified (immediate rewrite, <=>)"
);
590
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_EQV
);
591
s->
rel
(sol);
592
s->
post
();
593
s->
assign
(
a
);
594
CHECK_TEST
(!s->
failed
(),
"Failed"
);
595
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
596
delete
s;
597
}
598
if
(
imp
()) {
599
START_TEST
(
"Assignment reified (immediate rewrite, =>)"
);
600
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_IMP
);
601
s->
rel
(sol);
602
s->
post
();
603
s->
assign
(
a
);
604
CHECK_TEST
(!s->
failed
(),
"Failed"
);
605
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
606
delete
s;
607
}
608
if
(
pmi
()) {
609
START_TEST
(
"Assignment reified (immediate rewrite, <=)"
);
610
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_PMI
);
611
s->
rel
(sol);
612
s->
post
();
613
s->
assign
(
a
);
614
CHECK_TEST
(!s->
failed
(),
"Failed"
);
615
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
616
delete
s;
617
}
618
if
(
eqv
()) {
619
START_TEST
(
"Assignment reified (immediate failure, <=>)"
);
620
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_EQV
);
621
s->
rel
(!sol);
622
s->
post
();
623
s->
assign
(
a
);
624
CHECK_TEST
(s->
failed
(),
"Not failed"
);
625
delete
s;
626
}
627
if
(
imp
()) {
628
START_TEST
(
"Assignment reified (immediate failure, =>)"
);
629
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_IMP
);
630
s->
rel
(!sol);
631
s->
post
();
632
s->
assign
(
a
);
633
if
(sol) {
634
CHECK_TEST
(!s->
failed
(),
"Failed"
);
635
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
636
}
else
{
637
CHECK_TEST
(s->
failed
(),
"Not failed"
);
638
}
639
delete
s;
640
}
641
if
(
pmi
()) {
642
START_TEST
(
"Assignment reified (immediate failure, <=)"
);
643
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_PMI
);
644
s->
rel
(!sol);
645
s->
post
();
646
s->
assign
(
a
);
647
if
(sol) {
648
CHECK_TEST
(s->
failed
(),
"Not failed"
);
649
}
else
{
650
CHECK_TEST
(!s->
failed
(),
"Failed"
);
651
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
652
}
653
delete
s;
654
}
655
if
(
eqv
()) {
656
START_TEST
(
"Assignment reified (before posting, <=>)"
);
657
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_EQV
);
658
s->
assign
(
a
);
659
s->
post
();
660
CHECK_TEST
(!s->
failed
(),
"Failed"
);
661
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
662
CHECK_TEST
(s->
r
.
var
().
assigned
(),
"Control variable unassigned"
);
663
if
(sol) {
664
CHECK_TEST
(s->
r
.
var
().
val
()==1,
"Zero on solution"
);
665
}
else
{
666
CHECK_TEST
(s->
r
.
var
().
val
()==0,
"One on non-solution"
);
667
}
668
delete
s;
669
}
670
if
(
imp
()) {
671
START_TEST
(
"Assignment reified (before posting, =>)"
);
672
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_IMP
);
673
s->
assign
(
a
);
674
s->
post
();
675
CHECK_TEST
(!s->
failed
(),
"Failed"
);
676
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
677
if
(sol) {
678
CHECK_TEST
(!s->
r
.
var
().
assigned
(),
"Control variable assigned"
);
679
}
else
{
680
CHECK_TEST
(s->
r
.
var
().
assigned
(),
"Control variable unassigned"
);
681
CHECK_TEST
(s->
r
.
var
().
val
()==0,
"One on non-solution"
);
682
}
683
delete
s;
684
}
685
if
(
pmi
()) {
686
START_TEST
(
"Assignment reified (before posting, <=)"
);
687
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_PMI
);
688
s->
assign
(
a
);
689
s->
post
();
690
CHECK_TEST
(!s->
failed
(),
"Failed"
);
691
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
692
if
(sol) {
693
CHECK_TEST
(s->
r
.
var
().
assigned
(),
"Control variable unassigned"
);
694
CHECK_TEST
(s->
r
.
var
().
val
()==1,
"Zero on solution"
);
695
}
else
{
696
CHECK_TEST
(!s->
r
.
var
().
assigned
(),
"Control variable assigned"
);
697
}
698
delete
s;
699
}
700
if
(
eqv
()) {
701
START_TEST
(
"Assignment reified (after posting, <=>)"
);
702
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_EQV
);
703
s->
post
();
704
s->
assign
(
a
);
705
CHECK_TEST
(!s->
failed
(),
"Failed"
);
706
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
707
CHECK_TEST
(s->
r
.
var
().
assigned
(),
"Control variable unassigned"
);
708
if
(sol) {
709
CHECK_TEST
(s->
r
.
var
().
val
()==1,
"Zero on solution"
);
710
}
else
{
711
CHECK_TEST
(s->
r
.
var
().
val
()==0,
"One on non-solution"
);
712
}
713
delete
s;
714
}
715
if
(
imp
()) {
716
START_TEST
(
"Assignment reified (after posting, =>)"
);
717
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_IMP
);
718
s->
post
();
719
s->
assign
(
a
);
720
CHECK_TEST
(!s->
failed
(),
"Failed"
);
721
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
722
if
(sol) {
723
CHECK_TEST
(!s->
r
.
var
().
assigned
(),
"Control variable assigned"
);
724
}
else
{
725
CHECK_TEST
(s->
r
.
var
().
assigned
(),
"Control variable unassigned"
);
726
CHECK_TEST
(s->
r
.
var
().
val
()==0,
"One on non-solution"
);
727
}
728
delete
s;
729
}
730
if
(
pmi
()) {
731
START_TEST
(
"Assignment reified (after posting, <=)"
);
732
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_PMI
);
733
s->
post
();
734
s->
assign
(
a
);
735
CHECK_TEST
(!s->
failed
(),
"Failed"
);
736
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
737
if
(sol) {
738
CHECK_TEST
(s->
r
.
var
().
assigned
(),
"Control variable unassigned"
);
739
CHECK_TEST
(s->
r
.
var
().
val
()==1,
"Zero on solution"
);
740
}
else
{
741
CHECK_TEST
(!s->
r
.
var
().
assigned
(),
"Control variable assigned"
);
742
}
743
delete
s;
744
}
745
if
(
eqv
()) {
746
START_TEST
(
"Prune reified, <=>"
);
747
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_EQV
);
748
s->
post
();
749
while
(!s->
failed
() &&
750
(!s->
assigned
() || !s->
r
.
var
().
assigned
()))
751
if
(!s->
prune
(
a
,testfix)) {
752
problem =
"No fixpoint"
;
753
delete
s;
754
goto
failed
;
755
}
756
CHECK_TEST
(!s->
failed
(),
"Failed"
);
757
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
758
CHECK_TEST
(s->
r
.
var
().
assigned
(),
"Control variable unassigned"
);
759
if
(sol) {
760
CHECK_TEST
(s->
r
.
var
().
val
()==1,
"Zero on solution"
);
761
}
else
{
762
CHECK_TEST
(s->
r
.
var
().
val
()==0,
"One on non-solution"
);
763
}
764
delete
s;
765
}
766
if
(
imp
()) {
767
START_TEST
(
"Prune reified, =>"
);
768
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_IMP
);
769
s->
post
();
770
while
(!s->
failed
() &&
771
(!s->
assigned
() || (!sol && !s->
r
.
var
().
assigned
())))
772
if
(!s->
prune
(
a
,testfix)) {
773
problem =
"No fixpoint"
;
774
delete
s;
775
goto
failed
;
776
}
777
CHECK_TEST
(!s->
failed
(),
"Failed"
);
778
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
779
if
(sol) {
780
CHECK_TEST
(!s->
r
.
var
().
assigned
(),
"Control variable assigned"
);
781
}
else
{
782
CHECK_TEST
(s->
r
.
var
().
assigned
(),
"Control variable unassigned"
);
783
CHECK_TEST
(s->
r
.
var
().
val
()==0,
"One on non-solution"
);
784
}
785
delete
s;
786
}
787
if
(
pmi
()) {
788
START_TEST
(
"Prune reified, <="
);
789
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
,
RM_PMI
);
790
s->
post
();
791
while
(!s->
failed
() &&
792
(!s->
assigned
() || (sol && !s->
r
.
var
().
assigned
())))
793
if
(!s->
prune
(
a
,testfix)) {
794
problem =
"No fixpoint"
;
795
delete
s;
796
goto
failed
;
797
}
798
CHECK_TEST
(!s->
failed
(),
"Failed"
);
799
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
800
if
(sol) {
801
CHECK_TEST
(s->
r
.
var
().
assigned
(),
"Control variable unassigned"
);
802
CHECK_TEST
(s->
r
.
var
().
val
()==1,
"Zero on solution"
);
803
}
else
{
804
CHECK_TEST
(!s->
r
.
var
().
assigned
(),
"Control variable assigned"
);
805
}
806
delete
s;
807
}
808
}
809
810
if
(testsearch) {
811
if
(sol) {
812
START_TEST
(
"Search"
);
813
TestSpace
* s = e_s.
next
();
814
CHECK_TEST
(s != NULL,
"Solutions exhausted"
);
815
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
816
for
(
int
i
=
a
.size();
i
--; ) {
817
CHECK_TEST
(s->
x
[
i
].
assigned
(),
"Unassigned variable"
);
818
CHECK_TEST
(
a
[
i
] == s->
x
[
i
].val(),
"Wrong value in solution"
);
819
}
820
delete
s;
821
}
822
}
823
824
++
a
;
825
}
826
827
if
(testsearch) {
828
test
=
"Search"
;
829
if
(e_s.
next
() != NULL) {
830
problem =
"Excess solutions"
;
831
goto
failed
;
832
}
833
}
834
835
switch
(contest) {
836
case
CTL_NONE
:
break
;
837
case
CTL_DOMAIN
: {
838
START_TEST
(
"Full domain consistency"
);
839
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
);
840
s->
post
();
841
if
(!s->
failed
()) {
842
while
(!s->
failed
() && !s->
assigned
())
843
s->
prune
();
844
CHECK_TEST
(!s->
failed
(),
"Failed"
);
845
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
846
}
847
delete
s;
848
// Fall-through -- domain implies bounds(d) and bounds(z)
849
}
850
case
CTL_BOUNDS_D
: {
851
START_TEST
(
"Bounds(D)-consistency"
);
852
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
);
853
s->
post
();
854
for
(
int
i
= s->
x
.
size
();
i
--; )
855
s->
prune
(
i
,
false
);
856
if
(!s->
failed
()) {
857
while
(!s->
failed
() && !s->
assigned
())
858
s->
bound
();
859
CHECK_TEST
(!s->
failed
(),
"Failed"
);
860
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
861
}
862
delete
s;
863
// Fall-through -- bounds(d) implies bounds(z)
864
}
865
case
CTL_BOUNDS_Z
: {
866
START_TEST
(
"Bounds(Z)-consistency"
);
867
TestSpace
* s =
new
TestSpace
(arity,
dom
,
this
);
868
s->
post
();
869
for
(
int
i
= s->
x
.
size
();
i
--; )
870
s->
prune
(
i
,
true
);
871
if
(!s->
failed
()) {
872
while
(!s->
failed
() && !s->
assigned
())
873
s->
bound
();
874
CHECK_TEST
(!s->
failed
(),
"Failed"
);
875
CHECK_TEST
(s->
propagators
()==0,
"No subsumption"
);
876
}
877
delete
s;
878
break
;
879
}
880
}
881
882
delete
ap;
883
return
true
;
884
885
failed
:
886
if
(
opt
.
log
)
887
olog
<<
"FAILURE"
<< std::endl
888
<<
ind
(1) <<
"Test: "
<<
test
<< std::endl
889
<<
ind
(1) <<
"Problem: "
<< problem << std::endl;
890
if
(
a
() &&
opt
.
log
)
891
olog
<<
ind
(1) <<
"Assignment: "
<<
a
<< std::endl;
892
delete
ap;
893
894
return
false
;
895
}
896
897
}}
898
899
#undef START_TEST
900
#undef CHECK_TEST
901
902
// STATISTICS: test-int