Generated on Thu Jan 16 2025 00:00:00 for Gecode by doxygen 1.14.0
set.cpp
Go to the documentation of this file.
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) {
46 lubmax =
47 static_cast<unsigned int>(pow(static_cast<double>(2.0),
48 static_cast<int>(Gecode::Iter::Ranges::size(isr))));
49 }
50
52 cur++;
53 }
54
56 d = d0;
57 cur = 0;
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
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
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;
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
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
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);
159 Gecode::BoolVar sr(s.r.var());
160 b.update(*this, sr);
161 r.var(b); r.mode(s.r.mode());
162 }
163
166 return new SetTestSpace(*this);
167 }
168
169 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
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
198 return b ? (propagators() == 0) : true;
199 }
200
201 void
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
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
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
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
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
286 using namespace Gecode;
287 SetVarUnknownRanges ur(x[i]);
288 CountableSetRanges air(a.lub, a[i]);
290 CountableSetRanges> diff(ur, air);
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
299 SetTestSpace& c) {
300 using namespace Gecode;
301 SetVarUnknownRanges ur(x[i]);
302 CountableSetRanges air(a.lub, a[i]);
304 CountableSetRanges> diff(ur, air);
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]);
318 CountableSetRanges> inter(ur, air);
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]);
332 CountableSetRanges> inter(ur, air);
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
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
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
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;
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 }
485 CountableSetRanges air1(a.lub, a[i]);
487 CountableSetRanges> diff(ur1, air1);
489 CountableSetRanges air2(a.lub, a[i]);
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()) {
501 addToGlb(v, i, a);
502 }
503 break;
504 case 1:
505 if (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 );
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()) {
531 addToGlb(v, i, a);
532 } else {
534 removeFromLub(v, i, a);
535 }
536 }
537 return (!Base::fixpoint() || fixprob());
538 }
539
540 bool
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;
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 }
626 CountableSetRanges air1(a.lub, a[i]);
628 CountableSetRanges> diff(ur1, air1);
630 CountableSetRanges air2(a.lub, a[i]);
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()) {
642 addToGlb(v, i, a, c);
643 }
644 break;
645 case 1:
646 if (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 );
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()) {
674 addToGlb(v, i, a, c);
675 } else {
677 removeFromLub(v, i, a, c);
678 }
679 }
680 c.enable();
681 return same(c);
682 }
683
684 unsigned int
686 return Gecode::PropagatorGroup::all.size(*this);
687 }
688
689 void
691 Gecode::PropagatorGroup::all.enable(*this);
692 }
693
694 void
696 Gecode::PropagatorGroup::all.disable(*this);
697 (void) status();
698 }
699
700
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
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
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 = NULL;
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 = NULL;
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 = NULL;
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[] =
1191
1192 const Gecode::SetOpType SetOpTypes::sots[] =
1195
1196}}
1197
1198#undef START_TEST
1199#undef CHECK_TEST
1200
1201// STATISTICS: test-set
Boolean integer variables.
Definition int.hh:515
int val(void) const
Return assigned value.
Definition bool.hpp:57
void assign(FloatNum const &l, FloatNum const &u)
Assign lower bound l and upper bound u.
Definition val.hpp:65
FloatNum size(void) const
Return size of float value (distance between maximum and minimum)
Definition val.hpp:78
Range iterator for integer sets.
Definition int.hh:292
Integer sets.
Definition int.hh:174
static const IntSet empty
Empty set.
Definition int.hh:283
Range iterator for integer views.
Definition view.hpp:54
int max(void) const
Return largest value of range.
int min(void) const
Return smallest value of range.
unsigned int width(void) const
Return width of range (distance between minimum and maximum)
Range iterator for computing set difference.
Range iterator for computing intersection (binary)
Value iterator from range iterator.
static PropagatorGroup all
Group of all propagators.
Definition core.hpp:789
BoolVar var(void) const
Return Boolean control variable.
Definition reify.hpp:48
ReifyMode mode(void) const
Return reification mode.
Definition reify.hpp:56
Passing set variables.
Definition set.hh:491
Set variable array
Definition set.hh:573
Iterator for the unknown ranges of a set variable.
Definition set.hh:337
Computation spaces.
Definition core.hpp:1744
struct Gecode::Space::@055132133326276162005044145100211202071356247106::@155123175027073262103111264343315000271204104107 c
Data available only during copying.
bool assigned(void) const
Test whether view is assigned.
Definition var.hpp:111
static Gecode::Support::RandomGenerator rand
Random number generator.
Definition test.hh:134
static bool fixpoint(void)
Throw a coin whether to compute a fixpoint.
Definition test.hpp:66
Range iterator producing subsets of an IntSet.
Definition set.hh:99
Iterate all subsets of a given set.
Definition set.hh:118
int val(void) const
Return current subset.
Definition set.cpp:64
CountableSet(void)
Default constructor.
Definition set.hh:130
void init(const Gecode::IntSet &s)
Initialize with set s.
Definition set.cpp:55
void operator++(void)
Move to next subset.
Definition set.cpp:51
Generate all set assignments.
Definition set.hh:142
void operator++(void)
Move to next assignment.
Definition set.cpp:76
SetAssignment(int n, const Gecode::IntSet &d, int i=0)
Initialize with n set variables, initial bound d and i int variables.
Definition set.cpp:68
int withInt
How many integer variables to iterate.
Definition set.hh:156
Gecode::IntSet lub
The common superset for all domains.
Definition set.hh:154
Space for executing set tests.
Definition set.hh:182
bool disabled(const SetAssignment &a, SetTestSpace &c)
Prune values also in a space c with disabled propagators, but not those in assignment a.
Definition set.cpp:541
bool subsumed(bool b)
Check for subsumption if b is true.
Definition set.cpp:197
void post(void)
Post propagator.
Definition set.cpp:170
SetTest * test
The test currently run.
Definition set.hh:197
Gecode::SetVarArray x
Set variables to be tested.
Definition set.hh:187
bool assigned(void) const
Test whether all variables are assigned.
Definition set.cpp:274
Gecode::IntSet d
Initial domain.
Definition set.hh:185
void removeFromLub(int v, int i, const SetAssignment &a)
Remove value v from the upper bound of x[i].
Definition set.cpp:285
bool fixprob(void)
Perform fixpoint computation.
Definition set.cpp:341
virtual Gecode::Space * copy(void)
Copy space during cloning.
Definition set.cpp:165
Gecode::Reify r
Reification information.
Definition set.hh:193
SetTestSpace(int n, Gecode::IntSet &d0, int i, SetTest *t, bool log=true)
Create test space without reification.
Definition set.cpp:120
Gecode::IntVarArray y
Int variables to be tested.
Definition set.hh:189
bool failed(void)
Compute a fixpoint and check for failure.
Definition set.cpp:183
void disable(void)
Disable propagators in space and compute fixpoint (make all idle)
Definition set.cpp:695
void rel(int i, Gecode::SetRelType srt, const Gecode::IntSet &is)
Perform set tell operation on x[i].
Definition set.cpp:202
bool reified
Whether the test is for a reified propagator.
Definition set.hh:195
bool prune(const SetAssignment &a)
Perform random pruning.
Definition set.cpp:405
void addToGlb(int v, int i, const SetAssignment &a)
Remove value v from the lower bound of x[i].
Definition set.cpp:313
bool same(SetTestSpace &c)
Check whether propagation is the same as in c.
Definition set.cpp:374
void cardinality(int i, int cmin, int cmax)
Perform cardinality tell operation on x[i].
Definition set.cpp:223
void assign(const SetAssignment &a)
Assign all variables to values in a.
Definition set.cpp:258
void enable(void)
Enable propagators in space.
Definition set.cpp:690
unsigned int propagators(void)
Return the number of propagators.
Definition set.cpp:685
int withInt
How many integer variables are used by the test.
Definition set.hh:191
Base class for tests with set constraints
Definition set.hh:273
bool testsubsumed
Whether to check for subsumption.
Definition set.hh:295
virtual bool run(void)
Perform test.
Definition set.cpp:718
bool disabled
Whether to perform full tests for disabled propagators.
Definition set.hh:293
virtual bool solution(const SetAssignment &) const =0
Check for solution.
Simple class for describing identation.
Definition test.hh:66
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVar x1)
Post propagator for .
Definition rel.cpp:68
IntRelType
Relation types for integers.
Definition int.hh:940
ReifyMode
Mode for reification.
Definition int.hh:863
@ IRT_EQ
Equality ( )
Definition int.hh:941
@ IRT_NQ
Disequality ( )
Definition int.hh:942
@ IRT_GQ
Greater or equal ( )
Definition int.hh:945
@ IRT_LE
Less ( )
Definition int.hh:944
@ IRT_GR
Greater ( )
Definition int.hh:946
@ IRT_LQ
Less or equal ( )
Definition int.hh:943
@ RM_IMP
Implication for reification.
Definition int.hh:877
@ RM_PMI
Inverse implication for reification.
Definition int.hh:884
@ RM_EQV
Equivalence for reification (default)
Definition int.hh:870
Space(void)
Default constructor.
Definition core.cpp:115
SetOpType
Common operations for sets.
Definition set.hh:666
SetRelType
Common relation types for sets.
Definition set.hh:649
@ SOT_MINUS
Difference.
Definition set.hh:670
@ SOT_DUNION
Disjoint union.
Definition set.hh:668
@ SOT_UNION
Union.
Definition set.hh:667
@ SOT_INTER
Intersection
Definition set.hh:669
@ SRT_GQ
Greater or equal ( )
Definition set.hh:658
@ SRT_CMPL
Complement.
Definition set.hh:655
@ SRT_GR
Greater ( )
Definition set.hh:659
@ SRT_LQ
Less or equal ( )
Definition set.hh:656
@ SRT_NQ
Disequality ( )
Definition set.hh:651
@ SRT_LE
Less ( )
Definition set.hh:657
@ SRT_EQ
Equality ( )
Definition set.hh:650
@ SRT_SUP
Superset ( )
Definition set.hh:653
@ SRT_DISJ
Disjoint ( )
Definition set.hh:654
@ SRT_SUB
Subset ( )
Definition set.hh:652
SpaceStatus status(StatusStatistics &stat=unused_status)
Query space status.
Definition core.cpp:252
Space * clone(CloneStatistics &stat=unused_clone) const
Clone space.
Definition core.hpp:3228
@ SS_FAILED
Space is failed
Definition core.hpp:1684
unsigned int size(I &i)
Size of all ranges of range iterator i.
const int min
Smallest allowed integer in integer set.
Definition set.hh:99
const unsigned int card
Maximum cardinality of an integer set.
Definition set.hh:101
const int max
Largest allowed integer in integer set.
Definition set.hh:97
Gecode toplevel namespace
void dom(Home home, FloatVar x, FloatVal n)
Propagates .
Definition dom.cpp:40
SetExpr inter(const SetVarArgs &)
Intersection of set variables.
Definition set-expr.cpp:696
void log(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
LinIntExpr cardinality(const SetExpr &)
Cardinality of set expression.
Definition set-expr.cpp:817
Testing finite sets.
Definition set.cpp:42
General test support.
Definition afc.cpp:39
std::ostringstream olog
Stream used for logging.
Definition test.cpp:53
Options opt
The options.
Definition test.cpp:97
#define START_TEST(T)
Start new test.
Definition array.cpp:48
#define CHECK_TEST(T, M)
Check the test result and handle failed test.
Definition array.cpp:40
std::ostream & operator<<(std::ostream &os, const Test::Set::SetAssignment &a)
Definition set.cpp:105