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