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 * Vincent Barichard <Vincent.Barichard@univ-angers.fr>
7 *
8 * Copyright:
9 * Christian Schulte, 2005
10 * Mikael Lagerkvist, 2005
11 * Vincent Barichard, 2012
12 *
13 * This file is part of Gecode, the generic constraint
14 * development environment:
15 * http://www.gecode.org
16 *
17 * Permission is hereby granted, free of charge, to any person obtaining
18 * a copy of this software and associated documentation files (the
19 * "Software"), to deal in the Software without restriction, including
20 * without limitation the rights to use, copy, modify, merge, publish,
21 * distribute, sublicense, and/or sell copies of the Software, and to
22 * permit persons to whom the Software is furnished to do so, subject to
23 * the following conditions:
24 *
25 * The above copyright notice and this permission notice shall be
26 * included in all copies or substantial portions of the Software.
27 *
28 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
29 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
30 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
31 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
32 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
33 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
34 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
35 *
36 */
37
38#include "test/float.hh"
39
40#include <algorithm>
41#include <iomanip>
42
43namespace Test { namespace Float {
44
45 /*
46 * Complete assignments
47 *
48 */
49 void
50 CpltAssignment::next(Gecode::Support::RandomGenerator&) {
51 using namespace Gecode;
52 int i = n-1;
53 while (true) {
54 FloatNum ns = dsv[i].min() + step;
55 dsv[i] = FloatVal(ns,nextafter(ns,ns+1));
56 if ((dsv[i].max() < d.max()) || (i == 0))
57 return;
58 dsv[i--] = FloatVal(d.min(),nextafter(d.min(),d.max()));
59 }
60 }
61
62 /*
63 * Extended assignments
64 *
65 */
66 void
67 ExtAssignment::next(Gecode::Support::RandomGenerator&) {
68 using namespace Gecode;
69 assert(n > 1);
70 int i = n-2;
71 while (true) {
72 FloatNum ns = dsv[i].min() + step;
73 dsv[i] = FloatVal(ns,nextafter(ns,ns+1));
74 if ((dsv[i].max() < d.max()) || (i == 0)) {
75 if (curPb->extendAssignement(*this)) return;
76 if ((dsv[i].max() >= d.max()) && (i == 0)) return;
77 continue;
78 }
79 dsv[i--] = FloatVal(d.min(),nextafter(d.min(),d.max()));
80 }
81 }
82
83
84 /*
85 * Random assignments
86 *
87 */
88 void
89 RandomAssignment::next(Gecode::Support::RandomGenerator& rand) {
90 for (int i = n; i--; )
91 vals[i]= randval(rand);
92 a--;
93 }
94
95}}
96
97std::ostream&
98operator<<(std::ostream& os, const Test::Float::Assignment& a) {
99 int n = a.size();
100 os << "{";
101 for (int i=0; i<n; i++)
102 os << "[" << a[i].min() << "," << a[i].max() << "]" << ((i!=n-1) ? "," : "}");
103 return os;
104}
105
106namespace Test { namespace Float {
107
108 Gecode::FloatNum randFValDown(Gecode::FloatNum l, Gecode::FloatNum u, Gecode::Support::RandomGenerator& rand) {
109 using namespace Gecode;
110 using namespace Gecode::Float;
111 Rounding r;
112 return
113 r.add_down(
114 l,
115 r.mul_down(
116 r.div_down(
117 rand(static_cast<unsigned int>(Int::Limits::max)),
118 static_cast<FloatNum>(Int::Limits::max)
119 ),
120 r.sub_down(u,l)
121 )
122 );
123 }
124
125 Gecode::FloatNum randFValUp(Gecode::FloatNum l, Gecode::FloatNum u, Gecode::Support::RandomGenerator& rand) {
126 using namespace Gecode;
127 using namespace Gecode::Float;
128 Rounding r;
129 return
130 r.sub_up(
131 u,
132 r.mul_down(
133 r.div_down(
134 rand(static_cast<unsigned int>(Int::Limits::max)),
135 static_cast<FloatNum>(Int::Limits::max)
136 ),
137 r.sub_down(u,l)
138 )
139 );
140 }
141
142
143 TestSpace::TestSpace(int n, Gecode::FloatVal& d0, Gecode::FloatNum s,
144 Test* t)
145 : d(d0), step(s),
146 x(*this,n,Gecode::Float::Limits::min,Gecode::Float::Limits::max),
147 test(t), reified(false) {
148 Gecode::FloatVarArgs _x(*this,n,d.min(),d.max());
149 if (x.size() == 1)
150 Gecode::dom(*this,x[0],_x[0]);
151 else
152 Gecode::dom(*this,x,_x);
153 Gecode::BoolVar b(*this,0,1);
154 r = Gecode::Reify(b,Gecode::RM_EQV);
155 if (opt.log)
156 olog << ind(2) << "Initial: x[]=" << x
157 << std::endl;
158 }
159
160 TestSpace::TestSpace(int n, Gecode::FloatVal& d0, Gecode::FloatNum s,
161 Test* t, Gecode::ReifyMode rm)
162 : d(d0), step(s), x(*this,n,d.min(),d.max()), test(t), reified(true) {
163 Gecode::BoolVar b(*this,0,1);
164 r = Gecode::Reify(b,rm);
165 if (opt.log)
166 olog << ind(2) << "Initial: x[]=" << x
167 << " b=" << r.var()
168 << std::endl;
169 }
170
171 TestSpace::TestSpace(TestSpace& s)
172 : Gecode::Space(s), d(s.d), step(s.step), test(s.test), reified(s.reified) {
173 x.update(*this, s.x);
174 Gecode::BoolVar b;
175 Gecode::BoolVar sr(s.r.var());
176 b.update(*this, sr);
177 r.var(b); r.mode(s.r.mode());
178 }
179
180 Gecode::Space*
181 TestSpace::copy(void) {
182 return new TestSpace(*this);
183 }
184
185 void
186 TestSpace::enable(void) {
187 Gecode::PropagatorGroup::all.enable(*this);
188 }
189
190 void
191 TestSpace::disable(void) {
192 Gecode::PropagatorGroup::all.disable(*this);
193 (void) status();
194 }
195
196 void
197 TestSpace::dropUntil(const Assignment& a) {
198 for (int i = x.size(); i--; )
199 Gecode::rel(*this, x[i], Gecode::FRT_GQ, a[i].min());
200 }
201
202 bool
203 TestSpace::assigned(void) const {
204 for (int i=x.size(); i--; )
205 if (!x[i].assigned())
206 return false;
207 return true;
208 }
209
210 bool
211 TestSpace::matchAssignment(const Assignment& a) const {
212 for (int i=x.size(); i--; )
213 if ((x[i].min() < a[i].min()) && (x[i].max() > a[i].max()))
214 return false;
215 return true;
216 }
217
218 void
219 TestSpace::post(void) {
220 if (reified){
221 test->post(*this,x,r);
222 if (opt.log)
223 olog << ind(3) << "Posting reified propagator" << std::endl;
224 } else {
225 test->post(*this,x);
226 if (opt.log)
227 olog << ind(3) << "Posting propagator" << std::endl;
228 }
229 }
230
231 bool
232 TestSpace::failed(void) {
233 if (opt.log) {
234 olog << ind(3) << "Fixpoint: " << x;
235 bool f=(status() == Gecode::SS_FAILED);
236 olog << std::endl << ind(3) << " --> " << x << std::endl;
237 return f;
238 } else {
239 return status() == Gecode::SS_FAILED;
240 }
241 }
242
243 void
244 TestSpace::rel(int i, Gecode::FloatRelType frt, Gecode::FloatVal n) {
245 if (opt.log) {
246 olog << ind(4) << "x[" << i << "] ";
247 switch (frt) {
248 case Gecode::FRT_EQ: olog << "="; break;
249 case Gecode::FRT_NQ: olog << "!="; break;
250 case Gecode::FRT_LQ: olog << "<="; break;
251 case Gecode::FRT_LE: olog << "<"; break;
252 case Gecode::FRT_GQ: olog << ">="; break;
253 case Gecode::FRT_GR: olog << ">"; break;
254 }
255 olog << " [" << n.min() << "," << n.max() << "]" << std::endl;
256 }
257 Gecode::rel(*this, x[i], frt, n);
258 }
259
260 void
261 TestSpace::rel(bool sol) {
262 int n = sol ? 1 : 0;
263 assert(reified);
264 if (opt.log)
265 olog << ind(4) << "b = " << n << std::endl;
266 Gecode::rel(*this, r.var(), Gecode::IRT_EQ, n);
267 }
268
269 void
270 TestSpace::assign(const Assignment& a, MaybeType& sol, bool skip, Gecode::Support::RandomGenerator& rand) {
271 using namespace Gecode;
272 int i = skip ? static_cast<int>(rand(a.size())) : -1;
273
274 for (int j=a.size(); j--; )
275 if (i != j) {
276 if ((x[j].min() == a[j].max()) || (x[j].max() == a[j].min()))
277 {
278 sol = MT_MAYBE;
279 return;
280 }
281 rel(j, FRT_EQ, a[j]);
282 if (Base::fixpoint(rand) && failed())
283 return;
284 }
285 }
286
287 void
288 TestSpace::bound(Gecode::Support::RandomGenerator& rand) {
289 using namespace Gecode;
290 // Select variable to be assigned
291 int i = rand(x.size());
292 while (x[i].assigned()) {
293 i = (i+1) % x.size();
294 }
295 bool min = rand(2);
296 if (min)
297 rel(i, FRT_LQ, nextafter(x[i].min(), x[i].max()));
298 else
299 rel(i, FRT_GQ, nextafter(x[i].max(), x[i].min()));
300 }
301
302 Gecode::FloatNum
303 TestSpace::cut(int* cutDirections) {
304 using namespace Gecode;
305 using namespace Gecode::Float;
306 // Select variable to be cut
307 int i = 0;
308 while (x[i].assigned()) i++;
309 for (int j=x.size(); j--; ) {
310 if (!x[j].assigned() && (x[j].size() > x[i].size())) i = j;
311 }
312 Rounding rounding;
313 if (cutDirections[i]) {
314 FloatNum m = rounding.div_up(rounding.add_up(x[i].min(), x[i].max()), 2);
315 FloatNum n = nextafter(x[i].min(), x[i].max());
316 if (m > n)
317 rel(i, FRT_LQ, m);
318 else
319 rel(i, FRT_LQ, n);
320 } else {
321 FloatNum m = rounding.div_down(rounding.add_down(x[i].min(), x[i].max()), 2);
322 FloatNum n = nextafter(x[i].max(), x[i].min());
323 if (m < n)
324 rel(i, FRT_GQ, m);
325 else
326 rel(i, FRT_GQ, n);
327 }
328 return x[i].size();
329 }
330
331 void
332 TestSpace::prune(int i, Gecode::Support::RandomGenerator& rand) {
333 using namespace Gecode;
334 // Prune values
335 if (rand(2) && !x[i].assigned()) {
336 Gecode::FloatNum v= randFValUp(x[i].min(), x[i].max(), rand);
337 assert((v >= x[i].min()) && (v <= x[i].max()));
338 rel(i, Gecode::FRT_LQ, v);
339 }
340 if (rand(2) && !x[i].assigned()) {
341 Gecode::FloatNum v= randFValDown(x[i].min(), x[i].max(), rand);
342 assert((v <= x[i].max()) && (v >= x[i].min()));
343 rel(i, Gecode::FRT_GQ, v);
344 }
345 }
346
347 void
348 TestSpace::prune(Gecode::Support::RandomGenerator& rand) {
349 using namespace Gecode;
350 // Select variable to be pruned
351 int i = rand(x.size());
352 while (x[i].assigned()) {
353 i = (i+1) % x.size();
354 }
355 prune(i, rand);
356 }
357
358 bool
359 TestSpace::prune(const Assignment& a, bool testfix, Gecode::Support::RandomGenerator& rand) {
360 // Select variable to be pruned
361 int i = rand(x.size());
362 while (x[i].assigned())
363 i = (i+1) % x.size();
364 // Select mode for pruning
365 switch (rand(2)) {
366 case 0:
367 if (a[i].max() < x[i].max()) {
368 Gecode::FloatNum v= randFValDown(a[i].max(), x[i].max(), rand);
369 if (v==x[i].max())
370 v = a[i].max();
371 assert((v >= a[i].max()) && (v <= x[i].max()));
372 rel(i, Gecode::FRT_LQ, v);
373 }
374 break;
375 case 1:
376 if (a[i].min() > x[i].min()) {
377 Gecode::FloatNum v= randFValUp(x[i].min(), a[i].min(), rand);
378 if (v==x[i].min())
379 v = a[i].min();
380 assert((v <= a[i].min()) && (v >= x[i].min()));
381 rel(i, Gecode::FRT_GQ, v);
382 }
383 break;
384 }
385 if (Base::fixpoint(rand)) {
386 if (failed() || !testfix)
387 return true;
388 TestSpace* c = static_cast<TestSpace*>(clone());
389 if (opt.log)
390 olog << ind(3) << "Testing fixpoint on copy" << std::endl;
391 c->post();
392 if (c->failed()) {
393 delete c; return false;
394 }
395 for (int j=x.size(); j--; )
396 if (x[j].size() != c->x[j].size()) {
397 delete c; return false;
398 }
399 if (reified && (r.var().size() != c->r.var().size())) {
400 delete c; return false;
401 }
402 if (opt.log)
403 olog << ind(3) << "Finished testing fixpoint on copy" << std::endl;
404 delete c;
405 }
406 return true;
407 }
408
409 unsigned int
410 TestSpace::propagators(void) {
411 return Gecode::PropagatorGroup::all.size(*this);
412 }
413
414
415 const Gecode::FloatRelType FloatRelTypes::frts[] =
416 {Gecode::FRT_EQ,Gecode::FRT_NQ,Gecode::FRT_LQ,Gecode::FRT_LE,
417 Gecode::FRT_GQ,Gecode::FRT_GR};
418
419 Assignment*
420 Test::assignment(void) const {
421 switch (assigmentType) {
422 case CPLT_ASSIGNMENT:
423 return new CpltAssignment(arity,dom,step);
424 case RANDOM_ASSIGNMENT:
425 return new RandomAssignment(arity, dom, step, _rand);
426 case EXTEND_ASSIGNMENT:
427 return new ExtAssignment(arity, dom, step, this, _rand);
428 default :
429 GECODE_NEVER;
430 }
431 return nullptr; // Avoid compiler warnings
432 }
433
434 bool
435 Test::extendAssignement(Assignment&) const {
436 GECODE_NEVER;
437 return false;
438 }
439
440 bool
441 Test::subsumed(const TestSpace& ts) const {
442 if (!testsubsumed) return true;
443 if (const_cast<TestSpace&>(ts).propagators() == 0) return true;
444 if (assigmentType == EXTEND_ASSIGNMENT) return true;
445 return false;
446 }
447
448 /// Check the test result and handle failed test
449#define CHECK_TEST(T,M) \
450do { \
451if (opt.log) \
452 olog << ind(3) << "Check: " << (M) << std::endl; \
453if (!(T)) { \
454 problem = (M); delete s; goto failed; \
455} \
456} while (false)
457
458 /// Start new test
459#define START_TEST(T) \
460do { \
461 if (opt.log) { \
462 olog.str(""); \
463 olog << ind(2) << "Testing: " << (T) << std::endl; \
464 } \
465 test = (T); \
466} while (false)
467
468 bool
469 Test::ignore(const Assignment&) const {
470 return false;
471 }
472
473 void
474 Test::post(Gecode::Space&, Gecode::FloatVarArray&,
475 Gecode::Reify) {}
476
477 bool
478 Test::run(void) {
479 using namespace Gecode;
480 const char* test = "NONE";
481 const char* problem = "NONE";
482
483 // Set up assignments
484 Assignment* ap = assignment();
485 Assignment& a = *ap;
486
487 // Set up space for all solution search
488 TestSpace* search_s = new TestSpace(arity,dom,step,this);
489 post(*search_s,search_s->x);
490 branch(*search_s,search_s->x,FLOAT_VAR_NONE(),FLOAT_VAL_SPLIT_MIN());
491 Search::Options search_o;
492 search_o.threads = 1;
493 DFS<TestSpace> * e_s = new DFS<TestSpace>(search_s,search_o);
494 while (a.has_more()) {
495 MaybeType sol = solution(a);
496 if (opt.log) {
497 olog << ind(1) << "Assignment: " << a;
498 switch (sol) {
499 case MT_TRUE: olog << " (solution)"; break;
500 case MT_FALSE: olog << " (no solution)"; break;
501 case MT_MAYBE: olog << " (maybe)"; break;
502 }
503 olog << std::endl;
504 }
505 START_TEST("Assignment (after posting)");
506 {
507 TestSpace* s = new TestSpace(arity,dom,step,this);
508 TestSpace* sc = nullptr;
509 s->post();
510 switch (_rand(2)) {
511 case 0:
512 if (opt.log)
513 olog << ind(3) << "No copy" << std::endl;
514 sc = s;
515 s = nullptr;
516 break;
517 case 1:
518 if (opt.log)
519 olog << ind(3) << "Copy" << std::endl;
520 if (s->status() != SS_FAILED) {
521 sc = static_cast<TestSpace*>(s->clone());
522 } else {
523 sc = s; s = nullptr;
524 }
525 break;
526 default: assert(false);
527 }
528 sc->assign(a, sol, false, _rand);
529 if (sol == MT_TRUE) {
530 CHECK_TEST(!sc->failed(), "Failed on solution");
531 CHECK_TEST(subsumed(*sc), "No subsumption");
532 } else if (sol == MT_FALSE) {
533 CHECK_TEST(sc->failed(), "Solved on non-solution");
534 }
535 delete s; delete sc;
536 }
537 START_TEST("Partial assignment (after posting)");
538 {
539 TestSpace* s = new TestSpace(arity,dom,step,this);
540 s->post();
541 s->assign(a, sol, true, _rand);
542 (void) s->failed();
543 s->assign(a, sol, false, _rand);
544 if (sol == MT_TRUE) {
545 CHECK_TEST(!s->failed(), "Failed on solution");
546 CHECK_TEST(subsumed(*s), "No subsumption");
547 } else if (sol == MT_FALSE) {
548 CHECK_TEST(s->failed(), "Solved on non-solution");
549 }
550 delete s;
551 }
552 START_TEST("Assignment (after posting, disable)");
553 {
554 TestSpace* s = new TestSpace(arity,dom,step,this);
555 s->post();
556 s->disable();
557 s->enable();
558 s->assign(a, sol, false, _rand);
559 if (sol == MT_TRUE) {
560 CHECK_TEST(!s->failed(), "Failed on solution");
561 CHECK_TEST(subsumed(*s), "No subsumption");
562 } else if (sol == MT_FALSE) {
563 CHECK_TEST(s->failed(), "Solved on non-solution");
564 }
565 delete s;
566 }
567 START_TEST("Partial assignment (after posting, disable)");
568 {
569 TestSpace* s = new TestSpace(arity,dom,step,this);
570 s->post();
571 s->disable();
572 s->enable();
573 s->assign(a, sol, true, _rand);
574 (void) s->failed();
575 s->assign(a, sol, false, _rand);
576 if (sol == MT_TRUE) {
577 CHECK_TEST(!s->failed(), "Failed on solution");
578 CHECK_TEST(subsumed(*s), "No subsumption");
579 } else if (sol == MT_FALSE) {
580 CHECK_TEST(s->failed(), "Solved on non-solution");
581 }
582 delete s;
583 }
584 START_TEST("Assignment (before posting)");
585 {
586 TestSpace* s = new TestSpace(arity,dom,step,this);
587 s->assign(a, sol, false, _rand);
588 s->post();
589 if (sol == MT_TRUE) {
590 CHECK_TEST(!s->failed(), "Failed on solution");
591 CHECK_TEST(subsumed(*s), "No subsumption");
592 } else if (sol == MT_FALSE) {
593 CHECK_TEST(s->failed(), "Solved on non-solution");
594 }
595 delete s;
596 }
597 START_TEST("Partial assignment (before posting)");
598 {
599 TestSpace* s = new TestSpace(arity,dom,step,this);
600 s->assign(a, sol, true, _rand);
601 s->post();
602 (void) s->failed();
603 s->assign(a, sol, false, _rand);
604 if (sol == MT_TRUE) {
605 CHECK_TEST(!s->failed(), "Failed on solution");
606 CHECK_TEST(subsumed(*s), "No subsumption");
607 } else if (sol == MT_FALSE) {
608 CHECK_TEST(s->failed(), "Solved on non-solution");
609 }
610 delete s;
611 }
612 START_TEST("Prune");
613 {
614 TestSpace* s = new TestSpace(arity,dom,step,this);
615 s->post();
616 while (!s->failed() && !s->assigned() && !s->matchAssignment(a))
617 if (!s->prune(a, testfix, _rand)) {
618 problem = "No fixpoint";
619 delete s;
620 goto failed;
621 }
622 s->assign(a, sol, false, _rand);
623 if (sol == MT_TRUE) {
624 CHECK_TEST(!s->failed(), "Failed on solution");
625 CHECK_TEST(subsumed(*s), "No subsumption");
626 } else if (sol == MT_FALSE) {
627 CHECK_TEST(s->failed(), "Solved on non-solution");
628 }
629 delete s;
630 }
631 if (reified && !ignore(a) && (sol != MT_MAYBE)) {
632 if (eqv()) {
633 START_TEST("Assignment reified (rewrite after post, <=>)");
634 TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
635 s->post();
636 s->rel(sol == MT_TRUE);
637 s->assign(a, sol, false, _rand);
638 CHECK_TEST(!s->failed(), "Failed");
639 CHECK_TEST(subsumed(*s), "No subsumption");
640 delete s;
641 }
642 if (imp()) {
643 START_TEST("Assignment reified (rewrite after post, =>)");
644 TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
645 s->post();
646 s->rel(sol == MT_TRUE);
647 s->assign(a, sol, false, _rand);
648 CHECK_TEST(!s->failed(), "Failed");
649 CHECK_TEST(subsumed(*s), "No subsumption");
650 delete s;
651 }
652 if (pmi()) {
653 START_TEST("Assignment reified (rewrite after post, <=)");
654 TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
655 s->post();
656 s->rel(sol == MT_TRUE);
657 s->assign(a, sol, false, _rand);
658 CHECK_TEST(!s->failed(), "Failed");
659 CHECK_TEST(subsumed(*s), "No subsumption");
660 delete s;
661 }
662 if (eqv()) {
663 START_TEST("Assignment reified (immediate rewrite, <=>)");
664 TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
665 s->rel(sol == MT_TRUE);
666 s->post();
667 s->assign(a, sol, false, _rand);
668 CHECK_TEST(!s->failed(), "Failed");
669 CHECK_TEST(subsumed(*s), "No subsumption");
670 delete s;
671 }
672 if (imp()) {
673 START_TEST("Assignment reified (immediate rewrite, =>)");
674 TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
675 s->rel(sol == MT_TRUE);
676 s->post();
677 s->assign(a, sol, false, _rand);
678 CHECK_TEST(!s->failed(), "Failed");
679 CHECK_TEST(subsumed(*s), "No subsumption");
680 delete s;
681 }
682 if (pmi()) {
683 START_TEST("Assignment reified (immediate rewrite, <=)");
684 TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
685 s->rel(sol == MT_TRUE);
686 s->post();
687 s->assign(a, sol, false, _rand);
688 CHECK_TEST(!s->failed(), "Failed");
689 CHECK_TEST(subsumed(*s), "No subsumption");
690 delete s;
691 }
692 if (eqv()) {
693 START_TEST("Assignment reified (before posting, <=>)");
694 TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
695 s->assign(a, sol, false, _rand);
696 s->post();
697 CHECK_TEST(!s->failed(), "Failed");
698 CHECK_TEST(subsumed(*s), "No subsumption");
699 if (s->r.var().assigned()) {
700 if (sol == MT_TRUE) {
701 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
702 } else if (sol == MT_FALSE) {
703 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
704 }
705 }
706 delete s;
707 }
708 if (imp()) {
709 START_TEST("Assignment reified (before posting, =>)");
710 TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
711 s->assign(a, sol, false, _rand);
712 s->post();
713 CHECK_TEST(!s->failed(), "Failed");
714 CHECK_TEST(subsumed(*s), "No subsumption");
715 if (sol == MT_TRUE) {
716 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
717 } else if ((sol = MT_FALSE) && s->r.var().assigned()) {
718 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
719 }
720 delete s;
721 }
722 if (pmi()) {
723 START_TEST("Assignment reified (before posting, <=)");
724 TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
725 s->assign(a, sol, false, _rand);
726 s->post();
727 CHECK_TEST(!s->failed(), "Failed");
728 CHECK_TEST(subsumed(*s), "No subsumption");
729 if (sol == MT_TRUE) {
730 if (s->r.var().assigned()) {
731 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
732 }
733 } else if (sol == MT_FALSE) {
734 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
735 }
736 delete s;
737 }
738 if (eqv()) {
739 START_TEST("Assignment reified (after posting, <=>)");
740 TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
741 s->post();
742 s->assign(a, sol, false, _rand);
743 CHECK_TEST(!s->failed(), "Failed");
744 CHECK_TEST(subsumed(*s), "No subsumption");
745 if (s->r.var().assigned()) {
746 if (sol == MT_TRUE) {
747 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
748 } else if (sol == MT_FALSE) {
749 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
750 }
751 }
752 delete s;
753 }
754 if (imp()) {
755 START_TEST("Assignment reified (after posting, =>)");
756 TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
757 s->post();
758 s->assign(a, sol, false, _rand);
759 CHECK_TEST(!s->failed(), "Failed");
760 CHECK_TEST(subsumed(*s), "No subsumption");
761 if (sol == MT_TRUE) {
762 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
763 } else if (s->r.var().assigned()) {
764 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
765 }
766 delete s;
767 }
768 if (pmi()) {
769 START_TEST("Assignment reified (after posting, <=)");
770 TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
771 s->post();
772 s->assign(a, sol, false, _rand);
773 CHECK_TEST(!s->failed(), "Failed");
774 CHECK_TEST(subsumed(*s), "No subsumption");
775 if (sol == MT_TRUE) {
776 if (s->r.var().assigned()) {
777 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
778 }
779 } else if (sol == MT_FALSE) {
780 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
781 }
782 delete s;
783 }
784 if (eqv()) {
785 START_TEST("Prune reified, <=>");
786 TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
787 s->post();
788 while (!s->failed() && !s->matchAssignment(a) &&
789 (!s->assigned() || !s->r.var().assigned()))
790 if (!s->prune(a, testfix, _rand)) {
791 problem = "No fixpoint";
792 delete s;
793 goto failed;
794 }
795 CHECK_TEST(!s->failed(), "Failed");
796 CHECK_TEST(subsumed(*s), "No subsumption");
797 if (s->r.var().assigned()) {
798 if (sol == MT_TRUE) {
799 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
800 } else if (sol == MT_FALSE) {
801 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
802 }
803 }
804 delete s;
805 }
806 if (imp()) {
807 START_TEST("Prune reified, =>");
808 TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
809 s->post();
810 while (!s->failed() && !s->matchAssignment(a) &&
811 (!s->assigned() || ((sol == MT_FALSE) &&
812 !s->r.var().assigned())))
813 if (!s->prune(a, testfix, _rand)) {
814 problem = "No fixpoint";
815 delete s;
816 goto failed;
817 }
818 CHECK_TEST(!s->failed(), "Failed");
819 CHECK_TEST(subsumed(*s), "No subsumption");
820 if (sol == MT_TRUE) {
821 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
822 } else if ((sol == MT_FALSE) && s->r.var().assigned()) {
823 CHECK_TEST(s->r.var().val()==0, "One on non-solution");
824 }
825 delete s;
826 }
827 if (pmi()) {
828 START_TEST("Prune reified, <=");
829 TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
830 s->post();
831 while (!s->failed() && !s->matchAssignment(a) &&
832 (!s->assigned() || ((sol == MT_TRUE) &&
833 !s->r.var().assigned())))
834 if (!s->prune(a, testfix, _rand)) {
835 problem = "No fixpoint";
836 delete s;
837 goto failed;
838 }
839 CHECK_TEST(!s->failed(), "Failed");
840 CHECK_TEST(subsumed(*s), "No subsumption");
841 if ((sol == MT_TRUE) && s->r.var().assigned()) {
842 CHECK_TEST(s->r.var().val()==1, "Zero on solution");
843 } else if (sol == MT_FALSE) {
844 CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
845 }
846 delete s;
847 }
848 }
849
850 if (testsearch) {
851 if (sol == MT_TRUE) {
852 START_TEST("Search");
853 if (!search_s->failed()) {
854 TestSpace* ss = static_cast<TestSpace*>(search_s->clone());
855 ss->dropUntil(a);
856 delete e_s;
857 e_s = new DFS<TestSpace>(ss,search_o);
858 delete ss;
859 }
860 TestSpace* s = e_s->next();
861 CHECK_TEST(s != nullptr, "Solutions exhausted");
862 CHECK_TEST(subsumed(*s), "No subsumption");
863 for (int i=a.size(); i--; ) {
864 CHECK_TEST(s->x[i].assigned(), "Unassigned variable");
865 CHECK_TEST(Gecode::Float::overlap(a[i], s->x[i].val()), "Wrong value in solution");
866 }
867 delete s;
868 }
869 }
870
871 a.next(_rand);
872 }
873
874 if (testsearch) {
875 test = "Search";
876 if (!search_s->failed()) {
877 TestSpace* ss = static_cast<TestSpace*>(search_s->clone());
878 ss->dropUntil(a);
879 delete e_s;
880 e_s = new DFS<TestSpace>(ss,search_o);
881 delete ss;
882 }
883 if (e_s->next() != nullptr) {
884 problem = "Excess solutions";
885 goto failed;
886 }
887 }
888
889 delete ap;
890 delete search_s;
891 delete e_s;
892 return true;
893
894 failed:
895 if (opt.log)
896 olog << "FAILURE" << std::endl
897 << ind(1) << "Test: " << test << std::endl
898 << ind(1) << "Problem: " << problem << std::endl;
899 if (a.has_more() && opt.log)
900 olog << ind(1) << "Assignment: " << a << std::endl;
901 delete ap;
902 delete search_s;
903 delete e_s;
904
905 return false;
906 }
907
908}}
909
910#undef START_TEST
911#undef CHECK_TEST
912
913// STATISTICS: test-float