this repo has no description
dekker.one
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
48 CpltAssignment::next(Gecode::Support::RandomGenerator&) {
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 RandomAssignment::next(Gecode::Support::RandomGenerator& rand) {
63 for (int i = this->n; i--; )
64 this->vals[i]= this->randval(rand);
65 this->a--;
66 }
67
68 void
69 RandomMixAssignment::next(Gecode::Support::RandomGenerator& rand) {
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
90 TestSpace::TestSpace(int n, Gecode::IntSet& d0, Test* t)
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);
99 r = Gecode::Reify(b,Gecode::RM_EQV);
100 if (opt.log)
101 olog << ind(2) << "Initial: x[]=" << x
102 << std::endl;
103 }
104
105 TestSpace::TestSpace(int n, Gecode::IntSet& d0, Test* t,
106 Gecode::ReifyMode rm)
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
121 TestSpace::TestSpace(TestSpace& s)
122 : Gecode::Space(s), d(s.d), test(s.test), reified(s.reified) {
123 x.update(*this, s.x);
124 Gecode::BoolVar b;
125 Gecode::BoolVar sr(s.r.var());
126 b.update(*this, sr);
127 r.var(b); r.mode(s.r.mode());
128 }
129
130 Gecode::Space*
131 TestSpace::copy(void) {
132 return new TestSpace(*this);
133 }
134
135 bool
136 TestSpace::assigned(void) const {
137 for (int i=x.size(); i--; )
138 if (!x[i].assigned())
139 return false;
140 return true;
141 }
142
143 void
144 TestSpace::post(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
157 TestSpace::failed(void) {
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
169 TestSpace::rndvar(Gecode::Support::RandomGenerator& rand) {
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,
181 Gecode::Support::RandomGenerator& rand) {
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 v=a[i]+1+
189 static_cast<int>(rand(static_cast<unsigned int>(x[i].max()-a[i])));
190 assert((v > a[i]) && (v <= x[i].max()));
191 irt = IRT_LE;
192 }
193 break;
194 case 1:
195 if (a[i] > x[i].min()) {
196 v=x[i].min()+
197 static_cast<int>(rand(static_cast<unsigned int>(a[i]-x[i].min())));
198 assert((v < a[i]) && (v >= x[i].min()));
199 irt = IRT_GR;
200 }
201 break;
202 default:
203 {
204 Gecode::Int::ViewRanges<Gecode::Int::IntView> it(x[i]);
205 unsigned int skip = rand(static_cast<unsigned int>(x[i].size()-1));
206 while (true) {
207 if (it.width() > skip) {
208 v = it.min() + static_cast<int>(skip);
209 if (v == a[i]) {
210 if (it.width() == 1) {
211 ++it; v = it.min();
212 } else if (v < it.max()) {
213 ++v;
214 } else {
215 --v;
216 }
217 }
218 break;
219 }
220 skip -= it.width(); ++it;
221 }
222 irt = IRT_NQ;
223 break;
224 }
225 }
226 }
227
228 void
229 TestSpace::rel(int i, Gecode::IntRelType irt, int n) {
230 if (opt.log) {
231 olog << ind(4) << "x[" << i << "] ";
232 switch (irt) {
233 case Gecode::IRT_EQ: olog << "="; break;
234 case Gecode::IRT_NQ: olog << "!="; break;
235 case Gecode::IRT_LQ: olog << "<="; break;
236 case Gecode::IRT_LE: olog << "<"; break;
237 case Gecode::IRT_GQ: olog << ">="; break;
238 case Gecode::IRT_GR: olog << ">"; break;
239 }
240 olog << " " << n << std::endl;
241 }
242 Gecode::rel(*this, x[i], irt, n);
243 }
244
245 void
246 TestSpace::rel(bool sol) {
247 int n = sol ? 1 : 0;
248 assert(reified);
249 if (opt.log)
250 olog << ind(4) << "b = " << n << std::endl;
251 Gecode::rel(*this, r.var(), Gecode::IRT_EQ, n);
252 }
253
254 void
255 TestSpace::assign(const Assignment& a, bool skip, Gecode::Support::RandomGenerator& rand) {
256 using namespace Gecode;
257 int i = skip ?
258 static_cast<int>(rand(static_cast<unsigned int>(a.size()))) : -1;
259 for (int j=a.size(); j--; )
260 if (i != j) {
261 rel(j, IRT_EQ, a[j]);
262 if (Base::fixpoint(rand) && failed())
263 return;
264 }
265 }
266
267 void
268 TestSpace::bound(Gecode::Support::RandomGenerator& rand) {
269 using namespace Gecode;
270 int i = rndvar(rand);
271 bool min = rand(2);
272 rel(i, IRT_EQ, min ? x[i].min() : x[i].max());
273 }
274
275 void
276 TestSpace::prune(int i, bool bounds_only, Gecode::Support::RandomGenerator& rand) {
277 using namespace Gecode;
278 // Prune values
279 if (bounds_only) {
280 if (rand(2) && !x[i].assigned()) {
281 int v=x[i].min()+1+
282 static_cast<int>(rand(static_cast<unsigned int>(x[i].max()-x[i].min())));
283 assert((v > x[i].min()) && (v <= x[i].max()));
284 rel(i, Gecode::IRT_LE, v);
285 }
286 if (rand(2) && !x[i].assigned()) {
287 int v=x[i].min()+
288 static_cast<int>(rand(static_cast<unsigned int>(x[i].max()-x[i].min())));
289 assert((v < x[i].max()) && (v >= x[i].min()));
290 rel(i, Gecode::IRT_GR, v);
291 }
292 } else {
293 for (int vals =
294 static_cast<int>(rand(static_cast<unsigned int>(x[i].size()-1))+1); vals--; ) {
295 int v;
296 Gecode::Int::ViewRanges<Gecode::Int::IntView> it(x[i]);
297 unsigned int skip = rand(x[i].size()-1);
298 while (true) {
299 if (it.width() > skip) {
300 v = it.min() + static_cast<int>(skip); break;
301 }
302 skip -= it.width(); ++it;
303 }
304 rel(i, IRT_NQ, v);
305 }
306 }
307 }
308
309 void
310 TestSpace::prune(Gecode::Support::RandomGenerator& rand) {
311 prune(rndvar(rand), false, rand);
312 }
313
314 bool
315 TestSpace::prune(const Assignment& a, bool testfix, Gecode::Support::RandomGenerator& rand) {
316 using namespace Gecode;
317 // Select variable to be pruned
318 int i = rndvar(rand);
319 // Select mode for pruning
320 IntRelType irt;
321 int v;
322 rndrel(a, i, irt, v, rand);
323 if (irt != IRT_EQ)
324 rel(i, irt, v);
325 if (Base::fixpoint(rand)) {
326 if (failed() || !testfix)
327 return true;
328 TestSpace* c = static_cast<TestSpace*>(clone());
329 if (opt.log)
330 olog << ind(3) << "Testing fixpoint on copy" << std::endl;
331 c->post();
332 if (c->failed()) {
333 if (opt.log)
334 olog << ind(4) << "Copy failed after posting" << std::endl;
335 delete c; return false;
336 }
337 for (int j=x.size(); j--; )
338 if (x[j].size() != c->x[j].size()) {
339 if (opt.log)
340 olog << ind(4) << "Different domain size" << std::endl;
341 delete c; return false;
342 }
343 if (reified && (r.var().size() != c->r.var().size())) {
344 if (opt.log)
345 olog << ind(4) << "Different control variable" << std::endl;
346 delete c; return false;
347 }
348 if (opt.log)
349 olog << ind(3) << "Finished testing fixpoint on copy" << std::endl;
350 delete c;
351 }
352 return true;
353 }
354
355 void
356 TestSpace::enable(void) {
357 Gecode::PropagatorGroup::all.enable(*this);
358 }
359
360 void
361 TestSpace::disable(void) {
362 Gecode::PropagatorGroup::all.disable(*this);
363 (void) status();
364 }
365
366 bool
367 TestSpace::disabled(const Assignment& a, TestSpace& c, bool testfix, Gecode::Support::RandomGenerator& rand) {
368 using namespace Gecode;
369 // Disable propagators
370 c.disable();
371 // Select variable to be pruned
372 int i = rndvar(rand);
373 // Select mode for pruning
374 IntRelType irt;
375 int v;
376 rndrel(a, i, irt, v, rand);
377 if (irt != IRT_EQ) {
378 rel(i, irt, v);
379 c.rel(i, irt, v);
380 }
381 // Enable propagators
382 c.enable();
383 if (!testfix)
384 return true;
385 if (failed()) {
386 if (!c.failed()) {
387 if (opt.log)
388 olog << ind(3) << "No failure on disabled copy" << std::endl;
389 return false;
390 }
391 return true;
392 }
393 if (c.failed()) {
394 if (opt.log)
395 olog << ind(3) << "Failure on disabled copy" << std::endl;
396 return false;
397 }
398 for (int j=x.size(); j--; ) {
399 if (x[j].size() != c.x[j].size()) {
400 if (opt.log)
401 olog << ind(4) << "Different domain size" << std::endl;
402 return false;
403 }
404 if (reified && (r.var().size() != c.r.var().size())) {
405 if (opt.log)
406 olog << ind(4) << "Different control variable" << std::endl;
407 return false;
408 }
409 }
410 return true;
411 }
412
413 unsigned int
414 TestSpace::propagators(void) {
415 return Gecode::PropagatorGroup::all.size(*this);
416 }
417
418 const Gecode::IntPropLevel IntPropLevels::ipls[] =
419 {Gecode::IPL_DOM,Gecode::IPL_BND,Gecode::IPL_VAL};
420
421 const Gecode::IntPropLevel IntPropBasicAdvanced::ipls[] =
422 {Gecode::IPL_BASIC_ADVANCED,Gecode::IPL_ADVANCED,Gecode::IPL_BASIC};
423
424 const Gecode::IntRelType IntRelTypes::irts[] =
425 {Gecode::IRT_EQ,Gecode::IRT_NQ,Gecode::IRT_LQ,
426 Gecode::IRT_LE,Gecode::IRT_GQ,Gecode::IRT_GR};
427
428 const Gecode::BoolOpType BoolOpTypes::bots[] =
429 {Gecode::BOT_AND,Gecode::BOT_OR,Gecode::BOT_IMP,
430 Gecode::BOT_EQV,Gecode::BOT_XOR};
431
432 Assignment*
433 Test::assignment(void) const {
434 return new CpltAssignment(arity,dom);
435 }
436
437
438 /// Check the test result and handle failed test
439#define CHECK_TEST(T,M) \
440do { \
441if (opt.log) \
442 olog << ind(3) << "Check: " << (M) << std::endl; \
443if (!(T)) { \
444 problem = (M); delete s; goto failed; \
445} \
446} while (false)
447
448 /// Start new test
449#define START_TEST(T) \
450do { \
451 if (opt.log) { \
452 olog.str(""); \
453 olog << ind(2) << "Testing: " << (T) << std::endl; \
454 } \
455 test = (T); \
456} while (false)
457
458 bool
459 Test::ignore(const Assignment&) const {
460 return false;
461 }
462
463 void
464 Test::post(Gecode::Space&, Gecode::IntVarArray&,
465 Gecode::Reify) {}
466
467 bool
468 Test::run(void) {
469 using namespace Gecode;
470 const char* test = "NONE";
471 const char* problem = "NONE";
472
473 // Set up assignments
474 Assignment* ap = assignment();
475 Assignment& a = *ap;
476
477 // Set up space for all solution search
478 TestSpace* search_s = new TestSpace(arity,dom,this);
479 post(*search_s,search_s->x);
480 branch(*search_s,search_s->x,INT_VAR_NONE(),INT_VAL_MIN());
481 Search::Options search_o;
482 search_o.threads = 1;
483 DFS<TestSpace> e_s(search_s,search_o);
484 delete search_s;
485
486 while (a.has_more()) {
487 bool sol = solution(a);
488 if (opt.log) {
489 olog << ind(1) << "Assignment: " << a
490 << (sol ? " (solution)" : " (no solution)")
491 << std::endl;
492 }
493
494 START_TEST("Assignment (after posting)");
495 {
496 TestSpace* s = new TestSpace(arity,dom,this);
497 TestSpace* sc = nullptr;
498 s->post();
499 switch (_rand(2)) {
500 case 0:
501 if (opt.log)
502 olog << ind(3) << "No copy" << std::endl;
503 sc = s;
504 s = nullptr;
505 break;
506 case 1:
507 if (opt.log)
508 olog << ind(3) << "Copy" << std::endl;
509 if (s->status() != SS_FAILED) {
510 sc = static_cast<TestSpace*>(s->clone());
511 } else {
512 sc = s; s = nullptr;
513 }
514 break;
515 default: assert(false);
516 }
517 sc->assign(a, false, _rand);
518 if (sol) {
519 CHECK_TEST(!sc->failed(), "Failed on solution");
520 CHECK_TEST(sc->propagators()==0, "No subsumption");
521 } else {
522 CHECK_TEST(sc->failed(), "Solved on non-solution");
523 }
524 delete s; delete sc;
525 }
526 START_TEST("Partial assignment (after posting)");
527 {
528 TestSpace* s = new TestSpace(arity,dom,this);
529 s->post();
530 s->assign(a, true, _rand);
531 (void) s->failed();
532 s->assign(a, false, _rand);
533 if (sol) {
534 CHECK_TEST(!s->failed(), "Failed on solution");
535 CHECK_TEST(s->propagators()==0, "No subsumption");
536 } else {
537 CHECK_TEST(s->failed(), "Solved on non-solution");
538 }
539 delete s;
540 }
541 START_TEST("Assignment (after posting, disable)");
542 {
543 TestSpace* s = new TestSpace(arity,dom,this);
544 s->post();
545 s->disable();
546 s->assign(a, false, _rand);
547 s->enable();
548 if (sol) {
549 CHECK_TEST(!s->failed(), "Failed on solution");
550 CHECK_TEST(s->propagators()==0, "No subsumption");
551 } else {
552 CHECK_TEST(s->failed(), "Solved on non-solution");
553 }
554 delete s;
555 }
556 START_TEST("Partial assignment (after posting, disable)");
557 {
558 TestSpace* s = new TestSpace(arity,dom,this);
559 s->post();
560 s->assign(a, true, _rand);
561 s->disable();
562 (void) s->failed();
563 s->assign(a, false, _rand);
564 s->enable();
565 if (sol) {
566 CHECK_TEST(!s->failed(), "Failed on solution");
567 CHECK_TEST(s->propagators()==0, "No subsumption");
568 } else {
569 CHECK_TEST(s->failed(), "Solved on non-solution");
570 }
571 delete s;
572 }
573 START_TEST("Assignment (before posting)");
574 {
575 TestSpace* s = new TestSpace(arity,dom,this);
576 s->assign(a, false, _rand);
577 s->post();
578 if (sol) {
579 CHECK_TEST(!s->failed(), "Failed on solution");
580 CHECK_TEST(s->propagators()==0, "No subsumption");
581 } else {
582 CHECK_TEST(s->failed(), "Solved on non-solution");
583 }
584 delete s;
585 }
586 START_TEST("Partial assignment (before posting)");
587 {
588 TestSpace* s = new TestSpace(arity,dom,this);
589 s->assign(a, true, _rand);
590 s->post();
591 (void) s->failed();
592 s->assign(a, false, _rand);
593 if (sol) {
594 CHECK_TEST(!s->failed(), "Failed on solution");
595 CHECK_TEST(s->propagators()==0, "No subsumption");
596 } else {
597 CHECK_TEST(s->failed(), "Solved on non-solution");
598 }
599 delete s;
600 }
601 START_TEST("Prune");
602 {
603 TestSpace* s = new TestSpace(arity,dom,this);
604 s->post();
605 while (!s->failed() && !s->assigned())
606 if (!s->prune(a, testfix, _rand)) {
607 problem = "No fixpoint";
608 delete s;
609 goto failed;
610 }
611 s->assign(a, false, _rand);
612 if (sol) {
613 CHECK_TEST(!s->failed(), "Failed on solution");
614 CHECK_TEST(s->propagators()==0, "No subsumption");
615 } else {
616 CHECK_TEST(s->failed(), "Solved on non-solution");
617 }
618 delete s;
619 }
620 START_TEST("Prune (disable)");
621 {
622 TestSpace* s = new TestSpace(arity,dom,this);
623 TestSpace* c = static_cast<TestSpace*>(s->clone());
624 s->post(); c->post();
625 while (!s->failed() && !s->assigned())
626 if (!s->disabled(a, *c, testfix, _rand)) {
627 problem = "Different result after re-enable";
628 delete s; delete c;
629 goto failed;
630 }
631 if (testfix && (s->failed() != c->failed())) {
632 problem = "Different failure after re-enable";
633 delete s; delete c;
634 goto failed;
635 }
636 delete s; delete c;
637 }
638 if (!ignore(a)) {
639 if (eqv()) {
640 {
641 START_TEST("Assignment reified (rewrite after post, <=>)");
642 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
643 s->post();
644 s->rel(sol);
645 s->assign(a, false, _rand);
646 CHECK_TEST(!s->failed(), "Failed");
647 CHECK_TEST(s->propagators()==0, "No subsumption");
648 delete s;
649 }
650 {
651 START_TEST("Assignment reified (rewrite failure, <=>)");
652 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
653 s->post();
654 s->rel(!sol);
655 s->assign(a, false, _rand);
656 CHECK_TEST(s->failed(), "Not failed");
657 delete s;
658 }
659 {
660 START_TEST("Assignment reified (immediate rewrite, <=>)");
661 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
662 s->rel(sol);
663 s->post();
664 s->assign(a, false, _rand);
665 CHECK_TEST(!s->failed(), "Failed");
666 CHECK_TEST(s->propagators()==0, "No subsumption");
667 delete s;
668 }
669 {
670 START_TEST("Assignment reified (immediate failure, <=>)");
671 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
672 s->rel(!sol);
673 s->post();
674 s->assign(a, false, _rand);
675 CHECK_TEST(s->failed(), "Not failed");
676 delete s;
677 }
678 {
679 START_TEST("Assignment reified (before posting, <=>)");
680 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
681 s->assign(a, false, _rand);
682 s->post();
683 CHECK_TEST(!s->failed(), "Failed");
684 CHECK_TEST(s->propagators()==0, "No subsumption");
685 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
686 if (sol) {
687 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
688 } else {
689 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
690 }
691 delete s;
692 }
693 {
694 START_TEST("Assignment reified (after posting, <=>)");
695 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
696 s->post();
697 s->assign(a, false, _rand);
698 CHECK_TEST(!s->failed(), "Failed");
699 CHECK_TEST(s->propagators()==0, "No subsumption");
700 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
701 if (sol) {
702 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
703 } else {
704 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
705 }
706 delete s;
707 }
708 {
709 START_TEST("Assignment reified (after posting, <=>, disable)");
710 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
711 s->post();
712 s->disable();
713 s->assign(a, false, _rand);
714 s->enable();
715 CHECK_TEST(!s->failed(), "Failed");
716 CHECK_TEST(s->propagators()==0, "No subsumption");
717 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
718 if (sol) {
719 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
720 } else {
721 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
722 }
723 delete s;
724 }
725 {
726 START_TEST("Prune reified, <=>");
727 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
728 s->post();
729 while (!s->failed() &&
730 (!s->assigned() || !s->r.var().assigned()))
731 if (!s->prune(a, testfix, _rand)) {
732 problem = "No fixpoint";
733 delete s;
734 goto failed;
735 }
736 CHECK_TEST(!s->failed(), "Failed");
737 CHECK_TEST(s->propagators()==0, "No subsumption");
738 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
739 if (sol) {
740 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
741 } else {
742 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
743 }
744 delete s;
745 }
746 {
747 START_TEST("Prune reified, <=>, disable");
748 TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
749 TestSpace* c = static_cast<TestSpace*>(s->clone());
750 s->post(); c->post();
751 while (!s->failed() &&
752 (!s->assigned() || !s->r.var().assigned()))
753 if (!s->disabled(a, *c, testfix, _rand)) {
754 problem = "No fixpoint";
755 delete s;
756 delete c;
757 goto failed;
758 }
759 CHECK_TEST(!c->failed(), "Failed");
760 CHECK_TEST(c->propagators()==0, "No subsumption");
761 CHECK_TEST(c->r.var().assigned(), "Control variable unassigned");
762 if (sol) {
763 CHECK_TEST(c->r.var().val()==1, "Zero on solution");
764 } else {
765 CHECK_TEST(c->r.var().val()==0, "One on non-solution");
766 }
767 delete s;
768 delete c;
769 }
770 }
771
772 if (imp()) {
773 {
774 START_TEST("Assignment reified (rewrite after post, =>)");
775 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
776 s->post();
777 s->rel(sol);
778 s->assign(a, false, _rand);
779 CHECK_TEST(!s->failed(), "Failed");
780 CHECK_TEST(s->propagators()==0, "No subsumption");
781 delete s;
782 }
783 {
784 START_TEST("Assignment reified (rewrite failure, =>)");
785 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
786 s->post();
787 s->rel(!sol);
788 s->assign(a, false, _rand);
789 if (sol) {
790 CHECK_TEST(!s->failed(), "Failed");
791 CHECK_TEST(s->propagators()==0, "No subsumption");
792 } else {
793 CHECK_TEST(s->failed(), "Not failed");
794 }
795 delete s;
796 }
797 {
798 START_TEST("Assignment reified (immediate rewrite, =>)");
799 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
800 s->rel(sol);
801 s->post();
802 s->assign(a, false, _rand);
803 CHECK_TEST(!s->failed(), "Failed");
804 CHECK_TEST(s->propagators()==0, "No subsumption");
805 delete s;
806 }
807 {
808 START_TEST("Assignment reified (immediate failure, =>)");
809 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
810 s->rel(!sol);
811 s->post();
812 s->assign(a, false, _rand);
813 if (sol) {
814 CHECK_TEST(!s->failed(), "Failed");
815 CHECK_TEST(s->propagators()==0, "No subsumption");
816 } else {
817 CHECK_TEST(s->failed(), "Not failed");
818 }
819 delete s;
820 }
821 {
822 START_TEST("Assignment reified (before posting, =>)");
823 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
824 s->assign(a, false, _rand);
825 s->post();
826 CHECK_TEST(!s->failed(), "Failed");
827 CHECK_TEST(s->propagators()==0, "No subsumption");
828 if (sol) {
829 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
830 } else {
831 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
832 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
833 }
834 delete s;
835 }
836 {
837 START_TEST("Assignment reified (after posting, =>)");
838 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
839 s->post();
840 s->assign(a, false, _rand);
841 CHECK_TEST(!s->failed(), "Failed");
842 CHECK_TEST(s->propagators()==0, "No subsumption");
843 if (sol) {
844 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
845 } else {
846 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
847 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
848 }
849 delete s;
850 }
851 {
852 START_TEST("Assignment reified (after posting, =>, disable)");
853 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
854 s->post();
855 s->disable();
856 s->assign(a, false, _rand);
857 s->enable();
858 CHECK_TEST(!s->failed(), "Failed");
859 CHECK_TEST(s->propagators()==0, "No subsumption");
860 if (sol) {
861 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
862 } else {
863 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
864 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
865 }
866 delete s;
867 }
868 {
869 START_TEST("Prune reified, =>");
870 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
871 s->post();
872 while (!s->failed() &&
873 (!s->assigned() || (!sol && !s->r.var().assigned())))
874 if (!s->prune(a, testfix, _rand)) {
875 problem = "No fixpoint";
876 delete s;
877 goto failed;
878 }
879 CHECK_TEST(!s->failed(), "Failed");
880 CHECK_TEST(s->propagators()==0, "No subsumption");
881 if (sol) {
882 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
883 } else {
884 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
885 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
886 }
887 delete s;
888 }
889 {
890 START_TEST("Prune reified, =>, disable");
891 TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
892 TestSpace* c = static_cast<TestSpace*>(s->clone());
893 s->post(); c->post();
894 while (!s->failed() &&
895 (!s->assigned() || (!sol && !s->r.var().assigned())))
896 if (!s->disabled(a, *c, testfix, _rand)) {
897 problem = "No fixpoint";
898 delete s;
899 delete c;
900 goto failed;
901 }
902 CHECK_TEST(!c->failed(), "Failed");
903 CHECK_TEST(c->propagators()==0, "No subsumption");
904 if (sol) {
905 CHECK_TEST(!c->r.var().assigned(), "Control variable assigned");
906 } else {
907 CHECK_TEST(c->r.var().assigned(), "Control variable unassigned");
908 CHECK_TEST(c->r.var().val()==0, "One on non-solution");
909 }
910 delete s;
911 delete c;
912 }
913 }
914
915 if (pmi()) {
916 {
917 START_TEST("Assignment reified (rewrite after post, <=)");
918 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
919 s->post();
920 s->rel(sol);
921 s->assign(a, false, _rand);
922 CHECK_TEST(!s->failed(), "Failed");
923 CHECK_TEST(s->propagators()==0, "No subsumption");
924 delete s;
925 }
926 {
927 START_TEST("Assignment reified (rewrite failure, <=)");
928 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
929 s->post();
930 s->rel(!sol);
931 s->assign(a, false, _rand);
932 if (sol) {
933 CHECK_TEST(s->failed(), "Not failed");
934 } else {
935 CHECK_TEST(!s->failed(), "Failed");
936 CHECK_TEST(s->propagators()==0, "No subsumption");
937 }
938 delete s;
939 }
940 {
941 START_TEST("Assignment reified (immediate rewrite, <=)");
942 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
943 s->rel(sol);
944 s->post();
945 s->assign(a, false, _rand);
946 CHECK_TEST(!s->failed(), "Failed");
947 CHECK_TEST(s->propagators()==0, "No subsumption");
948 delete s;
949 }
950 {
951 START_TEST("Assignment reified (immediate failure, <=)");
952 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
953 s->rel(!sol);
954 s->post();
955 s->assign(a, false, _rand);
956 if (sol) {
957 CHECK_TEST(s->failed(), "Not failed");
958 } else {
959 CHECK_TEST(!s->failed(), "Failed");
960 CHECK_TEST(s->propagators()==0, "No subsumption");
961 }
962 delete s;
963 }
964 {
965 START_TEST("Assignment reified (before posting, <=)");
966 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
967 s->assign(a, false, _rand);
968 s->post();
969 CHECK_TEST(!s->failed(), "Failed");
970 CHECK_TEST(s->propagators()==0, "No subsumption");
971 if (sol) {
972 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
973 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
974 } else {
975 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
976 }
977 delete s;
978 }
979 {
980 START_TEST("Assignment reified (after posting, <=)");
981 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
982 s->post();
983 s->assign(a, false, _rand);
984 CHECK_TEST(!s->failed(), "Failed");
985 CHECK_TEST(s->propagators()==0, "No subsumption");
986 if (sol) {
987 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
988 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
989 } else {
990 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
991 }
992 delete s;
993 }
994 {
995 START_TEST("Assignment reified (after posting, <=, disable)");
996 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
997 s->post();
998 s->disable();
999 s->assign(a, false, _rand);
1000 s->enable();
1001 CHECK_TEST(!s->failed(), "Failed");
1002 CHECK_TEST(s->propagators()==0, "No subsumption");
1003 if (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 {
1012 START_TEST("Prune reified, <=");
1013 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
1014 s->post();
1015 while (!s->failed() &&
1016 (!s->assigned() || (sol && !s->r.var().assigned())))
1017 if (!s->prune(a, testfix, _rand)) {
1018 problem = "No fixpoint";
1019 delete s;
1020 goto failed;
1021 }
1022 CHECK_TEST(!s->failed(), "Failed");
1023 CHECK_TEST(s->propagators()==0, "No subsumption");
1024 if (sol) {
1025 CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1026 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1027 } else {
1028 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1029 }
1030 delete s;
1031 }
1032 {
1033 START_TEST("Prune reified, <=, disable");
1034 TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
1035 TestSpace* c = static_cast<TestSpace*>(s->clone());
1036 s->post(); c->post();
1037 while (!s->failed() &&
1038 (!s->assigned() || (sol && !s->r.var().assigned())))
1039 if (!s->disabled(a, *c, testfix, _rand)) {
1040 problem = "No fixpoint";
1041 delete s;
1042 delete c;
1043 goto failed;
1044 }
1045 CHECK_TEST(!c->failed(), "Failed");
1046 CHECK_TEST(c->propagators()==0, "No subsumption");
1047 if (sol) {
1048 CHECK_TEST(c->r.var().assigned(), "Control variable unassigned");
1049 CHECK_TEST(c->r.var().val()==1, "Zero on solution");
1050 } else {
1051 CHECK_TEST(!c->r.var().assigned(), "Control variable assigned");
1052 }
1053 delete s;
1054 delete c;
1055 }
1056 }
1057 }
1058
1059 if (testsearch) {
1060 if (sol) {
1061 START_TEST("Search");
1062 TestSpace* s = e_s.next();
1063 CHECK_TEST(s != nullptr, "Solutions exhausted");
1064 CHECK_TEST(s->propagators()==0, "No subsumption");
1065 for (int i=a.size(); i--; ) {
1066 CHECK_TEST(s->x[i].assigned(), "Unassigned variable");
1067 CHECK_TEST(a[i] == s->x[i].val(), "Wrong value in solution");
1068 }
1069 delete s;
1070 }
1071 }
1072
1073 a.next(_rand);
1074 }
1075
1076 if (testsearch) {
1077 test = "Search";
1078 if (e_s.next() != nullptr) {
1079 problem = "Excess solutions";
1080 goto failed;
1081 }
1082 }
1083
1084 switch (contest) {
1085 case CTL_NONE: break;
1086 case CTL_DOMAIN: {
1087 START_TEST("Full domain consistency");
1088 TestSpace* s = new TestSpace(arity,dom,this);
1089 s->post();
1090 if (!s->failed()) {
1091 while (!s->failed() && !s->assigned())
1092 s->prune(_rand);
1093 CHECK_TEST(!s->failed(), "Failed");
1094 CHECK_TEST(s->propagators()==0, "No subsumption");
1095 }
1096 delete s;
1097 // Fall-through -- domain implies bounds(d) and bounds(z)
1098 }
1099 case CTL_BOUNDS_D: {
1100 START_TEST("Bounds(D)-consistency");
1101 TestSpace* s = new TestSpace(arity,dom,this);
1102 s->post();
1103 for (int i = s->x.size(); i--; )
1104 s->prune(i, false, _rand);
1105 if (!s->failed()) {
1106 while (!s->failed() && !s->assigned())
1107 s->bound(_rand);
1108 CHECK_TEST(!s->failed(), "Failed");
1109 CHECK_TEST(s->propagators()==0, "No subsumption");
1110 }
1111 delete s;
1112 // Fall-through -- bounds(d) implies bounds(z)
1113 }
1114 case CTL_BOUNDS_Z: {
1115 START_TEST("Bounds(Z)-consistency");
1116 TestSpace* s = new TestSpace(arity,dom,this);
1117 s->post();
1118 for (int i = s->x.size(); i--; )
1119 s->prune(i, true, _rand);
1120 if (!s->failed()) {
1121 while (!s->failed() && !s->assigned())
1122 s->bound(_rand);
1123 CHECK_TEST(!s->failed(), "Failed");
1124 CHECK_TEST(s->propagators()==0, "No subsumption");
1125 }
1126 delete s;
1127 break;
1128 }
1129 }
1130
1131 delete ap;
1132 return true;
1133
1134 failed:
1135 if (opt.log)
1136 olog << "FAILURE" << std::endl
1137 << ind(1) << "Test: " << test << std::endl
1138 << ind(1) << "Problem: " << problem << std::endl;
1139 if (a.has_more() && opt.log)
1140 olog << ind(1) << "Assignment: " << a << std::endl;
1141 delete ap;
1142
1143 return false;
1144 }
1145
1146}}
1147
1148#undef START_TEST
1149#undef CHECK_TEST
1150
1151// STATISTICS: test-int