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::operator++(void) {
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;
90 if (ir()) {
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) {
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() && failed())
264 return;
265 }
266 for (int i=withInt; i--; ) {
267 rel(i, Gecode::IRT_EQ, a.ints()[i]);
268 if (Base::fixpoint() && 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) {
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 = Base::rand(x.size());
424 } else if (setsAssigned) {
425 i = Base::rand(y.size());
426 } else {
427 i = Base::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 (Base::rand(3)) {
440 case 0:
441 if (a.ints()[i] < y[i].max()) {
442 int v=a.ints()[i]+1+
443 Base::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 Base::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 = Base::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() || 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 (Base::rand(5)) {
498 case 0:
499 if (inter()) {
500 int v = Base::rand(Gecode::Iter::Ranges::size(inter));
501 addToGlb(v, i, a);
502 }
503 break;
504 case 1:
505 if (diff()) {
506 int v = Base::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 Base::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 Base::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 = Base::rand(Gecode::Iter::Ranges::size(inter));
531 addToGlb(v, i, a);
532 } else {
533 int v = Base::rand(Gecode::Iter::Ranges::size(diff));
534 removeFromLub(v, i, a);
535 }
536 }
537 return (!Base::fixpoint() || fixprob());
538 }
539
540 bool
541 SetTestSpace::disabled(const SetAssignment& a, SetTestSpace& c) {
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 = Base::rand(x.size());
561 } else if (setsAssigned) {
562 i = Base::rand(y.size());
563 } else {
564 i = Base::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 (Base::rand(3)) {
577 case 0:
578 if (a.ints()[i] < y[i].max()) {
579 int v=a.ints()[i]+1+
580 Base::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 Base::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 = Base::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 (Base::rand(5)) {
639 case 0:
640 if (inter()) {
641 int v = Base::rand(Gecode::Iter::Ranges::size(inter));
642 addToGlb(v, i, a, c);
643 }
644 break;
645 case 1:
646 if (diff()) {
647 int v = Base::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 Base::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 Base::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 = Base::rand(Gecode::Iter::Ranges::size(inter));
674 addToGlb(v, i, a, c);
675 } else {
676 int v = Base::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) \
703if (opt.log) \
704 olog << ind(3) << "Check: " << (M) << std::endl; \
705if (!(T)) { \
706 problem = (M); delete s; goto failed; \
707}
708
709 /// Start new test
710#define START_TEST(T) \
711 if (opt.log) { \
712 olog.str(""); \
713 olog << ind(2) << "Testing: " << (T) << std::endl; \
714 } \
715 test = (T);
716
717 bool
718 SetTest::run(void) {
719 using namespace Gecode;
720 const char* test = "NONE";
721 const char* problem = "NONE";
722
723 SetAssignment* ap = new SetAssignment(arity,lub,withInt);
724 SetAssignment& a = *ap;
725 while (a()) {
726 bool is_sol = solution(a);
727 if (opt.log)
728 olog << ind(1) << "Assignment: " << a
729 << (is_sol ? " (solution)" : " (no solution)")
730 << std::endl;
731 START_TEST("Assignment (after posting)");
732 {
733 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this);
734 SetTestSpace* sc = nullptr;
735 s->post();
736 switch (Base::rand(2)) {
737 case 0:
738 if (opt.log)
739 olog << ind(3) << "No copy" << std::endl;
740 sc = s;
741 s = nullptr;
742 break;
743 case 1:
744 if (opt.log)
745 olog << ind(3) << "Copy" << std::endl;
746 if (s->status() != Gecode::SS_FAILED) {
747 sc = static_cast<SetTestSpace*>(s->clone());
748 } else {
749 sc = s; s = nullptr;
750 }
751 break;
752 default: assert(false);
753 }
754 sc->assign(a);
755 if (is_sol) {
756 CHECK_TEST(!sc->failed(), "Failed on solution");
757 CHECK_TEST(sc->subsumed(testsubsumed), "No subsumption");
758 } else {
759 CHECK_TEST(sc->failed(), "Solved on non-solution");
760 }
761 delete s; delete sc;
762 }
763 START_TEST("Assignment (after posting, disable)");
764 {
765 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this);
766 s->post();
767 s->disable();
768 s->assign(a);
769 s->enable();
770 if (is_sol) {
771 CHECK_TEST(!s->failed(), "Failed on solution");
772 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
773 } else {
774 CHECK_TEST(s->failed(), "Solved on non-solution");
775 }
776 delete s;
777 }
778 START_TEST("Assignment (before posting)");
779 {
780 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this);
781 s->assign(a);
782 s->post();
783 if (is_sol) {
784 CHECK_TEST(!s->failed(), "Failed on solution");
785 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
786 } else {
787 CHECK_TEST(s->failed(), "Solved on non-solution");
788 }
789 delete s;
790 }
791 START_TEST("Prune");
792 {
793 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this);
794 s->post();
795 while (!s->failed() && !s->assigned())
796 if (!s->prune(a)) {
797 problem = "No fixpoint";
798 delete s;
799 goto failed;
800 }
801 s->assign(a);
802 if (is_sol) {
803 CHECK_TEST(!s->failed(), "Failed on solution");
804 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
805 } else {
806 CHECK_TEST(s->failed(), "Solved on non-solution");
807 }
808 delete s;
809 }
810 if (disabled) {
811 START_TEST("Prune (disable)");
812 {
813 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this);
814 SetTestSpace* c = new SetTestSpace(arity,lub,withInt,this);
815 s->post(); c->post();
816 while (!s->failed() && !s->assigned())
817 if (!s->disabled(a,*c)) {
818 problem = "Different result after re-enable";
819 delete s; delete c;
820 goto failed;
821 }
822 s->assign(a); c->assign(a);
823 if (s->failed() != c->failed()) {
824 problem = "Different failure after re-enable";
825 delete s; delete c;
826 goto failed;
827 }
828 delete s; delete c;
829 }
830 }
831 if (reified) {
832 START_TEST("Assignment reified (rewrite after post, <=>)");
833 {
834 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
835 s->post();
836 s->rel(is_sol);
837 s->assign(a);
838 CHECK_TEST(!s->failed(), "Failed");
839 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
840 delete s;
841 }
842 START_TEST("Assignment reified (rewrite after post, =>)");
843 {
844 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
845 s->post();
846 s->rel(is_sol);
847 s->assign(a);
848 CHECK_TEST(!s->failed(), "Failed");
849 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
850 delete s;
851 }
852 START_TEST("Assignment reified (rewrite after post, <=)");
853 {
854 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
855 s->post();
856 s->rel(is_sol);
857 s->assign(a);
858 CHECK_TEST(!s->failed(), "Failed");
859 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
860 delete s;
861 }
862 {
863 START_TEST("Assignment reified (rewrite failure, <=>)");
864 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
865 s->post();
866 s->rel(!is_sol);
867 s->assign(a);
868 CHECK_TEST(s->failed(), "Not failed");
869 delete s;
870 }
871 {
872 START_TEST("Assignment reified (rewrite failure, =>)");
873 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
874 s->post();
875 s->rel(!is_sol);
876 s->assign(a);
877 if (is_sol) {
878 CHECK_TEST(!s->failed(), "Failed");
879 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
880 } else {
881 CHECK_TEST(s->failed(), "Not failed");
882 }
883 delete s;
884 }
885 {
886 START_TEST("Assignment reified (rewrite failure, <=)");
887 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
888 s->post();
889 s->rel(!is_sol);
890 s->assign(a);
891 if (is_sol) {
892 CHECK_TEST(s->failed(), "Not failed");
893 } else {
894 CHECK_TEST(!s->failed(), "Failed");
895 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
896 }
897 delete s;
898 }
899 START_TEST("Assignment reified (immediate rewrite, <=>)");
900 {
901 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
902 s->rel(is_sol);
903 s->post();
904 s->assign(a);
905 CHECK_TEST(!s->failed(), "Failed");
906 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
907 delete s;
908 }
909 START_TEST("Assignment reified (immediate rewrite, =>)");
910 {
911 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
912 s->rel(is_sol);
913 s->post();
914 s->assign(a);
915 CHECK_TEST(!s->failed(), "Failed");
916 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
917 delete s;
918 }
919 START_TEST("Assignment reified (immediate rewrite, <=)");
920 {
921 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
922 s->rel(is_sol);
923 s->post();
924 s->assign(a);
925 CHECK_TEST(!s->failed(), "Failed");
926 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
927 delete s;
928 }
929 START_TEST("Assignment reified (immediate failure, <=>)");
930 {
931 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
932 s->rel(!is_sol);
933 s->post();
934 s->assign(a);
935 CHECK_TEST(s->failed(), "Not failed");
936 delete s;
937 }
938 START_TEST("Assignment reified (immediate failure, =>)");
939 {
940 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
941 s->rel(!is_sol);
942 s->post();
943 s->assign(a);
944 if (is_sol) {
945 CHECK_TEST(!s->failed(), "Failed");
946 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
947 } else {
948 CHECK_TEST(s->failed(), "Not failed");
949 }
950 delete s;
951 }
952 START_TEST("Assignment reified (immediate failure, <=)");
953 {
954 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
955 s->rel(!is_sol);
956 s->post();
957 s->assign(a);
958 if (is_sol) {
959 CHECK_TEST(s->failed(), "Not failed");
960 } else {
961 CHECK_TEST(!s->failed(), "Failed");
962 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
963 }
964 delete s;
965 }
966 START_TEST("Assignment reified (before posting, <=>)");
967 {
968 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
969 s->assign(a);
970 s->post();
971 CHECK_TEST(!s->failed(), "Failed");
972 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
973 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
974 if (is_sol) {
975 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
976 } else {
977 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
978 }
979 delete s;
980 }
981 START_TEST("Assignment reified (before posting, =>)");
982 {
983 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
984 s->assign(a);
985 s->post();
986 CHECK_TEST(!s->failed(), "Failed");
987 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
988 if (is_sol) {
989 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
990 } else {
991 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
992 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
993 }
994 delete s;
995 }
996 START_TEST("Assignment reified (before posting, <=)");
997 {
998 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
999 s->assign(a);
1000 s->post();
1001 CHECK_TEST(!s->failed(), "Failed");
1002 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1003 if (is_sol) {
1004 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1005 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1006 } else {
1007 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1008 }
1009 delete s;
1010 }
1011 START_TEST("Assignment reified (after posting, <=>)");
1012 {
1013 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
1014 s->post();
1015 s->assign(a);
1016 CHECK_TEST(!s->failed(), "Failed");
1017 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1018 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1019 if (is_sol) {
1020 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1021 } else {
1022 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
1023 }
1024 delete s;
1025 }
1026 START_TEST("Assignment reified (after posting, =>)");
1027 {
1028 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
1029 s->post();
1030 s->assign(a);
1031 CHECK_TEST(!s->failed(), "Failed");
1032 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1033 if (is_sol) {
1034 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1035 } else {
1036 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1037 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
1038 }
1039 delete s;
1040 }
1041 START_TEST("Assignment reified (after posting, <=)");
1042 {
1043 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
1044 s->post();
1045 s->assign(a);
1046 CHECK_TEST(!s->failed(), "Failed");
1047 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1048 if (is_sol) {
1049 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1050 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1051 } else {
1052 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1053 }
1054 delete s;
1055 }
1056 START_TEST("Assignment reified (after posting, <=>, disable)");
1057 {
1058 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
1059 s->post();
1060 s->disable();
1061 s->assign(a);
1062 s->enable();
1063 CHECK_TEST(!s->failed(), "Failed");
1064 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1065 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1066 if (is_sol) {
1067 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1068 } else {
1069 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
1070 }
1071 delete s;
1072 }
1073 START_TEST("Assignment reified (after posting, =>, disable)");
1074 {
1075 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
1076 s->post();
1077 s->disable();
1078 s->assign(a);
1079 s->enable();
1080 CHECK_TEST(!s->failed(), "Failed");
1081 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1082 if (is_sol) {
1083 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1084 } else {
1085 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1086 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
1087 }
1088 delete s;
1089 }
1090 START_TEST("Assignment reified (after posting, <=, disable)");
1091 {
1092 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
1093 s->post();
1094 s->disable();
1095 s->assign(a);
1096 s->enable();
1097 CHECK_TEST(!s->failed(), "Failed");
1098 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1099 if (is_sol) {
1100 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1101 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1102 } else {
1103 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1104 }
1105 delete s;
1106 }
1107 START_TEST("Prune reified, <=>");
1108 {
1109 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_EQV);
1110 s->post();
1111 while (!s->failed() &&
1112 (!s->assigned() || !s->r.var().assigned()))
1113 if (!s->prune(a)) {
1114 problem = "No fixpoint";
1115 delete s;
1116 goto failed;
1117 }
1118 CHECK_TEST(!s->failed(), "Failed");
1119 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1120 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1121 if (is_sol) {
1122 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1123 } else {
1124 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
1125 }
1126 delete s;
1127 }
1128 START_TEST("Prune reified, =>");
1129 {
1130 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_IMP);
1131 s->post();
1132 while (!s->failed() &&
1133 (!s->assigned() || (!is_sol && !s->r.var().assigned()))) {
1134 if (!s->prune(a)) {
1135 problem = "No fixpoint";
1136 delete s;
1137 goto failed;
1138 }
1139 }
1140 CHECK_TEST(!s->failed(), "Failed");
1141 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1142 if (is_sol) {
1143 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1144 } else {
1145 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1146 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
1147 }
1148 delete s;
1149 }
1150 START_TEST("Prune reified, <=");
1151 {
1152 SetTestSpace* s = new SetTestSpace(arity,lub,withInt,this,RM_PMI);
1153 s->post();
1154 while (!s->failed() &&
1155 (!s->assigned() || (is_sol && !s->r.var().assigned())))
1156 if (!s->prune(a)) {
1157 problem = "No fixpoint";
1158 delete s;
1159 goto failed;
1160 }
1161 CHECK_TEST(!s->failed(), "Failed");
1162 CHECK_TEST(s->subsumed(testsubsumed), "No subsumption");
1163 if (is_sol) {
1164 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1165 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1166 } else {
1167 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1168 }
1169 delete s;
1170 }
1171 }
1172 ++a;
1173 }
1174 delete ap;
1175 return true;
1176 failed:
1177 if (opt.log)
1178 olog << "FAILURE" << std::endl
1179 << ind(1) << "Test: " << test << std::endl
1180 << ind(1) << "Problem: " << problem << std::endl;
1181 if (a() && opt.log)
1182 olog << ind(1) << "Assignment: " << a << std::endl;
1183 delete ap;
1184
1185 return false;
1186 }
1187
1188 const Gecode::SetRelType SetRelTypes::srts[] =
1189 {Gecode::SRT_EQ,Gecode::SRT_NQ,Gecode::SRT_SUB,
1190 Gecode::SRT_SUP,Gecode::SRT_DISJ,Gecode::SRT_CMPL};
1191
1192 const Gecode::SetOpType SetOpTypes::sots[] =
1193 {Gecode::SOT_UNION, Gecode::SOT_DUNION,
1194 Gecode::SOT_INTER, Gecode::SOT_MINUS};
1195
1196}}
1197
1198#undef START_TEST
1199#undef CHECK_TEST
1200
1201// STATISTICS: test-set