Generated on Mon Sep 22 2014 12:49:25 for Gecode by doxygen 1.8.7
float.cpp
Go to the documentation of this file.
1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2 /*
3  * Main authors:
4  * Christian Schulte <schulte@gecode.org>
5  * Mikael Lagerkvist <lagerkvist@gecode.org>
6  * Vincent Barichard <Vincent.Barichard@univ-angers.fr>
7  *
8  * Copyright:
9  * Christian Schulte, 2005
10  * Mikael Lagerkvist, 2005
11  * Vincent Barichard, 2012
12  *
13  * Last modified:
14  * $Date: 2013-03-05 14:40:46 +0100 (Tue, 05 Mar 2013) $ by $Author: schulte $
15  * $Revision: 13435 $
16  *
17  * This file is part of Gecode, the generic constraint
18  * development environment:
19  * http://www.gecode.org
20  *
21  * Permission is hereby granted, free of charge, to any person obtaining
22  * a copy of this software and associated documentation files (the
23  * "Software"), to deal in the Software without restriction, including
24  * without limitation the rights to use, copy, modify, merge, publish,
25  * distribute, sublicense, and/or sell copies of the Software, and to
26  * permit persons to whom the Software is furnished to do so, subject to
27  * the following conditions:
28  *
29  * The above copyright notice and this permission notice shall be
30  * included in all copies or substantial portions of the Software.
31  *
32  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
33  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
34  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
35  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
36  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
37  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
38  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
39  *
40  */
41 
42 #include "test/float.hh"
43 
44 #include <algorithm>
45 
46 namespace Test { namespace Float {
47 
48  /*
49  * Complete assignments
50  *
51  */
52  void
54  using namespace Gecode;
55  int i = n-1;
56  while (true) {
57  FloatNum ns = dsv[i].min() + step;
58  dsv[i] = FloatVal(ns,nextafter(ns,ns+1));
59  if ((dsv[i].max() < d.max()) || (i == 0))
60  return;
61  dsv[i--] = FloatVal(d.min(),nextafter(d.min(),d.max()));
62  }
63  }
64 
65  /*
66  * Extended assignments
67  *
68  */
69  void
71  using namespace Gecode;
72  assert(n > 1);
73  int i = n-2;
74  while (true) {
75  FloatNum ns = dsv[i].min() + step;
76  dsv[i] = FloatVal(ns,nextafter(ns,ns+1));
77  if ((dsv[i].max() < d.max()) || (i == 0)) {
78  if (curPb->extendAssignement(*this)) return;
79  if ((dsv[i].max() >= d.max()) && (i == 0)) return;
80  continue;
81  }
82  dsv[i--] = FloatVal(d.min(),nextafter(d.min(),d.max()));
83  }
84  }
85 
86 
87  /*
88  * Random assignments
89  *
90  */
91  void
93  for (int i = n; i--; )
94  vals[i]=randval();
95  a--;
96  }
97 
98 }}
99 
100 std::ostream&
101 operator<<(std::ostream& os, const Test::Float::Assignment& a) {
102  int n = a.size();
103  os << "{";
104  for (int i=0; i<n; i++)
105  os << "[" << a[i].min() << "," << a[i].max() << "]" << ((i!=n-1) ? "," : "}");
106  return os;
107 }
108 
109 namespace Test { namespace Float {
110 
112  using namespace Gecode;
113  using namespace Gecode::Float;
114  Rounding r;
115  return
116  r.add_down(
117  l,
118  r.mul_down(
119  r.div_down(
120  Base::rand(static_cast<unsigned int>(Int::Limits::max)),
121  static_cast<FloatNum>(Int::Limits::max)
122  ),
123  r.sub_down(u,l)
124  )
125  );
126  }
127 
129  using namespace Gecode;
130  using namespace Gecode::Float;
131  Rounding r;
132  return
133  r.sub_up(
134  u,
135  r.mul_down(
136  r.div_down(
137  Base::rand(static_cast<unsigned int>(Int::Limits::max)),
138  static_cast<FloatNum>(Int::Limits::max)
139  ),
140  r.sub_down(u,l)
141  )
142  );
143  }
144 
145 
147  Test* t)
148  : d(d0), step(s),
149  x(*this,n,Gecode::Float::Limits::min,Gecode::Float::Limits::max),
150  test(t), reified(false) {
151  Gecode::FloatVarArgs _x(*this,n,d.min(),d.max());
152  if (x.size() == 1)
153  Gecode::dom(*this,x[0],_x[0]);
154  else
155  Gecode::dom(*this,x,_x);
156  Gecode::BoolVar b(*this,0,1);
158  if (opt.log)
159  olog << ind(2) << "Initial: x[]=" << x
160  << std::endl;
161  }
162 
164  Test* t, Gecode::ReifyMode rm)
165  : d(d0), step(s), x(*this,n,d.min(),d.max()), test(t), reified(true) {
166  Gecode::BoolVar b(*this,0,1);
167  r = Gecode::Reify(b,rm);
168  if (opt.log)
169  olog << ind(2) << "Initial: x[]=" << x
170  << " b=" << r.var()
171  << std::endl;
172  }
173 
175  : Gecode::Space(share,s), d(s.d), step(s.step), test(s.test), reified(s.reified) {
176  x.update(*this, share, s.x);
178  Gecode::BoolVar sr(s.r.var());
179  b.update(*this, share, sr);
180  r.var(b); r.mode(s.r.mode());
181  }
182 
183  Gecode::Space*
184  TestSpace::copy(bool share) {
185  return new TestSpace(share,*this);
186  }
187 
188  void
190  for (int i = x.size(); i--; )
191  Gecode::rel(*this, x[i], Gecode::FRT_GQ, a[i].min());
192  }
193 
194  bool
195  TestSpace::assigned(void) const {
196  for (int i=x.size(); i--; )
197  if (!x[i].assigned())
198  return false;
199  return true;
200  }
201 
202  bool
204  for (int i=x.size(); i--; )
205  if ((x[i].min() != a[i].min()) || (x[i].max() != a[i].max()))
206  return false;
207  return true;
208  }
209 
210  void
212  if (reified){
213  test->post(*this,x,r);
214  if (opt.log)
215  olog << ind(3) << "Posting reified propagator" << std::endl;
216  } else {
217  test->post(*this,x);
218  if (opt.log)
219  olog << ind(3) << "Posting propagator" << std::endl;
220  }
221  }
222 
223  bool
225  if (opt.log) {
226  olog << ind(3) << "Fixpoint: " << x;
227  bool f=(status() == Gecode::SS_FAILED);
228  olog << std::endl << ind(3) << " --> " << x << std::endl;
229  return f;
230  } else {
231  return status() == Gecode::SS_FAILED;
232  }
233  }
234 
235  void
237  if (opt.log) {
238  olog << ind(4) << "x[" << i << "] ";
239  switch (frt) {
240  case Gecode::FRT_EQ: olog << "="; break;
241  case Gecode::FRT_NQ: olog << "!="; break;
242  case Gecode::FRT_LQ: olog << "<="; break;
243  case Gecode::FRT_LE: olog << "<"; break;
244  case Gecode::FRT_GQ: olog << ">="; break;
245  case Gecode::FRT_GR: olog << ">"; break;
246  }
247  olog << " [" << n.min() << "," << n.max() << "]" << std::endl;
248  }
249  Gecode::rel(*this, x[i], frt, n);
250  }
251 
252  void
253  TestSpace::rel(bool sol) {
254  int n = sol ? 1 : 0;
255  assert(reified);
256  if (opt.log)
257  olog << ind(4) << "b = " << n << std::endl;
258  Gecode::rel(*this, r.var(), Gecode::IRT_EQ, n);
259  }
260 
261  void
262  TestSpace::assign(const Assignment& a, MaybeType& sol, bool skip) {
263  using namespace Gecode;
264  int i = skip ? static_cast<int>(Base::rand(a.size())) : -1;
265 
266  for (int j=a.size(); j--; )
267  if (i != j) {
268  if ((x[j].min() == a[j].max()) || (x[j].max() == a[j].min()))
269  {
270  sol = MT_MAYBE;
271  return;
272  }
273  rel(j, FRT_EQ, a[j]);
274  if (Base::fixpoint() && failed())
275  return;
276  }
277  }
278 
279  void
281  using namespace Gecode;
282  // Select variable to be assigned
283  int i = Base::rand(x.size());
284  while (x[i].assigned()) {
285  i = (i+1) % x.size();
286  }
287  bool min = Base::rand(2);
288  if (min)
289  rel(i, FRT_LQ, nextafter(x[i].min(), x[i].max()));
290  else
291  rel(i, FRT_GQ, nextafter(x[i].max(), x[i].min()));
292  }
293 
295  TestSpace::cut(int* cutDirections) {
296  using namespace Gecode;
297  using namespace Gecode::Float;
298  // Select variable to be cut
299  int i = 0;
300  while (x[i].assigned()) i++;
301  for (int j=x.size(); j--; ) {
302  if (!x[j].assigned() && (x[j].size() > x[i].size())) i = j;
303  }
304  Rounding r;
305  if (cutDirections[i]) {
306  FloatNum m = r.div_up(r.add_up(x[i].min(),x[i].max()),2);
307  FloatNum n = nextafter(x[i].min(), x[i].max());
308  if (m > n)
309  rel(i, FRT_LQ, m);
310  else
311  rel(i, FRT_LQ, n);
312  } else {
313  FloatNum m = r.div_down(r.add_down(x[i].min(),x[i].max()),2);
314  FloatNum n = nextafter(x[i].max(), x[i].min());
315  if (m < n)
316  rel(i, FRT_GQ, m);
317  else
318  rel(i, FRT_GQ, n);
319  }
320  return x[i].size();
321  }
322 
323  void
325  using namespace Gecode;
326  // Prune values
327  if (Base::rand(2) && !x[i].assigned()) {
328  Gecode::FloatNum v=randFValUp(x[i].min(),x[i].max());
329  assert((v >= x[i].min()) && (v <= x[i].max()));
330  rel(i, Gecode::FRT_LQ, v);
331  }
332  if (Base::rand(2) && !x[i].assigned()) {
333  Gecode::FloatNum v=randFValDown(x[i].min(),x[i].max());
334  assert((v <= x[i].max()) && (v >= x[i].min()));
335  rel(i, Gecode::FRT_GQ, v);
336  }
337  }
338 
339  void
341  using namespace Gecode;
342  // Select variable to be pruned
343  int i = Base::rand(x.size());
344  while (x[i].assigned()) {
345  i = (i+1) % x.size();
346  }
347  prune(i);
348  }
349 
350  bool
351  TestSpace::prune(const Assignment& a, bool testfix) {
352  // Select variable to be pruned
353  int i = Base::rand(x.size());
354  while (x[i].assigned())
355  i = (i+1) % x.size();
356  // Select mode for pruning
357  switch (Base::rand(2)) {
358  case 0:
359  if (a[i].max() < x[i].max()) {
360  Gecode::FloatNum v=randFValDown(a[i].max(),x[i].max());
361  assert((v >= a[i].max()) && (v <= x[i].max()));
362  rel(i, Gecode::FRT_LQ, v);
363  }
364  break;
365  case 1:
366  if (a[i].min() > x[i].min()) {
367  Gecode::FloatNum v=randFValUp(x[i].min(),a[i].min());
368  assert((v <= a[i].min()) && (v >= x[i].min()));
369  rel(i, Gecode::FRT_GQ, v);
370  }
371  break;
372  }
373  if (Base::fixpoint()) {
374  if (failed() || !testfix)
375  return true;
376  TestSpace* c = static_cast<TestSpace*>(clone());
377  if (opt.log)
378  olog << ind(3) << "Testing fixpoint on copy" << std::endl;
379  c->post();
380  if (c->failed()) {
381  delete c; return false;
382  }
383  for (int i=x.size(); i--; )
384  if (x[i].size() != c->x[i].size()) {
385  delete c; return false;
386  }
387  if (reified && (r.var().size() != c->r.var().size())) {
388  delete c; return false;
389  }
390  if (opt.log)
391  olog << ind(3) << "Finished testing fixpoint on copy" << std::endl;
392  delete c;
393  }
394  return true;
395  }
396 
397 
398  const Gecode::FloatRelType FloatRelTypes::frts[] =
401 
402  Assignment*
403  Test::assignment(void) const {
404  switch (assigmentType) {
405  case CPLT_ASSIGNMENT:
406  return new CpltAssignment(arity,dom,step);
407  case RANDOM_ASSIGNMENT:
408  return new RandomAssignment(arity,dom,step);
409  case EXTEND_ASSIGNMENT:
410  return new ExtAssignment(arity,dom,step,this);
411  default :
412  GECODE_NEVER;
413  }
414  return NULL; // Avoid compiler warnings
415  }
416 
417  bool
419  GECODE_NEVER;
420  return false;
421  }
422 
423  bool
424  Test::subsumed(const TestSpace& ts) const {
425  if (!testsubsumed) return true;
426  if (ts.propagators()==0) return true;
427  if (assigmentType == EXTEND_ASSIGNMENT) return true;
428  return false;
429  }
430 
432 #define CHECK_TEST(T,M) \
433 if (opt.log) \
434  olog << ind(3) << "Check: " << (M) << std::endl; \
435 if (!(T)) { \
436  problem = (M); delete s; goto failed; \
437 }
438 
440 #define START_TEST(T) \
441  if (opt.log) { \
442  olog.str(""); \
443  olog << ind(2) << "Testing: " << (T) << std::endl; \
444  } \
445  test = (T);
446 
447  bool
448  Test::ignore(const Assignment&) const {
449  return false;
450  }
451 
452  void
454  Gecode::Reify) {}
455 
456  bool
457  Test::run(void) {
458  using namespace Gecode;
459  const char* test = "NONE";
460  const char* problem = "NONE";
461 
462  // Set up assignments
463  Assignment* ap = assignment();
464  Assignment& a = *ap;
465 
466  // Set up space for all solution search
467  TestSpace* search_s = new TestSpace(arity,dom,step,this);
468  post(*search_s,search_s->x);
469  branch(*search_s,search_s->x,FLOAT_VAR_NONE(),FLOAT_VAL_SPLIT_MIN());
470  Search::Options search_o;
471  search_o.threads = 1;
472  DFS<TestSpace> * e_s = new DFS<TestSpace>(search_s,search_o);
473  while (a()) {
474  MaybeType sol = solution(a);
475  if (opt.log) {
476  olog << ind(1) << "Assignment: " << a;
477  switch (sol) {
478  case MT_TRUE: olog << " (solution)"; break;
479  case MT_FALSE: olog << " (no solution)"; break;
480  case MT_MAYBE: olog << " (maybe)"; break;
481  }
482  olog << std::endl;
483  }
484  START_TEST("Assignment (after posting)");
485  {
486  TestSpace* s = new TestSpace(arity,dom,step,this);
487  TestSpace* sc = NULL;
488  s->post();
489  switch (Base::rand(3)) {
490  case 0:
491  if (opt.log)
492  olog << ind(3) << "No copy" << std::endl;
493  sc = s;
494  s = NULL;
495  break;
496  case 1:
497  if (opt.log)
498  olog << ind(3) << "Unshared copy" << std::endl;
499  if (s->status() != SS_FAILED) {
500  sc = static_cast<TestSpace*>(s->clone(false));
501  } else {
502  sc = s; s = NULL;
503  }
504  break;
505  case 2:
506  if (opt.log)
507  olog << ind(3) << "Shared copy" << std::endl;
508  if (s->status() != SS_FAILED) {
509  sc = static_cast<TestSpace*>(s->clone(true));
510  } else {
511  sc = s; s = NULL;
512  }
513  break;
514  default: assert(false);
515  }
516  sc->assign(a,sol);
517  if (sol == MT_TRUE) {
518  CHECK_TEST(!sc->failed(), "Failed on solution");
519  CHECK_TEST(subsumed(*sc), "No subsumption");
520  } else if (sol == MT_FALSE) {
521  CHECK_TEST(sc->failed(), "Solved on non-solution");
522  }
523  delete s; delete sc;
524  }
525  START_TEST("Partial assignment (after posting)");
526  {
527  TestSpace* s = new TestSpace(arity,dom,step,this);
528  s->post();
529  s->assign(a,sol,true);
530  (void) s->failed();
531  s->assign(a,sol);
532  if (sol == MT_TRUE) {
533  CHECK_TEST(!s->failed(), "Failed on solution");
534  CHECK_TEST(subsumed(*s), "No subsumption");
535  } else if (sol == MT_FALSE) {
536  CHECK_TEST(s->failed(), "Solved on non-solution");
537  }
538  delete s;
539  }
540  START_TEST("Assignment (before posting)");
541  {
542  TestSpace* s = new TestSpace(arity,dom,step,this);
543  s->assign(a,sol);
544  s->post();
545  if (sol == MT_TRUE) {
546  CHECK_TEST(!s->failed(), "Failed on solution");
547  CHECK_TEST(subsumed(*s), "No subsumption");
548  } else if (sol == MT_FALSE) {
549  CHECK_TEST(s->failed(), "Solved on non-solution");
550  }
551  delete s;
552  }
553  START_TEST("Partial assignment (before posting)");
554  {
555  TestSpace* s = new TestSpace(arity,dom,step,this);
556  s->assign(a,sol,true);
557  s->post();
558  (void) s->failed();
559  s->assign(a,sol);
560  if (sol == MT_TRUE) {
561  CHECK_TEST(!s->failed(), "Failed on solution");
562  CHECK_TEST(subsumed(*s), "No subsumption");
563  } else if (sol == MT_FALSE) {
564  CHECK_TEST(s->failed(), "Solved on non-solution");
565  }
566  delete s;
567  }
568  START_TEST("Prune");
569  {
570  TestSpace* s = new TestSpace(arity,dom,step,this);
571  s->post();
572  while (!s->failed() && !s->assigned() && !s->matchAssignment(a))
573  if (!s->prune(a,testfix)) {
574  problem = "No fixpoint";
575  delete s;
576  goto failed;
577  }
578  s->assign(a,sol);
579  if (sol == MT_TRUE) {
580  CHECK_TEST(!s->failed(), "Failed on solution");
581  CHECK_TEST(subsumed(*s), "No subsumption");
582  } else if (sol == MT_FALSE) {
583  CHECK_TEST(s->failed(), "Solved on non-solution");
584  }
585  delete s;
586  }
587 
588  if (reified && !ignore(a) && (sol != MT_MAYBE)) {
589  if (eqv()) {
590  START_TEST("Assignment reified (rewrite after post, <=>)");
591  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
592  s->post();
593  s->rel(sol == MT_TRUE);
594  s->assign(a,sol);
595  CHECK_TEST(!s->failed(), "Failed");
596  CHECK_TEST(subsumed(*s), "No subsumption");
597  delete s;
598  }
599  if (imp()) {
600  START_TEST("Assignment reified (rewrite after post, =>)");
601  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
602  s->post();
603  s->rel(sol == MT_TRUE);
604  s->assign(a,sol);
605  CHECK_TEST(!s->failed(), "Failed");
606  CHECK_TEST(subsumed(*s), "No subsumption");
607  delete s;
608  }
609  if (pmi()) {
610  START_TEST("Assignment reified (rewrite after post, <=)");
611  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
612  s->post();
613  s->rel(sol == MT_TRUE);
614  s->assign(a,sol);
615  CHECK_TEST(!s->failed(), "Failed");
616  CHECK_TEST(subsumed(*s), "No subsumption");
617  delete s;
618  }
619  if (eqv()) {
620  START_TEST("Assignment reified (immediate rewrite, <=>)");
621  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
622  s->rel(sol == MT_TRUE);
623  s->post();
624  s->assign(a,sol);
625  CHECK_TEST(!s->failed(), "Failed");
626  CHECK_TEST(subsumed(*s), "No subsumption");
627  delete s;
628  }
629  if (imp()) {
630  START_TEST("Assignment reified (immediate rewrite, =>)");
631  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
632  s->rel(sol == MT_TRUE);
633  s->post();
634  s->assign(a,sol);
635  CHECK_TEST(!s->failed(), "Failed");
636  CHECK_TEST(subsumed(*s), "No subsumption");
637  delete s;
638  }
639  if (pmi()) {
640  START_TEST("Assignment reified (immediate rewrite, <=)");
641  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
642  s->rel(sol == MT_TRUE);
643  s->post();
644  s->assign(a,sol);
645  CHECK_TEST(!s->failed(), "Failed");
646  CHECK_TEST(subsumed(*s), "No subsumption");
647  delete s;
648  }
649  if (eqv()) {
650  START_TEST("Assignment reified (before posting, <=>)");
651  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
652  s->assign(a,sol);
653  s->post();
654  CHECK_TEST(!s->failed(), "Failed");
655  CHECK_TEST(subsumed(*s), "No subsumption");
656  if (s->r.var().assigned()) {
657  if (sol == MT_TRUE) {
658  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
659  } else if (sol == MT_FALSE) {
660  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
661  }
662  }
663  delete s;
664  }
665  if (imp()) {
666  START_TEST("Assignment reified (before posting, =>)");
667  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
668  s->assign(a,sol);
669  s->post();
670  CHECK_TEST(!s->failed(), "Failed");
671  CHECK_TEST(subsumed(*s), "No subsumption");
672  if (sol == MT_TRUE) {
673  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
674  } else if ((sol = MT_FALSE) && s->r.var().assigned()) {
675  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
676  }
677  delete s;
678  }
679  if (pmi()) {
680  START_TEST("Assignment reified (before posting, <=)");
681  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
682  s->assign(a,sol);
683  s->post();
684  CHECK_TEST(!s->failed(), "Failed");
685  CHECK_TEST(subsumed(*s), "No subsumption");
686  if (sol == MT_TRUE) {
687  if (s->r.var().assigned()) {
688  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
689  }
690  } else if (sol == MT_FALSE) {
691  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
692  }
693  delete s;
694  }
695  if (eqv()) {
696  START_TEST("Assignment reified (after posting, <=>)");
697  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
698  s->post();
699  s->assign(a,sol);
700  CHECK_TEST(!s->failed(), "Failed");
701  CHECK_TEST(subsumed(*s), "No subsumption");
702  if (s->r.var().assigned()) {
703  if (sol == MT_TRUE) {
704  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
705  } else if (sol == MT_FALSE) {
706  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
707  }
708  }
709  delete s;
710  }
711  if (imp()) {
712  START_TEST("Assignment reified (after posting, =>)");
713  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
714  s->post();
715  s->assign(a,sol);
716  CHECK_TEST(!s->failed(), "Failed");
717  CHECK_TEST(subsumed(*s), "No subsumption");
718  if (sol == MT_TRUE) {
719  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
720  } else if (s->r.var().assigned()) {
721  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
722  }
723  delete s;
724  }
725  if (pmi()) {
726  START_TEST("Assignment reified (after posting, <=)");
727  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
728  s->post();
729  s->assign(a,sol);
730  CHECK_TEST(!s->failed(), "Failed");
731  CHECK_TEST(subsumed(*s), "No subsumption");
732  if (sol == MT_TRUE) {
733  if (s->r.var().assigned()) {
734  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
735  }
736  } else if (sol == MT_FALSE) {
737  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
738  }
739  delete s;
740  }
741  if (eqv()) {
742  START_TEST("Prune reified, <=>");
743  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
744  s->post();
745  while (!s->failed() && !s->matchAssignment(a) &&
746  (!s->assigned() || !s->r.var().assigned()))
747  if (!s->prune(a,testfix)) {
748  problem = "No fixpoint";
749  delete s;
750  goto failed;
751  }
752  CHECK_TEST(!s->failed(), "Failed");
753  CHECK_TEST(subsumed(*s), "No subsumption");
754  if (s->r.var().assigned()) {
755  if (sol == MT_TRUE) {
756  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
757  } else if (sol == MT_FALSE) {
758  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
759  }
760  }
761  delete s;
762  }
763  if (imp()) {
764  START_TEST("Prune reified, =>");
765  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
766  s->post();
767  while (!s->failed() && !s->matchAssignment(a) &&
768  (!s->assigned() || ((sol == MT_FALSE) &&
769  !s->r.var().assigned())))
770  if (!s->prune(a,testfix)) {
771  problem = "No fixpoint";
772  delete s;
773  goto failed;
774  }
775  CHECK_TEST(!s->failed(), "Failed");
776  CHECK_TEST(subsumed(*s), "No subsumption");
777  if (sol == MT_TRUE) {
778  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
779  } else if ((sol == MT_FALSE) && s->r.var().assigned()) {
780  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
781  }
782  delete s;
783  }
784  if (pmi()) {
785  START_TEST("Prune reified, <=");
786  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
787  s->post();
788  while (!s->failed() && !s->matchAssignment(a) &&
789  (!s->assigned() || ((sol == MT_TRUE) &&
790  !s->r.var().assigned())))
791  if (!s->prune(a,testfix)) {
792  problem = "No fixpoint";
793  delete s;
794  goto failed;
795  }
796  CHECK_TEST(!s->failed(), "Failed");
797  CHECK_TEST(subsumed(*s), "No subsumption");
798  if ((sol == MT_TRUE) && s->r.var().assigned()) {
799  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
800  } else if (sol == MT_FALSE) {
801  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
802  }
803  delete s;
804  }
805  }
806 
807  if (testsearch) {
808  if (sol == MT_TRUE) {
809  START_TEST("Search");
810  if (!search_s->failed()) {
811  TestSpace* ss = static_cast<TestSpace*>(search_s->clone(false));
812  ss->dropUntil(a);
813  delete e_s;
814  e_s = new DFS<TestSpace>(ss,search_o);
815  delete ss;
816  }
817  TestSpace* s = e_s->next();
818  CHECK_TEST(s != NULL, "Solutions exhausted");
819  CHECK_TEST(subsumed(*s), "No subsumption");
820  for (int i=a.size(); i--; ) {
821  CHECK_TEST(s->x[i].assigned(), "Unassigned variable");
822  CHECK_TEST(Gecode::Float::overlap(a[i], s->x[i].val()), "Wrong value in solution");
823  }
824  delete s;
825  }
826  }
827 
828  ++a;
829  }
830 
831  if (testsearch) {
832  test = "Search";
833  if (!search_s->failed()) {
834  TestSpace* ss = static_cast<TestSpace*>(search_s->clone(false));
835  ss->dropUntil(a);
836  delete e_s;
837  e_s = new DFS<TestSpace>(ss,search_o);
838  delete ss;
839  }
840  if (e_s->next() != NULL) {
841  problem = "Excess solutions";
842  goto failed;
843  }
844  }
845 
846  delete ap;
847  delete search_s;
848  delete e_s;
849  return true;
850 
851  failed:
852  if (opt.log)
853  olog << "FAILURE" << std::endl
854  << ind(1) << "Test: " << test << std::endl
855  << ind(1) << "Problem: " << problem << std::endl;
856  if (a() && opt.log)
857  olog << ind(1) << "Assignment: " << a << std::endl;
858  delete ap;
859  delete search_s;
860  delete e_s;
861 
862  return false;
863  }
864 
865 }}
866 
867 #undef START_TEST
868 #undef CHECK_TEST
869 
870 // STATISTICS: test-float
void prune(int i)
Prune some random values from variable i.
Definition: float.cpp:324
bool subsumed(const TestSpace &ts) const
Test if ts is subsumed or not (i.e. if there is no more propagator unless the assignment is an extend...
Definition: float.cpp:424
const Gecode::FloatNum step
Definition: arithmetic.cpp:789
Gecode::FloatNum step
Step for going to next solution.
Definition: float.hh:249
NodeType t
Type of node.
Definition: bool-expr.cpp:234
NNF * l
Left subtree.
Definition: bool-expr.cpp:244
Inverse implication for reification.
Definition: int.hh:845
ReifyMode mode(void) const
Return reification mode.
Definition: reify.hpp:60
Simple class for describing identation.
Definition: test.hh:70
const FloatNum max
Largest allowed float value.
Definition: float.hh:831
#define START_TEST(T)
Start new test.
Definition: float.cpp:440
BoolVar var(void) const
Return Boolean control variable.
Definition: reify.hpp:52
union Gecode::@512::NNF::@54 u
Union depending on nodetype t.
Disequality ( )
Definition: float.hh:1056
void update(Space &home, bool share, VarImpVar< VarImp > &y)
Update this variable to be a clone of variable y.
Definition: var.hpp:128
static Gecode::Support::RandomGenerator rand
Random number generator.
Definition: test.hh:138
Space * clone(bool share=true, CloneStatistics &stat=unused_clone) const
Clone space.
Definition: core.hpp:2777
Gecode::FloatNum step
Step for next assignment.
Definition: float.hh:109
void prune(void)
Prune some random values for some random variable.
Definition: float.cpp:340
Less or equal ( )
Definition: float.hh:1057
Base class for tests with float constraints
Definition: float.hh:242
Passing float variables.
Definition: float.hh:966
bool overlap(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:502
unsigned int size(void) const
Return size (cardinality) of domain.
Definition: bool.hpp:85
void dom(Home home, FloatVar x, FloatVal n)
Propagates .
Definition: dom.cpp:44
Gecode::FloatNum randFValDown(Gecode::FloatNum l, Gecode::FloatNum u)
Definition: float.cpp:111
int n
Number of variables.
Definition: float.hh:86
Less ( )
Definition: float.hh:1058
void post(void)
Post propagator.
Definition: float.cpp:211
void bound(void)
Assing a random variable to a random bound.
Definition: float.cpp:280
Float variable array.
Definition: float.hh:1016
Computation spaces.
Definition: core.hpp:1325
virtual void operator++(void)
Move to next assignment.
Definition: float.cpp:70
FloatVarBranch FLOAT_VAR_NONE(void)
Select first unassigned variable.
Definition: var.hpp:92
int val(void) const
Return assigned value.
Definition: bool.hpp:61
Gecode::IntSet d(v, 7)
Test * test
The test currently run.
Definition: float.hh:181
void update(Space &, bool share, VarArray< Var > &a)
Update array to be a clone of array a.
Definition: array.hpp:1072
Reify imp(BoolVar x)
Use implication for reification.
Definition: reify.hpp:77
Greater or equal ( )
Definition: float.hh:1059
unsigned int propagators(void) const
Return number of propagators.
Definition: core.cpp:195
const FloatNum min
Smallest allowed float value.
Definition: float.hh:833
Gecode::IntArgs i(4, 1, 2, 3, 4)
Gecode::FloatNum randFValUp(Gecode::FloatNum l, Gecode::FloatNum u)
Definition: float.cpp:128
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
Equality ( )
Definition: int.hh:902
Options opt
The options.
Definition: test.cpp:101
Generate all assignments except the last variable and complete it to get a solution.
Definition: float.hh:126
std::ostream & operator<<(std::ostream &os, const Test::Float::Assignment &a)
Definition: float.cpp:101
NNF * r
Right subtree.
Definition: bool-expr.cpp:246
TestSpace(int n, Gecode::FloatVal &d, Gecode::FloatNum s, Test *t)
Create test space.
Definition: float.cpp:146
FloatRelType
Relation types for floats.
Definition: float.hh:1054
static bool fixpoint(void)
Throw a coin whether to compute a fixpoint.
Definition: test.hpp:70
bool assigned(void) const
Test whether all variables are assigned.
Definition: float.cpp:195
virtual void dropUntil(const Assignment &a)
Add constraints to skip solutions to the a assignment.
Definition: float.cpp:189
unsigned int size(I &i)
Size of all ranges of range iterator i.
Reification specification.
Definition: int.hh:852
virtual bool ignore(const Assignment &a) const
Whether to ignore assignment for reification.
Definition: float.cpp:448
virtual void operator++(void)
Move to next assignment.
Definition: float.cpp:53
bool log
Whether to log the tests.
Definition: test.hh:95
virtual void post(Gecode::Space &home, Gecode::FloatVarArray &x)=0
Post constraint.
FloatValBranch FLOAT_VAL_SPLIT_MIN(void)
Select values not greater than mean of smallest and largest value.
Definition: val.hpp:59
Generate random selection of assignments.
Definition: float.hh:148
struct Gecode::@512::NNF::@54::@55 b
For binary nodes (and, or, eqv)
Reify eqv(BoolVar x)
Use equivalence for reification.
Definition: reify.hpp:73
Gecode::Reify r
Reification information.
Definition: float.hh:179
Floating point rounding policy.
Definition: float.hh:137
Equality ( )
Definition: float.hh:1055
Greater ( )
Definition: float.hh:1060
Boolean integer variables.
Definition: int.hh:489
Gecode::FloatVarArray x
Variables to be tested.
Definition: float.hh:177
const int v[7]
Definition: distinct.cpp:206
Gecode::FloatVal d
Initial domain.
Definition: float.hh:173
virtual bool extendAssignement(Assignment &a) const
Complete the current assignment to get a feasible one (which satisfies all constraint). If such an assignment is computed, it returns true, false otherwise.
Definition: float.cpp:418
ExecStatus subsumed(Space &home, Propagator &p, TaskArray< Task > &t)
Check tasks t for subsumption.
Definition: subsumption.hpp:42
Float value type.
Definition: float.hh:321
void assign(const Assignment &a, MaybeType &sol, bool skip=false)
Assign all (or all but one, if skip is true) variables to values in a If assignment of a variable is ...
Definition: float.cpp:262
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:253
void ignore(Actor &a, ActorProperty p, bool duplicate=false)
Ignore actor property.
Definition: core.cpp:168
Gecode::FloatVal d
Domain for each variable.
Definition: float.hh:87
virtual Assignment * assignment(void) const
Create assignment.
Definition: float.cpp:403
MaybeType
Type for comparisons and solutions.
Definition: float.hh:55
std::ostringstream olog
Stream used for logging.
Definition: test.cpp:57
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVal n)
Propagates .
Definition: rel.cpp:47
bool matchAssignment(const Assignment &a) const
Test whether all variables match assignment a.
Definition: float.cpp:203
Space for executing tests.
Definition: float.hh:170
struct Gecode::Space::@49::@51 c
Data available only during copying.
SpaceStatus status(StatusStatistics &stat=unused_status)
Query space status.
Definition: core.cpp:251
int size(void) const
Return number of variables.
Definition: float.hpp:52
bool assigned(void) const
Test whether view is assigned.
Definition: var.hpp:123
virtual bool run(void)
Perform test.
Definition: float.cpp:457
void threads(double n)
Set number of parallel threads.
Definition: options.hpp:252
Implication for reification.
Definition: int.hh:838
bool failed(void)
Compute a fixpoint and check for failure.
Definition: float.cpp:224
bool assigned(void) const
Test if all variables are assigned.
Definition: array.hpp:1085
BrancherHandle branch(Home home, const FloatVarArgs &x, FloatVarBranch vars, FloatValBranch vals, FloatBranchFilter bf, FloatVarValPrint vvp)
Branch over x with variable selection vars and value selection vals.
Definition: branch.cpp:43
virtual void operator++(void)
Move to next assignment.
Definition: float.cpp:92
Gecode::FloatVal * dsv
Iterator for each variable.
Definition: float.hh:108
struct Gecode::@512::NNF::@54::@56 a
For atomic nodes.
bool reified
Does the constraint also exist as reified constraint.
Definition: float.hh:253
Space is failed
Definition: core.hpp:1264
friend FloatVal max(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:390
Generate all assignments.
Definition: float.hh:106
friend FloatVal min(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:402
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:985
#define CHECK_TEST(T, M)
Check the test result and handle failed test.
Definition: float.cpp:432
double FloatNum
Floating point number base type.
Definition: float.hh:108
ReifyMode
Mode for reification.
Definition: int.hh:824
#define GECODE_NEVER
Assert that this command is never executed.
Definition: macros.hpp:60
Gecode::FloatNum cut(int *cutDirections)
Cut the bigger variable to an half sized interval. It returns the new size of the cut interval...
Definition: float.cpp:295
Options for scripts
Definition: driver.hh:326
void rel(int i, Gecode::FloatRelType frt, Gecode::FloatVal n)
Perform integer tell operation on x[i].
Definition: float.cpp:236
Depth-first search engine.
Definition: search.hh:489
Gecode::FloatNum step
Step for going to next solution.
Definition: float.hh:175
bool reified
Whether the test is for a reified propagator.
Definition: float.hh:183
virtual Gecode::Space * copy(bool share)
Copy space during cloning.
Definition: float.cpp:184
Base class for assignments
Definition: float.hh:84
Equivalence for reification (default)
Definition: int.hh:831
Reify pmi(BoolVar x)
Use reverse implication for reification.
Definition: reify.hpp:81