Generated on Thu Apr 5 2018 19:44:19 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  * Last modified:
14  * $Date$ by $Author$
15  * $Revision$
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 #include <iomanip>
46 
47 namespace Test { namespace Float {
48 
49  /*
50  * Complete assignments
51  *
52  */
53  void
55  using namespace Gecode;
56  int i = n-1;
57  while (true) {
58  FloatNum ns = dsv[i].min() + step;
59  dsv[i] = FloatVal(ns,nextafter(ns,ns+1));
60  if ((dsv[i].max() < d.max()) || (i == 0))
61  return;
62  dsv[i--] = FloatVal(d.min(),nextafter(d.min(),d.max()));
63  }
64  }
65 
66  /*
67  * Extended assignments
68  *
69  */
70  void
72  using namespace Gecode;
73  assert(n > 1);
74  int i = n-2;
75  while (true) {
76  FloatNum ns = dsv[i].min() + step;
77  dsv[i] = FloatVal(ns,nextafter(ns,ns+1));
78  if ((dsv[i].max() < d.max()) || (i == 0)) {
79  if (curPb->extendAssignement(*this)) return;
80  if ((dsv[i].max() >= d.max()) && (i == 0)) return;
81  continue;
82  }
83  dsv[i--] = FloatVal(d.min(),nextafter(d.min(),d.max()));
84  }
85  }
86 
87 
88  /*
89  * Random assignments
90  *
91  */
92  void
94  for (int i = n; i--; )
95  vals[i]=randval();
96  a--;
97  }
98 
99 }}
100 
101 std::ostream&
102 operator<<(std::ostream& os, const Test::Float::Assignment& a) {
103  int n = a.size();
104  os << "{";
105  for (int i=0; i<n; i++)
106  os << "[" << a[i].min() << "," << a[i].max() << "]" << ((i!=n-1) ? "," : "}");
107  return os;
108 }
109 
110 namespace Test { namespace Float {
111 
113  using namespace Gecode;
114  using namespace Gecode::Float;
115  Rounding r;
116  return
117  r.add_down(
118  l,
119  r.mul_down(
120  r.div_down(
121  Base::rand(static_cast<unsigned int>(Int::Limits::max)),
122  static_cast<FloatNum>(Int::Limits::max)
123  ),
124  r.sub_down(u,l)
125  )
126  );
127  }
128 
130  using namespace Gecode;
131  using namespace Gecode::Float;
132  Rounding r;
133  return
134  r.sub_up(
135  u,
136  r.mul_down(
137  r.div_down(
138  Base::rand(static_cast<unsigned int>(Int::Limits::max)),
139  static_cast<FloatNum>(Int::Limits::max)
140  ),
141  r.sub_down(u,l)
142  )
143  );
144  }
145 
146 
148  Test* t)
149  : d(d0), step(s),
150  x(*this,n,Gecode::Float::Limits::min,Gecode::Float::Limits::max),
151  test(t), reified(false) {
152  Gecode::FloatVarArgs _x(*this,n,d.min(),d.max());
153  if (x.size() == 1)
154  Gecode::dom(*this,x[0],_x[0]);
155  else
156  Gecode::dom(*this,x,_x);
157  Gecode::BoolVar b(*this,0,1);
159  if (opt.log)
160  olog << ind(2) << "Initial: x[]=" << x
161  << std::endl;
162  }
163 
165  Test* t, Gecode::ReifyMode rm)
166  : d(d0), step(s), x(*this,n,d.min(),d.max()), test(t), reified(true) {
167  Gecode::BoolVar b(*this,0,1);
168  r = Gecode::Reify(b,rm);
169  if (opt.log)
170  olog << ind(2) << "Initial: x[]=" << x
171  << " b=" << r.var()
172  << std::endl;
173  }
174 
176  : Gecode::Space(s), d(s.d), step(s.step), test(s.test), reified(s.reified) {
177  x.update(*this, s.x);
179  Gecode::BoolVar sr(s.r.var());
180  b.update(*this, sr);
181  r.var(b); r.mode(s.r.mode());
182  }
183 
186  return new TestSpace(*this);
187  }
188 
189  void
192  }
193 
194  void
197  (void) status();
198  }
199 
200  void
202  for (int i = x.size(); i--; )
203  Gecode::rel(*this, x[i], Gecode::FRT_GQ, a[i].min());
204  }
205 
206  bool
207  TestSpace::assigned(void) const {
208  for (int i=x.size(); i--; )
209  if (!x[i].assigned())
210  return false;
211  return true;
212  }
213 
214  bool
216  for (int i=x.size(); i--; )
217  if ((x[i].min() < a[i].min()) && (x[i].max() > a[i].max()))
218  return false;
219  return true;
220  }
221 
222  void
224  if (reified){
225  test->post(*this,x,r);
226  if (opt.log)
227  olog << ind(3) << "Posting reified propagator" << std::endl;
228  } else {
229  test->post(*this,x);
230  if (opt.log)
231  olog << ind(3) << "Posting propagator" << std::endl;
232  }
233  }
234 
235  bool
237  if (opt.log) {
238  olog << ind(3) << "Fixpoint: " << x;
239  bool f=(status() == Gecode::SS_FAILED);
240  olog << std::endl << ind(3) << " --> " << x << std::endl;
241  return f;
242  } else {
243  return status() == Gecode::SS_FAILED;
244  }
245  }
246 
247  void
249  if (opt.log) {
250  olog << ind(4) << "x[" << i << "] ";
251  switch (frt) {
252  case Gecode::FRT_EQ: olog << "="; break;
253  case Gecode::FRT_NQ: olog << "!="; break;
254  case Gecode::FRT_LQ: olog << "<="; break;
255  case Gecode::FRT_LE: olog << "<"; break;
256  case Gecode::FRT_GQ: olog << ">="; break;
257  case Gecode::FRT_GR: olog << ">"; break;
258  }
259  olog << " [" << n.min() << "," << n.max() << "]" << std::endl;
260  }
261  Gecode::rel(*this, x[i], frt, n);
262  }
263 
264  void
265  TestSpace::rel(bool sol) {
266  int n = sol ? 1 : 0;
267  assert(reified);
268  if (opt.log)
269  olog << ind(4) << "b = " << n << std::endl;
270  Gecode::rel(*this, r.var(), Gecode::IRT_EQ, n);
271  }
272 
273  void
274  TestSpace::assign(const Assignment& a, MaybeType& sol, bool skip) {
275  using namespace Gecode;
276  int i = skip ? static_cast<int>(Base::rand(a.size())) : -1;
277 
278  for (int j=a.size(); j--; )
279  if (i != j) {
280  if ((x[j].min() == a[j].max()) || (x[j].max() == a[j].min()))
281  {
282  sol = MT_MAYBE;
283  return;
284  }
285  rel(j, FRT_EQ, a[j]);
286  if (Base::fixpoint() && failed())
287  return;
288  }
289  }
290 
291  void
293  using namespace Gecode;
294  // Select variable to be assigned
295  int i = Base::rand(x.size());
296  while (x[i].assigned()) {
297  i = (i+1) % x.size();
298  }
299  bool min = Base::rand(2);
300  if (min)
301  rel(i, FRT_LQ, nextafter(x[i].min(), x[i].max()));
302  else
303  rel(i, FRT_GQ, nextafter(x[i].max(), x[i].min()));
304  }
305 
307  TestSpace::cut(int* cutDirections) {
308  using namespace Gecode;
309  using namespace Gecode::Float;
310  // Select variable to be cut
311  int i = 0;
312  while (x[i].assigned()) i++;
313  for (int j=x.size(); j--; ) {
314  if (!x[j].assigned() && (x[j].size() > x[i].size())) i = j;
315  }
316  Rounding r;
317  if (cutDirections[i]) {
318  FloatNum m = r.div_up(r.add_up(x[i].min(),x[i].max()),2);
319  FloatNum n = nextafter(x[i].min(), x[i].max());
320  if (m > n)
321  rel(i, FRT_LQ, m);
322  else
323  rel(i, FRT_LQ, n);
324  } else {
325  FloatNum m = r.div_down(r.add_down(x[i].min(),x[i].max()),2);
326  FloatNum n = nextafter(x[i].max(), x[i].min());
327  if (m < n)
328  rel(i, FRT_GQ, m);
329  else
330  rel(i, FRT_GQ, n);
331  }
332  return x[i].size();
333  }
334 
335  void
337  using namespace Gecode;
338  // Prune values
339  if (Base::rand(2) && !x[i].assigned()) {
340  Gecode::FloatNum v=randFValUp(x[i].min(),x[i].max());
341  assert((v >= x[i].min()) && (v <= x[i].max()));
342  rel(i, Gecode::FRT_LQ, v);
343  }
344  if (Base::rand(2) && !x[i].assigned()) {
345  Gecode::FloatNum v=randFValDown(x[i].min(),x[i].max());
346  assert((v <= x[i].max()) && (v >= x[i].min()));
347  rel(i, Gecode::FRT_GQ, v);
348  }
349  }
350 
351  void
353  using namespace Gecode;
354  // Select variable to be pruned
355  int i = Base::rand(x.size());
356  while (x[i].assigned()) {
357  i = (i+1) % x.size();
358  }
359  prune(i);
360  }
361 
362  bool
363  TestSpace::prune(const Assignment& a, bool testfix) {
364  // Select variable to be pruned
365  int i = Base::rand(x.size());
366  while (x[i].assigned())
367  i = (i+1) % x.size();
368  // Select mode for pruning
369  switch (Base::rand(2)) {
370  case 0:
371  if (a[i].max() < x[i].max()) {
372  Gecode::FloatNum v=randFValDown(a[i].max(),x[i].max());
373  if (v==x[i].max())
374  v = a[i].max();
375  assert((v >= a[i].max()) && (v <= x[i].max()));
376  rel(i, Gecode::FRT_LQ, v);
377  }
378  break;
379  case 1:
380  if (a[i].min() > x[i].min()) {
381  Gecode::FloatNum v=randFValUp(x[i].min(),a[i].min());
382  if (v==x[i].min())
383  v = a[i].min();
384  assert((v <= a[i].min()) && (v >= x[i].min()));
385  rel(i, Gecode::FRT_GQ, v);
386  }
387  break;
388  }
389  if (Base::fixpoint()) {
390  if (failed() || !testfix)
391  return true;
392  TestSpace* c = static_cast<TestSpace*>(clone());
393  if (opt.log)
394  olog << ind(3) << "Testing fixpoint on copy" << std::endl;
395  c->post();
396  if (c->failed()) {
397  delete c; return false;
398  }
399  for (int i=x.size(); i--; )
400  if (x[i].size() != c->x[i].size()) {
401  delete c; return false;
402  }
403  if (reified && (r.var().size() != c->r.var().size())) {
404  delete c; return false;
405  }
406  if (opt.log)
407  olog << ind(3) << "Finished testing fixpoint on copy" << std::endl;
408  delete c;
409  }
410  return true;
411  }
412 
413  unsigned int
415  return Gecode::PropagatorGroup::all.size(*this);
416  }
417 
418 
419  const Gecode::FloatRelType FloatRelTypes::frts[] =
422 
423  Assignment*
424  Test::assignment(void) const {
425  switch (assigmentType) {
426  case CPLT_ASSIGNMENT:
427  return new CpltAssignment(arity,dom,step);
428  case RANDOM_ASSIGNMENT:
429  return new RandomAssignment(arity,dom,step);
430  case EXTEND_ASSIGNMENT:
431  return new ExtAssignment(arity,dom,step,this);
432  default :
433  GECODE_NEVER;
434  }
435  return NULL; // Avoid compiler warnings
436  }
437 
438  bool
440  GECODE_NEVER;
441  return false;
442  }
443 
444  bool
445  Test::subsumed(const TestSpace& ts) const {
446  if (!testsubsumed) return true;
447  if (const_cast<TestSpace&>(ts).propagators() == 0) return true;
448  if (assigmentType == EXTEND_ASSIGNMENT) return true;
449  return false;
450  }
451 
453 #define CHECK_TEST(T,M) \
454 if (opt.log) \
455  olog << ind(3) << "Check: " << (M) << std::endl; \
456 if (!(T)) { \
457  problem = (M); delete s; goto failed; \
458 }
459 
461 #define START_TEST(T) \
462  if (opt.log) { \
463  olog.str(""); \
464  olog << ind(2) << "Testing: " << (T) << std::endl; \
465  } \
466  test = (T);
467 
468  bool
469  Test::ignore(const Assignment&) const {
470  return false;
471  }
472 
473  void
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()) {
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 = NULL;
509  s->post();
510  switch (Base::rand(2)) {
511  case 0:
512  if (opt.log)
513  olog << ind(3) << "No copy" << std::endl;
514  sc = s;
515  s = NULL;
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 = NULL;
524  }
525  break;
526  default: assert(false);
527  }
528  sc->assign(a,sol);
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);
542  (void) s->failed();
543  s->assign(a,sol);
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);
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);
574  (void) s->failed();
575  s->assign(a,sol);
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);
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);
601  s->post();
602  (void) s->failed();
603  s->assign(a,sol);
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)) {
618  problem = "No fixpoint";
619  delete s;
620  goto failed;
621  }
622  s->assign(a,sol);
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);
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);
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);
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);
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);
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);
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);
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);
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);
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);
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);
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);
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)) {
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)) {
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)) {
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 != NULL, "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;
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() != NULL) {
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() && 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
void prune(int i)
Prune some random values from variable i.
Definition: float.cpp:336
NodeType t
Type of node.
Definition: bool-expr.cpp:234
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:445
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:244
Inverse implication for reification.
Definition: int.hh:848
Simple class for describing identation.
Definition: test.hh:70
unsigned int propagators(void)
Return the number of propagators.
Definition: float.cpp:414
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:973
const FloatNum max
Largest allowed float value.
Definition: float.hh:848
#define START_TEST(T)
Start new test.
Definition: float.cpp:461
ReifyMode mode(void) const
Return reification mode.
Definition: reify.hpp:60
Disequality ( )
Definition: float.hh:1071
void enable(void)
Enable propagators in space.
Definition: float.cpp:190
void update(Space &home, VarArray< Var > &a)
Update array to be a clone of array a.
Definition: array.hpp:1060
static Gecode::Support::RandomGenerator rand
Random number generator.
Definition: test.hh:138
ExecStatus subsumed(Space &home, Propagator &p, int c, TaskArray< Task > &t)
Check for subsumption (all tasks must be assigned)
Definition: subsumption.hpp:42
unsigned int size(void) const
Return size (cardinality) of domain.
Definition: bool.hpp:85
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:352
Less or equal ( )
Definition: float.hh:1072
void disable(Space &home)
Disable all propagators in a group.
Definition: core.cpp:944
static PropagatorGroup all
Group of all propagators.
Definition: core.hpp:779
bool assigned(void) const
Test whether view is assigned.
Definition: var.hpp:123
Passing float variables.
Definition: float.hh:981
bool overlap(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:502
bool assigned(void) const
Test if all variables are assigned.
Definition: array.hpp:1073
virtual T * next(void)
Return next solution (NULL, if none exists or search has been stopped)
Definition: base.hpp:50
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:112
int n
Number of variables.
Definition: float.hh:86
Less ( )
Definition: float.hh:1073
void post(void)
Post propagator.
Definition: float.cpp:223
void bound(void)
Assing a random variable to a random bound.
Definition: float.cpp:292
Float variable array.
Definition: float.hh:1031
Computation spaces.
Definition: core.hpp:1668
virtual void operator++(void)
Move to next assignment.
Definition: float.cpp:71
FloatVarBranch FLOAT_VAR_NONE(void)
Select first unassigned variable.
Definition: var.hpp:101
unsigned int size(Space &home) const
Return number of propagators in a group.
Definition: core.cpp:920
Test * test
The test currently run.
Definition: float.hh:181
Reify imp(BoolVar x)
Use implication for reification.
Definition: reify.hpp:77
Greater or equal ( )
Definition: float.hh:1074
const FloatNum min
Smallest allowed float value.
Definition: float.hh:850
Gecode::IntArgs i(4, 1, 2, 3, 4)
Gecode::FloatNum randFValUp(Gecode::FloatNum l, Gecode::FloatNum u)
Definition: float.cpp:129
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
Equality ( )
Definition: int.hh:905
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:102
virtual bool ignore(const Assignment &a) const
Whether to ignore assignment for reification.
Definition: float.cpp:469
TestSpace(int n, Gecode::FloatVal &d, Gecode::FloatNum s, Test *t)
Create test space.
Definition: float.cpp:147
Space * clone(CloneStatistics &stat=unused_clone) const
Clone space.
Definition: core.hpp:3144
FloatRelType
Relation types for floats.
Definition: float.hh:1069
static bool fixpoint(void)
Throw a coin whether to compute a fixpoint.
Definition: test.hpp:70
void disable(void)
Disable propagators in space and compute fixpoint (make all idle)
Definition: float.cpp:195
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:439
virtual void dropUntil(const Assignment &a)
Add constraints to skip solutions to the a assignment.
Definition: float.cpp:201
unsigned int size(I &i)
Size of all ranges of range iterator i.
Reification specification.
Definition: int.hh:855
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:124
void update(Space &home, VarImpVar< VarImp > &y)
Update this variable to be a clone of variable y.
Definition: var.hpp:128
virtual void operator++(void)
Move to next assignment.
Definition: float.cpp:54
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
union Gecode::@585::NNF::@62 u
Union depending on nodetype t.
Generate random selection of assignments.
Definition: float.hh:148
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:158
Equality ( )
Definition: float.hh:1070
bool assigned(void) const
Test whether all variables are assigned.
Definition: float.cpp:207
Greater ( )
Definition: float.hh:1075
Boolean integer variables.
Definition: int.hh:492
Gecode::FloatVarArray x
Variables to be tested.
Definition: float.hh:177
const int v[7]
Definition: distinct.cpp:263
Gecode::FloatVal d
Initial domain.
Definition: float.hh:173
General test support.
Definition: afc.cpp:43
struct Gecode::@585::NNF::@62::@63 b
For binary nodes (and, or, eqv)
Float value type.
Definition: float.hh:338
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:274
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:253
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:3944
struct Gecode::@585::NNF::@62::@64 a
For atomic nodes.
Gecode::FloatVal d
Domain for each variable.
Definition: float.hh:87
bool matchAssignment(const Assignment &a) const
Test whether all variables match assignment a.
Definition: float.cpp:215
Region r
Definition: region.cpp:69
void enable(Space &home, bool s=true)
Enable all propagators in a group.
Definition: core.cpp:953
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: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
Space for executing tests.
Definition: float.hh:170
BoolVar var(void) const
Return Boolean control variable.
Definition: reify.hpp:52
SpaceStatus status(StatusStatistics &stat=unused_status)
Query space status.
Definition: core.cpp:229
FloatNum sub_up(FloatNum x, FloatNum y)
Return upper bound of x minus y (domain: )
virtual bool run(void)
Perform test.
Definition: float.cpp:478
void threads(double n)
Set number of parallel threads.
Definition: options.hpp:296
int size(void) const
Return number of variables.
Definition: float.hpp:52
FloatNum add_up(FloatNum x, FloatNum y)
Return upper bound of x plus y (domain: )
Gecode toplevel namespace
Implication for reification.
Definition: int.hh:841
bool failed(void)
Compute a fixpoint and check for failure.
Definition: float.cpp:236
virtual void operator++(void)
Move to next assignment.
Definition: float.cpp:93
Gecode::FloatVal * dsv
Iterator for each variable.
Definition: float.hh:108
Space is failed
Definition: core.hpp:1608
friend FloatVal max(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:390
Generate all assignments.
Definition: float.hh:106
Floating point numbers.
Definition: abs.hpp:42
friend FloatVal min(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:402
#define CHECK_TEST(T, M)
Check the test result and handle failed test.
Definition: float.cpp:453
double FloatNum
Floating point number base type.
Definition: float.hh:110
ReifyMode
Mode for reification.
Definition: int.hh:827
#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:307
virtual Assignment * assignment(void) const
Create assignment.
Definition: float.cpp:424
Options for scripts
Definition: driver.hh:370
void rel(int i, Gecode::FloatRelType frt, Gecode::FloatVal n)
Perform integer tell operation on x[i].
Definition: float.cpp:248
Depth-first search engine.
Definition: search.hh:1039
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(void)
Copy space during cloning.
Definition: float.cpp:185
Base class for assignments
Definition: float.hh:84
Equivalence for reification (default)
Definition: int.hh:834
int val(void) const
Return assigned value.
Definition: bool.hpp:61
Reify pmi(BoolVar x)
Use reverse implication for reification.
Definition: reify.hpp:81