Generated on Sat Nov 9 2013 19:18:26 for Gecode by doxygen 1.8.4
eq.hpp
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  *
6  * Copyright:
7  * Christian Schulte, 2004
8  *
9  * Last modified:
10  * $Date: 2012-10-18 16:02:42 +0200 (Thu, 18 Oct 2012) $ by $Author: schulte $
11  * $Revision: 13154 $
12  *
13  * This file is part of Gecode, the generic constraint
14  * development environment:
15  * http://www.gecode.org
16  *
17  * Permission is hereby granted, free of charge, to any person obtaining
18  * a copy of this software and associated documentation files (the
19  * "Software"), to deal in the Software without restriction, including
20  * without limitation the rights to use, copy, modify, merge, publish,
21  * distribute, sublicense, and/or sell copies of the Software, and to
22  * permit persons to whom the Software is furnished to do so, subject to
23  * the following conditions:
24  *
25  * The above copyright notice and this permission notice shall be
26  * included in all copies or substantial portions of the Software.
27  *
28  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
29  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
30  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
31  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
32  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
33  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
34  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
35  *
36  */
37 
38 namespace Gecode { namespace Int { namespace Rel {
39 
40  /*
41  * Binary bounds consistent equality
42  *
43  */
44 
45  template<class View0, class View1>
47  EqBnd<View0,View1>::EqBnd(Home home, View0 x0, View1 x1)
48  : MixBinaryPropagator<View0,PC_INT_BND,View1,PC_INT_BND>(home,x0,x1) {}
49 
50  template<class View0, class View1>
52  EqBnd<View0,View1>::post(Home home, View0 x0, View1 x1){
53  if (x0.assigned()) {
54  GECODE_ME_CHECK(x1.eq(home,x0.val()));
55  } else if (x1.assigned()) {
56  GECODE_ME_CHECK(x0.eq(home,x1.val()));
57  } else if (!same(x0,x1)) {
58  GECODE_ME_CHECK(x0.lq(home,x1.max()));
59  GECODE_ME_CHECK(x1.lq(home,x0.max()));
60  GECODE_ME_CHECK(x0.gq(home,x1.min()));
61  GECODE_ME_CHECK(x1.gq(home,x0.min()));
62  (void) new (home) EqBnd<View0,View1>(home,x0,x1);
63  }
64  return ES_OK;
65  }
66 
67  template<class View0, class View1>
70  : MixBinaryPropagator<View0,PC_INT_BND,View1,PC_INT_BND>(home,share,p) {}
71 
72  template<class View0, class View1>
75  View0 x0, View1 x1)
76  : MixBinaryPropagator<View0,PC_INT_BND,View1,PC_INT_BND>(home,share,p,
77  x0,x1) {}
78 
79  template<class View0, class View1>
80  Actor*
81  EqBnd<View0,View1>::copy(Space& home, bool share) {
82  return new (home) EqBnd<View0,View1>(home,share,*this);
83  }
84 
85  template<class View0, class View1>
88  if (x0.assigned()) {
89  GECODE_ME_CHECK(x1.eq(home,x0.val()));
90  } else if (x1.assigned()) {
91  GECODE_ME_CHECK(x0.eq(home,x1.val()));
92  } else {
93  do {
94  GECODE_ME_CHECK(x0.gq(home,x1.min()));
95  GECODE_ME_CHECK(x1.gq(home,x0.min()));
96  } while (x0.min() != x1.min());
97  do {
98  GECODE_ME_CHECK(x0.lq(home,x1.max()));
99  GECODE_ME_CHECK(x1.lq(home,x0.max()));
100  } while (x0.max() != x1.max());
101  if (!x0.assigned())
102  return ES_FIX;
103  }
104  assert(x0.assigned() && x1.assigned());
105  return home.ES_SUBSUMED(*this);
106  }
107 
108  /*
109  * Binary domain consistent equality
110  *
111  */
112 
113  template<class View0, class View1>
115  EqDom<View0,View1>::EqDom(Home home, View0 x0, View1 x1)
116  : MixBinaryPropagator<View0,PC_INT_DOM,View1,PC_INT_DOM>(home,x0,x1) {}
117 
118  template<class View0, class View1>
119  ExecStatus
120  EqDom<View0,View1>::post(Home home, View0 x0, View1 x1){
121  if (x0.assigned()) {
122  GECODE_ME_CHECK(x1.eq(home,x0.val()));
123  } else if (x1.assigned()) {
124  GECODE_ME_CHECK(x0.eq(home,x1.val()));
125  } else if (!same(x0,x1)) {
126  GECODE_ME_CHECK(x0.lq(home,x1.max()));
127  GECODE_ME_CHECK(x1.lq(home,x0.max()));
128  GECODE_ME_CHECK(x0.gq(home,x1.min()));
129  GECODE_ME_CHECK(x1.gq(home,x0.min()));
130  (void) new (home) EqDom<View0,View1>(home,x0,x1);
131  }
132  return ES_OK;
133  }
134 
135 
136  template<class View0, class View1>
139  : MixBinaryPropagator<View0,PC_INT_DOM,View1,PC_INT_DOM>(home,share,p) {}
140 
141  template<class View0, class View1>
144  View0 x0, View1 x1)
145  : MixBinaryPropagator<View0,PC_INT_DOM,View1,PC_INT_DOM>(home,share,p,
146  x0,x1) {}
147 
148  template<class View0, class View1>
149  Actor*
150  EqDom<View0,View1>::copy(Space& home, bool share) {
151  return new (home) EqDom<View0,View1>(home,share,*this);
152  }
153 
154  template<class View0, class View1>
155  PropCost
156  EqDom<View0,View1>::cost(const Space&, const ModEventDelta& med) const {
157  if ((View0::me(med) == ME_INT_VAL) || (View1::me(med) == ME_INT_VAL))
159  else if ((View0::me(med) == ME_INT_DOM) || (View1::me(med) == ME_INT_DOM))
161  else
163  }
164 
165  template<class View0, class View1>
166  ExecStatus
168  if (x0.assigned()) {
169  GECODE_ME_CHECK(x1.eq(home,x0.val()));
170  return home.ES_SUBSUMED(*this);
171  }
172  if (x1.assigned()) {
173  GECODE_ME_CHECK(x0.eq(home,x1.val()));
174  return home.ES_SUBSUMED(*this);
175  }
176  if ((View0::me(med) != ME_INT_DOM) && (View1::me(med) != ME_INT_DOM)) {
177  do {
178  GECODE_ME_CHECK(x0.gq(home,x1.min()));
179  GECODE_ME_CHECK(x1.gq(home,x0.min()));
180  } while (x0.min() != x1.min());
181  do {
182  GECODE_ME_CHECK(x0.lq(home,x1.max()));
183  GECODE_ME_CHECK(x1.lq(home,x0.max()));
184  } while (x0.max() != x1.max());
185  if (x0.assigned())
186  return home.ES_SUBSUMED(*this);
187  if (x0.range() && x1.range())
188  return ES_FIX;
189  return home.ES_FIX_PARTIAL(*this,View0::med(ME_INT_DOM));
190  }
191  ViewRanges<View0> r0(x0);
192  GECODE_ME_CHECK(x1.inter_r(home,r0,shared(x0,x1)));
193  ViewRanges<View1> r1(x1);
194  GECODE_ME_CHECK(x0.narrow_r(home,r1,shared(x0,x1)));
195  if (x0.assigned())
196  return home.ES_SUBSUMED(*this);
197  return ES_FIX;
198  }
199 
200 
201 
202  /*
203  * Nary domain consistent equality
204  *
205  */
206 
207  template<class View>
210  : NaryPropagator<View,PC_INT_DOM>(home,x) {}
211 
212  template<class View>
213  ExecStatus
215  x.unique(home);
216  if (x.size() == 2) {
217  return EqDom<View,View>::post(home,x[0],x[1]);
218  } else if (x.size() > 2) {
219  int l = x[0].min();
220  int u = x[0].max();
221  for (int i=x.size(); i-- > 1; ) {
222  l = std::max(l,x[i].min());
223  u = std::min(u,x[i].max());
224  }
225  for (int i=x.size(); i--; ) {
226  GECODE_ME_CHECK(x[i].gq(home,l));
227  GECODE_ME_CHECK(x[i].lq(home,u));
228  }
229  (void) new (home) NaryEqDom<View>(home,x);
230  }
231  return ES_OK;
232  }
233 
234  template<class View>
237  : NaryPropagator<View,PC_INT_DOM>(home,share,p) {}
238 
239  template<class View>
240  Actor*
241  NaryEqDom<View>::copy(Space& home, bool share) {
242  return new (home) NaryEqDom<View>(home,share,*this);
243  }
244 
245  template<class View>
246  PropCost
247  NaryEqDom<View>::cost(const Space&, const ModEventDelta& med) const {
248  if (View::me(med) == ME_INT_VAL)
250  else
251  return PropCost::linear((View::me(med) == ME_INT_DOM) ?
252  PropCost::LO : PropCost::HI, x.size());
253  }
254 
255  template<class View>
256  ExecStatus
258  assert(x.size() > 2);
259 
260  ModEvent me = View::me(med);
261  if (me == ME_INT_VAL) {
262  // One of the variables is assigned
263  for (int i = 0; ; i++)
264  if (x[i].assigned()) {
265  int n = x[i].val();
266  x.move_lst(i);
267  for (int j = x.size(); j--; )
268  GECODE_ME_CHECK(x[j].eq(home,n));
269  return home.ES_SUBSUMED(*this);
270  }
271  GECODE_NEVER;
272  }
273 
274  if (me == ME_INT_BND) {
275  {
276  // One of the mins has changed
277  int mn = x[0].min();
278  restart_min:
279  for (int i = x.size(); i--; ) {
280  GECODE_ME_CHECK(x[i].gq(home,mn));
281  if (mn < x[i].min()) {
282  mn = x[i].min();
283  goto restart_min;
284  }
285  }
286  }
287  {
288  // One of the maxs has changed
289  int mx = x[0].max();
290  restart_max:
291  for (int i = x.size(); i--; ) {
292  GECODE_ME_CHECK(x[i].lq(home,mx));
293  if (mx > x[i].max()) {
294  mx = x[i].max();
295  goto restart_max;
296  }
297  }
298  }
299  if (x[0].assigned())
300  return home.ES_SUBSUMED(*this);
301  return home.ES_FIX_PARTIAL(*this,View::med(ME_INT_DOM));
302  }
303 
304  int n = x.size();
305 
306  Region re(home);
308  for (int i = n; i--; ) {
309  ViewRanges<View> i_xi(x[i]);
310  i_x[i] = i_xi;
311  }
312  Iter::Ranges::NaryInter r(re,i_x,n);
313 
314  if (!r())
315  return ES_FAILED;
316  ++r;
317  if (!r()) {
318  r.reset();
319  for (int i = n; i--; ) {
320  GECODE_ME_CHECK(x[i].gq(home,r.min()));
321  GECODE_ME_CHECK(x[i].lq(home,r.max()));
322  }
323  } else {
324  for (int i = n; i--; ) {
325  r.reset();
326  GECODE_ME_CHECK(x[i].narrow_r(home,r,false));
327  }
328  }
329  return ES_FIX;
330  }
331 
332 
333 
334  /*
335  * Nary bound consistent equality
336  *
337  */
338 
339  template<class View>
342  : NaryPropagator<View,PC_INT_BND>(home,x) {}
343 
344  template<class View>
345  ExecStatus
347  x.unique(home);
348  if (x.size() == 2) {
349  return EqBnd<View,View>::post(home,x[0],x[1]);
350  } else if (x.size() > 2) {
351  int l = x[0].min();
352  int u = x[0].max();
353  for (int i=x.size(); i-- > 1; ) {
354  l = std::max(l,x[i].min());
355  u = std::min(u,x[i].max());
356  }
357  for (int i=x.size(); i--; ) {
358  GECODE_ME_CHECK(x[i].gq(home,l));
359  GECODE_ME_CHECK(x[i].lq(home,u));
360  }
361  (void) new (home) NaryEqBnd<View>(home,x);
362  }
363  return ES_OK;
364  }
365 
366  template<class View>
369  : NaryPropagator<View,PC_INT_BND>(home,share,p) {}
370 
371  template<class View>
372  Actor*
373  NaryEqBnd<View>::copy(Space& home, bool share) {
374  return new (home) NaryEqBnd<View>(home,share,*this);
375  }
376 
377  template<class View>
378  PropCost
379  NaryEqBnd<View>::cost(const Space&, const ModEventDelta& med) const {
380  if (View::me(med) == ME_INT_VAL)
382  else
383  return PropCost::linear(PropCost::LO, x.size());
384  }
385 
386  template<class View>
387  ExecStatus
389  assert(x.size() > 2);
390  if (View::me(med) == ME_INT_VAL) {
391  // One of the variables is assigned
392  for (int i = 0; ; i++)
393  if (x[i].assigned()) {
394  int n = x[i].val();
395  x.move_lst(i);
396  for (int j = x.size(); j--; )
397  GECODE_ME_CHECK(x[j].eq(home,n));
398  return home.ES_SUBSUMED(*this);
399  }
400  GECODE_NEVER;
401  }
402 
403  int mn = x[0].min();
404  restart_min:
405  for (int i = x.size(); i--; ) {
406  GECODE_ME_CHECK(x[i].gq(home,mn));
407  if (mn < x[i].min()) {
408  mn = x[i].min();
409  goto restart_min;
410  }
411  }
412  int mx = x[0].max();
413  restart_max:
414  for (int i = x.size(); i--; ) {
415  GECODE_ME_CHECK(x[i].lq(home,mx));
416  if (mx > x[i].max()) {
417  mx = x[i].max();
418  goto restart_max;
419  }
420  }
421  return x[0].assigned() ? home.ES_SUBSUMED(*this) : ES_FIX;
422  }
423 
424 
425 
426  /*
427  * Reified domain consistent equality
428  *
429  */
430 
431  template<class View, class CtrlView, ReifyMode rm>
433  ReEqDom<View,CtrlView,rm>::ReEqDom(Home home, View x0, View x1, CtrlView b)
434  : ReBinaryPropagator<View,PC_INT_DOM,CtrlView>(home,x0,x1,b) {}
435 
436  template<class View, class CtrlView, ReifyMode rm>
437  ExecStatus
438  ReEqDom<View,CtrlView,rm>::post(Home home, View x0, View x1, CtrlView b) {
439  if (b.one()) {
440  if (rm == RM_PMI)
441  return ES_OK;
442  return EqDom<View,View>::post(home,x0,x1);
443  }
444  if (b.zero()) {
445  if (rm == RM_IMP)
446  return ES_OK;
447  return Nq<View>::post(home,x0,x1);
448  }
449  if (!same(x0,x1)) {
450  (void) new (home) ReEqDom(home,x0,x1,b);
451  } else if (rm != RM_IMP) {
452  GECODE_ME_CHECK(b.one(home));
453  }
454  return ES_OK;
455  }
456 
457 
458  template<class View, class CtrlView, ReifyMode rm>
461  : ReBinaryPropagator<View,PC_INT_DOM,CtrlView>(home,share,p) {}
462 
463  template<class View, class CtrlView, ReifyMode rm>
464  Actor*
466  return new (home) ReEqDom<View,CtrlView,rm>(home,share,*this);
467  }
468 
469  template<class View, class CtrlView, ReifyMode rm>
470  ExecStatus
472  if (b.one()) {
473  if (rm == RM_PMI)
474  return home.ES_SUBSUMED(*this);
475  GECODE_REWRITE(*this,(EqDom<View,View>::post(home(*this),x0,x1)));
476  }
477  if (b.zero()) {
478  if (rm == RM_IMP)
479  return home.ES_SUBSUMED(*this);
480  GECODE_REWRITE(*this,Nq<View>::post(home(*this),x0,x1));
481  }
482  switch (rtest_eq_dom(x0,x1)) {
483  case RT_TRUE:
484  if (rm != RM_IMP)
485  GECODE_ME_CHECK(b.one_none(home));
486  break;
487  case RT_FALSE:
488  if (rm != RM_PMI)
489  GECODE_ME_CHECK(b.zero_none(home));
490  break;
491  case RT_MAYBE:
492  return ES_FIX;
493  default: GECODE_NEVER;
494  }
495  return home.ES_SUBSUMED(*this);
496  }
497 
498 
499 
500  /*
501  * Reified bounds consistent equality
502  *
503  */
504 
505  template<class View, class CtrlView, ReifyMode rm>
507  ReEqBnd<View,CtrlView,rm>::ReEqBnd(Home home, View x0, View x1, CtrlView b)
508  : ReBinaryPropagator<View,PC_INT_BND,CtrlView>(home,x0,x1,b) {}
509 
510  template<class View, class CtrlView, ReifyMode rm>
511  ExecStatus
512  ReEqBnd<View,CtrlView,rm>::post(Home home, View x0, View x1, CtrlView b){
513  if (b.one()) {
514  if (rm == RM_PMI)
515  return ES_OK;
516  return EqBnd<View,View>::post(home,x0,x1);
517  }
518  if (b.zero()) {
519  if (rm == RM_IMP)
520  return ES_OK;
521  return Nq<View>::post(home,x0,x1);
522  }
523  if (!same(x0,x1)) {
524  (void) new (home) ReEqBnd(home,x0,x1,b);
525  } else if (rm != RM_IMP) {
526  GECODE_ME_CHECK(b.one(home));
527  }
528  return ES_OK;
529  }
530 
531 
532  template<class View, class CtrlView, ReifyMode rm>
535  : ReBinaryPropagator<View,PC_INT_BND,CtrlView>(home,share,p) {}
536 
537  template<class View, class CtrlView, ReifyMode rm>
538  Actor*
540  return new (home) ReEqBnd<View,CtrlView,rm>(home,share,*this);
541  }
542 
543  template<class View, class CtrlView, ReifyMode rm>
544  ExecStatus
546  if (b.one()) {
547  if (rm == RM_PMI)
548  return home.ES_SUBSUMED(*this);
549  GECODE_REWRITE(*this,(EqBnd<View,View>::post(home(*this),x0,x1)));
550  }
551  if (b.zero()) {
552  if (rm == RM_IMP)
553  return home.ES_SUBSUMED(*this);
554  GECODE_REWRITE(*this,Nq<View>::post(home(*this),x0,x1));
555  }
556  switch (rtest_eq_bnd(x0,x1)) {
557  case RT_TRUE:
558  if (rm != RM_IMP)
559  GECODE_ME_CHECK(b.one_none(home));
560  break;
561  case RT_FALSE:
562  if (rm != RM_PMI)
563  GECODE_ME_CHECK(b.zero_none(home));
564  break;
565  case RT_MAYBE:
566  return ES_FIX;
567  default: GECODE_NEVER;
568  }
569  return home.ES_SUBSUMED(*this);
570  }
571 
572 
573 
574 
575  /*
576  * Reified domain consistent equality (one variable)
577  *
578  */
579 
580  template<class View, class CtrlView, ReifyMode rm>
583  (Home home, View x, int c0, CtrlView b)
585 
586  template<class View, class CtrlView, ReifyMode rm>
587  ExecStatus
588  ReEqDomInt<View,CtrlView,rm>::post(Home home, View x, int c, CtrlView b) {
589  if (b.one()) {
590  if (rm != RM_PMI)
591  GECODE_ME_CHECK(x.eq(home,c));
592  } else if (b.zero()) {
593  if (rm != RM_IMP)
594  GECODE_ME_CHECK(x.nq(home,c));
595  } else if (x.assigned()) {
596  assert(b.none());
597  if (x.val() == c) {
598  if (rm != RM_IMP)
599  GECODE_ME_CHECK(b.one_none(home));
600  } else {
601  if (rm != RM_PMI)
602  GECODE_ME_CHECK(b.zero_none(home));
603  }
604  } else {
605  (void) new (home) ReEqDomInt(home,x,c,b);
606  }
607  return ES_OK;
608  }
609 
610 
611  template<class View, class CtrlView, ReifyMode rm>
614  ReEqDomInt& p)
615  : ReUnaryPropagator<View,PC_INT_DOM,CtrlView>(home,share,p), c(p.c) {}
616 
617  template<class View, class CtrlView, ReifyMode rm>
618  Actor*
620  return new (home) ReEqDomInt<View,CtrlView,rm>(home,share,*this);
621  }
622 
623  template<class View, class CtrlView, ReifyMode rm>
624  ExecStatus
626  if (b.one()) {
627  if (rm != RM_PMI)
628  GECODE_ME_CHECK(x0.eq(home,c));
629  } else if (b.zero()) {
630  if (rm != RM_IMP)
631  GECODE_ME_CHECK(x0.nq(home,c));
632  } else {
633  switch (rtest_eq_dom(x0,c)) {
634  case RT_TRUE:
635  if (rm != RM_IMP)
636  GECODE_ME_CHECK(b.one_none(home));
637  break;
638  case RT_FALSE:
639  if (rm != RM_PMI)
640  GECODE_ME_CHECK(b.zero_none(home));
641  break;
642  case RT_MAYBE:
643  return ES_FIX;
644  default: GECODE_NEVER;
645  }
646  }
647  return home.ES_SUBSUMED(*this);
648  }
649 
650 
651 
652 
653  /*
654  * Reified bounds consistent equality (one variable)
655  *
656  */
657 
658  template<class View, class CtrlView, ReifyMode rm>
661  (Home home, View x, int c0, CtrlView b)
663 
664  template<class View, class CtrlView, ReifyMode rm>
665  ExecStatus
666  ReEqBndInt<View,CtrlView,rm>::post(Home home, View x, int c, CtrlView b) {
667  if (b.one()) {
668  if (rm != RM_PMI)
669  GECODE_ME_CHECK(x.eq(home,c));
670  } else if (b.zero()) {
671  if (rm != RM_IMP)
672  GECODE_ME_CHECK(x.nq(home,c));
673  } else if (x.assigned()) {
674  assert(b.none());
675  if (x.val() == c) {
676  if (rm != RM_IMP)
677  GECODE_ME_CHECK(b.one_none(home));
678  } else {
679  if (rm != RM_PMI)
680  GECODE_ME_CHECK(b.zero_none(home));
681  }
682  } else {
683  (void) new (home) ReEqBndInt(home,x,c,b);
684  }
685  return ES_OK;
686  }
687 
688 
689  template<class View, class CtrlView, ReifyMode rm>
692  : ReUnaryPropagator<View,PC_INT_BND,CtrlView>(home,share,p), c(p.c) {}
693 
694  template<class View, class CtrlView, ReifyMode rm>
695  Actor*
697  return new (home) ReEqBndInt<View,CtrlView,rm>(home,share,*this);
698  }
699 
700  template<class View, class CtrlView, ReifyMode rm>
701  ExecStatus
703  if (b.one()) {
704  if (rm != RM_PMI)
705  GECODE_ME_CHECK(x0.eq(home,c));
706  } else if (b.zero()) {
707  if (rm != RM_IMP)
708  GECODE_ME_CHECK(x0.nq(home,c));
709  } else {
710  switch (rtest_eq_bnd(x0,c)) {
711  case RT_TRUE:
712  if (rm != RM_IMP)
713  GECODE_ME_CHECK(b.one_none(home));
714  break;
715  case RT_FALSE:
716  if (rm != RM_PMI)
717  GECODE_ME_CHECK(b.zero_none(home));
718  break;
719  case RT_MAYBE:
720  return ES_FIX;
721  default: GECODE_NEVER;
722  }
723  }
724  return home.ES_SUBSUMED(*this);
725  }
726 
727 }}}
728 
729 // STATISTICS: int-prop