Generated on Fri Jan 28 2022 04:43:06 for Gecode by doxygen 1.8.13
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  * 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 
43 namespace Test { namespace Float {
44 
45  /*
46  * Complete assignments
47  *
48  */
49  void
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
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
90  for (int i = n; i--; )
91  vals[i]=randval();
92  a--;
93  }
94 
95 }}
96 
97 std::ostream&
98 operator<<(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 
106 namespace Test { namespace Float {
107 
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  Base::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 
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  Base::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 
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);
155  if (opt.log)
156  olog << ind(2) << "Initial: x[]=" << x
157  << std::endl;
158  }
159 
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 
172  : Gecode::Space(s), d(s.d), step(s.step), test(s.test), reified(s.reified) {
173  x.update(*this, s.x);
175  Gecode::BoolVar sr(s.r.var());
176  b.update(*this, sr);
177  r.var(b); r.mode(s.r.mode());
178  }
179 
182  return new TestSpace(*this);
183  }
184 
185  void
188  }
189 
190  void
193  (void) status();
194  }
195 
196  void
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
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
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
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
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) {
271  using namespace Gecode;
272  int i = skip ? static_cast<int>(Base::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() && failed())
283  return;
284  }
285  }
286 
287  void
289  using namespace Gecode;
290  // Select variable to be assigned
291  int i = Base::rand(x.size());
292  while (x[i].assigned()) {
293  i = (i+1) % x.size();
294  }
295  bool min = Base::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 
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 r;
313  if (cutDirections[i]) {
314  FloatNum m = r.div_up(r.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 = r.div_down(r.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
333  using namespace Gecode;
334  // Prune values
335  if (Base::rand(2) && !x[i].assigned()) {
336  Gecode::FloatNum v=randFValUp(x[i].min(),x[i].max());
337  assert((v >= x[i].min()) && (v <= x[i].max()));
338  rel(i, Gecode::FRT_LQ, v);
339  }
340  if (Base::rand(2) && !x[i].assigned()) {
341  Gecode::FloatNum v=randFValDown(x[i].min(),x[i].max());
342  assert((v <= x[i].max()) && (v >= x[i].min()));
343  rel(i, Gecode::FRT_GQ, v);
344  }
345  }
346 
347  void
349  using namespace Gecode;
350  // Select variable to be pruned
351  int i = Base::rand(x.size());
352  while (x[i].assigned()) {
353  i = (i+1) % x.size();
354  }
355  prune(i);
356  }
357 
358  bool
359  TestSpace::prune(const Assignment& a, bool testfix) {
360  // Select variable to be pruned
361  int i = Base::rand(x.size());
362  while (x[i].assigned())
363  i = (i+1) % x.size();
364  // Select mode for pruning
365  switch (Base::rand(2)) {
366  case 0:
367  if (a[i].max() < x[i].max()) {
368  Gecode::FloatNum v=randFValDown(a[i].max(),x[i].max());
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());
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()) {
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 i=x.size(); i--; )
396  if (x[i].size() != c->x[i].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
411  return Gecode::PropagatorGroup::all.size(*this);
412  }
413 
414 
415  const Gecode::FloatRelType FloatRelTypes::frts[] =
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);
426  case EXTEND_ASSIGNMENT:
427  return new ExtAssignment(arity,dom,step,this);
428  default :
429  GECODE_NEVER;
430  }
431  return NULL; // Avoid compiler warnings
432  }
433 
434  bool
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 
449 #define CHECK_TEST(T,M) \
450 if (opt.log) \
451  olog << ind(3) << "Check: " << (M) << std::endl; \
452 if (!(T)) { \
453  problem = (M); delete s; goto failed; \
454 }
455 
457 #define START_TEST(T) \
458  if (opt.log) { \
459  olog.str(""); \
460  olog << ind(2) << "Testing: " << (T) << std::endl; \
461  } \
462  test = (T);
463 
464  bool
465  Test::ignore(const Assignment&) const {
466  return false;
467  }
468 
469  void
471  Gecode::Reify) {}
472 
473  bool
474  Test::run(void) {
475  using namespace Gecode;
476  const char* test = "NONE";
477  const char* problem = "NONE";
478 
479  // Set up assignments
480  Assignment* ap = assignment();
481  Assignment& a = *ap;
482 
483  // Set up space for all solution search
484  TestSpace* search_s = new TestSpace(arity,dom,step,this);
485  post(*search_s,search_s->x);
486  branch(*search_s,search_s->x,FLOAT_VAR_NONE(),FLOAT_VAL_SPLIT_MIN());
487  Search::Options search_o;
488  search_o.threads = 1;
489  DFS<TestSpace> * e_s = new DFS<TestSpace>(search_s,search_o);
490  while (a()) {
491  MaybeType sol = solution(a);
492  if (opt.log) {
493  olog << ind(1) << "Assignment: " << a;
494  switch (sol) {
495  case MT_TRUE: olog << " (solution)"; break;
496  case MT_FALSE: olog << " (no solution)"; break;
497  case MT_MAYBE: olog << " (maybe)"; break;
498  }
499  olog << std::endl;
500  }
501  START_TEST("Assignment (after posting)");
502  {
503  TestSpace* s = new TestSpace(arity,dom,step,this);
504  TestSpace* sc = NULL;
505  s->post();
506  switch (Base::rand(2)) {
507  case 0:
508  if (opt.log)
509  olog << ind(3) << "No copy" << std::endl;
510  sc = s;
511  s = NULL;
512  break;
513  case 1:
514  if (opt.log)
515  olog << ind(3) << "Copy" << std::endl;
516  if (s->status() != SS_FAILED) {
517  sc = static_cast<TestSpace*>(s->clone());
518  } else {
519  sc = s; s = NULL;
520  }
521  break;
522  default: assert(false);
523  }
524  sc->assign(a,sol);
525  if (sol == MT_TRUE) {
526  CHECK_TEST(!sc->failed(), "Failed on solution");
527  CHECK_TEST(subsumed(*sc), "No subsumption");
528  } else if (sol == MT_FALSE) {
529  CHECK_TEST(sc->failed(), "Solved on non-solution");
530  }
531  delete s; delete sc;
532  }
533  START_TEST("Partial assignment (after posting)");
534  {
535  TestSpace* s = new TestSpace(arity,dom,step,this);
536  s->post();
537  s->assign(a,sol,true);
538  (void) s->failed();
539  s->assign(a,sol);
540  if (sol == MT_TRUE) {
541  CHECK_TEST(!s->failed(), "Failed on solution");
542  CHECK_TEST(subsumed(*s), "No subsumption");
543  } else if (sol == MT_FALSE) {
544  CHECK_TEST(s->failed(), "Solved on non-solution");
545  }
546  delete s;
547  }
548  START_TEST("Assignment (after posting, disable)");
549  {
550  TestSpace* s = new TestSpace(arity,dom,step,this);
551  s->post();
552  s->disable();
553  s->enable();
554  s->assign(a,sol);
555  if (sol == MT_TRUE) {
556  CHECK_TEST(!s->failed(), "Failed on solution");
557  CHECK_TEST(subsumed(*s), "No subsumption");
558  } else if (sol == MT_FALSE) {
559  CHECK_TEST(s->failed(), "Solved on non-solution");
560  }
561  delete s;
562  }
563  START_TEST("Partial assignment (after posting, disable)");
564  {
565  TestSpace* s = new TestSpace(arity,dom,step,this);
566  s->post();
567  s->disable();
568  s->enable();
569  s->assign(a,sol,true);
570  (void) s->failed();
571  s->assign(a,sol);
572  if (sol == MT_TRUE) {
573  CHECK_TEST(!s->failed(), "Failed on solution");
574  CHECK_TEST(subsumed(*s), "No subsumption");
575  } else if (sol == MT_FALSE) {
576  CHECK_TEST(s->failed(), "Solved on non-solution");
577  }
578  delete s;
579  }
580  START_TEST("Assignment (before posting)");
581  {
582  TestSpace* s = new TestSpace(arity,dom,step,this);
583  s->assign(a,sol);
584  s->post();
585  if (sol == MT_TRUE) {
586  CHECK_TEST(!s->failed(), "Failed on solution");
587  CHECK_TEST(subsumed(*s), "No subsumption");
588  } else if (sol == MT_FALSE) {
589  CHECK_TEST(s->failed(), "Solved on non-solution");
590  }
591  delete s;
592  }
593  START_TEST("Partial assignment (before posting)");
594  {
595  TestSpace* s = new TestSpace(arity,dom,step,this);
596  s->assign(a,sol,true);
597  s->post();
598  (void) s->failed();
599  s->assign(a,sol);
600  if (sol == MT_TRUE) {
601  CHECK_TEST(!s->failed(), "Failed on solution");
602  CHECK_TEST(subsumed(*s), "No subsumption");
603  } else if (sol == MT_FALSE) {
604  CHECK_TEST(s->failed(), "Solved on non-solution");
605  }
606  delete s;
607  }
608  START_TEST("Prune");
609  {
610  TestSpace* s = new TestSpace(arity,dom,step,this);
611  s->post();
612  while (!s->failed() && !s->assigned() && !s->matchAssignment(a))
613  if (!s->prune(a,testfix)) {
614  problem = "No fixpoint";
615  delete s;
616  goto failed;
617  }
618  s->assign(a,sol);
619  if (sol == MT_TRUE) {
620  CHECK_TEST(!s->failed(), "Failed on solution");
621  CHECK_TEST(subsumed(*s), "No subsumption");
622  } else if (sol == MT_FALSE) {
623  CHECK_TEST(s->failed(), "Solved on non-solution");
624  }
625  delete s;
626  }
627  if (reified && !ignore(a) && (sol != MT_MAYBE)) {
628  if (eqv()) {
629  START_TEST("Assignment reified (rewrite after post, <=>)");
630  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
631  s->post();
632  s->rel(sol == MT_TRUE);
633  s->assign(a,sol);
634  CHECK_TEST(!s->failed(), "Failed");
635  CHECK_TEST(subsumed(*s), "No subsumption");
636  delete s;
637  }
638  if (imp()) {
639  START_TEST("Assignment reified (rewrite after post, =>)");
640  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
641  s->post();
642  s->rel(sol == MT_TRUE);
643  s->assign(a,sol);
644  CHECK_TEST(!s->failed(), "Failed");
645  CHECK_TEST(subsumed(*s), "No subsumption");
646  delete s;
647  }
648  if (pmi()) {
649  START_TEST("Assignment reified (rewrite after post, <=)");
650  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
651  s->post();
652  s->rel(sol == MT_TRUE);
653  s->assign(a,sol);
654  CHECK_TEST(!s->failed(), "Failed");
655  CHECK_TEST(subsumed(*s), "No subsumption");
656  delete s;
657  }
658  if (eqv()) {
659  START_TEST("Assignment reified (immediate rewrite, <=>)");
660  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
661  s->rel(sol == MT_TRUE);
662  s->post();
663  s->assign(a,sol);
664  CHECK_TEST(!s->failed(), "Failed");
665  CHECK_TEST(subsumed(*s), "No subsumption");
666  delete s;
667  }
668  if (imp()) {
669  START_TEST("Assignment reified (immediate rewrite, =>)");
670  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
671  s->rel(sol == MT_TRUE);
672  s->post();
673  s->assign(a,sol);
674  CHECK_TEST(!s->failed(), "Failed");
675  CHECK_TEST(subsumed(*s), "No subsumption");
676  delete s;
677  }
678  if (pmi()) {
679  START_TEST("Assignment reified (immediate rewrite, <=)");
680  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
681  s->rel(sol == MT_TRUE);
682  s->post();
683  s->assign(a,sol);
684  CHECK_TEST(!s->failed(), "Failed");
685  CHECK_TEST(subsumed(*s), "No subsumption");
686  delete s;
687  }
688  if (eqv()) {
689  START_TEST("Assignment reified (before posting, <=>)");
690  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
691  s->assign(a,sol);
692  s->post();
693  CHECK_TEST(!s->failed(), "Failed");
694  CHECK_TEST(subsumed(*s), "No subsumption");
695  if (s->r.var().assigned()) {
696  if (sol == MT_TRUE) {
697  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
698  } else if (sol == MT_FALSE) {
699  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
700  }
701  }
702  delete s;
703  }
704  if (imp()) {
705  START_TEST("Assignment reified (before posting, =>)");
706  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
707  s->assign(a,sol);
708  s->post();
709  CHECK_TEST(!s->failed(), "Failed");
710  CHECK_TEST(subsumed(*s), "No subsumption");
711  if (sol == MT_TRUE) {
712  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
713  } else if ((sol = MT_FALSE) && s->r.var().assigned()) {
714  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
715  }
716  delete s;
717  }
718  if (pmi()) {
719  START_TEST("Assignment reified (before posting, <=)");
720  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
721  s->assign(a,sol);
722  s->post();
723  CHECK_TEST(!s->failed(), "Failed");
724  CHECK_TEST(subsumed(*s), "No subsumption");
725  if (sol == MT_TRUE) {
726  if (s->r.var().assigned()) {
727  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
728  }
729  } else if (sol == MT_FALSE) {
730  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
731  }
732  delete s;
733  }
734  if (eqv()) {
735  START_TEST("Assignment reified (after posting, <=>)");
736  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
737  s->post();
738  s->assign(a,sol);
739  CHECK_TEST(!s->failed(), "Failed");
740  CHECK_TEST(subsumed(*s), "No subsumption");
741  if (s->r.var().assigned()) {
742  if (sol == MT_TRUE) {
743  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
744  } else if (sol == MT_FALSE) {
745  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
746  }
747  }
748  delete s;
749  }
750  if (imp()) {
751  START_TEST("Assignment reified (after posting, =>)");
752  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
753  s->post();
754  s->assign(a,sol);
755  CHECK_TEST(!s->failed(), "Failed");
756  CHECK_TEST(subsumed(*s), "No subsumption");
757  if (sol == MT_TRUE) {
758  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
759  } else if (s->r.var().assigned()) {
760  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
761  }
762  delete s;
763  }
764  if (pmi()) {
765  START_TEST("Assignment reified (after posting, <=)");
766  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
767  s->post();
768  s->assign(a,sol);
769  CHECK_TEST(!s->failed(), "Failed");
770  CHECK_TEST(subsumed(*s), "No subsumption");
771  if (sol == MT_TRUE) {
772  if (s->r.var().assigned()) {
773  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
774  }
775  } else if (sol == MT_FALSE) {
776  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
777  }
778  delete s;
779  }
780  if (eqv()) {
781  START_TEST("Prune reified, <=>");
782  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
783  s->post();
784  while (!s->failed() && !s->matchAssignment(a) &&
785  (!s->assigned() || !s->r.var().assigned()))
786  if (!s->prune(a,testfix)) {
787  problem = "No fixpoint";
788  delete s;
789  goto failed;
790  }
791  CHECK_TEST(!s->failed(), "Failed");
792  CHECK_TEST(subsumed(*s), "No subsumption");
793  if (s->r.var().assigned()) {
794  if (sol == MT_TRUE) {
795  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
796  } else if (sol == MT_FALSE) {
797  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
798  }
799  }
800  delete s;
801  }
802  if (imp()) {
803  START_TEST("Prune reified, =>");
804  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
805  s->post();
806  while (!s->failed() && !s->matchAssignment(a) &&
807  (!s->assigned() || ((sol == MT_FALSE) &&
808  !s->r.var().assigned())))
809  if (!s->prune(a,testfix)) {
810  problem = "No fixpoint";
811  delete s;
812  goto failed;
813  }
814  CHECK_TEST(!s->failed(), "Failed");
815  CHECK_TEST(subsumed(*s), "No subsumption");
816  if (sol == MT_TRUE) {
817  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
818  } else if ((sol == MT_FALSE) && s->r.var().assigned()) {
819  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
820  }
821  delete s;
822  }
823  if (pmi()) {
824  START_TEST("Prune reified, <=");
825  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
826  s->post();
827  while (!s->failed() && !s->matchAssignment(a) &&
828  (!s->assigned() || ((sol == MT_TRUE) &&
829  !s->r.var().assigned())))
830  if (!s->prune(a,testfix)) {
831  problem = "No fixpoint";
832  delete s;
833  goto failed;
834  }
835  CHECK_TEST(!s->failed(), "Failed");
836  CHECK_TEST(subsumed(*s), "No subsumption");
837  if ((sol == MT_TRUE) && s->r.var().assigned()) {
838  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
839  } else if (sol == MT_FALSE) {
840  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
841  }
842  delete s;
843  }
844  }
845 
846  if (testsearch) {
847  if (sol == MT_TRUE) {
848  START_TEST("Search");
849  if (!search_s->failed()) {
850  TestSpace* ss = static_cast<TestSpace*>(search_s->clone());
851  ss->dropUntil(a);
852  delete e_s;
853  e_s = new DFS<TestSpace>(ss,search_o);
854  delete ss;
855  }
856  TestSpace* s = e_s->next();
857  CHECK_TEST(s != NULL, "Solutions exhausted");
858  CHECK_TEST(subsumed(*s), "No subsumption");
859  for (int i=a.size(); i--; ) {
860  CHECK_TEST(s->x[i].assigned(), "Unassigned variable");
861  CHECK_TEST(Gecode::Float::overlap(a[i], s->x[i].val()), "Wrong value in solution");
862  }
863  delete s;
864  }
865  }
866 
867  ++a;
868  }
869 
870  if (testsearch) {
871  test = "Search";
872  if (!search_s->failed()) {
873  TestSpace* ss = static_cast<TestSpace*>(search_s->clone());
874  ss->dropUntil(a);
875  delete e_s;
876  e_s = new DFS<TestSpace>(ss,search_o);
877  delete ss;
878  }
879  if (e_s->next() != NULL) {
880  problem = "Excess solutions";
881  goto failed;
882  }
883  }
884 
885  delete ap;
886  delete search_s;
887  delete e_s;
888  return true;
889 
890  failed:
891  if (opt.log)
892  olog << "FAILURE" << std::endl
893  << ind(1) << "Test: " << test << std::endl
894  << ind(1) << "Problem: " << problem << std::endl;
895  if (a() && opt.log)
896  olog << ind(1) << "Assignment: " << a << std::endl;
897  delete ap;
898  delete search_s;
899  delete e_s;
900 
901  return false;
902  }
903 
904 }}
905 
906 #undef START_TEST
907 #undef CHECK_TEST
908 
909 // STATISTICS: test-float
void prune(int i)
Prune some random values from variable i.
Definition: float.cpp:332
NodeType t
Type of node.
Definition: bool-expr.cpp:230
FloatNum add_down(FloatNum x, FloatNum y)
Return lower bound of x plus y (domain: )
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:441
FloatNum div_up(FloatNum x, FloatNum y)
Return upper bound of x divided y (domain: )
FloatNum mul_down(FloatNum x, FloatNum y)
Return lower bound of x times y (domain: )
NNF * l
Left subtree.
Definition: bool-expr.cpp:240
Inverse implication for reification.
Definition: int.hh:869
Simple class for describing identation.
Definition: test.hh:66
unsigned int propagators(void)
Return the number of propagators.
Definition: float.cpp:410
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:908
const FloatNum max
Largest allowed float value.
Definition: float.hh:844
#define START_TEST(T)
Start new test.
Definition: float.cpp:457
ReifyMode mode(void) const
Return reification mode.
Definition: reify.hpp:56
Disequality ( )
Definition: float.hh:1070
void enable(void)
Enable propagators in space.
Definition: float.cpp:186
void update(Space &home, VarArray< Var > &a)
Update array to be a clone of array a.
Definition: array.hpp:995
static Gecode::Support::RandomGenerator rand
Random number generator.
Definition: test.hh:134
ExecStatus subsumed(Space &home, Propagator &p, int c, TaskArray< Task > &t)
Check for subsumption (all tasks must be assigned)
Definition: subsumption.hpp:38
unsigned int size(void) const
Return size (cardinality) of domain.
Definition: bool.hpp:81
Gecode::FloatNum step
Step for next assignment.
Definition: float.hh:105
void prune(void)
Prune some random values for some random variable.
Definition: float.cpp:348
Less or equal ( )
Definition: float.hh:1071
void disable(Space &home)
Disable all propagators in a group.
Definition: core.cpp:950
static PropagatorGroup all
Group of all propagators.
Definition: core.hpp:786
bool assigned(void) const
Test whether view is assigned.
Definition: var.hpp:111
Passing float variables.
Definition: float.hh:979
bool overlap(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:498
bool assigned(void) const
Test if all variables are assigned.
Definition: array.hpp:1008
virtual T * next(void)
Return next solution (NULL, if none exists or search has been stopped)
Definition: base.hpp:46
void dom(Home home, FloatVar x, FloatVal n)
Propagates .
Definition: dom.cpp:40
Gecode::FloatNum randFValDown(Gecode::FloatNum l, Gecode::FloatNum u)
Definition: float.cpp:108
int n
Number of variables.
Definition: float.hh:82
Less ( )
Definition: float.hh:1072
void post(void)
Post propagator.
Definition: float.cpp:219
void bound(void)
Assing a random variable to a random bound.
Definition: float.cpp:288
Float variable array.
Definition: float.hh:1030
Computation spaces.
Definition: core.hpp:1701
virtual void operator++(void)
Move to next assignment.
Definition: float.cpp:67
FloatVarBranch FLOAT_VAR_NONE(void)
Select first unassigned variable.
Definition: var.hpp:97
unsigned int size(Space &home) const
Return number of propagators in a group.
Definition: core.cpp:926
Test * test
The test currently run.
Definition: float.hh:177
Reify imp(BoolVar x)
Use implication for reification.
Definition: reify.hpp:73
Greater or equal ( )
Definition: float.hh:1073
const FloatNum min
Smallest allowed float value.
Definition: float.hh:846
Gecode::FloatNum randFValUp(Gecode::FloatNum l, Gecode::FloatNum u)
Definition: float.cpp:125
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:234
Equality ( )
Definition: int.hh:926
Options opt
The options.
Definition: test.cpp:97
Gecode::IntArgs i({1, 2, 3, 4})
Generate all assignments except the last variable and complete it to get a solution.
Definition: float.hh:122
std::ostream & operator<<(std::ostream &os, const Test::Float::Assignment &a)
Definition: float.cpp:98
virtual bool ignore(const Assignment &a) const
Whether to ignore assignment for reification.
Definition: float.cpp:465
TestSpace(int n, Gecode::FloatVal &d, Gecode::FloatNum s, Test *t)
Create test space.
Definition: float.cpp:143
Space * clone(CloneStatistics &stat=unused_clone) const
Clone space.
Definition: core.hpp:3181
FloatRelType
Relation types for floats.
Definition: float.hh:1068
static bool fixpoint(void)
Throw a coin whether to compute a fixpoint.
Definition: test.hpp:66
void disable(void)
Disable propagators in space and compute fixpoint (make all idle)
Definition: float.cpp:191
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:435
struct Gecode::@593::NNF::@62::@63 b
For binary nodes (and, or, eqv)
virtual void dropUntil(const Assignment &a)
Add constraints to skip solutions to the a assignment.
Definition: float.cpp:197
unsigned int size(I &i)
Size of all ranges of range iterator i.
Reification specification.
Definition: int.hh:876
struct Gecode::Space::@58::@60 c
Data available only during copying.
void branch(Home home, const IntVarArgs &x, const BoolVarArgs &y, IntBoolVarBranch vars, IntValBranch vals)
Branch function for integer and Boolean variables.
Definition: branch.cpp:120
void update(Space &home, VarImpVar< VarImp > &y)
Update this variable to be a clone of variable y.
Definition: var.hpp:116
virtual void operator++(void)
Move to next assignment.
Definition: float.cpp:50
bool log
Whether to log the tests.
Definition: test.hh:91
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:55
Generate random selection of assignments.
Definition: float.hh:144
Reify eqv(BoolVar x)
Use equivalence for reification.
Definition: reify.hpp:69
Gecode::Reify r
Reification information.
Definition: float.hh:175
Floating point rounding policy.
Definition: float.hh:154
Equality ( )
Definition: float.hh:1069
bool assigned(void) const
Test whether all variables are assigned.
Definition: float.cpp:203
union Gecode::@593::NNF::@62 u
Union depending on nodetype t.
Greater ( )
Definition: float.hh:1074
Boolean integer variables.
Definition: int.hh:512
Gecode::FloatVarArray x
Variables to be tested.
Definition: float.hh:173
const int v[7]
Definition: distinct.cpp:259
Gecode::FloatVal d
Initial domain.
Definition: float.hh:169
General test support.
Definition: afc.cpp:39
Float value type.
Definition: float.hh:334
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:270
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:249
FloatNum sub_down(FloatNum x, FloatNum y)
Return lower bound of x minus y (domain: )
void ignore(Actor &a, ActorProperty p, bool duplicate=false)
Ignore actor property.
Definition: core.hpp:4001
Gecode::FloatVal d
Domain for each variable.
Definition: float.hh:83
bool matchAssignment(const Assignment &a) const
Test whether all variables match assignment a.
Definition: float.cpp:211
Region r
Definition: region.cpp:65
void enable(Space &home, bool s=true)
Enable all propagators in a group.
Definition: core.cpp:959
FloatNum div_down(FloatNum x, FloatNum y)
Return lower bound of x divided by y (domain: )
MaybeType
Type for comparisons and solutions.
Definition: float.hh:51
std::ostringstream olog
Stream used for logging.
Definition: test.cpp:53
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVal n)
Propagates .
Definition: rel.cpp:43
Space for executing tests.
Definition: float.hh:166
BoolVar var(void) const
Return Boolean control variable.
Definition: reify.hpp:48
SpaceStatus status(StatusStatistics &stat=unused_status)
Query space status.
Definition: core.cpp:232
FloatNum sub_up(FloatNum x, FloatNum y)
Return upper bound of x minus y (domain: )
virtual bool run(void)
Perform test.
Definition: float.cpp:474
void threads(double n)
Set number of parallel threads.
Definition: options.hpp:292
int size(void) const
Return number of variables.
Definition: float.hpp:48
FloatNum add_up(FloatNum x, FloatNum y)
Return upper bound of x plus y (domain: )
Gecode toplevel namespace
Implication for reification.
Definition: int.hh:862
bool failed(void)
Compute a fixpoint and check for failure.
Definition: float.cpp:232
virtual void operator++(void)
Move to next assignment.
Definition: float.cpp:89
Gecode::FloatVal * dsv
Iterator for each variable.
Definition: float.hh:104
Space is failed
Definition: core.hpp:1641
friend FloatVal max(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:386
Generate all assignments.
Definition: float.hh:102
Floating point numbers.
Definition: abs.hpp:38
friend FloatVal min(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:398
#define CHECK_TEST(T, M)
Check the test result and handle failed test.
Definition: float.cpp:449
double FloatNum
Floating point number base type.
Definition: float.hh:106
ReifyMode
Mode for reification.
Definition: int.hh:848
#define GECODE_NEVER
Assert that this command is never executed.
Definition: macros.hpp:56
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:303
virtual Assignment * assignment(void) const
Create assignment.
Definition: float.cpp:420
Options for scripts
Definition: driver.hh:366
void rel(int i, Gecode::FloatRelType frt, Gecode::FloatVal n)
Perform integer tell operation on x[i].
Definition: float.cpp:244
struct Gecode::@593::NNF::@62::@64 a
For atomic nodes.
Depth-first search engine.
Definition: search.hh:1036
Gecode::FloatNum step
Step for going to next solution.
Definition: float.hh:171
bool reified
Whether the test is for a reified propagator.
Definition: float.hh:179
virtual Gecode::Space * copy(void)
Copy space during cloning.
Definition: float.cpp:181
Base class for assignments
Definition: float.hh:80
Equivalence for reification (default)
Definition: int.hh:855
int val(void) const
Return assigned value.
Definition: bool.hpp:57
Reify pmi(BoolVar x)
Use reverse implication for reification.
Definition: reify.hpp:77