Generated on Tue Feb 11 2025 17:33:26 for Gecode by doxygen 1.12.0
int.cpp
Go to the documentation of this file.
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Christian Schulte <schulte@gecode.org>
5 * Mikael Lagerkvist <lagerkvist@gecode.org>
6 *
7 * Copyright:
8 * Christian Schulte, 2005
9 * Mikael Lagerkvist, 2005
10 *
11 * This file is part of Gecode, the generic constraint
12 * development environment:
13 * http://www.gecode.org
14 *
15 * Permission is hereby granted, free of charge, to any person obtaining
16 * a copy of this software and associated documentation files (the
17 * "Software"), to deal in the Software without restriction, including
18 * without limitation the rights to use, copy, modify, merge, publish,
19 * distribute, sublicense, and/or sell copies of the Software, and to
20 * permit persons to whom the Software is furnished to do so, subject to
21 * the following conditions:
22 *
23 * The above copyright notice and this permission notice shall be
24 * included in all copies or substantial portions of the Software.
25 *
26 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
27 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
28 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
29 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
30 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
31 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
32 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
33 *
34 */
35
36#include "test/int.hh"
37
38#include <algorithm>
39
40namespace Test { namespace Int {
41
42
43 /*
44 * Complete assignments
45 *
46 */
47 void
49 int i = n-1;
50 while (true) {
51 ++dsv[i];
52 if (dsv[i]() || (i == 0))
53 return;
54 dsv[i--].init(d);
55 }
56 }
57
58 /*
59 * Random assignments
60 *
61 */
62 void
64 for (int i = n; i--; )
65 vals[i]=randval();
66 a--;
67 }
68
69 void
71 for (int i=n-_n1; i--; )
72 vals[i] = randval(d);
73 for (int i=_n1; i--; )
74 vals[n-_n1+i] = randval(_d1);
75 a--;
76 }
77
78}}
79
80std::ostream&
81operator<<(std::ostream& os, const Test::Int::Assignment& a) {
82 int n = a.size();
83 os << "{";
84 for (int i=0; i<n; i++)
85 os << a[i] << ((i!=n-1) ? "," : "}");
86 return os;
87}
88
89namespace Test { namespace Int {
90
92 : d(d0), x(*this,n,Gecode::Int::Limits::min,Gecode::Int::Limits::max),
93 test(t), reified(false) {
94 Gecode::IntVarArgs _x(*this,n,d);
95 if (x.size() == 1)
96 Gecode::dom(*this,x[0],_x[0]);
97 else
98 Gecode::dom(*this,x,_x);
99 Gecode::BoolVar b(*this,0,1);
101 if (opt.log)
102 olog << ind(2) << "Initial: x[]=" << x
103 << std::endl;
104 }
105
108 : d(d0), x(*this,n,Gecode::Int::Limits::min,Gecode::Int::Limits::max),
109 test(t), reified(true) {
110 Gecode::IntVarArgs _x(*this,n,d);
111 if (x.size() == 1)
112 Gecode::dom(*this,x[0],_x[0]);
113 else
114 Gecode::dom(*this,x,_x);
115 Gecode::BoolVar b(*this,0,1);
116 r = Gecode::Reify(b,rm);
117 if (opt.log)
118 olog << ind(2) << "Initial: x[]=" << x
119 << " b=" << r.var() << std::endl;
120 }
121
123 : Gecode::Space(s), d(s.d), test(s.test), reified(s.reified) {
124 x.update(*this, s.x);
126 Gecode::BoolVar sr(s.r.var());
127 b.update(*this, sr);
128 r.var(b); r.mode(s.r.mode());
129 }
130
133 return new TestSpace(*this);
134 }
135
136 bool
138 for (int i=x.size(); i--; )
139 if (!x[i].assigned())
140 return false;
141 return true;
142 }
143
144 void
146 if (reified){
147 test->post(*this,x,r);
148 if (opt.log)
149 olog << ind(3) << "Posting reified propagator" << std::endl;
150 } else {
151 test->post(*this,x);
152 if (opt.log)
153 olog << ind(3) << "Posting propagator" << std::endl;
154 }
155 }
156
157 bool
159 if (opt.log) {
160 olog << ind(3) << "Fixpoint: " << x;
161 bool f=(status() == Gecode::SS_FAILED);
162 olog << std::endl << ind(3) << " --> " << x << std::endl;
163 return f;
164 } else {
165 return status() == Gecode::SS_FAILED;
166 }
167 }
168
169 int
171 assert(!assigned());
172 // Select variable to be pruned
173 int i = static_cast<int>(Base::rand(static_cast<unsigned int>(x.size())));
174 while (x[i].assigned()) {
175 i = (i+1) % x.size();
176 }
177 return i;
178 }
179
180 void
182 Gecode::IntRelType& irt, int& v) {
183 using namespace Gecode;
184 // Select mode for pruning
185 irt = IRT_EQ; // Means do nothing!
186 switch (Base::rand(3)) {
187 case 0:
188 if (a[i] < x[i].max()) {
189 v=a[i]+1+
190 static_cast<int>(Base::rand(static_cast
191 <unsigned int>(x[i].max()-a[i])));
192 assert((v > a[i]) && (v <= x[i].max()));
193 irt = IRT_LE;
194 }
195 break;
196 case 1:
197 if (a[i] > x[i].min()) {
198 v=x[i].min()+
199 static_cast<int>(Base::rand(static_cast
200 <unsigned int>(a[i]-x[i].min())));
201 assert((v < a[i]) && (v >= x[i].min()));
202 irt = IRT_GR;
203 }
204 break;
205 default:
206 {
208 unsigned int skip =
209 Base::rand(static_cast<unsigned int>(x[i].size()-1));
210 while (true) {
211 if (it.width() > skip) {
212 v = it.min() + static_cast<int>(skip);
213 if (v == a[i]) {
214 if (it.width() == 1) {
215 ++it; v = it.min();
216 } else if (v < it.max()) {
217 ++v;
218 } else {
219 --v;
220 }
221 }
222 break;
223 }
224 skip -= it.width(); ++it;
225 }
226 irt = IRT_NQ;
227 break;
228 }
229 }
230 }
231
232 void
234 if (opt.log) {
235 olog << ind(4) << "x[" << i << "] ";
236 switch (irt) {
237 case Gecode::IRT_EQ: olog << "="; break;
238 case Gecode::IRT_NQ: olog << "!="; break;
239 case Gecode::IRT_LQ: olog << "<="; break;
240 case Gecode::IRT_LE: olog << "<"; break;
241 case Gecode::IRT_GQ: olog << ">="; break;
242 case Gecode::IRT_GR: olog << ">"; break;
243 }
244 olog << " " << n << std::endl;
245 }
246 Gecode::rel(*this, x[i], irt, n);
247 }
248
249 void
250 TestSpace::rel(bool sol) {
251 int n = sol ? 1 : 0;
252 assert(reified);
253 if (opt.log)
254 olog << ind(4) << "b = " << n << std::endl;
255 Gecode::rel(*this, r.var(), Gecode::IRT_EQ, n);
256 }
257
258 void
259 TestSpace::assign(const Assignment& a, bool skip) {
260 using namespace Gecode;
261 int i = skip ?
262 static_cast<int>(Base::rand(static_cast<unsigned int>(a.size()))) : -1;
263 for (int j=a.size(); j--; )
264 if (i != j) {
265 rel(j, IRT_EQ, a[j]);
266 if (Base::fixpoint() && failed())
267 return;
268 }
269 }
270
271 void
273 using namespace Gecode;
274 int i = rndvar();
275 bool min = Base::rand(2);
276 rel(i, IRT_EQ, min ? x[i].min() : x[i].max());
277 }
278
279 void
280 TestSpace::prune(int i, bool bounds_only) {
281 using namespace Gecode;
282 // Prune values
283 if (bounds_only) {
284 if (Base::rand(2) && !x[i].assigned()) {
285 int v=x[i].min()+1+
286 static_cast<int>(Base::rand(static_cast
287 <unsigned int>(x[i].max()-x[i].min())));
288 assert((v > x[i].min()) && (v <= x[i].max()));
289 rel(i, Gecode::IRT_LE, v);
290 }
291 if (Base::rand(2) && !x[i].assigned()) {
292 int v=x[i].min()+
293 static_cast<int>(Base::rand(static_cast
294 <unsigned int>(x[i].max()-x[i].min())));
295 assert((v < x[i].max()) && (v >= x[i].min()));
296 rel(i, Gecode::IRT_GR, v);
297 }
298 } else {
299 for (int vals =
300 static_cast<int>(Base::rand(static_cast<unsigned int>(x[i].size()-1))+1); vals--; ) {
301 int v;
303 unsigned int skip = Base::rand(x[i].size()-1);
304 while (true) {
305 if (it.width() > skip) {
306 v = it.min() + static_cast<int>(skip); break;
307 }
308 skip -= it.width(); ++it;
309 }
310 rel(i, IRT_NQ, v);
311 }
312 }
313 }
314
315 void
317 prune(rndvar(), false);
318 }
319
320 bool
321 TestSpace::prune(const Assignment& a, bool testfix) {
322 using namespace Gecode;
323 // Select variable to be pruned
324 int i = rndvar();
325 // Select mode for pruning
326 IntRelType irt;
327 int v;
328 rndrel(a,i,irt,v);
329 if (irt != IRT_EQ)
330 rel(i, irt, v);
331 if (Base::fixpoint()) {
332 if (failed() || !testfix)
333 return true;
334 TestSpace* c = static_cast<TestSpace*>(clone());
335 if (opt.log)
336 olog << ind(3) << "Testing fixpoint on copy" << std::endl;
337 c->post();
338 if (c->failed()) {
339 if (opt.log)
340 olog << ind(4) << "Copy failed after posting" << std::endl;
341 delete c; return false;
342 }
343 for (int j=x.size(); j--; )
344 if (x[j].size() != c->x[j].size()) {
345 if (opt.log)
346 olog << ind(4) << "Different domain size" << std::endl;
347 delete c; return false;
348 }
349 if (reified && (r.var().size() != c->r.var().size())) {
350 if (opt.log)
351 olog << ind(4) << "Different control variable" << std::endl;
352 delete c; return false;
353 }
354 if (opt.log)
355 olog << ind(3) << "Finished testing fixpoint on copy" << std::endl;
356 delete c;
357 }
358 return true;
359 }
360
361 void
365
366 void
369 (void) status();
370 }
371
372 bool
374 bool testfix) {
375 using namespace Gecode;
376 // Disable propagators
377 c.disable();
378 // Select variable to be pruned
379 int i = rndvar();
380 // Select mode for pruning
381 IntRelType irt;
382 int v;
383 rndrel(a,i,irt,v);
384 if (irt != IRT_EQ) {
385 rel(i, irt, v);
386 c.rel(i, irt, v);
387 }
388 // Enable propagators
389 c.enable();
390 if (!testfix)
391 return true;
392 if (failed()) {
393 if (!c.failed()) {
394 if (opt.log)
395 olog << ind(3) << "No failure on disabled copy" << std::endl;
396 return false;
397 }
398 return true;
399 }
400 if (c.failed()) {
401 if (opt.log)
402 olog << ind(3) << "Failure on disabled copy" << std::endl;
403 return false;
404 }
405 for (int j=x.size(); j--; ) {
406 if (x[j].size() != c.x[j].size()) {
407 if (opt.log)
408 olog << ind(4) << "Different domain size" << std::endl;
409 return false;
410 }
411 if (reified && (r.var().size() != c.r.var().size())) {
412 if (opt.log)
413 olog << ind(4) << "Different control variable" << std::endl;
414 return false;
415 }
416 }
417 return true;
418 }
419
420 unsigned int
424
425 const Gecode::IntPropLevel IntPropLevels::ipls[] =
427
428 const Gecode::IntPropLevel IntPropBasicAdvanced::ipls[] =
430
431 const Gecode::IntRelType IntRelTypes::irts[] =
434
435 const Gecode::BoolOpType BoolOpTypes::bots[] =
438
439 Assignment*
440 Test::assignment(void) const {
441 return new CpltAssignment(arity,dom);
442 }
443
444
446#define CHECK_TEST(T,M) \
447if (opt.log) \
448 olog << ind(3) << "Check: " << (M) << std::endl; \
449if (!(T)) { \
450 problem = (M); delete s; goto failed; \
451}
452
454#define START_TEST(T) \
455 if (opt.log) { \
456 olog.str(""); \
457 olog << ind(2) << "Testing: " << (T) << std::endl; \
458 } \
459 test = (T);
460
461 bool
462 Test::ignore(const Assignment&) const {
463 return false;
464 }
465
466 void
469
470 bool
471 Test::run(void) {
472 using namespace Gecode;
473 const char* test = "NONE";
474 const char* problem = "NONE";
475
476 // Set up assignments
477 Assignment* ap = assignment();
478 Assignment& a = *ap;
479
480 // Set up space for all solution search
481 TestSpace* search_s = new TestSpace(arity,dom,this);
482 post(*search_s,search_s->x);
483 branch(*search_s,search_s->x,INT_VAR_NONE(),INT_VAL_MIN());
484 Search::Options search_o;
485 search_o.threads = 1;
486 DFS<TestSpace> e_s(search_s,search_o);
487 delete search_s;
488
489 while (a()) {
490 bool sol = solution(a);
491 if (opt.log) {
492 olog << ind(1) << "Assignment: " << a
493 << (sol ? " (solution)" : " (no solution)")
494 << std::endl;
495 }
496
497 START_TEST("Assignment (after posting)");
498 {
499 TestSpace* s = new TestSpace(arity,dom,this);
500 TestSpace* sc = NULL;
501 s->post();
502 switch (Base::rand(2)) {
503 case 0:
504 if (opt.log)
505 olog << ind(3) << "No copy" << std::endl;
506 sc = s;
507 s = NULL;
508 break;
509 case 1:
510 if (opt.log)
511 olog << ind(3) << "Copy" << std::endl;
512 if (s->status() != SS_FAILED) {
513 sc = static_cast<TestSpace*>(s->clone());
514 } else {
515 sc = s; s = NULL;
516 }
517 break;
518 default: assert(false);
519 }
520 sc->assign(a);
521 if (sol) {
522 CHECK_TEST(!sc->failed(), "Failed on solution");
523 CHECK_TEST(sc->propagators()==0, "No subsumption");
524 } else {
525 CHECK_TEST(sc->failed(), "Solved on non-solution");
526 }
527 delete s; delete sc;
528 }
529 START_TEST("Partial assignment (after posting)");
530 {
531 TestSpace* s = new TestSpace(arity,dom,this);
532 s->post();
533 s->assign(a,true);
534 (void) s->failed();
535 s->assign(a);
536 if (sol) {
537 CHECK_TEST(!s->failed(), "Failed on solution");
538 CHECK_TEST(s->propagators()==0, "No subsumption");
539 } else {
540 CHECK_TEST(s->failed(), "Solved on non-solution");
541 }
542 delete s;
543 }
544 START_TEST("Assignment (after posting, disable)");
545 {
546 TestSpace* s = new TestSpace(arity,dom,this);
547 s->post();
548 s->disable();
549 s->assign(a);
550 s->enable();
551 if (sol) {
552 CHECK_TEST(!s->failed(), "Failed on solution");
553 CHECK_TEST(s->propagators()==0, "No subsumption");
554 } else {
555 CHECK_TEST(s->failed(), "Solved on non-solution");
556 }
557 delete s;
558 }
559 START_TEST("Partial assignment (after posting, disable)");
560 {
561 TestSpace* s = new TestSpace(arity,dom,this);
562 s->post();
563 s->assign(a,true);
564 s->disable();
565 (void) s->failed();
566 s->assign(a);
567 s->enable();
568 if (sol) {
569 CHECK_TEST(!s->failed(), "Failed on solution");
570 CHECK_TEST(s->propagators()==0, "No subsumption");
571 } else {
572 CHECK_TEST(s->failed(), "Solved on non-solution");
573 }
574 delete s;
575 }
576 START_TEST("Assignment (before posting)");
577 {
578 TestSpace* s = new TestSpace(arity,dom,this);
579 s->assign(a);
580 s->post();
581 if (sol) {
582 CHECK_TEST(!s->failed(), "Failed on solution");
583 CHECK_TEST(s->propagators()==0, "No subsumption");
584 } else {
585 CHECK_TEST(s->failed(), "Solved on non-solution");
586 }
587 delete s;
588 }
589 START_TEST("Partial assignment (before posting)");
590 {
591 TestSpace* s = new TestSpace(arity,dom,this);
592 s->assign(a,true);
593 s->post();
594 (void) s->failed();
595 s->assign(a);
596 if (sol) {
597 CHECK_TEST(!s->failed(), "Failed on solution");
598 CHECK_TEST(s->propagators()==0, "No subsumption");
599 } else {
600 CHECK_TEST(s->failed(), "Solved on non-solution");
601 }
602 delete s;
603 }
604 START_TEST("Prune");
605 {
606 TestSpace* s = new TestSpace(arity,dom,this);
607 s->post();
608 while (!s->failed() && !s->assigned())
609 if (!s->prune(a,testfix)) {
610 problem = "No fixpoint";
611 delete s;
612 goto failed;
613 }
614 s->assign(a);
615 if (sol) {
616 CHECK_TEST(!s->failed(), "Failed on solution");
617 CHECK_TEST(s->propagators()==0, "No subsumption");
618 } else {
619 CHECK_TEST(s->failed(), "Solved on non-solution");
620 }
621 delete s;
622 }
623 START_TEST("Prune (disable)");
624 {
625 TestSpace* s = new TestSpace(arity,dom,this);
626 TestSpace* c = static_cast<TestSpace*>(s->clone());
627 s->post(); c->post();
628 while (!s->failed() && !s->assigned())
629 if (!s->disabled(a,*c,testfix)) {
630 problem = "Different result after re-enable";
631 delete s; delete c;
632 goto failed;
633 }
634 if (testfix && (s->failed() != c->failed())) {
635 problem = "Different failure after re-enable";
636 delete s; delete c;
637 goto failed;
638 }
639 delete s; delete c;
640 }
641 if (!ignore(a)) {
642 if (eqv()) {
643 {
644 START_TEST("Assignment reified (rewrite after post, <=>)");
645 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
646 s->post();
647 s->rel(sol);
648 s->assign(a);
649 CHECK_TEST(!s->failed(), "Failed");
650 CHECK_TEST(s->propagators()==0, "No subsumption");
651 delete s;
652 }
653 {
654 START_TEST("Assignment reified (rewrite failure, <=>)");
655 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
656 s->post();
657 s->rel(!sol);
658 s->assign(a);
659 CHECK_TEST(s->failed(), "Not failed");
660 delete s;
661 }
662 {
663 START_TEST("Assignment reified (immediate rewrite, <=>)");
664 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
665 s->rel(sol);
666 s->post();
667 s->assign(a);
668 CHECK_TEST(!s->failed(), "Failed");
669 CHECK_TEST(s->propagators()==0, "No subsumption");
670 delete s;
671 }
672 {
673 START_TEST("Assignment reified (immediate failure, <=>)");
674 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
675 s->rel(!sol);
676 s->post();
677 s->assign(a);
678 CHECK_TEST(s->failed(), "Not failed");
679 delete s;
680 }
681 {
682 START_TEST("Assignment reified (before posting, <=>)");
683 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
684 s->assign(a);
685 s->post();
686 CHECK_TEST(!s->failed(), "Failed");
687 CHECK_TEST(s->propagators()==0, "No subsumption");
688 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
689 if (sol) {
690 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
691 } else {
692 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
693 }
694 delete s;
695 }
696 {
697 START_TEST("Assignment reified (after posting, <=>)");
698 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
699 s->post();
700 s->assign(a);
701 CHECK_TEST(!s->failed(), "Failed");
702 CHECK_TEST(s->propagators()==0, "No subsumption");
703 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
704 if (sol) {
705 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
706 } else {
707 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
708 }
709 delete s;
710 }
711 {
712 START_TEST("Assignment reified (after posting, <=>, disable)");
713 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
714 s->post();
715 s->disable();
716 s->assign(a);
717 s->enable();
718 CHECK_TEST(!s->failed(), "Failed");
719 CHECK_TEST(s->propagators()==0, "No subsumption");
720 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
721 if (sol) {
722 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
723 } else {
724 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
725 }
726 delete s;
727 }
728 {
729 START_TEST("Prune reified, <=>");
730 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
731 s->post();
732 while (!s->failed() &&
733 (!s->assigned() || !s->r.var().assigned()))
734 if (!s->prune(a,testfix)) {
735 problem = "No fixpoint";
736 delete s;
737 goto failed;
738 }
739 CHECK_TEST(!s->failed(), "Failed");
740 CHECK_TEST(s->propagators()==0, "No subsumption");
741 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
742 if (sol) {
743 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
744 } else {
745 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
746 }
747 delete s;
748 }
749 {
750 START_TEST("Prune reified, <=>, disable");
751 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
752 TestSpace* c = static_cast<TestSpace*>(s->clone());
753 s->post(); c->post();
754 while (!s->failed() &&
755 (!s->assigned() || !s->r.var().assigned()))
756 if (!s->disabled(a,*c,testfix)) {
757 problem = "No fixpoint";
758 delete s;
759 delete c;
760 goto failed;
761 }
762 CHECK_TEST(!c->failed(), "Failed");
763 CHECK_TEST(c->propagators()==0, "No subsumption");
764 CHECK_TEST(c->r.var().assigned(), "Control variable unassigned");
765 if (sol) {
766 CHECK_TEST(c->r.var().val()==1, "Zero on solution");
767 } else {
768 CHECK_TEST(c->r.var().val()==0, "One on non-solution");
769 }
770 delete s;
771 delete c;
772 }
773 }
774
775 if (imp()) {
776 {
777 START_TEST("Assignment reified (rewrite after post, =>)");
778 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
779 s->post();
780 s->rel(sol);
781 s->assign(a);
782 CHECK_TEST(!s->failed(), "Failed");
783 CHECK_TEST(s->propagators()==0, "No subsumption");
784 delete s;
785 }
786 {
787 START_TEST("Assignment reified (rewrite failure, =>)");
788 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
789 s->post();
790 s->rel(!sol);
791 s->assign(a);
792 if (sol) {
793 CHECK_TEST(!s->failed(), "Failed");
794 CHECK_TEST(s->propagators()==0, "No subsumption");
795 } else {
796 CHECK_TEST(s->failed(), "Not failed");
797 }
798 delete s;
799 }
800 {
801 START_TEST("Assignment reified (immediate rewrite, =>)");
802 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
803 s->rel(sol);
804 s->post();
805 s->assign(a);
806 CHECK_TEST(!s->failed(), "Failed");
807 CHECK_TEST(s->propagators()==0, "No subsumption");
808 delete s;
809 }
810 {
811 START_TEST("Assignment reified (immediate failure, =>)");
812 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
813 s->rel(!sol);
814 s->post();
815 s->assign(a);
816 if (sol) {
817 CHECK_TEST(!s->failed(), "Failed");
818 CHECK_TEST(s->propagators()==0, "No subsumption");
819 } else {
820 CHECK_TEST(s->failed(), "Not failed");
821 }
822 delete s;
823 }
824 {
825 START_TEST("Assignment reified (before posting, =>)");
826 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
827 s->assign(a);
828 s->post();
829 CHECK_TEST(!s->failed(), "Failed");
830 CHECK_TEST(s->propagators()==0, "No subsumption");
831 if (sol) {
832 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
833 } else {
834 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
835 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
836 }
837 delete s;
838 }
839 {
840 START_TEST("Assignment reified (after posting, =>)");
841 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
842 s->post();
843 s->assign(a);
844 CHECK_TEST(!s->failed(), "Failed");
845 CHECK_TEST(s->propagators()==0, "No subsumption");
846 if (sol) {
847 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
848 } else {
849 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
850 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
851 }
852 delete s;
853 }
854 {
855 START_TEST("Assignment reified (after posting, =>, disable)");
856 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
857 s->post();
858 s->disable();
859 s->assign(a);
860 s->enable();
861 CHECK_TEST(!s->failed(), "Failed");
862 CHECK_TEST(s->propagators()==0, "No subsumption");
863 if (sol) {
864 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
865 } else {
866 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
867 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
868 }
869 delete s;
870 }
871 {
872 START_TEST("Prune reified, =>");
873 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
874 s->post();
875 while (!s->failed() &&
876 (!s->assigned() || (!sol && !s->r.var().assigned())))
877 if (!s->prune(a,testfix)) {
878 problem = "No fixpoint";
879 delete s;
880 goto failed;
881 }
882 CHECK_TEST(!s->failed(), "Failed");
883 CHECK_TEST(s->propagators()==0, "No subsumption");
884 if (sol) {
885 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
886 } else {
887 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
888 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
889 }
890 delete s;
891 }
892 {
893 START_TEST("Prune reified, =>, disable");
894 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
895 TestSpace* c = static_cast<TestSpace*>(s->clone());
896 s->post(); c->post();
897 while (!s->failed() &&
898 (!s->assigned() || (!sol && !s->r.var().assigned())))
899 if (!s->disabled(a,*c,testfix)) {
900 problem = "No fixpoint";
901 delete s;
902 delete c;
903 goto failed;
904 }
905 CHECK_TEST(!c->failed(), "Failed");
906 CHECK_TEST(c->propagators()==0, "No subsumption");
907 if (sol) {
908 CHECK_TEST(!c->r.var().assigned(), "Control variable assigned");
909 } else {
910 CHECK_TEST(c->r.var().assigned(), "Control variable unassigned");
911 CHECK_TEST(c->r.var().val()==0, "One on non-solution");
912 }
913 delete s;
914 delete c;
915 }
916 }
917
918 if (pmi()) {
919 {
920 START_TEST("Assignment reified (rewrite after post, <=)");
921 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
922 s->post();
923 s->rel(sol);
924 s->assign(a);
925 CHECK_TEST(!s->failed(), "Failed");
926 CHECK_TEST(s->propagators()==0, "No subsumption");
927 delete s;
928 }
929 {
930 START_TEST("Assignment reified (rewrite failure, <=)");
931 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
932 s->post();
933 s->rel(!sol);
934 s->assign(a);
935 if (sol) {
936 CHECK_TEST(s->failed(), "Not failed");
937 } else {
938 CHECK_TEST(!s->failed(), "Failed");
939 CHECK_TEST(s->propagators()==0, "No subsumption");
940 }
941 delete s;
942 }
943 {
944 START_TEST("Assignment reified (immediate rewrite, <=)");
945 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
946 s->rel(sol);
947 s->post();
948 s->assign(a);
949 CHECK_TEST(!s->failed(), "Failed");
950 CHECK_TEST(s->propagators()==0, "No subsumption");
951 delete s;
952 }
953 {
954 START_TEST("Assignment reified (immediate failure, <=)");
955 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
956 s->rel(!sol);
957 s->post();
958 s->assign(a);
959 if (sol) {
960 CHECK_TEST(s->failed(), "Not failed");
961 } else {
962 CHECK_TEST(!s->failed(), "Failed");
963 CHECK_TEST(s->propagators()==0, "No subsumption");
964 }
965 delete s;
966 }
967 {
968 START_TEST("Assignment reified (before posting, <=)");
969 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
970 s->assign(a);
971 s->post();
972 CHECK_TEST(!s->failed(), "Failed");
973 CHECK_TEST(s->propagators()==0, "No subsumption");
974 if (sol) {
975 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
976 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
977 } else {
978 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
979 }
980 delete s;
981 }
982 {
983 START_TEST("Assignment reified (after posting, <=)");
984 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
985 s->post();
986 s->assign(a);
987 CHECK_TEST(!s->failed(), "Failed");
988 CHECK_TEST(s->propagators()==0, "No subsumption");
989 if (sol) {
990 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
991 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
992 } else {
993 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
994 }
995 delete s;
996 }
997 {
998 START_TEST("Assignment reified (after posting, <=, disable)");
999 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
1000 s->post();
1001 s->disable();
1002 s->assign(a);
1003 s->enable();
1004 CHECK_TEST(!s->failed(), "Failed");
1005 CHECK_TEST(s->propagators()==0, "No subsumption");
1006 if (sol) {
1007 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1008 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1009 } else {
1010 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1011 }
1012 delete s;
1013 }
1014 {
1015 START_TEST("Prune reified, <=");
1016 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
1017 s->post();
1018 while (!s->failed() &&
1019 (!s->assigned() || (sol && !s->r.var().assigned())))
1020 if (!s->prune(a,testfix)) {
1021 problem = "No fixpoint";
1022 delete s;
1023 goto failed;
1024 }
1025 CHECK_TEST(!s->failed(), "Failed");
1026 CHECK_TEST(s->propagators()==0, "No subsumption");
1027 if (sol) {
1028 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1029 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1030 } else {
1031 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1032 }
1033 delete s;
1034 }
1035 {
1036 START_TEST("Prune reified, <=, disable");
1037 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
1038 TestSpace* c = static_cast<TestSpace*>(s->clone());
1039 s->post(); c->post();
1040 while (!s->failed() &&
1041 (!s->assigned() || (sol && !s->r.var().assigned())))
1042 if (!s->disabled(a,*c,testfix)) {
1043 problem = "No fixpoint";
1044 delete s;
1045 delete c;
1046 goto failed;
1047 }
1048 CHECK_TEST(!c->failed(), "Failed");
1049 CHECK_TEST(c->propagators()==0, "No subsumption");
1050 if (sol) {
1051 CHECK_TEST(c->r.var().assigned(), "Control variable unassigned");
1052 CHECK_TEST(c->r.var().val()==1, "Zero on solution");
1053 } else {
1054 CHECK_TEST(!c->r.var().assigned(), "Control variable assigned");
1055 }
1056 delete s;
1057 delete c;
1058 }
1059 }
1060 }
1061
1062 if (testsearch) {
1063 if (sol) {
1064 START_TEST("Search");
1065 TestSpace* s = e_s.next();
1066 CHECK_TEST(s != NULL, "Solutions exhausted");
1067 CHECK_TEST(s->propagators()==0, "No subsumption");
1068 for (int i=a.size(); i--; ) {
1069 CHECK_TEST(s->x[i].assigned(), "Unassigned variable");
1070 CHECK_TEST(a[i] == s->x[i].val(), "Wrong value in solution");
1071 }
1072 delete s;
1073 }
1074 }
1075
1076 ++a;
1077 }
1078
1079 if (testsearch) {
1080 test = "Search";
1081 if (e_s.next() != NULL) {
1082 problem = "Excess solutions";
1083 goto failed;
1084 }
1085 }
1086
1087 switch (contest) {
1088 case CTL_NONE: break;
1089 case CTL_DOMAIN: {
1090 START_TEST("Full domain consistency");
1091 TestSpace* s = new TestSpace(arity,dom,this);
1092 s->post();
1093 if (!s->failed()) {
1094 while (!s->failed() && !s->assigned())
1095 s->prune();
1096 CHECK_TEST(!s->failed(), "Failed");
1097 CHECK_TEST(s->propagators()==0, "No subsumption");
1098 }
1099 delete s;
1100 // Fall-through -- domain implies bounds(d) and bounds(z)
1101 }
1102 case CTL_BOUNDS_D: {
1103 START_TEST("Bounds(D)-consistency");
1104 TestSpace* s = new TestSpace(arity,dom,this);
1105 s->post();
1106 for (int i = s->x.size(); i--; )
1107 s->prune(i, false);
1108 if (!s->failed()) {
1109 while (!s->failed() && !s->assigned())
1110 s->bound();
1111 CHECK_TEST(!s->failed(), "Failed");
1112 CHECK_TEST(s->propagators()==0, "No subsumption");
1113 }
1114 delete s;
1115 // Fall-through -- bounds(d) implies bounds(z)
1116 }
1117 case CTL_BOUNDS_Z: {
1118 START_TEST("Bounds(Z)-consistency");
1119 TestSpace* s = new TestSpace(arity,dom,this);
1120 s->post();
1121 for (int i = s->x.size(); i--; )
1122 s->prune(i, true);
1123 if (!s->failed()) {
1124 while (!s->failed() && !s->assigned())
1125 s->bound();
1126 CHECK_TEST(!s->failed(), "Failed");
1127 CHECK_TEST(s->propagators()==0, "No subsumption");
1128 }
1129 delete s;
1130 break;
1131 }
1132 }
1133
1134 delete ap;
1135 return true;
1136
1137 failed:
1138 if (opt.log)
1139 olog << "FAILURE" << std::endl
1140 << ind(1) << "Test: " << test << std::endl
1141 << ind(1) << "Problem: " << problem << std::endl;
1142 if (a() && opt.log)
1143 olog << ind(1) << "Assignment: " << a << std::endl;
1144 delete ap;
1145
1146 return false;
1147 }
1148
1149}}
1150
1151#undef START_TEST
1152#undef CHECK_TEST
1153
1154// STATISTICS: test-int
struct Gecode::@603::NNF::@65::@66 b
For binary nodes (and, or, eqv)
NodeType t
Type of node.
int n
Number of negative literals for node type.
struct Gecode::@603::NNF::@65::@67 a
For atomic nodes.
Node * x
Pointer to corresponding Boolean expression node.
int size(void) const
Return size of array (number of elements)
Definition array.hpp:1607
Boolean integer variables.
Definition int.hh:512
unsigned int size(void) const
Return size (cardinality) of domain.
Definition bool.hpp:81
int val(void) const
Return assigned value.
Definition bool.hpp:57
Depth-first search engine.
Definition search.hh:1036
void init(const IntSet &s)
Initialize with values for s.
Integer sets.
Definition int.hh:174
Passing integer variables.
Definition int.hh:656
Integer variable array.
Definition int.hh:763
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)
Options for scripts
Definition driver.hh:366
void threads(double n)
Set number of parallel threads.
Definition options.hpp:292
unsigned int size(Space &home) const
Return number of propagators in a group.
Definition core.cpp:955
void disable(Space &home)
Disable all propagators in a group.
Definition core.cpp:979
void enable(Space &home, bool s=true)
Enable all propagators in a group.
Definition core.cpp:988
static PropagatorGroup all
Group of all propagators.
Definition core.hpp:789
Reification specification.
Definition int.hh:876
BoolVar var(void) const
Return Boolean control variable.
Definition reify.hpp:48
ReifyMode mode(void) const
Return reification mode.
Definition reify.hpp:56
virtual T * next(void)
Return next solution (NULL, if none exists or search has been stopped)
Definition base.hpp:46
Computation spaces.
Definition core.hpp:1742
struct Gecode::Space::@61::@63 c
Data available only during copying.
bool assigned(void) const
Test if all variables are assigned.
Definition array.hpp:1026
int size(void) const
Return size of array (number of elements)
Definition array.hpp:926
void update(Space &home, VarArray< Var > &a)
Update array to be a clone of array a.
Definition array.hpp:1013
void update(Space &home, VarImpVar< VarImp > &y)
Update this variable to be a clone of variable y.
Definition var.hpp:116
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
Base class for assignments
Definition int.hh:59
Gecode::IntSet d
Domain for each variable.
Definition int.hh:62
int n
Number of variables.
Definition int.hh:61
Generate all assignments.
Definition int.hh:79
Gecode::IntSetValues * dsv
Iterator for each variable.
Definition int.hh:81
virtual void operator++(void)
Move to next assignment.
Definition int.cpp:48
int a
How many assigments still to be generated Generate new value according to domain.
Definition int.hh:99
int * vals
The current values for the variables.
Definition int.hh:98
virtual void operator++(void)
Move to next assignment.
Definition int.cpp:63
int _n1
How many variables in the second set.
Definition int.hh:120
Gecode::IntSet _d1
Domain for second set of variables Generate new value according to domain d.
Definition int.hh:121
int a
How many assigments still to be generated.
Definition int.hh:119
int * vals
The current values for the variables.
Definition int.hh:118
virtual void operator++(void)
Move to next assignment.
Definition int.cpp:70
int randval(const Gecode::IntSet &d)
Definition int.hpp:109
Space for executing tests.
Definition int.hh:149
Gecode::Reify r
Reification information.
Definition int.hh:156
TestSpace(int n, Gecode::IntSet &d, Test *t)
Create test space without reification.
Definition int.cpp:91
Gecode::IntSet d
Initial domain.
Definition int.hh:152
void rndrel(const Assignment &a, int i, Gecode::IntRelType &irt, int &v)
Randomly select a pruning rel for variable i.
Definition int.cpp:181
Test * test
The test currently run.
Definition int.hh:158
virtual Gecode::Space * copy(void)
Copy space during cloning.
Definition int.cpp:132
void post(void)
Post propagator.
Definition int.cpp:145
bool assigned(void) const
Test whether all variables are assigned.
Definition int.cpp:137
void prune(void)
Prune some random values for some random variable.
Definition int.cpp:316
void bound(void)
Assing a random variable to a random bound.
Definition int.cpp:272
void assign(const Assignment &a, bool skip=false)
Assign all (or all but one, if skip is true) variables to values in a.
Definition int.cpp:259
bool failed(void)
Compute a fixpoint and check for failure.
Definition int.cpp:158
bool reified
Whether the test is for a reified propagator.
Definition int.hh:160
void prune(int i, bool bounds_only)
Prune some random values from variable i.
Definition int.cpp:280
int rndvar(void)
Randomly select an unassigned variable.
Definition int.cpp:170
bool disabled(const Assignment &a, TestSpace &c, bool testfix)
Prune values also in a space c with disabled propagators, but not those in assignment a.
Definition int.cpp:373
void disable(void)
Disable propagators in space and compute fixpoint (make all idle)
Definition int.cpp:367
Gecode::IntVarArray x
Variables to be tested.
Definition int.hh:154
void enable(void)
Enable propagators in space.
Definition int.cpp:362
void rel(int i, Gecode::IntRelType irt, int n)
Perform integer tell operation on x[i].
Definition int.cpp:233
unsigned int propagators(void)
Return the number of propagators.
Definition int.cpp:421
virtual void post(Gecode::Space &home, Gecode::IntVarArray &x)=0
Post constraint.
virtual Assignment * assignment(void) const
Create assignment.
Definition int.cpp:440
bool log
Whether to log the tests.
Definition test.hh:91
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:925
ReifyMode
Mode for reification.
Definition int.hh:848
BoolOpType
Operation types for Booleans.
Definition int.hh:950
IntPropLevel
Propagation levels for integer propagators.
Definition int.hh:974
@ IRT_EQ
Equality ( )
Definition int.hh:926
@ IRT_NQ
Disequality ( )
Definition int.hh:927
@ IRT_GQ
Greater or equal ( )
Definition int.hh:930
@ IRT_LE
Less ( )
Definition int.hh:929
@ IRT_GR
Greater ( )
Definition int.hh:931
@ IRT_LQ
Less or equal ( )
Definition int.hh:928
@ RM_EQV
Equivalence for reification (default)
Definition int.hh:855
@ BOT_OR
Disjunction.
Definition int.hh:952
@ BOT_EQV
Equivalence.
Definition int.hh:954
@ BOT_IMP
Implication.
Definition int.hh:953
@ BOT_XOR
Exclusive or.
Definition int.hh:955
@ BOT_AND
Conjunction.
Definition int.hh:951
@ IPL_BASIC
Use basic propagation algorithm.
Definition int.hh:981
@ IPL_BASIC_ADVANCED
Use both.
Definition int.hh:983
@ IPL_DOM
Domain propagation Options: basic versus advanced propagation.
Definition int.hh:979
@ IPL_VAL
Value propagation.
Definition int.hh:977
@ IPL_ADVANCED
Use advanced propagation algorithm.
Definition int.hh:982
@ IPL_BND
Bounds propagation.
Definition int.hh:978
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:3224
@ SS_FAILED
Space is failed
Definition core.hpp:1682
Gecode toplevel namespace
void dom(Home home, FloatVar x, FloatVal n)
Propagates .
Definition dom.cpp:40
@ CTL_BOUNDS_Z
Test for bounds(z)-consistency.
Definition int.hh:143
@ CTL_BOUNDS_D
Test for bounds(d)-consistency.
Definition int.hh:142
@ CTL_NONE
No consistency-test.
Definition int.hh:140
@ CTL_DOMAIN
Test for domain-consistency.
Definition int.hh:141
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::Int::Assignment &a)
Definition int.cpp:81