Generated on Thu Jan 20 2022 00:00:00 for Gecode by doxygen 1.9.1
int.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  *
7  * Copyright:
8  * Christian Schulte, 2005
9  * Mikael Lagerkvist, 2005
10  *
11  * This file is part of Gecode, the generic constraint
12  * development environment:
13  * http://www.gecode.org
14  *
15  * Permission is hereby granted, free of charge, to any person obtaining
16  * a copy of this software and associated documentation files (the
17  * "Software"), to deal in the Software without restriction, including
18  * without limitation the rights to use, copy, modify, merge, publish,
19  * distribute, sublicense, and/or sell copies of the Software, and to
20  * permit persons to whom the Software is furnished to do so, subject to
21  * the following conditions:
22  *
23  * The above copyright notice and this permission notice shall be
24  * included in all copies or substantial portions of the Software.
25  *
26  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
27  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
28  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
29  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
30  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
31  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
32  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
33  *
34  */
35 
36 #include "test/int.hh"
37 
38 #include <algorithm>
39 
40 namespace Test { namespace Int {
41 
42 
43  /*
44  * Complete assignments
45  *
46  */
47  void
49  int i = n-1;
50  while (true) {
51  ++dsv[i];
52  if (dsv[i]() || (i == 0))
53  return;
54  dsv[i--].init(d);
55  }
56  }
57 
58  /*
59  * Random assignments
60  *
61  */
62  void
64  for (int i = n; i--; )
65  vals[i]=randval();
66  a--;
67  }
68 
69  void
71  for (int i=n-_n1; i--; )
72  vals[i] = randval(d);
73  for (int i=_n1; i--; )
74  vals[n-_n1+i] = randval(_d1);
75  a--;
76  }
77 
78 }}
79 
80 std::ostream&
81 operator<<(std::ostream& os, const Test::Int::Assignment& a) {
82  int n = a.size();
83  os << "{";
84  for (int i=0; i<n; i++)
85  os << a[i] << ((i!=n-1) ? "," : "}");
86  return os;
87 }
88 
89 namespace Test { namespace Int {
90 
92  : d(d0), x(*this,n,Gecode::Int::Limits::min,Gecode::Int::Limits::max),
93  test(t), reified(false) {
94  Gecode::IntVarArgs _x(*this,n,d);
95  if (x.size() == 1)
96  Gecode::dom(*this,x[0],_x[0]);
97  else
98  Gecode::dom(*this,x,_x);
99  Gecode::BoolVar b(*this,0,1);
101  if (opt.log)
102  olog << ind(2) << "Initial: x[]=" << x
103  << std::endl;
104  }
105 
108  : d(d0), x(*this,n,Gecode::Int::Limits::min,Gecode::Int::Limits::max),
109  test(t), reified(true) {
110  Gecode::IntVarArgs _x(*this,n,d);
111  if (x.size() == 1)
112  Gecode::dom(*this,x[0],_x[0]);
113  else
114  Gecode::dom(*this,x,_x);
115  Gecode::BoolVar b(*this,0,1);
116  r = Gecode::Reify(b,rm);
117  if (opt.log)
118  olog << ind(2) << "Initial: x[]=" << x
119  << " b=" << r.var() << std::endl;
120  }
121 
123  : Gecode::Space(s), d(s.d), test(s.test), reified(s.reified) {
124  x.update(*this, s.x);
126  Gecode::BoolVar sr(s.r.var());
127  b.update(*this, sr);
128  r.var(b); r.mode(s.r.mode());
129  }
130 
133  return new TestSpace(*this);
134  }
135 
136  bool
137  TestSpace::assigned(void) const {
138  for (int i=x.size(); i--; )
139  if (!x[i].assigned())
140  return false;
141  return true;
142  }
143 
144  void
146  if (reified){
147  test->post(*this,x,r);
148  if (opt.log)
149  olog << ind(3) << "Posting reified propagator" << std::endl;
150  } else {
151  test->post(*this,x);
152  if (opt.log)
153  olog << ind(3) << "Posting propagator" << std::endl;
154  }
155  }
156 
157  bool
159  if (opt.log) {
160  olog << ind(3) << "Fixpoint: " << x;
161  bool f=(status() == Gecode::SS_FAILED);
162  olog << std::endl << ind(3) << " --> " << x << std::endl;
163  return f;
164  } else {
165  return status() == Gecode::SS_FAILED;
166  }
167  }
168 
169  int
171  assert(!assigned());
172  // Select variable to be pruned
173  int i = static_cast<int>(Base::rand(static_cast<unsigned int>(x.size())));
174  while (x[i].assigned()) {
175  i = (i+1) % x.size();
176  }
177  return i;
178  }
179 
180  void
182  Gecode::IntRelType& irt, int& v) {
183  using namespace Gecode;
184  // Select mode for pruning
185  irt = IRT_EQ; // Means do nothing!
186  switch (Base::rand(3)) {
187  case 0:
188  if (a[i] < x[i].max()) {
189  v=a[i]+1+
190  static_cast<int>(Base::rand(static_cast
191  <unsigned int>(x[i].max()-a[i])));
192  assert((v > a[i]) && (v <= x[i].max()));
193  irt = IRT_LE;
194  }
195  break;
196  case 1:
197  if (a[i] > x[i].min()) {
198  v=x[i].min()+
199  static_cast<int>(Base::rand(static_cast
200  <unsigned int>(a[i]-x[i].min())));
201  assert((v < a[i]) && (v >= x[i].min()));
202  irt = IRT_GR;
203  }
204  break;
205  default:
206  {
208  unsigned int skip =
209  Base::rand(static_cast<unsigned int>(x[i].size()-1));
210  while (true) {
211  if (it.width() > skip) {
212  v = it.min() + static_cast<int>(skip);
213  if (v == a[i]) {
214  if (it.width() == 1) {
215  ++it; v = it.min();
216  } else if (v < it.max()) {
217  ++v;
218  } else {
219  --v;
220  }
221  }
222  break;
223  }
224  skip -= it.width(); ++it;
225  }
226  irt = IRT_NQ;
227  break;
228  }
229  }
230  }
231 
232  void
234  if (opt.log) {
235  olog << ind(4) << "x[" << i << "] ";
236  switch (irt) {
237  case Gecode::IRT_EQ: olog << "="; break;
238  case Gecode::IRT_NQ: olog << "!="; break;
239  case Gecode::IRT_LQ: olog << "<="; break;
240  case Gecode::IRT_LE: olog << "<"; break;
241  case Gecode::IRT_GQ: olog << ">="; break;
242  case Gecode::IRT_GR: olog << ">"; break;
243  }
244  olog << " " << n << std::endl;
245  }
246  Gecode::rel(*this, x[i], irt, n);
247  }
248 
249  void
250  TestSpace::rel(bool sol) {
251  int n = sol ? 1 : 0;
252  assert(reified);
253  if (opt.log)
254  olog << ind(4) << "b = " << n << std::endl;
255  Gecode::rel(*this, r.var(), Gecode::IRT_EQ, n);
256  }
257 
258  void
259  TestSpace::assign(const Assignment& a, bool skip) {
260  using namespace Gecode;
261  int i = skip ?
262  static_cast<int>(Base::rand(static_cast<unsigned int>(a.size()))) : -1;
263  for (int j=a.size(); j--; )
264  if (i != j) {
265  rel(j, IRT_EQ, a[j]);
266  if (Base::fixpoint() && failed())
267  return;
268  }
269  }
270 
271  void
273  using namespace Gecode;
274  int i = rndvar();
275  bool min = Base::rand(2);
276  rel(i, IRT_EQ, min ? x[i].min() : x[i].max());
277  }
278 
279  void
280  TestSpace::prune(int i, bool bounds_only) {
281  using namespace Gecode;
282  // Prune values
283  if (bounds_only) {
284  if (Base::rand(2) && !x[i].assigned()) {
285  int v=x[i].min()+1+
286  static_cast<int>(Base::rand(static_cast
287  <unsigned int>(x[i].max()-x[i].min())));
288  assert((v > x[i].min()) && (v <= x[i].max()));
289  rel(i, Gecode::IRT_LE, v);
290  }
291  if (Base::rand(2) && !x[i].assigned()) {
292  int v=x[i].min()+
293  static_cast<int>(Base::rand(static_cast
294  <unsigned int>(x[i].max()-x[i].min())));
295  assert((v < x[i].max()) && (v >= x[i].min()));
296  rel(i, Gecode::IRT_GR, v);
297  }
298  } else {
299  for (int vals =
300  static_cast<int>(Base::rand(static_cast<unsigned int>(x[i].size()-1))+1); vals--; ) {
301  int v;
303  unsigned int skip = Base::rand(x[i].size()-1);
304  while (true) {
305  if (it.width() > skip) {
306  v = it.min() + static_cast<int>(skip); break;
307  }
308  skip -= it.width(); ++it;
309  }
310  rel(i, IRT_NQ, v);
311  }
312  }
313  }
314 
315  void
317  prune(rndvar(), false);
318  }
319 
320  bool
321  TestSpace::prune(const Assignment& a, bool testfix) {
322  using namespace Gecode;
323  // Select variable to be pruned
324  int i = rndvar();
325  // Select mode for pruning
326  IntRelType irt;
327  int v;
328  rndrel(a,i,irt,v);
329  if (irt != IRT_EQ)
330  rel(i, irt, v);
331  if (Base::fixpoint()) {
332  if (failed() || !testfix)
333  return true;
334  TestSpace* c = static_cast<TestSpace*>(clone());
335  if (opt.log)
336  olog << ind(3) << "Testing fixpoint on copy" << std::endl;
337  c->post();
338  if (c->failed()) {
339  if (opt.log)
340  olog << ind(4) << "Copy failed after posting" << std::endl;
341  delete c; return false;
342  }
343  for (int j=x.size(); j--; )
344  if (x[j].size() != c->x[j].size()) {
345  if (opt.log)
346  olog << ind(4) << "Different domain size" << std::endl;
347  delete c; return false;
348  }
349  if (reified && (r.var().size() != c->r.var().size())) {
350  if (opt.log)
351  olog << ind(4) << "Different control variable" << std::endl;
352  delete c; return false;
353  }
354  if (opt.log)
355  olog << ind(3) << "Finished testing fixpoint on copy" << std::endl;
356  delete c;
357  }
358  return true;
359  }
360 
361  void
364  }
365 
366  void
369  (void) status();
370  }
371 
372  bool
374  bool testfix) {
375  using namespace Gecode;
376  // Disable propagators
377  c.disable();
378  // Select variable to be pruned
379  int i = rndvar();
380  // Select mode for pruning
381  IntRelType irt;
382  int v;
383  rndrel(a,i,irt,v);
384  if (irt != IRT_EQ) {
385  rel(i, irt, v);
386  c.rel(i, irt, v);
387  }
388  // Enable propagators
389  c.enable();
390  if (!testfix)
391  return true;
392  if (failed()) {
393  if (!c.failed()) {
394  if (opt.log)
395  olog << ind(3) << "No failure on disabled copy" << std::endl;
396  return false;
397  }
398  return true;
399  }
400  if (c.failed()) {
401  if (opt.log)
402  olog << ind(3) << "Failure on disabled copy" << std::endl;
403  return false;
404  }
405  for (int j=x.size(); j--; ) {
406  if (x[j].size() != c.x[j].size()) {
407  if (opt.log)
408  olog << ind(4) << "Different domain size" << std::endl;
409  return false;
410  }
411  if (reified && (r.var().size() != c.r.var().size())) {
412  if (opt.log)
413  olog << ind(4) << "Different control variable" << std::endl;
414  return false;
415  }
416  }
417  return true;
418  }
419 
420  unsigned int
422  return Gecode::PropagatorGroup::all.size(*this);
423  }
424 
425  const Gecode::IntPropLevel IntPropLevels::ipls[] =
427 
428  const Gecode::IntPropLevel IntPropBasicAdvanced::ipls[] =
430 
431  const Gecode::IntRelType IntRelTypes::irts[] =
434 
435  const Gecode::BoolOpType BoolOpTypes::bots[] =
438 
439  Assignment*
440  Test::assignment(void) const {
441  return new CpltAssignment(arity,dom);
442  }
443 
444 
446 #define CHECK_TEST(T,M) \
447 if (opt.log) \
448  olog << ind(3) << "Check: " << (M) << std::endl; \
449 if (!(T)) { \
450  problem = (M); delete s; goto failed; \
451 }
452 
454 #define START_TEST(T) \
455  if (opt.log) { \
456  olog.str(""); \
457  olog << ind(2) << "Testing: " << (T) << std::endl; \
458  } \
459  test = (T);
460 
461  bool
462  Test::ignore(const Assignment&) const {
463  return false;
464  }
465 
466  void
468  Gecode::Reify) {}
469 
470  bool
471  Test::run(void) {
472  using namespace Gecode;
473  const char* test = "NONE";
474  const char* problem = "NONE";
475 
476  // Set up assignments
477  Assignment* ap = assignment();
478  Assignment& a = *ap;
479 
480  // Set up space for all solution search
481  TestSpace* search_s = new TestSpace(arity,dom,this);
482  post(*search_s,search_s->x);
483  branch(*search_s,search_s->x,INT_VAR_NONE(),INT_VAL_MIN());
484  Search::Options search_o;
485  search_o.threads = 1;
486  DFS<TestSpace> e_s(search_s,search_o);
487  delete search_s;
488 
489  while (a()) {
490  bool sol = solution(a);
491  if (opt.log) {
492  olog << ind(1) << "Assignment: " << a
493  << (sol ? " (solution)" : " (no solution)")
494  << std::endl;
495  }
496 
497  START_TEST("Assignment (after posting)");
498  {
499  TestSpace* s = new TestSpace(arity,dom,this);
500  TestSpace* sc = NULL;
501  s->post();
502  switch (Base::rand(2)) {
503  case 0:
504  if (opt.log)
505  olog << ind(3) << "No copy" << std::endl;
506  sc = s;
507  s = NULL;
508  break;
509  case 1:
510  if (opt.log)
511  olog << ind(3) << "Copy" << std::endl;
512  if (s->status() != SS_FAILED) {
513  sc = static_cast<TestSpace*>(s->clone());
514  } else {
515  sc = s; s = NULL;
516  }
517  break;
518  default: assert(false);
519  }
520  sc->assign(a);
521  if (sol) {
522  CHECK_TEST(!sc->failed(), "Failed on solution");
523  CHECK_TEST(sc->propagators()==0, "No subsumption");
524  } else {
525  CHECK_TEST(sc->failed(), "Solved on non-solution");
526  }
527  delete s; delete sc;
528  }
529  START_TEST("Partial assignment (after posting)");
530  {
531  TestSpace* s = new TestSpace(arity,dom,this);
532  s->post();
533  s->assign(a,true);
534  (void) s->failed();
535  s->assign(a);
536  if (sol) {
537  CHECK_TEST(!s->failed(), "Failed on solution");
538  CHECK_TEST(s->propagators()==0, "No subsumption");
539  } else {
540  CHECK_TEST(s->failed(), "Solved on non-solution");
541  }
542  delete s;
543  }
544  START_TEST("Assignment (after posting, disable)");
545  {
546  TestSpace* s = new TestSpace(arity,dom,this);
547  s->post();
548  s->disable();
549  s->assign(a);
550  s->enable();
551  if (sol) {
552  CHECK_TEST(!s->failed(), "Failed on solution");
553  CHECK_TEST(s->propagators()==0, "No subsumption");
554  } else {
555  CHECK_TEST(s->failed(), "Solved on non-solution");
556  }
557  delete s;
558  }
559  START_TEST("Partial assignment (after posting, disable)");
560  {
561  TestSpace* s = new TestSpace(arity,dom,this);
562  s->post();
563  s->assign(a,true);
564  s->disable();
565  (void) s->failed();
566  s->assign(a);
567  s->enable();
568  if (sol) {
569  CHECK_TEST(!s->failed(), "Failed on solution");
570  CHECK_TEST(s->propagators()==0, "No subsumption");
571  } else {
572  CHECK_TEST(s->failed(), "Solved on non-solution");
573  }
574  delete s;
575  }
576  START_TEST("Assignment (before posting)");
577  {
578  TestSpace* s = new TestSpace(arity,dom,this);
579  s->assign(a);
580  s->post();
581  if (sol) {
582  CHECK_TEST(!s->failed(), "Failed on solution");
583  CHECK_TEST(s->propagators()==0, "No subsumption");
584  } else {
585  CHECK_TEST(s->failed(), "Solved on non-solution");
586  }
587  delete s;
588  }
589  START_TEST("Partial assignment (before posting)");
590  {
591  TestSpace* s = new TestSpace(arity,dom,this);
592  s->assign(a,true);
593  s->post();
594  (void) s->failed();
595  s->assign(a);
596  if (sol) {
597  CHECK_TEST(!s->failed(), "Failed on solution");
598  CHECK_TEST(s->propagators()==0, "No subsumption");
599  } else {
600  CHECK_TEST(s->failed(), "Solved on non-solution");
601  }
602  delete s;
603  }
604  START_TEST("Prune");
605  {
606  TestSpace* s = new TestSpace(arity,dom,this);
607  s->post();
608  while (!s->failed() && !s->assigned())
609  if (!s->prune(a,testfix)) {
610  problem = "No fixpoint";
611  delete s;
612  goto failed;
613  }
614  s->assign(a);
615  if (sol) {
616  CHECK_TEST(!s->failed(), "Failed on solution");
617  CHECK_TEST(s->propagators()==0, "No subsumption");
618  } else {
619  CHECK_TEST(s->failed(), "Solved on non-solution");
620  }
621  delete s;
622  }
623  START_TEST("Prune (disable)");
624  {
625  TestSpace* s = new TestSpace(arity,dom,this);
626  TestSpace* c = static_cast<TestSpace*>(s->clone());
627  s->post(); c->post();
628  while (!s->failed() && !s->assigned())
629  if (!s->disabled(a,*c,testfix)) {
630  problem = "Different result after re-enable";
631  delete s; delete c;
632  goto failed;
633  }
634  if (testfix && (s->failed() != c->failed())) {
635  problem = "Different failure after re-enable";
636  delete s; delete c;
637  goto failed;
638  }
639  delete s; delete c;
640  }
641  if (!ignore(a)) {
642  if (eqv()) {
643  {
644  START_TEST("Assignment reified (rewrite after post, <=>)");
645  TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
646  s->post();
647  s->rel(sol);
648  s->assign(a);
649  CHECK_TEST(!s->failed(), "Failed");
650  CHECK_TEST(s->propagators()==0, "No subsumption");
651  delete s;
652  }
653  {
654  START_TEST("Assignment reified (rewrite failure, <=>)");
655  TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
656  s->post();
657  s->rel(!sol);
658  s->assign(a);
659  CHECK_TEST(s->failed(), "Not failed");
660  delete s;
661  }
662  {
663  START_TEST("Assignment reified (immediate rewrite, <=>)");
664  TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
665  s->rel(sol);
666  s->post();
667  s->assign(a);
668  CHECK_TEST(!s->failed(), "Failed");
669  CHECK_TEST(s->propagators()==0, "No subsumption");
670  delete s;
671  }
672  {
673  START_TEST("Assignment reified (immediate failure, <=>)");
674  TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
675  s->rel(!sol);
676  s->post();
677  s->assign(a);
678  CHECK_TEST(s->failed(), "Not failed");
679  delete s;
680  }
681  {
682  START_TEST("Assignment reified (before posting, <=>)");
683  TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
684  s->assign(a);
685  s->post();
686  CHECK_TEST(!s->failed(), "Failed");
687  CHECK_TEST(s->propagators()==0, "No subsumption");
688  CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
689  if (sol) {
690  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
691  } else {
692  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
693  }
694  delete s;
695  }
696  {
697  START_TEST("Assignment reified (after posting, <=>)");
698  TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
699  s->post();
700  s->assign(a);
701  CHECK_TEST(!s->failed(), "Failed");
702  CHECK_TEST(s->propagators()==0, "No subsumption");
703  CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
704  if (sol) {
705  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
706  } else {
707  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
708  }
709  delete s;
710  }
711  {
712  START_TEST("Assignment reified (after posting, <=>, disable)");
713  TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
714  s->post();
715  s->disable();
716  s->assign(a);
717  s->enable();
718  CHECK_TEST(!s->failed(), "Failed");
719  CHECK_TEST(s->propagators()==0, "No subsumption");
720  CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
721  if (sol) {
722  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
723  } else {
724  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
725  }
726  delete s;
727  }
728  {
729  START_TEST("Prune reified, <=>");
730  TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
731  s->post();
732  while (!s->failed() &&
733  (!s->assigned() || !s->r.var().assigned()))
734  if (!s->prune(a,testfix)) {
735  problem = "No fixpoint";
736  delete s;
737  goto failed;
738  }
739  CHECK_TEST(!s->failed(), "Failed");
740  CHECK_TEST(s->propagators()==0, "No subsumption");
741  CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
742  if (sol) {
743  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
744  } else {
745  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
746  }
747  delete s;
748  }
749  {
750  START_TEST("Prune reified, <=>, disable");
751  TestSpace* s = new TestSpace(arity,dom,this,RM_EQV);
752  TestSpace* c = static_cast<TestSpace*>(s->clone());
753  s->post(); c->post();
754  while (!s->failed() &&
755  (!s->assigned() || !s->r.var().assigned()))
756  if (!s->disabled(a,*c,testfix)) {
757  problem = "No fixpoint";
758  delete s;
759  delete c;
760  goto failed;
761  }
762  CHECK_TEST(!c->failed(), "Failed");
763  CHECK_TEST(c->propagators()==0, "No subsumption");
764  CHECK_TEST(c->r.var().assigned(), "Control variable unassigned");
765  if (sol) {
766  CHECK_TEST(c->r.var().val()==1, "Zero on solution");
767  } else {
768  CHECK_TEST(c->r.var().val()==0, "One on non-solution");
769  }
770  delete s;
771  delete c;
772  }
773  }
774 
775  if (imp()) {
776  {
777  START_TEST("Assignment reified (rewrite after post, =>)");
778  TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
779  s->post();
780  s->rel(sol);
781  s->assign(a);
782  CHECK_TEST(!s->failed(), "Failed");
783  CHECK_TEST(s->propagators()==0, "No subsumption");
784  delete s;
785  }
786  {
787  START_TEST("Assignment reified (rewrite failure, =>)");
788  TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
789  s->post();
790  s->rel(!sol);
791  s->assign(a);
792  if (sol) {
793  CHECK_TEST(!s->failed(), "Failed");
794  CHECK_TEST(s->propagators()==0, "No subsumption");
795  } else {
796  CHECK_TEST(s->failed(), "Not failed");
797  }
798  delete s;
799  }
800  {
801  START_TEST("Assignment reified (immediate rewrite, =>)");
802  TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
803  s->rel(sol);
804  s->post();
805  s->assign(a);
806  CHECK_TEST(!s->failed(), "Failed");
807  CHECK_TEST(s->propagators()==0, "No subsumption");
808  delete s;
809  }
810  {
811  START_TEST("Assignment reified (immediate failure, =>)");
812  TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
813  s->rel(!sol);
814  s->post();
815  s->assign(a);
816  if (sol) {
817  CHECK_TEST(!s->failed(), "Failed");
818  CHECK_TEST(s->propagators()==0, "No subsumption");
819  } else {
820  CHECK_TEST(s->failed(), "Not failed");
821  }
822  delete s;
823  }
824  {
825  START_TEST("Assignment reified (before posting, =>)");
826  TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
827  s->assign(a);
828  s->post();
829  CHECK_TEST(!s->failed(), "Failed");
830  CHECK_TEST(s->propagators()==0, "No subsumption");
831  if (sol) {
832  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
833  } else {
834  CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
835  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
836  }
837  delete s;
838  }
839  {
840  START_TEST("Assignment reified (after posting, =>)");
841  TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
842  s->post();
843  s->assign(a);
844  CHECK_TEST(!s->failed(), "Failed");
845  CHECK_TEST(s->propagators()==0, "No subsumption");
846  if (sol) {
847  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
848  } else {
849  CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
850  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
851  }
852  delete s;
853  }
854  {
855  START_TEST("Assignment reified (after posting, =>, disable)");
856  TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
857  s->post();
858  s->disable();
859  s->assign(a);
860  s->enable();
861  CHECK_TEST(!s->failed(), "Failed");
862  CHECK_TEST(s->propagators()==0, "No subsumption");
863  if (sol) {
864  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
865  } else {
866  CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
867  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
868  }
869  delete s;
870  }
871  {
872  START_TEST("Prune reified, =>");
873  TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
874  s->post();
875  while (!s->failed() &&
876  (!s->assigned() || (!sol && !s->r.var().assigned())))
877  if (!s->prune(a,testfix)) {
878  problem = "No fixpoint";
879  delete s;
880  goto failed;
881  }
882  CHECK_TEST(!s->failed(), "Failed");
883  CHECK_TEST(s->propagators()==0, "No subsumption");
884  if (sol) {
885  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
886  } else {
887  CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
888  CHECK_TEST(s->r.var().val()==0, "One on non-solution");
889  }
890  delete s;
891  }
892  {
893  START_TEST("Prune reified, =>, disable");
894  TestSpace* s = new TestSpace(arity,dom,this,RM_IMP);
895  TestSpace* c = static_cast<TestSpace*>(s->clone());
896  s->post(); c->post();
897  while (!s->failed() &&
898  (!s->assigned() || (!sol && !s->r.var().assigned())))
899  if (!s->disabled(a,*c,testfix)) {
900  problem = "No fixpoint";
901  delete s;
902  delete c;
903  goto failed;
904  }
905  CHECK_TEST(!c->failed(), "Failed");
906  CHECK_TEST(c->propagators()==0, "No subsumption");
907  if (sol) {
908  CHECK_TEST(!c->r.var().assigned(), "Control variable assigned");
909  } else {
910  CHECK_TEST(c->r.var().assigned(), "Control variable unassigned");
911  CHECK_TEST(c->r.var().val()==0, "One on non-solution");
912  }
913  delete s;
914  delete c;
915  }
916  }
917 
918  if (pmi()) {
919  {
920  START_TEST("Assignment reified (rewrite after post, <=)");
921  TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
922  s->post();
923  s->rel(sol);
924  s->assign(a);
925  CHECK_TEST(!s->failed(), "Failed");
926  CHECK_TEST(s->propagators()==0, "No subsumption");
927  delete s;
928  }
929  {
930  START_TEST("Assignment reified (rewrite failure, <=)");
931  TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
932  s->post();
933  s->rel(!sol);
934  s->assign(a);
935  if (sol) {
936  CHECK_TEST(s->failed(), "Not failed");
937  } else {
938  CHECK_TEST(!s->failed(), "Failed");
939  CHECK_TEST(s->propagators()==0, "No subsumption");
940  }
941  delete s;
942  }
943  {
944  START_TEST("Assignment reified (immediate rewrite, <=)");
945  TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
946  s->rel(sol);
947  s->post();
948  s->assign(a);
949  CHECK_TEST(!s->failed(), "Failed");
950  CHECK_TEST(s->propagators()==0, "No subsumption");
951  delete s;
952  }
953  {
954  START_TEST("Assignment reified (immediate failure, <=)");
955  TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
956  s->rel(!sol);
957  s->post();
958  s->assign(a);
959  if (sol) {
960  CHECK_TEST(s->failed(), "Not failed");
961  } else {
962  CHECK_TEST(!s->failed(), "Failed");
963  CHECK_TEST(s->propagators()==0, "No subsumption");
964  }
965  delete s;
966  }
967  {
968  START_TEST("Assignment reified (before posting, <=)");
969  TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
970  s->assign(a);
971  s->post();
972  CHECK_TEST(!s->failed(), "Failed");
973  CHECK_TEST(s->propagators()==0, "No subsumption");
974  if (sol) {
975  CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
976  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
977  } else {
978  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
979  }
980  delete s;
981  }
982  {
983  START_TEST("Assignment reified (after posting, <=)");
984  TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
985  s->post();
986  s->assign(a);
987  CHECK_TEST(!s->failed(), "Failed");
988  CHECK_TEST(s->propagators()==0, "No subsumption");
989  if (sol) {
990  CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
991  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
992  } else {
993  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
994  }
995  delete s;
996  }
997  {
998  START_TEST("Assignment reified (after posting, <=, disable)");
999  TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
1000  s->post();
1001  s->disable();
1002  s->assign(a);
1003  s->enable();
1004  CHECK_TEST(!s->failed(), "Failed");
1005  CHECK_TEST(s->propagators()==0, "No subsumption");
1006  if (sol) {
1007  CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1008  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1009  } else {
1010  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1011  }
1012  delete s;
1013  }
1014  {
1015  START_TEST("Prune reified, <=");
1016  TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
1017  s->post();
1018  while (!s->failed() &&
1019  (!s->assigned() || (sol && !s->r.var().assigned())))
1020  if (!s->prune(a,testfix)) {
1021  problem = "No fixpoint";
1022  delete s;
1023  goto failed;
1024  }
1025  CHECK_TEST(!s->failed(), "Failed");
1026  CHECK_TEST(s->propagators()==0, "No subsumption");
1027  if (sol) {
1028  CHECK_TEST(s->r.var().assigned(), "Control variable unassigned");
1029  CHECK_TEST(s->r.var().val()==1, "Zero on solution");
1030  } else {
1031  CHECK_TEST(!s->r.var().assigned(), "Control variable assigned");
1032  }
1033  delete s;
1034  }
1035  {
1036  START_TEST("Prune reified, <=, disable");
1037  TestSpace* s = new TestSpace(arity,dom,this,RM_PMI);
1038  TestSpace* c = static_cast<TestSpace*>(s->clone());
1039  s->post(); c->post();
1040  while (!s->failed() &&
1041  (!s->assigned() || (sol && !s->r.var().assigned())))
1042  if (!s->disabled(a,*c,testfix)) {
1043  problem = "No fixpoint";
1044  delete s;
1045  delete c;
1046  goto failed;
1047  }
1048  CHECK_TEST(!c->failed(), "Failed");
1049  CHECK_TEST(c->propagators()==0, "No subsumption");
1050  if (sol) {
1051  CHECK_TEST(c->r.var().assigned(), "Control variable unassigned");
1052  CHECK_TEST(c->r.var().val()==1, "Zero on solution");
1053  } else {
1054  CHECK_TEST(!c->r.var().assigned(), "Control variable assigned");
1055  }
1056  delete s;
1057  delete c;
1058  }
1059  }
1060  }
1061 
1062  if (testsearch) {
1063  if (sol) {
1064  START_TEST("Search");
1065  TestSpace* s = e_s.next();
1066  CHECK_TEST(s != NULL, "Solutions exhausted");
1067  CHECK_TEST(s->propagators()==0, "No subsumption");
1068  for (int i=a.size(); i--; ) {
1069  CHECK_TEST(s->x[i].assigned(), "Unassigned variable");
1070  CHECK_TEST(a[i] == s->x[i].val(), "Wrong value in solution");
1071  }
1072  delete s;
1073  }
1074  }
1075 
1076  ++a;
1077  }
1078 
1079  if (testsearch) {
1080  test = "Search";
1081  if (e_s.next() != NULL) {
1082  problem = "Excess solutions";
1083  goto failed;
1084  }
1085  }
1086 
1087  switch (contest) {
1088  case CTL_NONE: break;
1089  case CTL_DOMAIN: {
1090  START_TEST("Full domain consistency");
1091  TestSpace* s = new TestSpace(arity,dom,this);
1092  s->post();
1093  if (!s->failed()) {
1094  while (!s->failed() && !s->assigned())
1095  s->prune();
1096  CHECK_TEST(!s->failed(), "Failed");
1097  CHECK_TEST(s->propagators()==0, "No subsumption");
1098  }
1099  delete s;
1100  // Fall-through -- domain implies bounds(d) and bounds(z)
1101  }
1102  case CTL_BOUNDS_D: {
1103  START_TEST("Bounds(D)-consistency");
1104  TestSpace* s = new TestSpace(arity,dom,this);
1105  s->post();
1106  for (int i = s->x.size(); i--; )
1107  s->prune(i, false);
1108  if (!s->failed()) {
1109  while (!s->failed() && !s->assigned())
1110  s->bound();
1111  CHECK_TEST(!s->failed(), "Failed");
1112  CHECK_TEST(s->propagators()==0, "No subsumption");
1113  }
1114  delete s;
1115  // Fall-through -- bounds(d) implies bounds(z)
1116  }
1117  case CTL_BOUNDS_Z: {
1118  START_TEST("Bounds(Z)-consistency");
1119  TestSpace* s = new TestSpace(arity,dom,this);
1120  s->post();
1121  for (int i = s->x.size(); i--; )
1122  s->prune(i, true);
1123  if (!s->failed()) {
1124  while (!s->failed() && !s->assigned())
1125  s->bound();
1126  CHECK_TEST(!s->failed(), "Failed");
1127  CHECK_TEST(s->propagators()==0, "No subsumption");
1128  }
1129  delete s;
1130  break;
1131  }
1132  }
1133 
1134  delete ap;
1135  return true;
1136 
1137  failed:
1138  if (opt.log)
1139  olog << "FAILURE" << std::endl
1140  << ind(1) << "Test: " << test << std::endl
1141  << ind(1) << "Problem: " << problem << std::endl;
1142  if (a() && opt.log)
1143  olog << ind(1) << "Assignment: " << a << std::endl;
1144  delete ap;
1145 
1146  return false;
1147  }
1148 
1149 }}
1150 
1151 #undef START_TEST
1152 #undef CHECK_TEST
1153 
1154 // STATISTICS: test-int
struct Gecode::@602::NNF::@65::@66 b
For binary nodes (and, or, eqv)
NodeType t
Type of node.
Definition: bool-expr.cpp:230
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:234
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:249
struct Gecode::@602::NNF::@65::@67 a
For atomic nodes.
Boolean integer variables.
Definition: int.hh:512
unsigned int size(void) const
Return size (cardinality) of domain.
Definition: bool.hpp:81
int val(void) const
Return assigned value.
Definition: bool.hpp:57
Depth-first search engine.
Definition: search.hh:1036
std::basic_ostream< Char, Traits > & operator<<(std::basic_ostream< Char, Traits > &os, const FloatView &x)
Print float variable view.
void init(const IntSet &s)
Initialize with values for s.
Definition: int-set-1.hpp:285
Integer sets.
Definition: int.hh:174
Passing integer variables.
Definition: int.hh:656
Integer variable array.
Definition: int.hh:763
int max(void) const
Return largest value of range.
int min(void) const
Return smallest value of range.
unsigned int width(void) const
Return width of range (distance between minimum and maximum)
Options for scripts
Definition: driver.hh:366
void threads(double n)
Set number of parallel threads.
Definition: options.hpp:292
unsigned int size(Space &home) const
Return number of propagators in a group.
Definition: core.cpp:955
void disable(Space &home)
Disable all propagators in a group.
Definition: core.cpp:979
void enable(Space &home, bool s=true)
Enable all propagators in a group.
Definition: core.cpp:988
static PropagatorGroup all
Group of all propagators.
Definition: core.hpp:789
Reification specification.
Definition: int.hh:876
BoolVar var(void) const
Return Boolean control variable.
Definition: reify.hpp:48
ReifyMode mode(void) const
Return reification mode.
Definition: reify.hpp:56
virtual T * next(void)
Return next solution (NULL, if none exists or search has been stopped)
Definition: base.hpp:46
Computation spaces.
Definition: core.hpp:1742
struct Gecode::Space::@61::@63 c
Data available only during copying.
bool assigned(void) const
Test if all variables are assigned.
Definition: array.hpp:1026
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:926
void update(Space &home, VarArray< Var > &a)
Update array to be a clone of array a.
Definition: array.hpp:1013
bool assigned(void) const
Test whether view is assigned.
Definition: var.hpp:111
static Gecode::Support::RandomGenerator rand
Random number generator.
Definition: test.hh:134
static bool fixpoint(void)
Throw a coin whether to compute a fixpoint.
Definition: test.hpp:66
Base class for assignments
Definition: int.hh:59
Gecode::IntSet d
Domain for each variable.
Definition: int.hh:62
int n
Number of variables.
Definition: int.hh:61
Generate all assignments.
Definition: int.hh:79
Gecode::IntSetValues * dsv
Iterator for each variable.
Definition: int.hh:81
virtual void operator++(void)
Move to next assignment.
Definition: int.cpp:48
int a
How many assigments still to be generated Generate new value according to domain.
Definition: int.hh:99
int * vals
The current values for the variables.
Definition: int.hh:98
virtual void operator++(void)
Move to next assignment.
Definition: int.cpp:63
int _n1
How many variables in the second set.
Definition: int.hh:120
Gecode::IntSet _d1
Domain for second set of variables Generate new value according to domain d.
Definition: int.hh:121
int a
How many assigments still to be generated.
Definition: int.hh:119
int * vals
The current values for the variables.
Definition: int.hh:118
virtual void operator++(void)
Move to next assignment.
Definition: int.cpp:70
int randval(const Gecode::IntSet &d)
Definition: int.hpp:109
Space for executing tests.
Definition: int.hh:149
Gecode::Reify r
Reification information.
Definition: int.hh:156
TestSpace(int n, Gecode::IntSet &d, Test *t)
Create test space without reification.
Definition: int.cpp:91
Gecode::IntSet d
Initial domain.
Definition: int.hh:152
void rndrel(const Assignment &a, int i, Gecode::IntRelType &irt, int &v)
Randomly select a pruning rel for variable i.
Definition: int.cpp:181
Test * test
The test currently run.
Definition: int.hh:158
virtual Gecode::Space * copy(void)
Copy space during cloning.
Definition: int.cpp:132
void post(void)
Post propagator.
Definition: int.cpp:145
bool assigned(void) const
Test whether all variables are assigned.
Definition: int.cpp:137
void prune(void)
Prune some random values for some random variable.
Definition: int.cpp:316
void bound(void)
Assing a random variable to a random bound.
Definition: int.cpp:272
void assign(const Assignment &a, bool skip=false)
Assign all (or all but one, if skip is true) variables to values in a.
Definition: int.cpp:259
bool failed(void)
Compute a fixpoint and check for failure.
Definition: int.cpp:158
bool reified
Whether the test is for a reified propagator.
Definition: int.hh:160
void prune(int i, bool bounds_only)
Prune some random values from variable i.
Definition: int.cpp:280
int rndvar(void)
Randomly select an unassigned variable.
Definition: int.cpp:170
bool disabled(const Assignment &a, TestSpace &c, bool testfix)
Prune values also in a space c with disabled propagators, but not those in assignment a.
Definition: int.cpp:373
void disable(void)
Disable propagators in space and compute fixpoint (make all idle)
Definition: int.cpp:367
Gecode::IntVarArray x
Variables to be tested.
Definition: int.hh:154
void enable(void)
Enable propagators in space.
Definition: int.cpp:362
void rel(int i, Gecode::IntRelType irt, int n)
Perform integer tell operation on x[i].
Definition: int.cpp:233
unsigned int propagators(void)
Return the number of propagators.
Definition: int.cpp:421
virtual bool run(void)
Perform test.
Definition: int.cpp:471
virtual bool ignore(const Assignment &) const
Whether to ignore assignment for reification.
Definition: int.cpp:462
virtual void post(Gecode::Space &home, Gecode::IntVarArray &x)=0
Post constraint.
virtual Assignment * assignment(void) const
Create assignment.
Definition: int.cpp:440
bool log
Whether to log the tests.
Definition: test.hh:91
Simple class for describing identation.
Definition: test.hh:66
void dom(Home home, FloatVar x, FloatVal n)
Propagates .
Definition: dom.cpp:40
void ignore(Actor &a, ActorProperty p, bool duplicate=false)
Ignore actor property.
Definition: core.hpp:4074
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVal n)
Propagates .
Definition: rel.cpp:43
Reify imp(BoolVar x)
Use implication for reification.
Definition: reify.hpp:73
IntRelType
Relation types for integers.
Definition: int.hh:925
Reify eqv(BoolVar x)
Use equivalence for reification.
Definition: reify.hpp:69
ReifyMode
Mode for reification.
Definition: int.hh:848
BoolOpType
Operation types for Booleans.
Definition: int.hh:950
Reify pmi(BoolVar x)
Use reverse implication for reification.
Definition: reify.hpp:77
IntPropLevel
Propagation levels for integer propagators.
Definition: int.hh:974
@ IRT_EQ
Equality ( )
Definition: int.hh:926
@ IRT_NQ
Disequality ( )
Definition: int.hh:927
@ IRT_GQ
Greater or equal ( )
Definition: int.hh:930
@ IRT_LE
Less ( )
Definition: int.hh:929
@ IRT_GR
Greater ( )
Definition: int.hh:931
@ IRT_LQ
Less or equal ( )
Definition: int.hh:928
@ RM_IMP
Implication for reification.
Definition: int.hh:862
@ RM_PMI
Inverse implication for reification.
Definition: int.hh:869
@ RM_EQV
Equivalence for reification (default)
Definition: int.hh:855
@ BOT_OR
Disjunction.
Definition: int.hh:952
@ BOT_EQV
Equivalence.
Definition: int.hh:954
@ BOT_IMP
Implication.
Definition: int.hh:953
@ BOT_XOR
Exclusive or.
Definition: int.hh:955
@ BOT_AND
Conjunction.
Definition: int.hh:951
@ IPL_BASIC
Use basic propagation algorithm.
Definition: int.hh:981
@ IPL_BASIC_ADVANCED
Use both.
Definition: int.hh:983
@ IPL_DOM
Domain propagation Options: basic versus advanced propagation.
Definition: int.hh:979
@ IPL_VAL
Value propagation.
Definition: int.hh:977
@ IPL_ADVANCED
Use advanced propagation algorithm.
Definition: int.hh:982
@ IPL_BND
Bounds propagation.
Definition: int.hh:978
SpaceStatus status(StatusStatistics &stat=unused_status)
Query space status.
Definition: core.cpp:252
Space * clone(CloneStatistics &stat=unused_clone) const
Clone space.
Definition: core.hpp:3224
@ SS_FAILED
Space is failed
Definition: core.hpp:1682
IntValBranch INT_VAL_MIN(void)
Select smallest value.
Definition: val.hpp:55
IntVarBranch INT_VAR_NONE(void)
Select first unassigned variable.
Definition: var.hpp:96
unsigned int size(I &i)
Size of all ranges of range iterator i.
Gecode::IntArgs i({1, 2, 3, 4})
Gecode::IntSet d(v, 7)
const int v[7]
Definition: distinct.cpp:259
@ CTL_BOUNDS_Z
Test for bounds(z)-consistency.
Definition: int.hh:143
@ CTL_BOUNDS_D
Test for bounds(d)-consistency.
Definition: int.hh:142
@ CTL_NONE
No consistency-test.
Definition: int.hh:140
@ CTL_DOMAIN
Test for domain-consistency.
Definition: int.hh:141
General test support.
Definition: afc.cpp:39
std::ostringstream olog
Stream used for logging.
Definition: test.cpp:53
Options opt
The options.
Definition: test.cpp:97
#define START_TEST(T)
Start new test.
Definition: int.cpp:454
#define CHECK_TEST(T, M)
Check the test result and handle failed test.
Definition: int.cpp:446