Generated on Tue Jul 18 2017 18:41:42 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: 2016-10-20 17:25:30 +0200 (Thu, 20 Oct 2016) $ by $Author: schulte $
15  * $Revision: 15217 $
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(share,s), d(s.d), step(s.step), test(s.test), reified(s.reified) {
177  x.update(*this, share, s.x);
179  Gecode::BoolVar sr(s.r.var());
180  b.update(*this, share, sr);
181  r.var(b); r.mode(s.r.mode());
182  }
183 
185  TestSpace::copy(bool share) {
186  return new TestSpace(share,*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(3)) {
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) << "Unshared copy" << std::endl;
520  if (s->status() != SS_FAILED) {
521  sc = static_cast<TestSpace*>(s->clone(false));
522  } else {
523  sc = s; s = NULL;
524  }
525  break;
526  case 2:
527  if (opt.log)
528  olog << ind(3) << "Shared copy" << std::endl;
529  if (s->status() != SS_FAILED) {
530  sc = static_cast<TestSpace*>(s->clone(true));
531  } else {
532  sc = s; s = NULL;
533  }
534  break;
535  default: assert(false);
536  }
537  sc->assign(a,sol);
538  if (sol == MT_TRUE) {
539  CHECK_TEST(!sc->failed(), "Failed on solution");
540  CHECK_TEST(subsumed(*sc), "No subsumption");
541  } else if (sol == MT_FALSE) {
542  CHECK_TEST(sc->failed(), "Solved on non-solution");
543  }
544  delete s; delete sc;
545  }
546  START_TEST("Partial assignment (after posting)");
547  {
548  TestSpace* s = new TestSpace(arity,dom,step,this);
549  s->post();
550  s->assign(a,sol,true);
551  (void) s->failed();
552  s->assign(a,sol);
553  if (sol == MT_TRUE) {
554  CHECK_TEST(!s->failed(), "Failed on solution");
555  CHECK_TEST(subsumed(*s), "No subsumption");
556  } else if (sol == MT_FALSE) {
557  CHECK_TEST(s->failed(), "Solved on non-solution");
558  }
559  delete s;
560  }
561  START_TEST("Assignment (after posting, disable)");
562  {
563  TestSpace* s = new TestSpace(arity,dom,step,this);
564  s->post();
565  s->disable();
566  s->enable();
567  s->assign(a,sol);
568  if (sol == MT_TRUE) {
569  CHECK_TEST(!s->failed(), "Failed on solution");
570  CHECK_TEST(subsumed(*s), "No subsumption");
571  } else if (sol == MT_FALSE) {
572  CHECK_TEST(s->failed(), "Solved on non-solution");
573  }
574  delete s;
575  }
576  START_TEST("Partial assignment (after posting, disable)");
577  {
578  TestSpace* s = new TestSpace(arity,dom,step,this);
579  s->post();
580  s->disable();
581  s->enable();
582  s->assign(a,sol,true);
583  (void) s->failed();
584  s->assign(a,sol);
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("Assignment (before posting)");
594  {
595  TestSpace* s = new TestSpace(arity,dom,step,this);
596  s->assign(a,sol);
597  s->post();
598  if (sol == MT_TRUE) {
599  CHECK_TEST(!s->failed(), "Failed on solution");
600  CHECK_TEST(subsumed(*s), "No subsumption");
601  } else if (sol == MT_FALSE) {
602  CHECK_TEST(s->failed(), "Solved on non-solution");
603  }
604  delete s;
605  }
606  START_TEST("Partial assignment (before posting)");
607  {
608  TestSpace* s = new TestSpace(arity,dom,step,this);
609  s->assign(a,sol,true);
610  s->post();
611  (void) s->failed();
612  s->assign(a,sol);
613  if (sol == MT_TRUE) {
614  CHECK_TEST(!s->failed(), "Failed on solution");
615  CHECK_TEST(subsumed(*s), "No subsumption");
616  } else if (sol == MT_FALSE) {
617  CHECK_TEST(s->failed(), "Solved on non-solution");
618  }
619  delete s;
620  }
621  START_TEST("Prune");
622  {
623  TestSpace* s = new TestSpace(arity,dom,step,this);
624  s->post();
625  while (!s->failed() && !s->assigned() && !s->matchAssignment(a))
626  if (!s->prune(a,testfix)) {
627  problem = "No fixpoint";
628  delete s;
629  goto failed;
630  }
631  s->assign(a,sol);
632  if (sol == MT_TRUE) {
633  CHECK_TEST(!s->failed(), "Failed on solution");
634  CHECK_TEST(subsumed(*s), "No subsumption");
635  } else if (sol == MT_FALSE) {
636  CHECK_TEST(s->failed(), "Solved on non-solution");
637  }
638  delete s;
639  }
640  if (reified && !ignore(a) && (sol != MT_MAYBE)) {
641  if (eqv()) {
642  START_TEST("Assignment reified (rewrite after post, <=>)");
643  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
644  s->post();
645  s->rel(sol == MT_TRUE);
646  s->assign(a,sol);
647  CHECK_TEST(!s->failed(), "Failed");
648  CHECK_TEST(subsumed(*s), "No subsumption");
649  delete s;
650  }
651  if (imp()) {
652  START_TEST("Assignment reified (rewrite after post, =>)");
653  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
654  s->post();
655  s->rel(sol == MT_TRUE);
656  s->assign(a,sol);
657  CHECK_TEST(!s->failed(), "Failed");
658  CHECK_TEST(subsumed(*s), "No subsumption");
659  delete s;
660  }
661  if (pmi()) {
662  START_TEST("Assignment reified (rewrite after post, <=)");
663  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
664  s->post();
665  s->rel(sol == MT_TRUE);
666  s->assign(a,sol);
667  CHECK_TEST(!s->failed(), "Failed");
668  CHECK_TEST(subsumed(*s), "No subsumption");
669  delete s;
670  }
671  if (eqv()) {
672  START_TEST("Assignment reified (immediate rewrite, <=>)");
673  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
674  s->rel(sol == MT_TRUE);
675  s->post();
676  s->assign(a,sol);
677  CHECK_TEST(!s->failed(), "Failed");
678  CHECK_TEST(subsumed(*s), "No subsumption");
679  delete s;
680  }
681  if (imp()) {
682  START_TEST("Assignment reified (immediate rewrite, =>)");
683  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
684  s->rel(sol == MT_TRUE);
685  s->post();
686  s->assign(a,sol);
687  CHECK_TEST(!s->failed(), "Failed");
688  CHECK_TEST(subsumed(*s), "No subsumption");
689  delete s;
690  }
691  if (pmi()) {
692  START_TEST("Assignment reified (immediate rewrite, <=)");
693  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
694  s->rel(sol == MT_TRUE);
695  s->post();
696  s->assign(a,sol);
697  CHECK_TEST(!s->failed(), "Failed");
698  CHECK_TEST(subsumed(*s), "No subsumption");
699  delete s;
700  }
701  if (eqv()) {
702  START_TEST("Assignment reified (before posting, <=>)");
703  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
704  s->assign(a,sol);
705  s->post();
706  CHECK_TEST(!s->failed(), "Failed");
707  CHECK_TEST(subsumed(*s), "No subsumption");
708  if (s->r.var().assigned()) {
709  if (sol == MT_TRUE) {
710  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
711  } else if (sol == MT_FALSE) {
712  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
713  }
714  }
715  delete s;
716  }
717  if (imp()) {
718  START_TEST("Assignment reified (before posting, =>)");
719  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
720  s->assign(a,sol);
721  s->post();
722  CHECK_TEST(!s->failed(), "Failed");
723  CHECK_TEST(subsumed(*s), "No subsumption");
724  if (sol == MT_TRUE) {
725  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
726  } else if ((sol = MT_FALSE) && s->r.var().assigned()) {
727  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
728  }
729  delete s;
730  }
731  if (pmi()) {
732  START_TEST("Assignment reified (before posting, <=)");
733  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
734  s->assign(a,sol);
735  s->post();
736  CHECK_TEST(!s->failed(), "Failed");
737  CHECK_TEST(subsumed(*s), "No subsumption");
738  if (sol == MT_TRUE) {
739  if (s->r.var().assigned()) {
740  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
741  }
742  } else if (sol == MT_FALSE) {
743  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
744  }
745  delete s;
746  }
747  if (eqv()) {
748  START_TEST("Assignment reified (after posting, <=>)");
749  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
750  s->post();
751  s->assign(a,sol);
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("Assignment reified (after posting, =>)");
765  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
766  s->post();
767  s->assign(a,sol);
768  CHECK_TEST(!s->failed(), "Failed");
769  CHECK_TEST(subsumed(*s), "No subsumption");
770  if (sol == MT_TRUE) {
771  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
772  } else if (s->r.var().assigned()) {
773  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
774  }
775  delete s;
776  }
777  if (pmi()) {
778  START_TEST("Assignment reified (after posting, <=)");
779  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
780  s->post();
781  s->assign(a,sol);
782  CHECK_TEST(!s->failed(), "Failed");
783  CHECK_TEST(subsumed(*s), "No subsumption");
784  if (sol == MT_TRUE) {
785  if (s->r.var().assigned()) {
786  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
787  }
788  } else if (sol == MT_FALSE) {
789  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
790  }
791  delete s;
792  }
793  if (eqv()) {
794  START_TEST("Prune reified, <=>");
795  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
796  s->post();
797  while (!s->failed() && !s->matchAssignment(a) &&
798  (!s->assigned() || !s->r.var().assigned()))
799  if (!s->prune(a,testfix)) {
800  problem = "No fixpoint";
801  delete s;
802  goto failed;
803  }
804  CHECK_TEST(!s->failed(), "Failed");
805  CHECK_TEST(subsumed(*s), "No subsumption");
806  if (s->r.var().assigned()) {
807  if (sol == MT_TRUE) {
808  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
809  } else if (sol == MT_FALSE) {
810  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
811  }
812  }
813  delete s;
814  }
815  if (imp()) {
816  START_TEST("Prune reified, =>");
817  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
818  s->post();
819  while (!s->failed() && !s->matchAssignment(a) &&
820  (!s->assigned() || ((sol == MT_FALSE) &&
821  !s->r.var().assigned())))
822  if (!s->prune(a,testfix)) {
823  problem = "No fixpoint";
824  delete s;
825  goto failed;
826  }
827  CHECK_TEST(!s->failed(), "Failed");
828  CHECK_TEST(subsumed(*s), "No subsumption");
829  if (sol == MT_TRUE) {
830  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
831  } else if ((sol == MT_FALSE) && s->r.var().assigned()) {
832  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
833  }
834  delete s;
835  }
836  if (pmi()) {
837  START_TEST("Prune reified, <=");
838  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
839  s->post();
840  while (!s->failed() && !s->matchAssignment(a) &&
841  (!s->assigned() || ((sol == MT_TRUE) &&
842  !s->r.var().assigned())))
843  if (!s->prune(a,testfix)) {
844  problem = "No fixpoint";
845  delete s;
846  goto failed;
847  }
848  CHECK_TEST(!s->failed(), "Failed");
849  CHECK_TEST(subsumed(*s), "No subsumption");
850  if ((sol == MT_TRUE) && s->r.var().assigned()) {
851  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
852  } else if (sol == MT_FALSE) {
853  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
854  }
855  delete s;
856  }
857  }
858 
859  if (testsearch) {
860  if (sol == MT_TRUE) {
861  START_TEST("Search");
862  if (!search_s->failed()) {
863  TestSpace* ss = static_cast<TestSpace*>(search_s->clone(false));
864  ss->dropUntil(a);
865  delete e_s;
866  e_s = new DFS<TestSpace>(ss,search_o);
867  delete ss;
868  }
869  TestSpace* s = e_s->next();
870  CHECK_TEST(s != NULL, "Solutions exhausted");
871  CHECK_TEST(subsumed(*s), "No subsumption");
872  for (int i=a.size(); i--; ) {
873  CHECK_TEST(s->x[i].assigned(), "Unassigned variable");
874  CHECK_TEST(Gecode::Float::overlap(a[i], s->x[i].val()), "Wrong value in solution");
875  }
876  delete s;
877  }
878  }
879 
880  ++a;
881  }
882 
883  if (testsearch) {
884  test = "Search";
885  if (!search_s->failed()) {
886  TestSpace* ss = static_cast<TestSpace*>(search_s->clone(false));
887  ss->dropUntil(a);
888  delete e_s;
889  e_s = new DFS<TestSpace>(ss,search_o);
890  delete ss;
891  }
892  if (e_s->next() != NULL) {
893  problem = "Excess solutions";
894  goto failed;
895  }
896  }
897 
898  delete ap;
899  delete search_s;
900  delete e_s;
901  return true;
902 
903  failed:
904  if (opt.log)
905  olog << "FAILURE" << std::endl
906  << ind(1) << "Test: " << test << std::endl
907  << ind(1) << "Problem: " << problem << std::endl;
908  if (a() && opt.log)
909  olog << ind(1) << "Assignment: " << a << std::endl;
910  delete ap;
911  delete search_s;
912  delete e_s;
913 
914  return false;
915  }
916 
917 }}
918 
919 #undef START_TEST
920 #undef CHECK_TEST
921 
922 // 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:850
Simple class for describing identation.
Definition: test.hh:70
union Gecode::@579::NNF::@61 u
Union depending on nodetype t.
unsigned int propagators(void)
Return the number of propagators.
Definition: float.cpp:414
void 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
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:985
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, 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
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:941
static PropagatorGroup all
Group of all propagators.
Definition: core.hpp:855
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:1085
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
Space * clone(bool share_data=true, bool share_info=true, CloneStatistics &stat=unused_clone) const
Clone space.
Definition: core.hpp:3326
Float variable array.
Definition: float.hh:1031
Computation spaces.
Definition: core.hpp:1748
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:917
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
struct Gecode::@579::NNF::@61::@63 a
For atomic nodes.
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:907
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
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:857
struct Gecode::@579::NNF::@61::@62 b
For binary nodes (and, or, eqv)
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
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:494
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
Post propagator for f(x \diamond_{\mathit{op}} y) \sim_r z \f$ void rel(Home home
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:4141
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:82
void enable(Space &home, bool s=true)
Enable all propagators in a group.
Definition: core.cpp:950
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
struct Gecode::Space::@56::@58 c
Data available only during copying.
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:224
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:843
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:1689
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:829
#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:366
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:739
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:185
Base class for assignments
Definition: float.hh:84
Equivalence for reification (default)
Definition: int.hh:836
int val(void) const
Return assigned value.
Definition: bool.hpp:61
Reify pmi(BoolVar x)
Use reverse implication for reification.
Definition: reify.hpp:81