Generated on for Gecode by doxygen 1.15.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.dev>
5 * Mikael Zayenz Lagerkvist <lagerkvist@gecode.dev>
6 *
7 * Copyright:
8 * Christian Schulte, 2005
9 * Mikael Zayenz Lagerkvist, 2005, 2026
10 *
11 * This file is part of Gecode, the generic constraint
12 * development environment:
13 * http://www.gecode.dev
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 */
63 for (int i = this->n; i--; )
64 this->vals[i]= this->randval(rand);
65 this->a--;
66 }
67
68 void
70 for (int i=n-_n1; i--; )
71 vals[i] = randval(d, rand);
72 for (int i=_n1; i--; )
73 vals[n-_n1+i] = randval(_d1, rand);
74 a--;
75 }
76
77}}
78
79std::ostream&
80operator<<(std::ostream& os, const Test::Int::Assignment& a) {
81 int n = a.size();
82 os << "{";
83 for (int i=0; i<n; i++)
84 os << a[i] << ((i!=n-1) ? "," : "}");
85 return os;
86}
87
88namespace Test { namespace Int {
89
91 : d(d0), x(*this,n,Gecode::Int::Limits::min,Gecode::Int::Limits::max),
92 test(t), reified(false) {
93 Gecode::IntVarArgs _x(*this,n,d);
94 if (x.size() == 1)
95 Gecode::dom(*this,x[0],_x[0]);
96 else
97 Gecode::dom(*this,x,_x);
98 Gecode::BoolVar b(*this,0,1);
100 if (opt.log)
101 olog << ind(2) << "Initial: x[]=" << x
102 << std::endl;
103 }
104
107 : d(d0), x(*this,n,Gecode::Int::Limits::min,Gecode::Int::Limits::max),
108 test(t), reified(true) {
109 Gecode::IntVarArgs _x(*this,n,d);
110 if (x.size() == 1)
111 Gecode::dom(*this,x[0],_x[0]);
112 else
113 Gecode::dom(*this,x,_x);
114 Gecode::BoolVar b(*this,0,1);
115 r = Gecode::Reify(b,rm);
116 if (opt.log)
117 olog << ind(2) << "Initial: x[]=" << x
118 << " b=" << r.var() << std::endl;
119 }
120
122 : Gecode::Space(s), d(s.d), test(s.test), reified(s.reified) {
123 x.update(*this, s.x);
125 Gecode::BoolVar sr(s.r.var());
126 b.update(*this, sr);
127 r.var(b); r.mode(s.r.mode());
128 }
129
132 return new TestSpace(*this);
133 }
134
135 bool
137 for (int i=x.size(); i--; )
138 if (!x[i].assigned())
139 return false;
140 return true;
141 }
142
143 void
145 if (reified){
146 test->post(*this,x,r);
147 if (opt.log)
148 olog << ind(3) << "Posting reified propagator" << std::endl;
149 } else {
150 test->post(*this,x);
151 if (opt.log)
152 olog << ind(3) << "Posting propagator" << std::endl;
153 }
154 }
155
156 bool
158 if (opt.log) {
159 olog << ind(3) << "Fixpoint: " << x;
160 bool f=(status() == Gecode::SS_FAILED);
161 olog << std::endl << ind(3) << " --> " << x << std::endl;
162 return f;
163 } else {
164 return status() == Gecode::SS_FAILED;
165 }
166 }
167
168 int
170 assert(!assigned());
171 // Select variable to be pruned
172 int i = static_cast<int>(rand(static_cast<unsigned int>(x.size())));
173 while (x[i].assigned()) {
174 i = (i+1) % x.size();
175 }
176 return i;
177 }
178
179 void
180 TestSpace::rndrel(const Assignment& a, int i, Gecode::IntRelType& irt, int& v,
182 using namespace Gecode;
183 // Select mode for pruning
184 irt = IRT_EQ; // Means do nothing!
185 switch (rand(3)) {
186 case 0:
187 if (a[i] < x[i].max()) {
188 unsigned int n =
189 static_cast<unsigned int>(x[i].max()) - static_cast<unsigned int>(a[i]);
190 unsigned int offset = rand(n);
191 v = static_cast<int>(static_cast<long long>(a[i]) + 1LL + offset);
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 unsigned int n =
199 static_cast<unsigned int>(a[i]) - static_cast<unsigned int>(x[i].min());
200 unsigned int offset = rand(n);
201 v = static_cast<int>(static_cast<long long>(x[i].min()) + offset);
202 assert((v < a[i]) && (v >= x[i].min()));
203 irt = IRT_GR;
204 }
205 break;
206 default:
207 {
209 unsigned int skip = rand(static_cast<unsigned int>(x[i].size()-1));
210 while (true) {
211 if (it.width() > skip) {
212 v = static_cast<int>(static_cast<long long>(it.min()) + 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
260 using namespace Gecode;
261 int i = skip ?
262 static_cast<int>(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(rand) && failed())
267 return;
268 }
269 }
270
271 void
273 using namespace Gecode;
274 int i = rndvar(rand);
275 bool min = 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, Gecode::Support::RandomGenerator& rand) {
281 using namespace Gecode;
282 // Prune values
283 if (bounds_only) {
284 if (rand(2) && !x[i].assigned()) {
285 unsigned int n =
286 static_cast<unsigned int>(x[i].max()) -
287 static_cast<unsigned int>(x[i].min());
288 unsigned int offset = rand(n);
289 int v = static_cast<int>(static_cast<long long>(x[i].min()) +
290 1LL + offset);
291 assert((v > x[i].min()) && (v <= x[i].max()));
292 rel(i, Gecode::IRT_LE, v);
293 }
294 if (rand(2) && !x[i].assigned()) {
295 unsigned int n =
296 static_cast<unsigned int>(x[i].max()) -
297 static_cast<unsigned int>(x[i].min());
298 unsigned int offset = rand(n);
299 int v = static_cast<int>(static_cast<long long>(x[i].min()) + offset);
300 assert((v < x[i].max()) && (v >= x[i].min()));
301 rel(i, Gecode::IRT_GR, v);
302 }
303 } else {
304 for (int vals =
305 static_cast<int>(rand(static_cast<unsigned int>(x[i].size()-1))+1); vals--; ) {
306 int v;
308 unsigned int skip = rand(x[i].size()-1);
309 while (true) {
310 if (it.width() > skip) {
311 v = static_cast<int>(static_cast<long long>(it.min()) + skip);
312 break;
313 }
314 skip -= it.width(); ++it;
315 }
316 rel(i, IRT_NQ, v);
317 }
318 }
319 }
320
321 void
323 prune(rndvar(rand), false, rand);
324 }
325
326 bool
328 using namespace Gecode;
329 // Select variable to be pruned
330 int i = rndvar(rand);
331 // Select mode for pruning
332 IntRelType irt;
333 int v;
334 rndrel(a, i, irt, v, rand);
335 if (irt != IRT_EQ)
336 rel(i, irt, v);
337 if (Base::fixpoint(rand)) {
338 if (failed() || !testfix)
339 return true;
340 TestSpace* c = static_cast<TestSpace*>(clone());
341 if (opt.log)
342 olog << ind(3) << "Testing fixpoint on copy" << std::endl;
343 c->post();
344 if (c->failed()) {
345 if (opt.log)
346 olog << ind(4) << "Copy failed after posting" << std::endl;
347 delete c; return false;
348 }
349 for (int j=x.size(); j--; )
350 if (x[j].size() != c->x[j].size()) {
351 if (opt.log)
352 olog << ind(4) << "Different domain size" << std::endl;
353 delete c; return false;
354 }
355 if (reified && (r.var().size() != c->r.var().size())) {
356 if (opt.log)
357 olog << ind(4) << "Different control variable" << std::endl;
358 delete c; return false;
359 }
360 if (opt.log)
361 olog << ind(3) << "Finished testing fixpoint on copy" << std::endl;
362 delete c;
363 }
364 return true;
365 }
366
367 void
369 Gecode::PropagatorGroup::all.enable(*this);
370 }
371
372 void
374 Gecode::PropagatorGroup::all.disable(*this);
375 (void) status();
376 }
377
378 bool
380 using namespace Gecode;
381 // Disable propagators
382 c.disable();
383 // Select variable to be pruned
384 int i = rndvar(rand);
385 // Select mode for pruning
386 IntRelType irt;
387 int v;
388 rndrel(a, i, irt, v, rand);
389 if (irt != IRT_EQ) {
390 rel(i, irt, v);
391 c.rel(i, irt, v);
392 }
393 // Enable propagators
394 c.enable();
395 if (!testfix)
396 return true;
397 if (failed()) {
398 if (!c.failed()) {
399 if (opt.log)
400 olog << ind(3) << "No failure on disabled copy" << std::endl;
401 return false;
402 }
403 return true;
404 }
405 if (c.failed()) {
406 if (opt.log)
407 olog << ind(3) << "Failure on disabled copy" << std::endl;
408 return false;
409 }
410 for (int j=x.size(); j--; ) {
411 if (x[j].size() != c.x[j].size()) {
412 if (opt.log)
413 olog << ind(4) << "Different domain size" << std::endl;
414 return false;
415 }
416 if (reified && (r.var().size() != c.r.var().size())) {
417 if (opt.log)
418 olog << ind(4) << "Different control variable" << std::endl;
419 return false;
420 }
421 }
422 return true;
423 }
424
425 unsigned int
427 return Gecode::PropagatorGroup::all.size(*this);
428 }
429
430 const Gecode::IntPropLevel IntPropLevels::ipls[] =
432
433 const Gecode::IntPropLevel IntPropBasicAdvanced::ipls[] =
435
436 const Gecode::IntRelType IntRelTypes::irts[] =
439
440 const Gecode::BoolOpType BoolOpTypes::bots[] =
443
445 Test::assignment(void) const {
446 return new CpltAssignment(arity,dom);
447 }
448
449
451#define CHECK_TEST(T,M) \
452do { \
453if (opt.log) \
454 olog << ind(3) << "Check: " << (M) << std::endl; \
455if (!(T)) { \
456 problem = (M); delete s; goto failed; \
457} \
458} while (false)
459
461#define START_TEST(T) \
462do { \
463 if (opt.log) { \
464 olog.str(""); \
465 olog << ind(2) << "Testing: " << (T) << std::endl; \
466 } \
467 test = (T); \
468} while (false)
469
470 bool
471 Test::ignore(const Assignment&) const {
472 return false;
473 }
474
475 void
478
479 bool
480 Test::run(void) {
481 using namespace Gecode;
482 const char* test = "NONE";
483 const char* problem = "NONE";
484
485 // Set up assignments
486 Assignment* ap = assignment();
487 Assignment& a = *ap;
488
489 // Set up space for all solution search
490 TestSpace* search_s = new TestSpace(arity,dom,this);
491 post(*search_s,search_s->x);
492 branch(*search_s,search_s->x,INT_VAR_NONE(),INT_VAL_MIN());
493 Search::Options search_o;
494 search_o.threads = 1;
495 DFS<TestSpace> e_s(search_s,search_o);
496 delete search_s;
497
498 while (a.has_more()) {
499 bool sol = solution(a);
500 if (opt.log) {
501 olog << ind(1) << "Assignment: " << a
502 << (sol ? " (solution)" : " (no solution)")
503 << std::endl;
504 }
505
506 START_TEST("Assignment (after posting)");
507 {
508 TestSpace* s = new TestSpace(arity,dom,this);
509 TestSpace* sc = nullptr;
510 s->post();
511 switch (_rand(2)) {
512 case 0:
513 if (opt.log)
514 olog << ind(3) << "No copy" << std::endl;
515 sc = s;
516 s = nullptr;
517 break;
518 case 1:
519 if (opt.log)
520 olog << ind(3) << "Copy" << std::endl;
521 if (s->status() != SS_FAILED) {
522 sc = static_cast<TestSpace*>(s->clone());
523 } else {
524 sc = s; s = nullptr;
525 }
526 break;
527 default: assert(false);
528 }
529 sc->assign(a, false, _rand);
530 if (sol) {
531 CHECK_TEST(!sc->failed(), "Failed on solution");
532 CHECK_TEST(sc->propagators()==0, "No subsumption");
533 } else {
534 CHECK_TEST(sc->failed(), "Solved on non-solution");
535 }
536 delete s; delete sc;
537 }
538 START_TEST("Partial assignment (after posting)");
539 {
540 TestSpace* s = new TestSpace(arity,dom,this);
541 s->post();
542 s->assign(a, true, _rand);
543 (void) s->failed();
544 s->assign(a, false, _rand);
545 if (sol) {
546 CHECK_TEST(!s->failed(), "Failed on solution");
547 CHECK_TEST(s->propagators()==0, "No subsumption");
548 } else {
549 CHECK_TEST(s->failed(), "Solved on non-solution");
550 }
551 delete s;
552 }
553 START_TEST("Assignment (after posting, disable)");
554 {
555 TestSpace* s = new TestSpace(arity,dom,this);
556 s->post();
557 s->disable();
558 s->assign(a, false, _rand);
559 s->enable();
560 if (sol) {
561 CHECK_TEST(!s->failed(), "Failed on solution");
562 CHECK_TEST(s->propagators()==0, "No subsumption");
563 } else {
564 CHECK_TEST(s->failed(), "Solved on non-solution");
565 }
566 delete s;
567 }
568 START_TEST("Partial assignment (after posting, disable)");
569 {
570 TestSpace* s = new TestSpace(arity,dom,this);
571 s->post();
572 s->assign(a, true, _rand);
573 s->disable();
574 (void) s->failed();
575 s->assign(a, false, _rand);
576 s->enable();
577 if (sol) {
578 CHECK_TEST(!s->failed(), "Failed on solution");
579 CHECK_TEST(s->propagators()==0, "No subsumption");
580 } else {
581 CHECK_TEST(s->failed(), "Solved on non-solution");
582 }
583 delete s;
584 }
585 START_TEST("Assignment (before posting)");
586 {
587 TestSpace* s = new TestSpace(arity,dom,this);
588 s->assign(a, false, _rand);
589 s->post();
590 if (sol) {
591 CHECK_TEST(!s->failed(), "Failed on solution");
592 CHECK_TEST(s->propagators()==0, "No subsumption");
593 } else {
594 CHECK_TEST(s->failed(), "Solved on non-solution");
595 }
596 delete s;
597 }
598 START_TEST("Partial assignment (before posting)");
599 {
600 TestSpace* s = new TestSpace(arity,dom,this);
601 s->assign(a, true, _rand);
602 s->post();
603 (void) s->failed();
604 s->assign(a, false, _rand);
605 if (sol) {
606 CHECK_TEST(!s->failed(), "Failed on solution");
607 CHECK_TEST(s->propagators()==0, "No subsumption");
608 } else {
609 CHECK_TEST(s->failed(), "Solved on non-solution");
610 }
611 delete s;
612 }
613 START_TEST("Prune");
614 {
615 TestSpace* s = new TestSpace(arity,dom,this);
616 s->post();
617 while (!s->failed() && !s->assigned())
618 if (!s->prune(a, testfix, _rand)) {
619 problem = "No fixpoint";
620 delete s;
621 goto failed;
622 }
623 s->assign(a, false, _rand);
624 if (sol) {
625 CHECK_TEST(!s->failed(), "Failed on solution");
626 CHECK_TEST(s->propagators()==0, "No subsumption");
627 } else {
628 CHECK_TEST(s->failed(), "Solved on non-solution");
629 }
630 delete s;
631 }
632 START_TEST("Prune (disable)");
633 {
634 TestSpace* s = new TestSpace(arity,dom,this);
635 TestSpace* c = static_cast<TestSpace*>(s->clone());
636 s->post(); c->post();
637 while (!s->failed() && !s->assigned())
638 if (!s->disabled(a, *c, testfix, _rand)) {
639 problem = "Different result after re-enable";
640 delete s; delete c;
641 goto failed;
642 }
643 if (testfix && (s->failed() != c->failed())) {
644 problem = "Different failure after re-enable";
645 delete s; delete c;
646 goto failed;
647 }
648 delete s; delete c;
649 }
650 if (!ignore(a)) {
651 if (eqv()) {
652 {
653 START_TEST("Assignment reified (rewrite after post, <=>)");
654 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
655 s->post();
656 s->rel(sol);
657 s->assign(a, false, _rand);
658 CHECK_TEST(!s->failed(), "Failed");
659 CHECK_TEST(s->propagators()==0, "No subsumption");
660 delete s;
661 }
662 {
663 START_TEST("Assignment reified (rewrite failure, <=>)");
664 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
665 s->post();
666 s->rel(!sol);
667 s->assign(a, false, _rand);
668 CHECK_TEST(s->failed(), "Not failed");
669 delete s;
670 }
671 {
672 START_TEST("Assignment reified (immediate rewrite, <=>)");
673 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
674 s->rel(sol);
675 s->post();
676 s->assign(a, false, _rand);
677 CHECK_TEST(!s->failed(), "Failed");
678 CHECK_TEST(s->propagators()==0, "No subsumption");
679 delete s;
680 }
681 {
682 START_TEST("Assignment reified (immediate failure, <=>)");
683 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
684 s->rel(!sol);
685 s->post();
686 s->assign(a, false, _rand);
687 CHECK_TEST(s->failed(), "Not failed");
688 delete s;
689 }
690 {
691 START_TEST("Assignment reified (before posting, <=>)");
692 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
693 s->assign(a, false, _rand);
694 s->post();
695 CHECK_TEST(!s->failed(), "Failed");
696 CHECK_TEST(s->propagators()==0, "No subsumption");
697 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
698 if (sol) {
699 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
700 } else {
701 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
702 }
703 delete s;
704 }
705 {
706 START_TEST("Assignment reified (after posting, <=>)");
707 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
708 s->post();
709 s->assign(a, false, _rand);
710 CHECK_TEST(!s->failed(), "Failed");
711 CHECK_TEST(s->propagators()==0, "No subsumption");
712 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
713 if (sol) {
714 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
715 } else {
716 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
717 }
718 delete s;
719 }
720 {
721 START_TEST("Assignment reified (after posting, <=>, disable)");
722 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
723 s->post();
724 s->disable();
725 s->assign(a, false, _rand);
726 s->enable();
727 CHECK_TEST(!s->failed(), "Failed");
728 CHECK_TEST(s->propagators()==0, "No subsumption");
729 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
730 if (sol) {
731 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
732 } else {
733 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
734 }
735 delete s;
736 }
737 {
738 START_TEST("Prune reified, <=>");
739 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
740 s->post();
741 while (!s->failed() &&
742 (!s->assigned() || !s->r.var().assigned()))
743 if (!s->prune(a, testfix, _rand)) {
744 problem = "No fixpoint";
745 delete s;
746 goto failed;
747 }
748 CHECK_TEST(!s->failed(), "Failed");
749 CHECK_TEST(s->propagators()==0, "No subsumption");
750 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
751 if (sol) {
752 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
753 } else {
754 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
755 }
756 delete s;
757 }
758 {
759 START_TEST("Prune reified, <=>, disable");
760 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
761 TestSpace* c = static_cast<TestSpace*>(s->clone());
762 s->post(); c->post();
763 while (!s->failed() &&
764 (!s->assigned() || !s->r.var().assigned()))
765 if (!s->disabled(a, *c, testfix, _rand)) {
766 problem = "No fixpoint";
767 delete s;
768 delete c;
769 goto failed;
770 }
771 CHECK_TEST(!c->failed(), "Failed");
772 CHECK_TEST(c->propagators()==0, "No subsumption");
773 CHECK_TEST(c->r.var().assigned(), "Control variable unassigned");
774 if (sol) {
775 CHECK_TEST(c->r.var().val()==1, "Zero on solution");
776 } else {
777 CHECK_TEST(c->r.var().val()==0, "One on non-solution");
778 }
779 delete s;
780 delete c;
781 }
782 }
783
784 if (imp()) {
785 {
786 START_TEST("Assignment reified (rewrite after post, =>)");
787 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
788 s->post();
789 s->rel(sol);
790 s->assign(a, false, _rand);
791 CHECK_TEST(!s->failed(), "Failed");
792 CHECK_TEST(s->propagators()==0, "No subsumption");
793 delete s;
794 }
795 {
796 START_TEST("Assignment reified (rewrite failure, =>)");
797 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
798 s->post();
799 s->rel(!sol);
800 s->assign(a, false, _rand);
801 if (sol) {
802 CHECK_TEST(!s->failed(), "Failed");
803 CHECK_TEST(s->propagators()==0, "No subsumption");
804 } else {
805 CHECK_TEST(s->failed(), "Not failed");
806 }
807 delete s;
808 }
809 {
810 START_TEST("Assignment reified (immediate rewrite, =>)");
811 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
812 s->rel(sol);
813 s->post();
814 s->assign(a, false, _rand);
815 CHECK_TEST(!s->failed(), "Failed");
816 CHECK_TEST(s->propagators()==0, "No subsumption");
817 delete s;
818 }
819 {
820 START_TEST("Assignment reified (immediate failure, =>)");
821 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
822 s->rel(!sol);
823 s->post();
824 s->assign(a, false, _rand);
825 if (sol) {
826 CHECK_TEST(!s->failed(), "Failed");
827 CHECK_TEST(s->propagators()==0, "No subsumption");
828 } else {
829 CHECK_TEST(s->failed(), "Not failed");
830 }
831 delete s;
832 }
833 {
834 START_TEST("Assignment reified (before posting, =>)");
835 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
836 s->assign(a, false, _rand);
837 s->post();
838 CHECK_TEST(!s->failed(), "Failed");
839 CHECK_TEST(s->propagators()==0, "No subsumption");
840 if (sol) {
841 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
842 } else {
843 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
844 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
845 }
846 delete s;
847 }
848 {
849 START_TEST("Assignment reified (after posting, =>)");
850 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
851 s->post();
852 s->assign(a, false, _rand);
853 CHECK_TEST(!s->failed(), "Failed");
854 CHECK_TEST(s->propagators()==0, "No subsumption");
855 if (sol) {
856 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
857 } else {
858 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
859 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
860 }
861 delete s;
862 }
863 {
864 START_TEST("Assignment reified (after posting, =>, disable)");
865 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
866 s->post();
867 s->disable();
868 s->assign(a, false, _rand);
869 s->enable();
870 CHECK_TEST(!s->failed(), "Failed");
871 CHECK_TEST(s->propagators()==0, "No subsumption");
872 if (sol) {
873 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
874 } else {
875 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
876 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
877 }
878 delete s;
879 }
880 {
881 START_TEST("Prune reified, =>");
882 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
883 s->post();
884 while (!s->failed() &&
885 (!s->assigned() || (!sol && !s->r.var().assigned())))
886 if (!s->prune(a, testfix, _rand)) {
887 problem = "No fixpoint";
888 delete s;
889 goto failed;
890 }
891 CHECK_TEST(!s->failed(), "Failed");
892 CHECK_TEST(s->propagators()==0, "No subsumption");
893 if (sol) {
894 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
895 } else {
896 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
897 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
898 }
899 delete s;
900 }
901 {
902 START_TEST("Prune reified, =>, disable");
903 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
904 TestSpace* c = static_cast<TestSpace*>(s->clone());
905 s->post(); c->post();
906 while (!s->failed() &&
907 (!s->assigned() || (!sol && !s->r.var().assigned())))
908 if (!s->disabled(a, *c, testfix, _rand)) {
909 problem = "No fixpoint";
910 delete s;
911 delete c;
912 goto failed;
913 }
914 CHECK_TEST(!c->failed(), "Failed");
915 CHECK_TEST(c->propagators()==0, "No subsumption");
916 if (sol) {
917 CHECK_TEST(!c->r.var().assigned(), "Control variable assigned");
918 } else {
919 CHECK_TEST(c->r.var().assigned(), "Control variable unassigned");
920 CHECK_TEST(c->r.var().val()==0, "One on non-solution");
921 }
922 delete s;
923 delete c;
924 }
925 }
926
927 if (pmi()) {
928 {
929 START_TEST("Assignment reified (rewrite after post, <=)");
930 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
931 s->post();
932 s->rel(sol);
933 s->assign(a, false, _rand);
934 CHECK_TEST(!s->failed(), "Failed");
935 CHECK_TEST(s->propagators()==0, "No subsumption");
936 delete s;
937 }
938 {
939 START_TEST("Assignment reified (rewrite failure, <=)");
940 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
941 s->post();
942 s->rel(!sol);
943 s->assign(a, false, _rand);
944 if (sol) {
945 CHECK_TEST(s->failed(), "Not failed");
946 } else {
947 CHECK_TEST(!s->failed(), "Failed");
948 CHECK_TEST(s->propagators()==0, "No subsumption");
949 }
950 delete s;
951 }
952 {
953 START_TEST("Assignment reified (immediate rewrite, <=)");
954 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
955 s->rel(sol);
956 s->post();
957 s->assign(a, false, _rand);
958 CHECK_TEST(!s->failed(), "Failed");
959 CHECK_TEST(s->propagators()==0, "No subsumption");
960 delete s;
961 }
962 {
963 START_TEST("Assignment reified (immediate failure, <=)");
964 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
965 s->rel(!sol);
966 s->post();
967 s->assign(a, false, _rand);
968 if (sol) {
969 CHECK_TEST(s->failed(), "Not failed");
970 } else {
971 CHECK_TEST(!s->failed(), "Failed");
972 CHECK_TEST(s->propagators()==0, "No subsumption");
973 }
974 delete s;
975 }
976 {
977 START_TEST("Assignment reified (before posting, <=)");
978 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
979 s->assign(a, false, _rand);
980 s->post();
981 CHECK_TEST(!s->failed(), "Failed");
982 CHECK_TEST(s->propagators()==0, "No subsumption");
983 if (sol) {
984 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
985 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
986 } else {
987 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
988 }
989 delete s;
990 }
991 {
992 START_TEST("Assignment reified (after posting, <=)");
993 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
994 s->post();
995 s->assign(a, false, _rand);
996 CHECK_TEST(!s->failed(), "Failed");
997 CHECK_TEST(s->propagators()==0, "No subsumption");
998 if (sol) {
999 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1000 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1001 } else {
1002 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1003 }
1004 delete s;
1005 }
1006 {
1007 START_TEST("Assignment reified (after posting, <=, disable)");
1008 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
1009 s->post();
1010 s->disable();
1011 s->assign(a, false, _rand);
1012 s->enable();
1013 CHECK_TEST(!s->failed(), "Failed");
1014 CHECK_TEST(s->propagators()==0, "No subsumption");
1015 if (sol) {
1016 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1017 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1018 } else {
1019 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1020 }
1021 delete s;
1022 }
1023 {
1024 START_TEST("Prune reified, <=");
1025 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
1026 s->post();
1027 while (!s->failed() &&
1028 (!s->assigned() || (sol && !s->r.var().assigned())))
1029 if (!s->prune(a, testfix, _rand)) {
1030 problem = "No fixpoint";
1031 delete s;
1032 goto failed;
1033 }
1034 CHECK_TEST(!s->failed(), "Failed");
1035 CHECK_TEST(s->propagators()==0, "No subsumption");
1036 if (sol) {
1037 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1038 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1039 } else {
1040 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1041 }
1042 delete s;
1043 }
1044 {
1045 START_TEST("Prune reified, <=, disable");
1046 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
1047 TestSpace* c = static_cast<TestSpace*>(s->clone());
1048 s->post(); c->post();
1049 while (!s->failed() &&
1050 (!s->assigned() || (sol && !s->r.var().assigned())))
1051 if (!s->disabled(a, *c, testfix, _rand)) {
1052 problem = "No fixpoint";
1053 delete s;
1054 delete c;
1055 goto failed;
1056 }
1057 CHECK_TEST(!c->failed(), "Failed");
1058 CHECK_TEST(c->propagators()==0, "No subsumption");
1059 if (sol) {
1060 CHECK_TEST(c->r.var().assigned(), "Control variable unassigned");
1061 CHECK_TEST(c->r.var().val()==1, "Zero on solution");
1062 } else {
1063 CHECK_TEST(!c->r.var().assigned(), "Control variable assigned");
1064 }
1065 delete s;
1066 delete c;
1067 }
1068 }
1069 }
1070
1071 if (testsearch) {
1072 if (sol) {
1073 START_TEST("Search");
1074 TestSpace* s = e_s.next();
1075 CHECK_TEST(s != nullptr, "Solutions exhausted");
1076 CHECK_TEST(s->propagators()==0, "No subsumption");
1077 for (int i=a.size(); i--; ) {
1078 CHECK_TEST(s->x[i].assigned(), "Unassigned variable");
1079 CHECK_TEST(a[i] == s->x[i].val(), "Wrong value in solution");
1080 }
1081 delete s;
1082 }
1083 }
1084
1085 a.next(_rand);
1086 }
1087
1088 if (testsearch) {
1089 test = "Search";
1090 if (e_s.next() != nullptr) {
1091 problem = "Excess solutions";
1092 goto failed;
1093 }
1094 }
1095
1096 switch (contest) {
1097 case CTL_NONE: break;
1098 case CTL_DOMAIN: {
1099 START_TEST("Full domain consistency");
1100 TestSpace* s = new TestSpace(arity,dom,this);
1101 s->post();
1102 if (!s->failed()) {
1103 while (!s->failed() && !s->assigned())
1104 s->prune(_rand);
1105 CHECK_TEST(!s->failed(), "Failed");
1106 CHECK_TEST(s->propagators()==0, "No subsumption");
1107 }
1108 delete s;
1109 // Fall-through -- domain implies bounds(d) and bounds(z)
1110 }
1111 case CTL_BOUNDS_D: {
1112 START_TEST("Bounds(D)-consistency");
1113 TestSpace* s = new TestSpace(arity,dom,this);
1114 s->post();
1115 for (int i = s->x.size(); i--; )
1116 s->prune(i, false, _rand);
1117 if (!s->failed()) {
1118 while (!s->failed() && !s->assigned())
1119 s->bound(_rand);
1120 CHECK_TEST(!s->failed(), "Failed");
1121 CHECK_TEST(s->propagators()==0, "No subsumption");
1122 }
1123 delete s;
1124 // Fall-through -- bounds(d) implies bounds(z)
1125 }
1126 case CTL_BOUNDS_Z: {
1127 START_TEST("Bounds(Z)-consistency");
1128 TestSpace* s = new TestSpace(arity,dom,this);
1129 s->post();
1130 for (int i = s->x.size(); i--; )
1131 s->prune(i, true, _rand);
1132 if (!s->failed()) {
1133 while (!s->failed() && !s->assigned())
1134 s->bound(_rand);
1135 CHECK_TEST(!s->failed(), "Failed");
1136 CHECK_TEST(s->propagators()==0, "No subsumption");
1137 }
1138 delete s;
1139 break;
1140 }
1141 }
1142
1143 delete ap;
1144 return true;
1145
1146 failed:
1147 if (opt.log)
1148 olog << "FAILURE" << std::endl
1149 << ind(1) << "Test: " << test << std::endl
1150 << ind(1) << "Problem: " << problem << std::endl;
1151 if (a.has_more() && opt.log)
1152 olog << ind(1) << "Assignment: " << a << std::endl;
1153 delete ap;
1154
1155 return false;
1156 }
1157
1158}}
1159
1160#undef START_TEST
1161#undef CHECK_TEST
1162
1163// STATISTICS: test-int
Boolean integer variables.
Definition int.hh:533
int val(void) const
Return assigned value.
Definition bool.hpp:57
Depth-first search engine.
Definition search.hh:1080
FloatNum size(void) const
Return size of float value (distance between maximum and minimum).
Definition val.hpp:78
Integer sets.
Definition int.hh:178
Passing integer variables.
Definition int.hh:680
Integer variable array.
Definition int.hh:791
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:410
void threads(double n)
Set number of parallel threads.
Definition options.hpp:321
static PropagatorGroup all
Group of all propagators.
Definition core.hpp:796
Reification specification.
Definition int.hh:910
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 (nullptr, if none exists or search has been stopped).
Definition base.hpp:46
Computation spaces.
Definition core.hpp:1775
struct Gecode::Space::@055132133326276162005044145100211202071356247106::@155123175027073262103111264343315000271204104107 c
Data available only during copying.
SpaceStatus status(void)
Query space status without collecting statistics.
Definition core.hpp:3306
bool assigned(void) const
Test if all variables are assigned.
Definition array.hpp:1036
int size(void) const
Return size of array (number of elements).
Definition array.hpp:936
bool assigned(void) const
Test whether view is assigned.
Definition var.hpp:111
Gecode::Support::RandomGenerator _rand
Random number generator.
Definition test.hh:164
bool fixpoint(void)
Throw a coin whether to compute a fixpoint.
Definition test.hpp:67
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
virtual void next(Gecode::Support::RandomGenerator &rand)
Move to next assignment.
Definition int.cpp:48
Gecode::IntSetValues * dsv
Iterator for each variable.
Definition int.hh:81
int a
How many assignments 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
int randval(Gecode::Support::RandomGenerator &rand)
Definition int.hpp:76
virtual void next(Gecode::Support::RandomGenerator &rand)
Move to next assignment.
Definition int.cpp:62
int _n1
How many variables in the second set.
Definition int.hh:120
int randval(const Gecode::IntSet &d, Gecode::Support::RandomGenerator &rand)
Definition int.hpp:109
Gecode::IntSet _d1
Domain for second set of variables Generate new value according to domain d.
Definition int.hh:121
virtual void next(Gecode::Support::RandomGenerator &rand)
Move to next assignment.
Definition int.cpp:69
int a
How many assignments still to be generated.
Definition int.hh:119
int * vals
The current values for the variables.
Definition int.hh:118
Space for executing tests.
Definition int.hh:149
int rndvar(Gecode::Support::RandomGenerator &rand)
Randomly select an unassigned variable.
Definition int.cpp:169
Gecode::Reify r
Reification information.
Definition int.hh:156
void assign(const Assignment &a, bool skip, Gecode::Support::RandomGenerator &rand)
Assign all (or all but one, if skip is true) variables to values in a.
Definition int.cpp:259
TestSpace(int n, Gecode::IntSet &d, Test *t)
Create test space without reification.
Definition int.cpp:90
Gecode::IntSet d
Initial domain.
Definition int.hh:152
void rndrel(const Assignment &a, int i, Gecode::IntRelType &irt, int &v, Gecode::Support::RandomGenerator &rand)
Randomly select a pruning rel for variable i.
Definition int.cpp:180
Test * test
The test currently run.
Definition int.hh:158
virtual Gecode::Space * copy(void)
Copy space during cloning.
Definition int.cpp:131
bool disabled(const Assignment &a, TestSpace &c, bool testfix, Gecode::Support::RandomGenerator &rand)
Prune values also in a space c with disabled propagators, but not those in assignment a.
Definition int.cpp:379
void post(void)
Post propagator.
Definition int.cpp:144
bool assigned(void) const
Test whether all variables are assigned.
Definition int.cpp:136
void prune(int i, bool bounds_only, Gecode::Support::RandomGenerator &rand)
Prune some random values from variable i.
Definition int.cpp:280
bool failed(void)
Compute a fixpoint and check for failure.
Definition int.cpp:157
bool reified
Whether the test is for a reified propagator.
Definition int.hh:160
void disable(void)
Disable propagators in space and compute fixpoint (make all idle).
Definition int.cpp:373
Gecode::IntVarArray x
Variables to be tested.
Definition int.hh:154
void bound(Gecode::Support::RandomGenerator &rand)
Assign a random variable to a random bound.
Definition int.cpp:272
void enable(void)
Enable propagators in space.
Definition int.cpp:368
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:426
bool pmi(void) const
Test whether reverse implication as reification mode is supported.
Definition int.hpp:160
virtual bool run(void)
Perform test.
Definition int.cpp:480
virtual bool ignore(const Assignment &) const
Whether to ignore assignment for reification.
Definition int.cpp:471
bool testsearch
Whether to perform search test.
Definition int.hh:238
bool testfix
Whether to perform fixpoint test.
Definition int.hh:240
virtual void post(Gecode::Space &home, Gecode::IntVarArray &x)=0
Post constraint.
bool eqv(void) const
Test whether equivalence as reification mode is supported.
Definition int.hpp:152
int arity
Number of variables.
Definition int.hh:226
virtual bool solution(const Assignment &) const =0
Check for solution.
virtual Assignment * assignment(void) const
Create assignment.
Definition int.cpp:445
Gecode::IntSet dom
Domain of variables.
Definition int.hh:228
bool imp(void) const
Test whether implication as reification mode is supported.
Definition int.hpp:156
ConTestLevel contest
Whether to test for certain consistency.
Definition int.hh:236
Simple class for describing indentation.
Definition test.hh:67
LinearCongruentialGenerator< 2147483647, 48271, 44488, 3399 > RandomGenerator
Default values for linear congruential generator.
Definition random.hpp:183
void branch(Home home, const FloatVarArgs &x, FloatVarBranch vars, FloatValBranch vals, FloatBranchFilter bf=nullptr, FloatVarValPrint vvp=nullptr)
Branch over x with variable selection vars and value selection vals.
Definition branch.cpp:39
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:959
ReifyMode
Mode for reification.
Definition int.hh:882
BoolOpType
Operation types for Booleans.
Definition int.hh:984
IntPropLevel
Propagation levels for integer propagators.
Definition int.hh:1008
@ IRT_EQ
Equality ( ).
Definition int.hh:960
@ IRT_NQ
Disequality ( ).
Definition int.hh:961
@ IRT_GQ
Greater or equal ( ).
Definition int.hh:964
@ IRT_LE
Less ( ).
Definition int.hh:963
@ IRT_GR
Greater ( ).
Definition int.hh:965
@ IRT_LQ
Less or equal ( ).
Definition int.hh:962
@ RM_IMP
Implication for reification.
Definition int.hh:896
@ RM_PMI
Inverse implication for reification.
Definition int.hh:903
@ RM_EQV
Equivalence for reification (default).
Definition int.hh:889
@ BOT_OR
Disjunction.
Definition int.hh:986
@ BOT_EQV
Equivalence.
Definition int.hh:988
@ BOT_IMP
Implication.
Definition int.hh:987
@ BOT_XOR
Exclusive or.
Definition int.hh:989
@ BOT_AND
Conjunction.
Definition int.hh:985
@ IPL_BASIC
Use basic propagation algorithm.
Definition int.hh:1015
@ IPL_BASIC_ADVANCED
Use both.
Definition int.hh:1017
@ IPL_DOM
Domain propagation Options: basic versus advanced propagation.
Definition int.hh:1013
@ IPL_VAL
Value propagation.
Definition int.hh:1011
@ IPL_ADVANCED
Use advanced propagation algorithm.
Definition int.hh:1016
@ IPL_BND
Bounds propagation.
Definition int.hh:1012
Space(void)
Default constructor.
Definition core.cpp:121
Space * clone(void) const
Clone space.
Definition core.hpp:3312
SpaceStatus status(StatusStatistics &stat)
Query space status.
Definition core.cpp:282
@ SS_FAILED
Space is failed
Definition core.hpp:1715
Gecode toplevel namespace
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
IntVarBranch INT_VAR_NONE(void)
Select first unassigned variable.
Definition var.hpp:96
void dom(Home home, FloatVar x, FloatVal n)
Propagates .
Definition dom.cpp:40
IntValBranch INT_VAL_MIN(void)
Select smallest value.
Definition val.hpp:55
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Testing finite domain integers.
Definition int.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:54
Options opt
The options.
Definition test.cpp:95
#define START_TEST(T)
Start new test.
Definition array.cpp:52
#define CHECK_TEST(T, M)
Check the test result and handle failed test.
Definition array.cpp:42
std::ostream & operator<<(std::ostream &os, const Test::Int::Assignment &a)
Definition int.cpp:80