this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Guido Tack <tack@gecode.org>
5 * Christian Schulte <schulte@gecode.org>
6 * Mikael Lagerkvist <lagerkvist@gecode.org>
7 *
8 * Copyright:
9 * Guido Tack, 2005
10 * Christian Schulte, 2005
11 * Mikael Lagerkvist, 2005
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 "test/set.hh"
39
40#include <algorithm>
41
42namespace Test { namespace Set {
43
44 CountableSet::CountableSet(const Gecode::IntSet& d0) : d(d0), cur(0) {
45 Gecode::IntSetRanges isr(d);
46 lubmax =
47 static_cast<unsigned int>(pow(static_cast<double>(2.0),
48 static_cast<int>(Gecode::Iter::Ranges::size(isr))));
49 }
50
51 void CountableSet::operator++(void) {
52 cur++;
53 }
54
55 void CountableSet::init(const Gecode::IntSet& d0) {
56 d = d0;
57 cur = 0;
58 Gecode::IntSetRanges isr(d);
59 lubmax =
60 static_cast<unsigned int>(pow(static_cast<double>(2.0),
61 static_cast<int>(Gecode::Iter::Ranges::size(isr))));
62 }
63
64 int CountableSet::val(void) const {
65 return cur;
66 }
67
68 SetAssignment::SetAssignment(int n0, const Gecode::IntSet& d0, int _withInt)
69 : n(n0), dsv(new CountableSet[n]), ir(_withInt, d0), done(false), lub(d0),
70 withInt(_withInt) {
71 for (int i=n; i--; )
72 dsv[i].init(lub);
73 }
74
75 void
76 SetAssignment::next(Gecode::Support::RandomGenerator& rand) {
77 int i = n-1;
78 while (true) {
79 ++dsv[i];
80 if (dsv[i]())
81 return;
82 dsv[i].init(lub);
83 --i;
84 if (i<0) {
85 if (withInt==0) {
86 done = true;
87 return;
88 }
89 ir.next(rand);
90 if (ir.has_more()) {
91 i = n-1;
92 for (int j=n; j--; )
93 dsv[j].init(lub);
94 } else {
95 done = true;
96 return;
97 }
98 }
99 }
100 }
101
102}}
103
104std::ostream&
105operator<<(std::ostream& os, const Test::Set::SetAssignment& a) {
106 int n = a.size();
107 os << "{";
108 for (int i=0; i<n; i++) {
109 Test::Set::CountableSetRanges csv(a.lub, a[i]);
110 Gecode::IntSet icsv(csv);
111 os << icsv << ((i!=n-1) ? "," : "}");
112 }
113 if (a.withInt > 0)
114 os << a.ints();
115 return os;
116}
117
118namespace Test { namespace Set {
119
120 SetTestSpace::SetTestSpace(int n, Gecode::IntSet& d0, int i,
121 SetTest* t, bool log)
122 : d(d0), y(*this, i, d),
123 withInt(i), r(Gecode::BoolVar(*this, 0, 1),Gecode::RM_EQV),
124 reified(false), test(t) {
125 using namespace Gecode;
126 IntSet u(Gecode::Set::Limits::min,Gecode::Set::Limits::max);
127 x = SetVarArray(*this, n, Gecode::IntSet::empty, u);
128 SetVarArgs _x(*this, n, Gecode::IntSet::empty, d);
129 if (x.size() == 1)
130 dom(*this,x[0],_x[0]);
131 else
132 dom(*this,x,_x);
133 if (opt.log && log) {
134 olog << ind(2) << "Initial: x[]=" << x;
135 olog << " y[]=" << y;
136 olog << std::endl;
137 }
138 }
139
140 SetTestSpace::SetTestSpace(int n, Gecode::IntSet& d0, int i,
141 SetTest* t, Gecode::ReifyMode rm, bool log)
142 : d(d0), x(*this, n, Gecode::IntSet::empty, d), y(*this, i, d),
143 withInt(i), r(Gecode::BoolVar(*this, 0, 1),rm),
144 reified(true), test(t) {
145 if (opt.log && log) {
146 olog << ind(2) << "Initial: x[]=" << x;
147 olog << " y[]=" << y;
148 olog << " b=" << r.var();
149 olog << std::endl;
150 }
151 }
152
153 SetTestSpace::SetTestSpace(SetTestSpace& s)
154 : Gecode::Space(s), d(s.d), withInt(s.withInt),
155 reified(s.reified), test(s.test) {
156 x.update(*this, s.x);
157 y.update(*this, s.y);
158 Gecode::BoolVar b;
159 Gecode::BoolVar sr(s.r.var());
160 b.update(*this, sr);
161 r.var(b); r.mode(s.r.mode());
162 }
163
164 Gecode::Space*
165 SetTestSpace::copy(void) {
166 return new SetTestSpace(*this);
167 }
168
169 void
170 SetTestSpace::post(void) {
171 if (reified){
172 test->post(*this,x,y,r);
173 if (opt.log)
174 olog << ind(3) << "Posting reified propagator" << std::endl;
175 } else {
176 test->post(*this,x,y);
177 if (opt.log)
178 olog << ind(3) << "Posting propagator" << std::endl;
179 }
180 }
181
182 bool
183 SetTestSpace::failed(void) {
184 if (opt.log) {
185 olog << ind(3) << "Fixpoint: x[]=" << x
186 << " y[]=" << y << std::endl;
187 bool f=(status() == Gecode::SS_FAILED);
188 olog << ind(3) << " --> x[]=" << x
189 << " y[]=" << y << std::endl;
190 return f;
191 } else {
192 return status() == Gecode::SS_FAILED;
193 }
194 }
195
196 bool
197 SetTestSpace::subsumed(bool b) {
198 return b ? (propagators() == 0) : true;
199 }
200
201 void
202 SetTestSpace::rel(int i, Gecode::SetRelType srt, const Gecode::IntSet& is) {
203 if (opt.log) {
204 olog << ind(4) << "x[" << i << "] ";
205 switch (srt) {
206 case Gecode::SRT_EQ: olog << "="; break;
207 case Gecode::SRT_LQ: olog << "<="; break;
208 case Gecode::SRT_LE: olog << "<"; break;
209 case Gecode::SRT_GQ: olog << ">="; break;
210 case Gecode::SRT_GR: olog << ">"; break;
211 case Gecode::SRT_NQ: olog << "!="; break;
212 case Gecode::SRT_SUB: olog << "sub"; break;
213 case Gecode::SRT_SUP: olog << "sup"; break;
214 case Gecode::SRT_DISJ: olog << "||"; break;
215 case Gecode::SRT_CMPL: olog << "^-1 = "; break;
216 }
217 olog << is << std::endl;
218 }
219 Gecode::dom(*this, x[i], srt, is);
220 }
221
222 void
223 SetTestSpace::cardinality(int i, int cmin, int cmax) {
224 if (opt.log) {
225 olog << ind(4) << cmin << " <= #(x[" << i << "]) <= " << cmax
226 << std::endl;
227 }
228 Gecode::cardinality(*this, x[i], cmin, cmax);
229 }
230
231 void
232 SetTestSpace::rel(int i, Gecode::IntRelType irt, int n) {
233 if (opt.log) {
234 olog << ind(4) << "y[" << i << "] ";
235 switch (irt) {
236 case Gecode::IRT_EQ: olog << "="; break;
237 case Gecode::IRT_NQ: olog << "!="; break;
238 case Gecode::IRT_LQ: olog << "<="; break;
239 case Gecode::IRT_LE: olog << "<"; break;
240 case Gecode::IRT_GQ: olog << ">="; break;
241 case Gecode::IRT_GR: olog << ">"; break;
242 }
243 olog << " " << n << std::endl;
244 }
245 Gecode::rel(*this, y[i], irt, n);
246 }
247
248 void
249 SetTestSpace::rel(bool sol) {
250 int n = sol ? 1 : 0;
251 assert(reified);
252 if (opt.log)
253 olog << ind(4) << "b = " << n << std::endl;
254 Gecode::rel(*this, r.var(), Gecode::IRT_EQ, n);
255 }
256
257 void
258 SetTestSpace::assign(const SetAssignment& a, Gecode::Support::RandomGenerator& rand) {
259 for (int i=a.size(); i--; ) {
260 CountableSetRanges csv(a.lub, a[i]);
261 Gecode::IntSet ai(csv);
262 rel(i, Gecode::SRT_EQ, ai);
263 if (Base::fixpoint(rand) && failed())
264 return;
265 }
266 for (int i=withInt; i--; ) {
267 rel(i, Gecode::IRT_EQ, a.ints()[i]);
268 if (Base::fixpoint(rand) && failed())
269 return;
270 }
271 }
272
273 bool
274 SetTestSpace::assigned(void) const {
275 for (int i=x.size(); i--; )
276 if (!x[i].assigned())
277 return false;
278 for (int i=y.size(); i--; )
279 if (!y[i].assigned())
280 return false;
281 return true;
282 }
283
284 void
285 SetTestSpace::removeFromLub(int v, int i, const SetAssignment& a) {
286 using namespace Gecode;
287 SetVarUnknownRanges ur(x[i]);
288 CountableSetRanges air(a.lub, a[i]);
289 Gecode::Iter::Ranges::Diff<Gecode::SetVarUnknownRanges,
290 CountableSetRanges> diff(ur, air);
291 Gecode::Iter::Ranges::ToValues<Gecode::Iter::Ranges::Diff
292 <Gecode::SetVarUnknownRanges, CountableSetRanges> > diffV(diff);
293 for (int j=0; j<v; j++, ++diffV) {}
294 rel(i, Gecode::SRT_DISJ, Gecode::IntSet(diffV.val(), diffV.val()));
295 }
296
297 void
298 SetTestSpace::removeFromLub(int v, int i, const SetAssignment& a,
299 SetTestSpace& c) {
300 using namespace Gecode;
301 SetVarUnknownRanges ur(x[i]);
302 CountableSetRanges air(a.lub, a[i]);
303 Gecode::Iter::Ranges::Diff<Gecode::SetVarUnknownRanges,
304 CountableSetRanges> diff(ur, air);
305 Gecode::Iter::Ranges::ToValues<Gecode::Iter::Ranges::Diff
306 <Gecode::SetVarUnknownRanges, CountableSetRanges> > diffV(diff);
307 for (int j=0; j<v; j++, ++diffV) {}
308 rel(i, Gecode::SRT_DISJ, Gecode::IntSet(diffV.val(), diffV.val()));
309 c.rel(i, Gecode::SRT_DISJ, Gecode::IntSet(diffV.val(), diffV.val()));
310 }
311
312 void
313 SetTestSpace::addToGlb(int v, int i, const SetAssignment& a) {
314 using namespace Gecode;
315 SetVarUnknownRanges ur(x[i]);
316 CountableSetRanges air(a.lub, a[i]);
317 Gecode::Iter::Ranges::Inter<Gecode::SetVarUnknownRanges,
318 CountableSetRanges> inter(ur, air);
319 Gecode::Iter::Ranges::ToValues<Gecode::Iter::Ranges::Inter
320 <Gecode::SetVarUnknownRanges, CountableSetRanges> > interV(inter);
321 for (int j=0; j<v; j++, ++interV) {}
322 rel(i, Gecode::SRT_SUP, Gecode::IntSet(interV.val(), interV.val()));
323 }
324
325 void
326 SetTestSpace::addToGlb(int v, int i, const SetAssignment& a,
327 SetTestSpace& c) {
328 using namespace Gecode;
329 SetVarUnknownRanges ur(x[i]);
330 CountableSetRanges air(a.lub, a[i]);
331 Gecode::Iter::Ranges::Inter<Gecode::SetVarUnknownRanges,
332 CountableSetRanges> inter(ur, air);
333 Gecode::Iter::Ranges::ToValues<Gecode::Iter::Ranges::Inter
334 <Gecode::SetVarUnknownRanges, CountableSetRanges> > interV(inter);
335 for (int j=0; j<v; j++, ++interV) {}
336 rel(i, Gecode::SRT_SUP, Gecode::IntSet(interV.val(), interV.val()));
337 c.rel(i, Gecode::SRT_SUP, Gecode::IntSet(interV.val(), interV.val()));
338 }
339
340 bool
341 SetTestSpace::fixprob(void) {
342 if (failed())
343 return true;
344 SetTestSpace* c = static_cast<SetTestSpace*>(clone());
345 if (opt.log)
346 olog << ind(3) << "Testing fixpoint on copy" << std::endl;
347 c->post();
348 if (c->failed()) {
349 delete c; return false;
350 }
351
352 for (int i=x.size(); i--; )
353 if (x[i].glbSize() != c->x[i].glbSize() ||
354 x[i].lubSize() != c->x[i].lubSize() ||
355 x[i].cardMin() != c->x[i].cardMin() ||
356 x[i].cardMax() != c->x[i].cardMax()) {
357 delete c;
358 return false;
359 }
360 for (int i=y.size(); i--; )
361 if (y[i].size() != c->y[i].size()) {
362 delete c; return false;
363 }
364 if (reified && (r.var().size() != c->r.var().size())) {
365 delete c; return false;
366 }
367 if (opt.log)
368 olog << ind(3) << "Finished testing fixpoint on copy" << std::endl;
369 delete c;
370 return true;
371 }
372
373 bool
374 SetTestSpace::same(SetTestSpace& c) {
375 if (opt.log)
376 olog << ind(3) << "Testing whether enabled space is the same"
377 << std::endl;
378 bool f = failed();
379 bool cf = c.failed();
380 if (f != cf)
381 return false;
382 if (f)
383 return true;
384
385 for (int i=x.size(); i--; )
386 if (x[i].glbSize() != c.x[i].glbSize() ||
387 x[i].lubSize() != c.x[i].lubSize() ||
388 x[i].cardMin() != c.x[i].cardMin() ||
389 x[i].cardMax() != c.x[i].cardMax())
390 return false;
391
392 for (int i=y.size(); i--; )
393 if (y[i].size() != c.y[i].size())
394 return false;
395
396 if (reified && (r.var().size() != c.r.var().size()))
397 return false;
398 if (opt.log)
399 olog << ind(3) << "Finished testing whether enabled space is the same"
400 << std::endl;
401 return true;
402 }
403
404 bool
405 SetTestSpace::prune(const SetAssignment& a, Gecode::Support::RandomGenerator& rand) {
406 using namespace Gecode;
407 bool setsAssigned = true;
408 for (int j=x.size(); j--; )
409 if (!x[j].assigned()) {
410 setsAssigned = false;
411 break;
412 }
413 bool intsAssigned = true;
414 for (int j=y.size(); j--; )
415 if (!y[j].assigned()) {
416 intsAssigned = false;
417 break;
418 }
419
420 // Select variable to be pruned
421 int i;
422 if (intsAssigned) {
423 i = rand(x.size());
424 } else if (setsAssigned) {
425 i = rand(y.size());
426 } else {
427 i = rand(x.size()+y.size());
428 }
429
430 if (setsAssigned || i>=x.size()) {
431 if (i>=x.size())
432 i = i-x.size();
433 while (y[i].assigned()) {
434 i = (i+1) % y.size();
435 }
436 // Prune int var
437
438 // Select mode for pruning
439 switch (rand(3)) {
440 case 0:
441 if (a.ints()[i] < y[i].max()) {
442 int v=a.ints()[i]+1+
443 rand(static_cast<unsigned int>(y[i].max()-a.ints()[i]));
444 assert((v > a.ints()[i]) && (v <= y[i].max()));
445 rel(i, Gecode::IRT_LE, v);
446 }
447 break;
448 case 1:
449 if (a.ints()[i] > y[i].min()) {
450 int v=y[i].min()+
451 rand(static_cast<unsigned int>(a.ints()[i]-y[i].min()));
452 assert((v < a.ints()[i]) && (v >= y[i].min()));
453 rel(i, Gecode::IRT_GR, v);
454 }
455 break;
456 default:
457 int v;
458 Gecode::Int::ViewRanges<Gecode::Int::IntView> it(y[i]);
459 unsigned int skip = rand(y[i].size()-1);
460 while (true) {
461 if (it.width() > skip) {
462 v = it.min() + skip;
463 if (v == a.ints()[i]) {
464 if (it.width() == 1) {
465 ++it; v = it.min();
466 } else if (v < it.max()) {
467 ++v;
468 } else {
469 --v;
470 }
471 }
472 break;
473 }
474 skip -= it.width();
475 ++it;
476 }
477 rel(i, Gecode::IRT_NQ, v);
478 }
479 return (!Base::fixpoint(rand) || fixprob());
480 }
481 while (x[i].assigned()) {
482 i = (i+1) % x.size();
483 }
484 Gecode::SetVarUnknownRanges ur1(x[i]);
485 CountableSetRanges air1(a.lub, a[i]);
486 Gecode::Iter::Ranges::Diff<Gecode::SetVarUnknownRanges,
487 CountableSetRanges> diff(ur1, air1);
488 Gecode::SetVarUnknownRanges ur2(x[i]);
489 CountableSetRanges air2(a.lub, a[i]);
490 Gecode::Iter::Ranges::Inter<Gecode::SetVarUnknownRanges,
491 CountableSetRanges> inter(ur2, air2);
492
493 CountableSetRanges aisizer(a.lub, a[i]);
494 unsigned int aisize = Gecode::Iter::Ranges::size(aisizer);
495
496 // Select mode for pruning
497 switch (rand(5)) {
498 case 0:
499 if (inter()) {
500 int v = rand(Gecode::Iter::Ranges::size(inter));
501 addToGlb(v, i, a);
502 }
503 break;
504 case 1:
505 if (diff()) {
506 int v = rand(Gecode::Iter::Ranges::size(diff));
507 removeFromLub(v, i, a);
508 }
509 break;
510 case 2:
511 if (x[i].cardMin() < aisize) {
512 unsigned int newc = x[i].cardMin() + 1 +
513 rand(aisize - x[i].cardMin());
514 assert( newc > x[i].cardMin() );
515 assert( newc <= aisize );
516 cardinality(i, newc, Gecode::Set::Limits::card);
517 }
518 break;
519 case 3:
520 if (x[i].cardMax() > aisize) {
521 unsigned int newc = x[i].cardMax() - 1 -
522 rand(x[i].cardMax() - aisize);
523 assert( newc < x[i].cardMax() );
524 assert( newc >= aisize );
525 cardinality(i, 0, newc);
526 }
527 break;
528 default:
529 if (inter()) {
530 int v = rand(Gecode::Iter::Ranges::size(inter));
531 addToGlb(v, i, a);
532 } else {
533 int v = rand(Gecode::Iter::Ranges::size(diff));
534 removeFromLub(v, i, a);
535 }
536 }
537 return (!Base::fixpoint(rand) || fixprob());
538 }
539
540 bool
541 SetTestSpace::disabled(const SetAssignment& a, SetTestSpace& c, Gecode::Support::RandomGenerator& rand) {
542 c.disable();
543 using namespace Gecode;
544 bool setsAssigned = true;
545 for (int j=x.size(); j--; )
546 if (!x[j].assigned()) {
547 setsAssigned = false;
548 break;
549 }
550 bool intsAssigned = true;
551 for (int j=y.size(); j--; )
552 if (!y[j].assigned()) {
553 intsAssigned = false;
554 break;
555 }
556
557 // Select variable to be pruned
558 int i;
559 if (intsAssigned) {
560 i = rand(x.size());
561 } else if (setsAssigned) {
562 i = rand(y.size());
563 } else {
564 i = rand(x.size()+y.size());
565 }
566
567 if (setsAssigned || i>=x.size()) {
568 if (i>=x.size())
569 i = i-x.size();
570 while (y[i].assigned()) {
571 i = (i+1) % y.size();
572 }
573 // Prune int var
574
575 // Select mode for pruning
576 switch (rand(3)) {
577 case 0:
578 if (a.ints()[i] < y[i].max()) {
579 int v=a.ints()[i]+1+
580 rand(static_cast<unsigned int>(y[i].max()-a.ints()[i]));
581 assert((v > a.ints()[i]) && (v <= y[i].max()));
582 rel(i, Gecode::IRT_LE, v);
583 c.rel(i, Gecode::IRT_LE, v);
584 }
585 break;
586 case 1:
587 if (a.ints()[i] > y[i].min()) {
588 int v=y[i].min()+
589 rand(static_cast<unsigned int>(a.ints()[i]-y[i].min()));
590 assert((v < a.ints()[i]) && (v >= y[i].min()));
591 rel(i, Gecode::IRT_GR, v);
592 c.rel(i, Gecode::IRT_GR, v);
593 }
594 break;
595 default:
596 int v;
597 Gecode::Int::ViewRanges<Gecode::Int::IntView> it(y[i]);
598 unsigned int skip = rand(y[i].size()-1);
599 while (true) {
600 if (it.width() > skip) {
601 v = it.min() + skip;
602 if (v == a.ints()[i]) {
603 if (it.width() == 1) {
604 ++it; v = it.min();
605 } else if (v < it.max()) {
606 ++v;
607 } else {
608 --v;
609 }
610 }
611 break;
612 }
613 skip -= it.width();
614 ++it;
615 }
616 rel(i, Gecode::IRT_NQ, v);
617 c.rel(i, Gecode::IRT_NQ, v);
618 }
619 c.enable();
620 return same(c);
621 }
622 while (x[i].assigned()) {
623 i = (i+1) % x.size();
624 }
625 Gecode::SetVarUnknownRanges ur1(x[i]);
626 CountableSetRanges air1(a.lub, a[i]);
627 Gecode::Iter::Ranges::Diff<Gecode::SetVarUnknownRanges,
628 CountableSetRanges> diff(ur1, air1);
629 Gecode::SetVarUnknownRanges ur2(x[i]);
630 CountableSetRanges air2(a.lub, a[i]);
631 Gecode::Iter::Ranges::Inter<Gecode::SetVarUnknownRanges,
632 CountableSetRanges> inter(ur2, air2);
633
634 CountableSetRanges aisizer(a.lub, a[i]);
635 unsigned int aisize = Gecode::Iter::Ranges::size(aisizer);
636
637 // Select mode for pruning
638 switch (rand(5)) {
639 case 0:
640 if (inter()) {
641 int v = rand(Gecode::Iter::Ranges::size(inter));
642 addToGlb(v, i, a, c);
643 }
644 break;
645 case 1:
646 if (diff()) {
647 int v = rand(Gecode::Iter::Ranges::size(diff));
648 removeFromLub(v, i, a, c);
649 }
650 break;
651 case 2:
652 if (x[i].cardMin() < aisize) {
653 unsigned int newc = x[i].cardMin() + 1 +
654 rand(aisize - x[i].cardMin());
655 assert( newc > x[i].cardMin() );
656 assert( newc <= aisize );
657 cardinality(i, newc, Gecode::Set::Limits::card);
658 c.cardinality(i, newc, Gecode::Set::Limits::card);
659 }
660 break;
661 case 3:
662 if (x[i].cardMax() > aisize) {
663 unsigned int newc = x[i].cardMax() - 1 -
664 rand(x[i].cardMax() - aisize);
665 assert( newc < x[i].cardMax() );
666 assert( newc >= aisize );
667 cardinality(i, 0, newc);
668 c.cardinality(i, 0, newc);
669 }
670 break;
671 default:
672 if (inter()) {
673 int v = rand(Gecode::Iter::Ranges::size(inter));
674 addToGlb(v, i, a, c);
675 } else {
676 int v = rand(Gecode::Iter::Ranges::size(diff));
677 removeFromLub(v, i, a, c);
678 }
679 }
680 c.enable();
681 return same(c);
682 }
683
684 unsigned int
685 SetTestSpace::propagators(void) {
686 return Gecode::PropagatorGroup::all.size(*this);
687 }
688
689 void
690 SetTestSpace::enable(void) {
691 Gecode::PropagatorGroup::all.enable(*this);
692 }
693
694 void
695 SetTestSpace::disable(void) {
696 Gecode::PropagatorGroup::all.disable(*this);
697 (void) status();
698 }
699
700
701 /// Check the test result and handle failed test
702#define CHECK_TEST(T,M) \
703do { \
704if (opt.log) \
705 olog << ind(3) << "Check: " << (M) << std::endl; \
706if (!(T)) { \
707 problem = (M); delete s; goto failed; \
708} \
709} while (false)
710
711 /// Start new test
712#define START_TEST(T) \
713 do { \
714 if (opt.log) { \
715 olog.str(""); \
716 olog << ind(2) << "Testing: " << (T) << std::endl; \
717 } \
718 test = (T); \
719 } while (false)
720
721 bool
722 SetTest::run(void) {
723 using namespace Gecode;
724 const char* test = "NONE";
725 const char* problem = "NONE";
726
727 SetAssignment* ap = new SetAssignment(arity,lub,withInt);
728 SetAssignment& a = *ap;
729 while (a()) {
730 bool is_sol = solution(a);
731 if (opt.log)
732 olog << ind(1) << "Assignment: " << a
733 << (is_sol ? " (solution)" : " (no solution)")
734 << std::endl;
735 START_TEST("Assignment (after posting)");
736 {
737 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this);
738 SetTestSpace* sc = nullptr;
739 s->post();
740 switch (_rand(2)) {
741 case 0:
742 if (opt.log)
743 olog << ind(3) << "No copy" << std::endl;
744 sc = s;
745 s = nullptr;
746 break;
747 case 1:
748 if (opt.log)
749 olog << ind(3) << "Copy" << std::endl;
750 if (s->status() != Gecode::SS_FAILED) {
751 sc = static_cast<SetTestSpace*>(s->clone());
752 } else {
753 sc = s; s = nullptr;
754 }
755 break;
756 default: assert(false);
757 }
758 sc->assign(a, _rand);
759 if (is_sol) {
760 CHECK_TEST(!sc->failed(), "Failed on solution");
761 CHECK_TEST(sc->subsumed(testsubsumed), "No subsumption");
762 } else {
763 CHECK_TEST(sc->failed(), "Solved on non-solution");
764 }
765 delete s; delete sc;
766 }
767 START_TEST("Assignment (after posting, disable)");
768 {
769 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this);
770 s->post();
771 s->disable();
772 s->assign(a, _rand);
773 s->enable();
774 if (is_sol) {
775 CHECK_TEST(!s->failed(), "Failed on solution");
776 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
777 } else {
778 CHECK_TEST(s->failed(), "Solved on non-solution");
779 }
780 delete s;
781 }
782 START_TEST("Assignment (before posting)");
783 {
784 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this);
785 s->assign(a, _rand);
786 s->post();
787 if (is_sol) {
788 CHECK_TEST(!s->failed(), "Failed on solution");
789 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
790 } else {
791 CHECK_TEST(s->failed(), "Solved on non-solution");
792 }
793 delete s;
794 }
795 START_TEST("Prune");
796 {
797 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this);
798 s->post();
799 while (!s->failed() && !s->assigned())
800 if (!s->prune(a, _rand)) {
801 problem = "No fixpoint";
802 delete s;
803 goto failed;
804 }
805 s->assign(a, _rand);
806 if (is_sol) {
807 CHECK_TEST(!s->failed(), "Failed on solution");
808 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
809 } else {
810 CHECK_TEST(s->failed(), "Solved on non-solution");
811 }
812 delete s;
813 }
814 if (disabled) {
815 START_TEST("Prune (disable)");
816 {
817 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this);
818 SetTestSpace* c = new SetTestSpace(arity,lub,withInt,this);
819 s->post(); c->post();
820 while (!s->failed() && !s->assigned())
821 if (!s->disabled(a, *c, _rand)) {
822 problem = "Different result after re-enable";
823 delete s; delete c;
824 goto failed;
825 }
826 s->assign(a, _rand);
827 c->assign(a, _rand);
828 if (s->failed() != c->failed()) {
829 problem = "Different failure after re-enable";
830 delete s; delete c;
831 goto failed;
832 }
833 delete s; delete c;
834 }
835 }
836 if (reified) {
837 START_TEST("Assignment reified (rewrite after post, <=>)");
838 {
839 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
840 s->post();
841 s->rel(is_sol);
842 s->assign(a, _rand);
843 CHECK_TEST(!s->failed(), "Failed");
844 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
845 delete s;
846 }
847 START_TEST("Assignment reified (rewrite after post, =>)");
848 {
849 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
850 s->post();
851 s->rel(is_sol);
852 s->assign(a, _rand);
853 CHECK_TEST(!s->failed(), "Failed");
854 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
855 delete s;
856 }
857 START_TEST("Assignment reified (rewrite after post, <=)");
858 {
859 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
860 s->post();
861 s->rel(is_sol);
862 s->assign(a, _rand);
863 CHECK_TEST(!s->failed(), "Failed");
864 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
865 delete s;
866 }
867 {
868 START_TEST("Assignment reified (rewrite failure, <=>)");
869 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
870 s->post();
871 s->rel(!is_sol);
872 s->assign(a, _rand);
873 CHECK_TEST(s->failed(), "Not failed");
874 delete s;
875 }
876 {
877 START_TEST("Assignment reified (rewrite failure, =>)");
878 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
879 s->post();
880 s->rel(!is_sol);
881 s->assign(a, _rand);
882 if (is_sol) {
883 CHECK_TEST(!s->failed(), "Failed");
884 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
885 } else {
886 CHECK_TEST(s->failed(), "Not failed");
887 }
888 delete s;
889 }
890 {
891 START_TEST("Assignment reified (rewrite failure, <=)");
892 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
893 s->post();
894 s->rel(!is_sol);
895 s->assign(a, _rand);
896 if (is_sol) {
897 CHECK_TEST(s->failed(), "Not failed");
898 } else {
899 CHECK_TEST(!s->failed(), "Failed");
900 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
901 }
902 delete s;
903 }
904 START_TEST("Assignment reified (immediate rewrite, <=>)");
905 {
906 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
907 s->rel(is_sol);
908 s->post();
909 s->assign(a, _rand);
910 CHECK_TEST(!s->failed(), "Failed");
911 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
912 delete s;
913 }
914 START_TEST("Assignment reified (immediate rewrite, =>)");
915 {
916 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
917 s->rel(is_sol);
918 s->post();
919 s->assign(a, _rand);
920 CHECK_TEST(!s->failed(), "Failed");
921 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
922 delete s;
923 }
924 START_TEST("Assignment reified (immediate rewrite, <=)");
925 {
926 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
927 s->rel(is_sol);
928 s->post();
929 s->assign(a, _rand);
930 CHECK_TEST(!s->failed(), "Failed");
931 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
932 delete s;
933 }
934 START_TEST("Assignment reified (immediate failure, <=>)");
935 {
936 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
937 s->rel(!is_sol);
938 s->post();
939 s->assign(a, _rand);
940 CHECK_TEST(s->failed(), "Not failed");
941 delete s;
942 }
943 START_TEST("Assignment reified (immediate failure, =>)");
944 {
945 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
946 s->rel(!is_sol);
947 s->post();
948 s->assign(a, _rand);
949 if (is_sol) {
950 CHECK_TEST(!s->failed(), "Failed");
951 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
952 } else {
953 CHECK_TEST(s->failed(), "Not failed");
954 }
955 delete s;
956 }
957 START_TEST("Assignment reified (immediate failure, <=)");
958 {
959 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
960 s->rel(!is_sol);
961 s->post();
962 s->assign(a, _rand);
963 if (is_sol) {
964 CHECK_TEST(s->failed(), "Not failed");
965 } else {
966 CHECK_TEST(!s->failed(), "Failed");
967 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
968 }
969 delete s;
970 }
971 START_TEST("Assignment reified (before posting, <=>)");
972 {
973 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
974 s->assign(a, _rand);
975 s->post();
976 CHECK_TEST(!s->failed(), "Failed");
977 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
978 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
979 if (is_sol) {
980 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
981 } else {
982 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
983 }
984 delete s;
985 }
986 START_TEST("Assignment reified (before posting, =>)");
987 {
988 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
989 s->assign(a, _rand);
990 s->post();
991 CHECK_TEST(!s->failed(), "Failed");
992 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
993 if (is_sol) {
994 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
995 } else {
996 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
997 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
998 }
999 delete s;
1000 }
1001 START_TEST("Assignment reified (before posting, <=)");
1002 {
1003 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
1004 s->assign(a, _rand);
1005 s->post();
1006 CHECK_TEST(!s->failed(), "Failed");
1007 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1008 if (is_sol) {
1009 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1010 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1011 } else {
1012 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1013 }
1014 delete s;
1015 }
1016 START_TEST("Assignment reified (after posting, <=>)");
1017 {
1018 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
1019 s->post();
1020 s->assign(a, _rand);
1021 CHECK_TEST(!s->failed(), "Failed");
1022 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1023 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1024 if (is_sol) {
1025 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1026 } else {
1027 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
1028 }
1029 delete s;
1030 }
1031 START_TEST("Assignment reified (after posting, =>)");
1032 {
1033 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
1034 s->post();
1035 s->assign(a, _rand);
1036 CHECK_TEST(!s->failed(), "Failed");
1037 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1038 if (is_sol) {
1039 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1040 } else {
1041 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1042 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
1043 }
1044 delete s;
1045 }
1046 START_TEST("Assignment reified (after posting, <=)");
1047 {
1048 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
1049 s->post();
1050 s->assign(a, _rand);
1051 CHECK_TEST(!s->failed(), "Failed");
1052 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1053 if (is_sol) {
1054 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1055 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1056 } else {
1057 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1058 }
1059 delete s;
1060 }
1061 START_TEST("Assignment reified (after posting, <=>, disable)");
1062 {
1063 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
1064 s->post();
1065 s->disable();
1066 s->assign(a, _rand);
1067 s->enable();
1068 CHECK_TEST(!s->failed(), "Failed");
1069 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1070 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1071 if (is_sol) {
1072 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1073 } else {
1074 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
1075 }
1076 delete s;
1077 }
1078 START_TEST("Assignment reified (after posting, =>, disable)");
1079 {
1080 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
1081 s->post();
1082 s->disable();
1083 s->assign(a, _rand);
1084 s->enable();
1085 CHECK_TEST(!s->failed(), "Failed");
1086 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1087 if (is_sol) {
1088 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1089 } else {
1090 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1091 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
1092 }
1093 delete s;
1094 }
1095 START_TEST("Assignment reified (after posting, <=, disable)");
1096 {
1097 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
1098 s->post();
1099 s->disable();
1100 s->assign(a, _rand);
1101 s->enable();
1102 CHECK_TEST(!s->failed(), "Failed");
1103 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1104 if (is_sol) {
1105 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1106 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1107 } else {
1108 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1109 }
1110 delete s;
1111 }
1112 START_TEST("Prune reified, <=>");
1113 {
1114 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
1115 s->post();
1116 while (!s->failed() &&
1117 (!s->assigned() || !s->r.var().assigned()))
1118 if (!s->prune(a, _rand)) {
1119 problem = "No fixpoint";
1120 delete s;
1121 goto failed;
1122 }
1123 CHECK_TEST(!s->failed(), "Failed");
1124 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1125 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1126 if (is_sol) {
1127 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1128 } else {
1129 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
1130 }
1131 delete s;
1132 }
1133 START_TEST("Prune reified, =>");
1134 {
1135 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
1136 s->post();
1137 while (!s->failed() &&
1138 (!s->assigned() || (!is_sol && !s->r.var().assigned()))) {
1139 if (!s->prune(a, _rand)) {
1140 problem = "No fixpoint";
1141 delete s;
1142 goto failed;
1143 }
1144 }
1145 CHECK_TEST(!s->failed(), "Failed");
1146 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1147 if (is_sol) {
1148 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1149 } else {
1150 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1151 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
1152 }
1153 delete s;
1154 }
1155 START_TEST("Prune reified, <=");
1156 {
1157 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
1158 s->post();
1159 while (!s->failed() &&
1160 (!s->assigned() || (is_sol && !s->r.var().assigned())))
1161 if (!s->prune(a, _rand)) {
1162 problem = "No fixpoint";
1163 delete s;
1164 goto failed;
1165 }
1166 CHECK_TEST(!s->failed(), "Failed");
1167 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1168 if (is_sol) {
1169 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1170 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1171 } else {
1172 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1173 }
1174 delete s;
1175 }
1176 }
1177 a.next(_rand);
1178 }
1179 delete ap;
1180 return true;
1181 failed:
1182 if (opt.log)
1183 olog << "FAILURE" << std::endl
1184 << ind(1) << "Test: " << test << std::endl
1185 << ind(1) << "Problem: " << problem << std::endl;
1186 if (a() && opt.log)
1187 olog << ind(1) << "Assignment: " << a << std::endl;
1188 delete ap;
1189
1190 return false;
1191 }
1192
1193 const Gecode::SetRelType SetRelTypes::srts[] =
1194 {Gecode::SRT_EQ,Gecode::SRT_NQ,Gecode::SRT_SUB,
1195 Gecode::SRT_SUP,Gecode::SRT_DISJ,Gecode::SRT_CMPL};
1196
1197 const Gecode::SetOpType SetOpTypes::sots[] =
1198 {Gecode::SOT_UNION, Gecode::SOT_DUNION,
1199 Gecode::SOT_INTER, Gecode::SOT_MINUS};
1200
1201}}
1202
1203#undef START_TEST
1204#undef CHECK_TEST
1205
1206// STATISTICS: test-set