Generated on Sat Feb 7 2015 02:01:17 for Gecode by doxygen 1.8.9.1
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: 2015-01-16 06:05:16 +0100 (Fri, 16 Jan 2015) $ by $Author: tack $
15  * $Revision: 14357 $
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 
184  Gecode::Space*
185  TestSpace::copy(bool share) {
186  return new TestSpace(share,*this);
187  }
188 
189  void
191  for (int i = x.size(); i--; )
192  Gecode::rel(*this, x[i], Gecode::FRT_GQ, a[i].min());
193  }
194 
195  bool
196  TestSpace::assigned(void) const {
197  for (int i=x.size(); i--; )
198  if (!x[i].assigned())
199  return false;
200  return true;
201  }
202 
203  bool
205  for (int i=x.size(); i--; )
206  if ((x[i].min() < a[i].min()) && (x[i].max() > a[i].max()))
207  return false;
208  return true;
209  }
210 
211  void
213  if (reified){
214  test->post(*this,x,r);
215  if (opt.log)
216  olog << ind(3) << "Posting reified propagator" << std::endl;
217  } else {
218  test->post(*this,x);
219  if (opt.log)
220  olog << ind(3) << "Posting propagator" << std::endl;
221  }
222  }
223 
224  bool
226  if (opt.log) {
227  olog << ind(3) << "Fixpoint: " << x;
228  bool f=(status() == Gecode::SS_FAILED);
229  olog << std::endl << ind(3) << " --> " << x << std::endl;
230  return f;
231  } else {
232  return status() == Gecode::SS_FAILED;
233  }
234  }
235 
236  void
238  if (opt.log) {
239  olog << ind(4) << "x[" << i << "] ";
240  switch (frt) {
241  case Gecode::FRT_EQ: olog << "="; break;
242  case Gecode::FRT_NQ: olog << "!="; break;
243  case Gecode::FRT_LQ: olog << "<="; break;
244  case Gecode::FRT_LE: olog << "<"; break;
245  case Gecode::FRT_GQ: olog << ">="; break;
246  case Gecode::FRT_GR: olog << ">"; break;
247  }
248  olog << " [" << n.min() << "," << n.max() << "]" << std::endl;
249  }
250  Gecode::rel(*this, x[i], frt, n);
251  }
252 
253  void
254  TestSpace::rel(bool sol) {
255  int n = sol ? 1 : 0;
256  assert(reified);
257  if (opt.log)
258  olog << ind(4) << "b = " << n << std::endl;
259  Gecode::rel(*this, r.var(), Gecode::IRT_EQ, n);
260  }
261 
262  void
263  TestSpace::assign(const Assignment& a, MaybeType& sol, bool skip) {
264  using namespace Gecode;
265  int i = skip ? static_cast<int>(Base::rand(a.size())) : -1;
266 
267  for (int j=a.size(); j--; )
268  if (i != j) {
269  if ((x[j].min() == a[j].max()) || (x[j].max() == a[j].min()))
270  {
271  sol = MT_MAYBE;
272  return;
273  }
274  rel(j, FRT_EQ, a[j]);
275  if (Base::fixpoint() && failed())
276  return;
277  }
278  }
279 
280  void
282  using namespace Gecode;
283  // Select variable to be assigned
284  int i = Base::rand(x.size());
285  while (x[i].assigned()) {
286  i = (i+1) % x.size();
287  }
288  bool min = Base::rand(2);
289  if (min)
290  rel(i, FRT_LQ, nextafter(x[i].min(), x[i].max()));
291  else
292  rel(i, FRT_GQ, nextafter(x[i].max(), x[i].min()));
293  }
294 
296  TestSpace::cut(int* cutDirections) {
297  using namespace Gecode;
298  using namespace Gecode::Float;
299  // Select variable to be cut
300  int i = 0;
301  while (x[i].assigned()) i++;
302  for (int j=x.size(); j--; ) {
303  if (!x[j].assigned() && (x[j].size() > x[i].size())) i = j;
304  }
305  Rounding r;
306  if (cutDirections[i]) {
307  FloatNum m = r.div_up(r.add_up(x[i].min(),x[i].max()),2);
308  FloatNum n = nextafter(x[i].min(), x[i].max());
309  if (m > n)
310  rel(i, FRT_LQ, m);
311  else
312  rel(i, FRT_LQ, n);
313  } else {
314  FloatNum m = r.div_down(r.add_down(x[i].min(),x[i].max()),2);
315  FloatNum n = nextafter(x[i].max(), x[i].min());
316  if (m < n)
317  rel(i, FRT_GQ, m);
318  else
319  rel(i, FRT_GQ, n);
320  }
321  return x[i].size();
322  }
323 
324  void
326  using namespace Gecode;
327  // Prune values
328  if (Base::rand(2) && !x[i].assigned()) {
329  Gecode::FloatNum v=randFValUp(x[i].min(),x[i].max());
330  assert((v >= x[i].min()) && (v <= x[i].max()));
331  rel(i, Gecode::FRT_LQ, v);
332  }
333  if (Base::rand(2) && !x[i].assigned()) {
334  Gecode::FloatNum v=randFValDown(x[i].min(),x[i].max());
335  assert((v <= x[i].max()) && (v >= x[i].min()));
336  rel(i, Gecode::FRT_GQ, v);
337  }
338  }
339 
340  void
342  using namespace Gecode;
343  // Select variable to be pruned
344  int i = Base::rand(x.size());
345  while (x[i].assigned()) {
346  i = (i+1) % x.size();
347  }
348  prune(i);
349  }
350 
351  bool
352  TestSpace::prune(const Assignment& a, bool testfix) {
353  // Select variable to be pruned
354  int i = Base::rand(x.size());
355  while (x[i].assigned())
356  i = (i+1) % x.size();
357  // Select mode for pruning
358  switch (Base::rand(2)) {
359  case 0:
360  if (a[i].max() < x[i].max()) {
361  Gecode::FloatNum v=randFValDown(a[i].max(),x[i].max());
362  if (v==x[i].max())
363  v = a[i].max();
364  assert((v >= a[i].max()) && (v <= x[i].max()));
365  rel(i, Gecode::FRT_LQ, v);
366  }
367  break;
368  case 1:
369  if (a[i].min() > x[i].min()) {
370  Gecode::FloatNum v=randFValUp(x[i].min(),a[i].min());
371  if (v==x[i].min())
372  v = a[i].min();
373  assert((v <= a[i].min()) && (v >= x[i].min()));
374  rel(i, Gecode::FRT_GQ, v);
375  }
376  break;
377  }
378  if (Base::fixpoint()) {
379  if (failed() || !testfix)
380  return true;
381  TestSpace* c = static_cast<TestSpace*>(clone());
382  if (opt.log)
383  olog << ind(3) << "Testing fixpoint on copy" << std::endl;
384  c->post();
385  if (c->failed()) {
386  delete c; return false;
387  }
388  for (int i=x.size(); i--; )
389  if (x[i].size() != c->x[i].size()) {
390  delete c; return false;
391  }
392  if (reified && (r.var().size() != c->r.var().size())) {
393  delete c; return false;
394  }
395  if (opt.log)
396  olog << ind(3) << "Finished testing fixpoint on copy" << std::endl;
397  delete c;
398  }
399  return true;
400  }
401 
402 
403  const Gecode::FloatRelType FloatRelTypes::frts[] =
406 
407  Assignment*
408  Test::assignment(void) const {
409  switch (assigmentType) {
410  case CPLT_ASSIGNMENT:
411  return new CpltAssignment(arity,dom,step);
412  case RANDOM_ASSIGNMENT:
413  return new RandomAssignment(arity,dom,step);
414  case EXTEND_ASSIGNMENT:
415  return new ExtAssignment(arity,dom,step,this);
416  default :
417  GECODE_NEVER;
418  }
419  return NULL; // Avoid compiler warnings
420  }
421 
422  bool
424  GECODE_NEVER;
425  return false;
426  }
427 
428  bool
429  Test::subsumed(const TestSpace& ts) const {
430  if (!testsubsumed) return true;
431  if (ts.propagators()==0) return true;
432  if (assigmentType == EXTEND_ASSIGNMENT) return true;
433  return false;
434  }
435 
437 #define CHECK_TEST(T,M) \
438 if (opt.log) \
439  olog << ind(3) << "Check: " << (M) << std::endl; \
440 if (!(T)) { \
441  problem = (M); delete s; goto failed; \
442 }
443 
445 #define START_TEST(T) \
446  if (opt.log) { \
447  olog.str(""); \
448  olog << ind(2) << "Testing: " << (T) << std::endl; \
449  } \
450  test = (T);
451 
452  bool
453  Test::ignore(const Assignment&) const {
454  return false;
455  }
456 
457  void
459  Gecode::Reify) {}
460 
461  bool
462  Test::run(void) {
463  using namespace Gecode;
464  const char* test = "NONE";
465  const char* problem = "NONE";
466 
467  // Set up assignments
468  Assignment* ap = assignment();
469  Assignment& a = *ap;
470 
471  // Set up space for all solution search
472  TestSpace* search_s = new TestSpace(arity,dom,step,this);
473  post(*search_s,search_s->x);
474  branch(*search_s,search_s->x,FLOAT_VAR_NONE(),FLOAT_VAL_SPLIT_MIN());
475  Search::Options search_o;
476  search_o.threads = 1;
477  DFS<TestSpace> * e_s = new DFS<TestSpace>(search_s,search_o);
478  while (a()) {
479  MaybeType sol = solution(a);
480  if (opt.log) {
481  olog << ind(1) << "Assignment: " << a;
482  switch (sol) {
483  case MT_TRUE: olog << " (solution)"; break;
484  case MT_FALSE: olog << " (no solution)"; break;
485  case MT_MAYBE: olog << " (maybe)"; break;
486  }
487  olog << std::endl;
488  }
489  START_TEST("Assignment (after posting)");
490  {
491  TestSpace* s = new TestSpace(arity,dom,step,this);
492  TestSpace* sc = NULL;
493  s->post();
494  switch (Base::rand(3)) {
495  case 0:
496  if (opt.log)
497  olog << ind(3) << "No copy" << std::endl;
498  sc = s;
499  s = NULL;
500  break;
501  case 1:
502  if (opt.log)
503  olog << ind(3) << "Unshared copy" << std::endl;
504  if (s->status() != SS_FAILED) {
505  sc = static_cast<TestSpace*>(s->clone(false));
506  } else {
507  sc = s; s = NULL;
508  }
509  break;
510  case 2:
511  if (opt.log)
512  olog << ind(3) << "Shared copy" << std::endl;
513  if (s->status() != SS_FAILED) {
514  sc = static_cast<TestSpace*>(s->clone(true));
515  } else {
516  sc = s; s = NULL;
517  }
518  break;
519  default: assert(false);
520  }
521  sc->assign(a,sol);
522  if (sol == MT_TRUE) {
523  CHECK_TEST(!sc->failed(), "Failed on solution");
524  CHECK_TEST(subsumed(*sc), "No subsumption");
525  } else if (sol == MT_FALSE) {
526  CHECK_TEST(sc->failed(), "Solved on non-solution");
527  }
528  delete s; delete sc;
529  }
530  START_TEST("Partial assignment (after posting)");
531  {
532  TestSpace* s = new TestSpace(arity,dom,step,this);
533  s->post();
534  s->assign(a,sol,true);
535  (void) s->failed();
536  s->assign(a,sol);
537  if (sol == MT_TRUE) {
538  CHECK_TEST(!s->failed(), "Failed on solution");
539  CHECK_TEST(subsumed(*s), "No subsumption");
540  } else if (sol == MT_FALSE) {
541  CHECK_TEST(s->failed(), "Solved on non-solution");
542  }
543  delete s;
544  }
545  START_TEST("Assignment (before posting)");
546  {
547  TestSpace* s = new TestSpace(arity,dom,step,this);
548  s->assign(a,sol);
549  s->post();
550  if (sol == MT_TRUE) {
551  CHECK_TEST(!s->failed(), "Failed on solution");
552  CHECK_TEST(subsumed(*s), "No subsumption");
553  } else if (sol == MT_FALSE) {
554  CHECK_TEST(s->failed(), "Solved on non-solution");
555  }
556  delete s;
557  }
558  START_TEST("Partial assignment (before posting)");
559  {
560  TestSpace* s = new TestSpace(arity,dom,step,this);
561  s->assign(a,sol,true);
562  s->post();
563  (void) s->failed();
564  s->assign(a,sol);
565  if (sol == MT_TRUE) {
566  CHECK_TEST(!s->failed(), "Failed on solution");
567  CHECK_TEST(subsumed(*s), "No subsumption");
568  } else if (sol == MT_FALSE) {
569  CHECK_TEST(s->failed(), "Solved on non-solution");
570  }
571  delete s;
572  }
573  START_TEST("Prune");
574  {
575  TestSpace* s = new TestSpace(arity,dom,step,this);
576  s->post();
577  while (!s->failed() && !s->assigned() && !s->matchAssignment(a))
578  if (!s->prune(a,testfix)) {
579  problem = "No fixpoint";
580  delete s;
581  goto failed;
582  }
583  s->assign(a,sol);
584  if (sol == MT_TRUE) {
585  CHECK_TEST(!s->failed(), "Failed on solution");
586  CHECK_TEST(subsumed(*s), "No subsumption");
587  } else if (sol == MT_FALSE) {
588  CHECK_TEST(s->failed(), "Solved on non-solution");
589  }
590  delete s;
591  }
592 
593  if (reified && !ignore(a) && (sol != MT_MAYBE)) {
594  if (eqv()) {
595  START_TEST("Assignment reified (rewrite after post, <=>)");
596  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
597  s->post();
598  s->rel(sol == MT_TRUE);
599  s->assign(a,sol);
600  CHECK_TEST(!s->failed(), "Failed");
601  CHECK_TEST(subsumed(*s), "No subsumption");
602  delete s;
603  }
604  if (imp()) {
605  START_TEST("Assignment reified (rewrite after post, =>)");
606  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
607  s->post();
608  s->rel(sol == MT_TRUE);
609  s->assign(a,sol);
610  CHECK_TEST(!s->failed(), "Failed");
611  CHECK_TEST(subsumed(*s), "No subsumption");
612  delete s;
613  }
614  if (pmi()) {
615  START_TEST("Assignment reified (rewrite after post, <=)");
616  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
617  s->post();
618  s->rel(sol == MT_TRUE);
619  s->assign(a,sol);
620  CHECK_TEST(!s->failed(), "Failed");
621  CHECK_TEST(subsumed(*s), "No subsumption");
622  delete s;
623  }
624  if (eqv()) {
625  START_TEST("Assignment reified (immediate rewrite, <=>)");
626  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
627  s->rel(sol == MT_TRUE);
628  s->post();
629  s->assign(a,sol);
630  CHECK_TEST(!s->failed(), "Failed");
631  CHECK_TEST(subsumed(*s), "No subsumption");
632  delete s;
633  }
634  if (imp()) {
635  START_TEST("Assignment reified (immediate rewrite, =>)");
636  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
637  s->rel(sol == MT_TRUE);
638  s->post();
639  s->assign(a,sol);
640  CHECK_TEST(!s->failed(), "Failed");
641  CHECK_TEST(subsumed(*s), "No subsumption");
642  delete s;
643  }
644  if (pmi()) {
645  START_TEST("Assignment reified (immediate rewrite, <=)");
646  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
647  s->rel(sol == MT_TRUE);
648  s->post();
649  s->assign(a,sol);
650  CHECK_TEST(!s->failed(), "Failed");
651  CHECK_TEST(subsumed(*s), "No subsumption");
652  delete s;
653  }
654  if (eqv()) {
655  START_TEST("Assignment reified (before posting, <=>)");
656  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
657  s->assign(a,sol);
658  s->post();
659  CHECK_TEST(!s->failed(), "Failed");
660  CHECK_TEST(subsumed(*s), "No subsumption");
661  if (s->r.var().assigned()) {
662  if (sol == MT_TRUE) {
663  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
664  } else if (sol == MT_FALSE) {
665  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
666  }
667  }
668  delete s;
669  }
670  if (imp()) {
671  START_TEST("Assignment reified (before posting, =>)");
672  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
673  s->assign(a,sol);
674  s->post();
675  CHECK_TEST(!s->failed(), "Failed");
676  CHECK_TEST(subsumed(*s), "No subsumption");
677  if (sol == MT_TRUE) {
678  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
679  } else if ((sol = MT_FALSE) && s->r.var().assigned()) {
680  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
681  }
682  delete s;
683  }
684  if (pmi()) {
685  START_TEST("Assignment reified (before posting, <=)");
686  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
687  s->assign(a,sol);
688  s->post();
689  CHECK_TEST(!s->failed(), "Failed");
690  CHECK_TEST(subsumed(*s), "No subsumption");
691  if (sol == MT_TRUE) {
692  if (s->r.var().assigned()) {
693  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
694  }
695  } else if (sol == MT_FALSE) {
696  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
697  }
698  delete s;
699  }
700  if (eqv()) {
701  START_TEST("Assignment reified (after posting, <=>)");
702  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
703  s->post();
704  s->assign(a,sol);
705  CHECK_TEST(!s->failed(), "Failed");
706  CHECK_TEST(subsumed(*s), "No subsumption");
707  if (s->r.var().assigned()) {
708  if (sol == MT_TRUE) {
709  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
710  } else if (sol == MT_FALSE) {
711  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
712  }
713  }
714  delete s;
715  }
716  if (imp()) {
717  START_TEST("Assignment reified (after posting, =>)");
718  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
719  s->post();
720  s->assign(a,sol);
721  CHECK_TEST(!s->failed(), "Failed");
722  CHECK_TEST(subsumed(*s), "No subsumption");
723  if (sol == MT_TRUE) {
724  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
725  } else if (s->r.var().assigned()) {
726  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
727  }
728  delete s;
729  }
730  if (pmi()) {
731  START_TEST("Assignment reified (after posting, <=)");
732  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
733  s->post();
734  s->assign(a,sol);
735  CHECK_TEST(!s->failed(), "Failed");
736  CHECK_TEST(subsumed(*s), "No subsumption");
737  if (sol == MT_TRUE) {
738  if (s->r.var().assigned()) {
739  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
740  }
741  } else if (sol == MT_FALSE) {
742  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
743  }
744  delete s;
745  }
746  if (eqv()) {
747  START_TEST("Prune reified, <=>");
748  TestSpace* s = new TestSpace(arity,dom,step,this,RM_EQV);
749  s->post();
750  while (!s->failed() && !s->matchAssignment(a) &&
751  (!s->assigned() || !s->r.var().assigned()))
752  if (!s->prune(a,testfix)) {
753  problem = "No fixpoint";
754  delete s;
755  goto failed;
756  }
757  CHECK_TEST(!s->failed(), "Failed");
758  CHECK_TEST(subsumed(*s), "No subsumption");
759  if (s->r.var().assigned()) {
760  if (sol == MT_TRUE) {
761  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
762  } else if (sol == MT_FALSE) {
763  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
764  }
765  }
766  delete s;
767  }
768  if (imp()) {
769  START_TEST("Prune reified, =>");
770  TestSpace* s = new TestSpace(arity,dom,step,this,RM_IMP);
771  s->post();
772  while (!s->failed() && !s->matchAssignment(a) &&
773  (!s->assigned() || ((sol == MT_FALSE) &&
774  !s->r.var().assigned())))
775  if (!s->prune(a,testfix)) {
776  problem = "No fixpoint";
777  delete s;
778  goto failed;
779  }
780  CHECK_TEST(!s->failed(), "Failed");
781  CHECK_TEST(subsumed(*s), "No subsumption");
782  if (sol == MT_TRUE) {
783  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
784  } else if ((sol == MT_FALSE) && s->r.var().assigned()) {
785  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
786  }
787  delete s;
788  }
789  if (pmi()) {
790  START_TEST("Prune reified, <=");
791  TestSpace* s = new TestSpace(arity,dom,step,this,RM_PMI);
792  s->post();
793  while (!s->failed() && !s->matchAssignment(a) &&
794  (!s->assigned() || ((sol == MT_TRUE) &&
795  !s->r.var().assigned())))
796  if (!s->prune(a,testfix)) {
797  problem = "No fixpoint";
798  delete s;
799  goto failed;
800  }
801  CHECK_TEST(!s->failed(), "Failed");
802  CHECK_TEST(subsumed(*s), "No subsumption");
803  if ((sol == MT_TRUE) && s->r.var().assigned()) {
804  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
805  } else if (sol == MT_FALSE) {
806  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
807  }
808  delete s;
809  }
810  }
811 
812  if (testsearch) {
813  if (sol == MT_TRUE) {
814  START_TEST("Search");
815  if (!search_s->failed()) {
816  TestSpace* ss = static_cast<TestSpace*>(search_s->clone(false));
817  ss->dropUntil(a);
818  delete e_s;
819  e_s = new DFS<TestSpace>(ss,search_o);
820  delete ss;
821  }
822  TestSpace* s = e_s->next();
823  CHECK_TEST(s != NULL, "Solutions exhausted");
824  CHECK_TEST(subsumed(*s), "No subsumption");
825  for (int i=a.size(); i--; ) {
826  CHECK_TEST(s->x[i].assigned(), "Unassigned variable");
827  CHECK_TEST(Gecode::Float::overlap(a[i], s->x[i].val()), "Wrong value in solution");
828  }
829  delete s;
830  }
831  }
832 
833  ++a;
834  }
835 
836  if (testsearch) {
837  test = "Search";
838  if (!search_s->failed()) {
839  TestSpace* ss = static_cast<TestSpace*>(search_s->clone(false));
840  ss->dropUntil(a);
841  delete e_s;
842  e_s = new DFS<TestSpace>(ss,search_o);
843  delete ss;
844  }
845  if (e_s->next() != NULL) {
846  problem = "Excess solutions";
847  goto failed;
848  }
849  }
850 
851  delete ap;
852  delete search_s;
853  delete e_s;
854  return true;
855 
856  failed:
857  if (opt.log)
858  olog << "FAILURE" << std::endl
859  << ind(1) << "Test: " << test << std::endl
860  << ind(1) << "Problem: " << problem << std::endl;
861  if (a() && opt.log)
862  olog << ind(1) << "Assignment: " << a << std::endl;
863  delete ap;
864  delete search_s;
865  delete e_s;
866 
867  return false;
868  }
869 
870 }}
871 
872 #undef START_TEST
873 #undef CHECK_TEST
874 
875 // STATISTICS: test-float
void prune(int i)
Prune some random values from variable i.
Definition: float.cpp:325
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:429
const Gecode::FloatNum step
Definition: arithmetic.cpp:789
Gecode::FloatNum step
Step for going to next solution.
Definition: float.hh:249
NodeType t
Type of node.
Definition: bool-expr.cpp:234
FloatNum add_down(FloatNum x, FloatNum y)
Return lower bound of x plus y (domain: )
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:847
ReifyMode mode(void) const
Return reification mode.
Definition: reify.hpp:60
Simple class for describing identation.
Definition: test.hh:70
const FloatNum max
Largest allowed float value.
Definition: float.hh:831
#define START_TEST(T)
Start new test.
Definition: float.cpp:445
BoolVar var(void) const
Return Boolean control variable.
Definition: reify.hpp:52
Disequality ( )
Definition: float.hh:1056
void update(Space &home, bool share, VarImpVar< VarImp > &y)
Update this variable to be a clone of variable y.
Definition: var.hpp:128
static Gecode::Support::RandomGenerator rand
Random number generator.
Definition: test.hh:138
Space * clone(bool share=true, CloneStatistics &stat=unused_clone) const
Clone space.
Definition: core.hpp:2854
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:341
Less or equal ( )
Definition: float.hh:1057
Passing float variables.
Definition: float.hh:966
bool overlap(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:502
unsigned int size(void) const
Return size (cardinality) of domain.
Definition: bool.hpp:85
void dom(Home home, FloatVar x, FloatVal n)
Propagates .
Definition: dom.cpp:44
Gecode::FloatNum randFValDown(Gecode::FloatNum l, Gecode::FloatNum u)
Definition: float.cpp:112
int n
Number of variables.
Definition: float.hh:86
Less ( )
Definition: float.hh:1058
void post(void)
Post propagator.
Definition: float.cpp:212
void bound(void)
Assing a random variable to a random bound.
Definition: float.cpp:281
Float variable array.
Definition: float.hh:1016
Computation spaces.
Definition: core.hpp:1362
virtual void operator++(void)
Move to next assignment.
Definition: float.cpp:71
FloatVarBranch FLOAT_VAR_NONE(void)
Select first unassigned variable.
Definition: var.hpp:92
int val(void) const
Return assigned value.
Definition: bool.hpp:61
Gecode::IntSet d(v, 7)
Test * test
The test currently run.
Definition: float.hh:181
void update(Space &, bool share, VarArray< Var > &a)
Update array to be a clone of array a.
Definition: array.hpp:1072
Reify imp(BoolVar x)
Use implication for reification.
Definition: reify.hpp:77
Greater or equal ( )
Definition: float.hh:1059
unsigned int propagators(void) const
Return number of propagators.
Definition: core.cpp:196
const FloatNum min
Smallest allowed float value.
Definition: float.hh:833
Gecode::IntArgs i(4, 1, 2, 3, 4)
Gecode::FloatNum randFValUp(Gecode::FloatNum l, Gecode::FloatNum u)
Definition: float.cpp:129
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
Equality ( )
Definition: int.hh:904
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
NNF * r
Right subtree.
Definition: bool-expr.cpp:246
TestSpace(int n, Gecode::FloatVal &d, Gecode::FloatNum s, Test *t)
Create test space.
Definition: float.cpp:147
FloatRelType
Relation types for floats.
Definition: float.hh:1054
static bool fixpoint(void)
Throw a coin whether to compute a fixpoint.
Definition: test.hpp:70
bool assigned(void) const
Test whether all variables are assigned.
Definition: float.cpp:196
virtual void dropUntil(const Assignment &a)
Add constraints to skip solutions to the a assignment.
Definition: float.cpp:190
unsigned int size(I &i)
Size of all ranges of range iterator i.
Reification specification.
Definition: int.hh:854
virtual bool ignore(const Assignment &a) const
Whether to ignore assignment for reification.
Definition: float.cpp:453
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:137
struct Gecode::Space::@52::@54 c
Data available only during copying.
Equality ( )
Definition: float.hh:1055
Greater ( )
Definition: float.hh:1060
Boolean integer variables.
Definition: int.hh:491
Gecode::FloatVarArray x
Variables to be tested.
Definition: float.hh:177
union Gecode::@518::NNF::@57 u
Union depending on nodetype t.
const int v[7]
Definition: distinct.cpp:207
Gecode::FloatVal d
Initial domain.
Definition: float.hh:173
General test support.
Definition: afc.cpp:43
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:423
ExecStatus subsumed(Space &home, Propagator &p, TaskArray< Task > &t)
Check tasks t for subsumption.
Definition: subsumption.hpp:42
Float value type.
Definition: float.hh:321
void assign(const Assignment &a, MaybeType &sol, bool skip=false)
Assign all (or all but one, if skip is true) variables to values in a If assignment of a variable is ...
Definition: float.cpp:263
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.cpp:169
Gecode::FloatVal d
Domain for each variable.
Definition: float.hh:87
FloatNum div_down(FloatNum x, FloatNum y)
Return lower bound of x divided by y (domain: )
virtual Assignment * assignment(void) const
Create assignment.
Definition: float.cpp:408
MaybeType
Type for comparisons and solutions.
Definition: float.hh:55
T * next(void)
Return next solution (NULL, if none exists or search has been stopped)
Definition: dfs.hpp:52
std::ostringstream olog
Stream used for logging.
Definition: test.cpp:57
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVal n)
Propagates .
Definition: rel.cpp:47
bool matchAssignment(const Assignment &a) const
Test whether all variables match assignment a.
Definition: float.cpp:204
Space for executing tests.
Definition: float.hh:170
SpaceStatus status(StatusStatistics &stat=unused_status)
Query space status.
Definition: core.cpp:252
int size(void) const
Return number of variables.
Definition: float.hpp:52
bool assigned(void) const
Test whether view is assigned.
Definition: var.hpp:123
FloatNum sub_up(FloatNum x, FloatNum y)
Return upper bound of x minus y (domain: )
virtual bool run(void)
Perform test.
Definition: float.cpp:462
void threads(double n)
Set number of parallel threads.
Definition: options.hpp:252
FloatNum add_up(FloatNum x, FloatNum y)
Return upper bound of x plus y (domain: )
struct Gecode::@518::NNF::@57::@58 b
For binary nodes (and, or, eqv)
Gecode toplevel namespace
Implication for reification.
Definition: int.hh:840
bool failed(void)
Compute a fixpoint and check for failure.
Definition: float.cpp:225
bool assigned(void) const
Test if all variables are assigned.
Definition: array.hpp:1085
BrancherHandle branch(Home home, const FloatVarArgs &x, FloatVarBranch vars, FloatValBranch vals, FloatBranchFilter bf, FloatVarValPrint vvp)
Branch over x with variable selection vars and value selection vals.
Definition: branch.cpp:43
virtual void operator++(void)
Move to next assignment.
Definition: float.cpp:93
Gecode::FloatVal * dsv
Iterator for each variable.
Definition: float.hh:108
bool reified
Does the constraint also exist as reified constraint.
Definition: float.hh:253
Space is failed
Definition: core.hpp:1301
friend FloatVal max(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:390
Generate all assignments.
Definition: float.hh:106
Floating point numbers.
Definition: div.hpp:40
friend FloatVal min(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:402
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:985
#define CHECK_TEST(T, M)
Check the test result and handle failed test.
Definition: float.cpp:437
double FloatNum
Floating point number base type.
Definition: float.hh:108
ReifyMode
Mode for reification.
Definition: int.hh:826
#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:296
Options for scripts
Definition: driver.hh:326
void rel(int i, Gecode::FloatRelType frt, Gecode::FloatVal n)
Perform integer tell operation on x[i].
Definition: float.cpp:237
struct Gecode::@518::NNF::@57::@59 a
For atomic nodes.
Depth-first search engine.
Definition: search.hh:494
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:833
Reify pmi(BoolVar x)
Use reverse implication for reification.
Definition: reify.hpp:81