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::operator++(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
63 RandomAssignment::operator++(void) {
64 for (int i = n; i--; )
65 vals[i]=randval();
66 a--;
67 }
68
69 void
70 RandomMixAssignment::operator++(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
91 TestSpace::TestSpace(int n, Gecode::IntSet& d0, Test* t)
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);
100 r = Gecode::Reify(b,Gecode::RM_EQV);
101 if (opt.log)
102 olog << ind(2) << "Initial: x[]=" << x
103 << std::endl;
104 }
105
106 TestSpace::TestSpace(int n, Gecode::IntSet& d0, Test* t,
107 Gecode::ReifyMode rm)
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
122 TestSpace::TestSpace(TestSpace& s)
123 : Gecode::Space(s), d(s.d), test(s.test), reified(s.reified) {
124 x.update(*this, s.x);
125 Gecode::BoolVar b;
126 Gecode::BoolVar sr(s.r.var());
127 b.update(*this, sr);
128 r.var(b); r.mode(s.r.mode());
129 }
130
131 Gecode::Space*
132 TestSpace::copy(void) {
133 return new TestSpace(*this);
134 }
135
136 bool
137 TestSpace::assigned(void) const {
138 for (int i=x.size(); i--; )
139 if (!x[i].assigned())
140 return false;
141 return true;
142 }
143
144 void
145 TestSpace::post(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
158 TestSpace::failed(void) {
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
170 TestSpace::rndvar(void) {
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
181 TestSpace::rndrel(const Assignment& a, int i,
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 {
207 Gecode::Int::ViewRanges<Gecode::Int::IntView> it(x[i]);
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
233 TestSpace::rel(int i, Gecode::IntRelType irt, int n) {
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
272 TestSpace::bound(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;
302 Gecode::Int::ViewRanges<Gecode::Int::IntView> it(x[i]);
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
316 TestSpace::prune(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
362 TestSpace::enable(void) {
363 Gecode::PropagatorGroup::all.enable(*this);
364 }
365
366 void
367 TestSpace::disable(void) {
368 Gecode::PropagatorGroup::all.disable(*this);
369 (void) status();
370 }
371
372 bool
373 TestSpace::disabled(const Assignment& a, TestSpace& c,
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
421 TestSpace::propagators(void) {
422 return Gecode::PropagatorGroup::all.size(*this);
423 }
424
425 const Gecode::IntPropLevel IntPropLevels::ipls[] =
426 {Gecode::IPL_DOM,Gecode::IPL_BND,Gecode::IPL_VAL};
427
428 const Gecode::IntPropLevel IntPropBasicAdvanced::ipls[] =
429 {Gecode::IPL_BASIC_ADVANCED,Gecode::IPL_ADVANCED,Gecode::IPL_BASIC};
430
431 const Gecode::IntRelType IntRelTypes::irts[] =
432 {Gecode::IRT_EQ,Gecode::IRT_NQ,Gecode::IRT_LQ,
433 Gecode::IRT_LE,Gecode::IRT_GQ,Gecode::IRT_GR};
434
435 const Gecode::BoolOpType BoolOpTypes::bots[] =
436 {Gecode::BOT_AND,Gecode::BOT_OR,Gecode::BOT_IMP,
437 Gecode::BOT_EQV,Gecode::BOT_XOR};
438
439 Assignment*
440 Test::assignment(void) const {
441 return new CpltAssignment(arity,dom);
442 }
443
444
445 /// Check the test result and handle failed test
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
453 /// Start new test
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
467 Test::post(Gecode::Space&, Gecode::IntVarArray&,
468 Gecode::Reify) {}
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 = nullptr;
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 = nullptr;
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 = nullptr;
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 != nullptr, "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() != nullptr) {
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