Generated on Thu Apr 11 13:59:19 2019 for Gecode by doxygen 1.6.3

minmax.hpp

Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
00002 /*
00003  *  Main authors:
00004  *     Guido Tack <tack@gecode.org>
00005  *     Christian Schulte <schulte@gecode.org>
00006  *     Gabor Szokoli <szokoli@gecode.org>
00007  *     Denys Duchier <denys.duchier@univ-orleans.fr>
00008  *
00009  *  Copyright:
00010  *     Guido Tack, 2004
00011  *     Christian Schulte, 2004
00012  *     Gabor Szokoli, 2004
00013  *
00014  *  This file is part of Gecode, the generic constraint
00015  *  development environment:
00016  *     http://www.gecode.org
00017  *
00018  *  Permission is hereby granted, free of charge, to any person obtaining
00019  *  a copy of this software and associated documentation files (the
00020  *  "Software"), to deal in the Software without restriction, including
00021  *  without limitation the rights to use, copy, modify, merge, publish,
00022  *  distribute, sublicense, and/or sell copies of the Software, and to
00023  *  permit persons to whom the Software is furnished to do so, subject to
00024  *  the following conditions:
00025  *
00026  *  The above copyright notice and this permission notice shall be
00027  *  included in all copies or substantial portions of the Software.
00028  *
00029  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00030  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00031  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00032  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00033  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00034  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00035  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00036  *
00037  */
00038 
00039 
00040 
00041 #include <gecode/set.hh>
00042 #include <gecode/int.hh>
00043 
00044 namespace Gecode { namespace Set { namespace Int {
00045 
00046   template<class View>
00047   forceinline
00048   MinElement<View>::MinElement(Home home, View y0, Gecode::Int::IntView y1)
00049     : MixBinaryPropagator<View,PC_SET_ANY,Gecode::Int::IntView,Gecode::Int::PC_INT_BND> (home, y0, y1) {}
00050 
00051   template<class View>
00052   forceinline ExecStatus
00053   MinElement<View>::post(Home home, View x0, Gecode::Int::IntView x1) {
00054     GECODE_ME_CHECK(x0.cardMin(home,1));
00055     (void) new (home) MinElement(home,x0,x1);
00056     return ES_OK;
00057   }
00058 
00059   template<class View>
00060   forceinline
00061   MinElement<View>::MinElement(Space& home, MinElement& p)
00062     : MixBinaryPropagator<View,PC_SET_ANY,Gecode::Int::IntView,Gecode::Int::PC_INT_BND> (home, p) {}
00063 
00064   template<class View>
00065   Actor*
00066   MinElement<View>::copy(Space& home) {
00067    return new (home) MinElement(home,*this);
00068   }
00069 
00070   template<class View>
00071   ExecStatus
00072   MinElement<View>::propagate(Space& home, const ModEventDelta&) {
00073     //x1 is an element of x0.ub
00074     //x1 =< smallest element of x0.lb
00075     //x1 =< x0.cardinialityMin-est largest element of x0.ub
00076     //(these 2 take care of determined x0)
00077     //No element in x0 is smaller than x1
00078     //if x1 is determined, it is part of the ub.
00079 
00080     //Consequently:
00081     //The domain of x1 is a subset of x0.ub up to the first element in x0.lb.
00082     //x0 lacks everything smaller than smallest possible x1.
00083 
00084     {
00085       LubRanges<View> ub(x0);
00086       GECODE_ME_CHECK(x1.inter_r(home,ub,false));
00087     }
00088     GECODE_ME_CHECK(x1.lq(home,x0.glbMin()));
00089     //if cardMin>lbSize?
00090     assert(x0.cardMin()>=1);
00091 
00092     {
00094       unsigned int size = 0;
00095       int maxN = BndSet::MAX_OF_EMPTY;
00096       for (LubRanges<View> ubr(x0); ubr(); ++ubr, ++size) {}
00097       Region r;
00098       int* ub = r.alloc<int>(size*2);
00099       {
00100         int i=0;
00101         for (LubRanges<View> ubr(x0); ubr(); ++ubr, ++i) {
00102           ub[2*i]   = ubr.min();
00103           ub[2*i+1] = ubr.max();
00104         }
00105       }
00106       unsigned int x0cm = x0.cardMin()-1;
00107       for (unsigned int i=size; i--;) {
00108         unsigned int width = static_cast<unsigned int>(ub[2*i+1]-ub[2*i]+1);
00109         if (width > x0cm) {
00110           maxN = static_cast<int>(ub[2*i+1]-x0cm);
00111           break;
00112         }
00113         x0cm -= width;
00114       }
00115       GECODE_ME_CHECK(x1.lq(home,maxN));
00116     }
00117 
00118     GECODE_ME_CHECK( x0.exclude(home,
00119                                 Limits::min, x1.min()-1) );
00120 
00121     if (x1.assigned()) {
00122       GECODE_ME_CHECK(x0.include(home,x1.val()));
00123       GECODE_ME_CHECK(x0.exclude(home,
00124                                  Limits::min, x1.val()-1));
00125       return home.ES_SUBSUMED(*this);
00126     }
00127 
00128     return ES_FIX;
00129   }
00130 
00131 
00132   template<class View>
00133   forceinline
00134   NotMinElement<View>::NotMinElement(Home home, View y0,
00135                                      Gecode::Int::IntView y1)
00136     : MixBinaryPropagator<View,PC_SET_ANY,
00137       Gecode::Int::IntView,Gecode::Int::PC_INT_DOM> (home, y0, y1) {}
00138 
00139   template<class View>
00140   forceinline ExecStatus
00141   NotMinElement<View>::post(Home home, View x0, Gecode::Int::IntView x1) {
00142     (void) new (home) NotMinElement(home,x0,x1);
00143     return ES_OK;
00144   }
00145 
00146   template<class View>
00147   forceinline
00148   NotMinElement<View>::NotMinElement(Space& home, NotMinElement& p)
00149     : MixBinaryPropagator<View,PC_SET_ANY,
00150       Gecode::Int::IntView,Gecode::Int::PC_INT_DOM> (home, p) {}
00151 
00152   template<class View>
00153   Actor*
00154   NotMinElement<View>::copy(Space& home) {
00155     return new (home) NotMinElement(home,*this);
00156   }
00157 
00158   template<class View>
00159   ExecStatus
00160   NotMinElement<View>::propagate(Space& home, const ModEventDelta&) {
00161     // cheap tests for entailment:
00162     // if x0 is empty, then entailed
00163     // if max(x1) < min(x0.lub) or min(x1) > max(x0.lub), then entailed
00164     // if min(x0.glb) < min(x1), then entailed
00165     if ((x0.cardMax() == 0) ||
00166         ((x1.max() < x0.lubMin()) || (x1.min() > x0.lubMax())) ||
00167         ((x0.glbSize() > 0) && (x0.glbMin() < x1.min())))
00168       return home.ES_SUBSUMED(*this);
00169     // if x1 is determined and = x0.lub.min: remove it from x0,
00170     // then entailed
00171     if (x1.assigned() && x1.val()==x0.lubMin()) {
00172       GECODE_ME_CHECK(x0.exclude(home,x1.val()));
00173       return home.ES_SUBSUMED(*this);
00174     }
00175     // if min(x0) is decided: remove min(x0) from the domain of x1
00176     // then entailed
00177     if (x0.glbMin() == x0.lubMin()) {
00178       GECODE_ME_CHECK(x1.nq(home,x0.glbMin()));
00179       return home.ES_SUBSUMED(*this);
00180     }
00181     // if x1 is determined and = x0.glb.min, then we need at least
00182     // one more element; if there is only one below, then we must
00183     // take it.
00184     if (x1.assigned() && x0.glbSize() > 0 && x1.val()==x0.glbMin()) {
00185       unsigned int oldGlbSize = x0.glbSize();
00186       // if there is only 1 unknown below x1, then we must take it
00187       UnknownRanges<View> ur(x0);
00188       assert(ur());
00189       // the iterator is not empty: otherwise x0 would be determined
00190       // and min(x0) would have been decided and the preceding if
00191       // would have caught it.  Also, the first range is not above
00192       // x1 otherwise the very first if would have caught it.
00193       // so let's check if the very first range of unknowns is of
00194       // size 1 and there is no second one or it starts above x1.
00195       if (ur.width()==1) {
00196         int i=ur.min();
00197         ++ur;
00198         if (!ur() || ur.min()>x1.val()) {
00199           GECODE_ME_CHECK(x0.include(home,i));
00200           return home.ES_SUBSUMED(*this);
00201         }
00202       }
00203       GECODE_ME_CHECK(x0.cardMin(home, oldGlbSize+1));
00204     }
00205     // if dom(x1) and lub(x0) are disjoint, then entailed;
00206     {
00207       LubRanges<View> ub(x0);
00208       Gecode::Int::ViewRanges<Gecode::Int::IntView> d(x1);
00209       Gecode::Iter::Ranges::Inter<LubRanges<View>,
00210         Gecode::Int::ViewRanges<Gecode::Int::IntView> > ir(ub,d);
00211       if (!ir()) return home.ES_SUBSUMED(*this);
00212     }
00213     // x0 is fated to eventually contain at least x0.cardMin elements.
00214     // therefore min(x0) <= x0.cardMin-th largest element of x0.lub
00215     // if x1 > than that, then entailed.
00216     {
00217       // to find the x0.cardMin-th largest element of x0.lub, we need
00218       // some sort of reverse range iterator. we will need to fake one
00219       // by storing the ranges of the forward iterator in an array.
00220       // first we need to know how large the array needs to be. so, let's
00221       // count the ranges:
00222       int num_ranges = 0;
00223       for (LubRanges<View> ur(x0); ur(); ++ur, ++num_ranges) {}
00224       // create an array for storing min and max of each range
00225       Region r;
00226       int* _ur = r.alloc<int>(num_ranges*2);
00227       // now, we fill the array:
00228       {
00229         int i = 0;
00230         for (LubRanges<View> ur(x0); ur(); ++ur, ++i) {
00231           _ur[2*i  ] = ur.min();
00232           _ur[2*i+1] = ur.max();
00233         }
00234       }
00235       // now we search from the top the range that contains the
00236       // nth largest value.
00237       unsigned int n = x0.cardMin();
00238       int nth_largest = BndSet::MAX_OF_EMPTY;
00239       for (int i=num_ranges; i--; ) {
00240         // number of values in range
00241         unsigned int num_values = static_cast<unsigned int>(_ur[2*i+1]-_ur[2*i]+1);
00242         // does the range contain the value?
00243         if (num_values >= n) {
00244           // record it and exit the loop
00245           nth_largest = static_cast<int>(_ur[2*i+1]-n+1);
00246           break;
00247         }
00248         // otherwise, we skipped num_values
00249         n -= num_values;
00250       }
00251       // if x1.min > nth_largest, then entailed
00252       if (x1.min() > nth_largest)
00253         return home.ES_SUBSUMED(*this);
00254     }
00255     return ES_FIX;
00256   }
00257 
00258   template<class View, ReifyMode rm>
00259   forceinline
00260   ReMinElement<View,rm>::ReMinElement(Home home, View y0,
00261                                       Gecode::Int::IntView y1,
00262                                       Gecode::Int::BoolView b2)
00263     : Gecode::Int::ReMixBinaryPropagator<View,PC_SET_ANY,
00264       Gecode::Int::IntView,Gecode::Int::PC_INT_DOM,
00265       Gecode::Int::BoolView> (home, y0, y1, b2) {}
00266 
00267   template<class View, ReifyMode rm>
00268   forceinline ExecStatus
00269   ReMinElement<View,rm>::post(Home home, View x0, Gecode::Int::IntView x1,
00270                               Gecode::Int::BoolView b2) {
00271     (void) new (home) ReMinElement(home,x0,x1,b2);
00272     return ES_OK;
00273   }
00274 
00275   template<class View, ReifyMode rm>
00276   forceinline
00277   ReMinElement<View,rm>::ReMinElement(Space& home, ReMinElement& p)
00278     : Gecode::Int::ReMixBinaryPropagator<View,PC_SET_ANY,
00279       Gecode::Int::IntView,Gecode::Int::PC_INT_DOM,
00280       Gecode::Int::BoolView> (home, p) {}
00281 
00282   template<class View, ReifyMode rm>
00283   Actor*
00284   ReMinElement<View,rm>::copy(Space& home) {
00285    return new (home) ReMinElement(home,*this);
00286   }
00287 
00288   template<class View, ReifyMode rm>
00289   ExecStatus
00290   ReMinElement<View,rm>::propagate(Space& home, const ModEventDelta&) {
00291     // check if b is determined
00292     if (b.one()) {
00293       if (rm == RM_PMI)
00294         return home.ES_SUBSUMED(*this);
00295       GECODE_REWRITE(*this, (MinElement<View>::post(home(*this),x0,x1)));
00296     }
00297     if (b.zero()) {
00298       if (rm == RM_IMP)
00299         return home.ES_SUBSUMED(*this);
00300       GECODE_REWRITE(*this, (NotMinElement<View>::post(home(*this),x0,x1)));
00301     }
00302     // cheap tests for => b=0
00303     // if x0 is empty, then b=0 and entailed
00304     // if max(x1) < min(x0.lub) or min(x1) > max(x0.lub), then b=0 and entailed
00305     // if min(x0.glb) < min(x1), then b=0 and entailed
00306     if ((x0.cardMax() == 0) ||
00307         ((x1.max() < x0.lubMin()) || (x1.min() > x0.lubMax())) ||
00308         ((x0.glbSize() > 0) && (x0.glbMin() < x1.min())))
00309       {
00310         if (rm != RM_PMI)
00311           GECODE_ME_CHECK(b.zero(home));
00312         return home.ES_SUBSUMED(*this);
00313       }
00314     // if min(x0) is decided
00315     if (x0.glbMin() == x0.lubMin()) {
00316       // if x1 is det: check if = min(x0), assign b, entailed
00317       if (x1.assigned()) {
00318         if (x1.val() == x0.glbMin()) {
00319           if (rm != RM_IMP)
00320             GECODE_ME_CHECK(b.one(home));
00321         } else {
00322           if (rm != RM_PMI)
00323             GECODE_ME_CHECK(b.zero(home));
00324         }
00325         return home.ES_SUBSUMED(*this);
00326       }
00327       // if min(x0) not in dom(x1): b=0, entailed
00328       else if ((x0.glbMin() < x1.min()) ||
00329                (x0.glbMin() > x1.max()) ||
00330                !x1.in(x0.glbMin()))
00331         {
00332           if (rm != RM_PMI)
00333             GECODE_ME_CHECK(b.zero(home));
00334           return home.ES_SUBSUMED(*this);
00335         }
00336     }
00337     // // if dom(x1) and lub(x0) are disjoint, then b=0, entailed;
00338     // {
00339     //   LubRanges<View> ub(x0);
00340     //   Gecode::Int::ViewRanges<Gecode::Int::IntView> d(x1);
00341     //   Gecode::Iter::Ranges::Inter<LubRanges<View>,
00342     //     Gecode::Int::ViewRanges<Gecode::Int::IntView> > ir(ub,d);
00343     //   if (!ir()) {
00344     //     GECODE_ME_CHECK(b.zero(home));
00345     //     return home.ES_SUBSUMED(*this);
00346     //   }
00347     // }
00348     // // x0 is fated to eventually contain at least x0.cardMin elements.
00349     // // therefore min(x0) <= x0.cardMin-th largest element of x0.lub
00350     // // if x1 > than that, then b=0 and entailed.
00351     // {
00352     //   // to find the x0.cardMin-th largest element of x0.lub, we need
00353     //   // some sort of reverse range iterator. we will need to fake one
00354     //   // by storing the ranges of the forward iterator in an array.
00355     //   // first we need to know how large the array needs to be. so, let's
00356     //   // count the ranges:
00357     //   int num_ranges = 0;
00358     //   for (LubRanges<View> ur(x0); ur(); ++ur, ++num_ranges) {}
00359     //   // create an array for storing min and max of each range
00360     //   Region re(home);
00361     //   int* _ur = re.alloc<int>(num_ranges*2);
00362     //   // now, we fill the array:
00363     //   int i = 0;
00364     //   for (LubRanges<View> ur(x0); ur(); ++ur, ++i) {
00365     //     _ur[2*i  ] = ur.min();
00366     //     _ur[2*i+1] = ur.max();
00367     //   }
00368     //   // now we search from the top the range that contains the
00369     //   // nth largest value.
00370     //   int n = x0.cardMin();
00371     //   int nth_largest = BndSet::MAX_OF_EMPTY;
00372     //   for (int i=num_ranges; i--; ) {
00373     //     // number of values in range
00374     //     int num_values = _ur[2*i+1]-_ur[2*i]+1;
00375     //     // does the range contain the value?
00376     //     if (num_values >= n)
00377     //       {
00378     //         // record it and exit the loop
00379     //         nth_largest = _ur[2*i+1]-n+1;
00380     //         break;
00381     //       }
00382     //     // otherwise, we skipped num_values
00383     //     n -= num_values;
00384     //   }
00385     //   // if x1.min > nth_largest, then entailed
00386     //   if (x1.min() > nth_largest) {
00387     //     GECODE_ME_CHECK(b.zero(home));
00388     //     return home.ES_SUBSUMED(*this);
00389     //   }
00390     // }
00391     return ES_FIX;
00392   }
00393 
00394   template<class View>
00395   forceinline
00396   MaxElement<View>::MaxElement(Home home, View y0, Gecode::Int::IntView y1)
00397     : MixBinaryPropagator<View,PC_SET_ANY,
00398       Gecode::Int::IntView,Gecode::Int::PC_INT_BND> (home, y0, y1) {}
00399 
00400   template<class View>
00401   forceinline
00402   MaxElement<View>::MaxElement(Space& home, MaxElement& p)
00403     : MixBinaryPropagator<View,PC_SET_ANY,
00404       Gecode::Int::IntView,Gecode::Int::PC_INT_BND> (home, p) {}
00405 
00406   template<class View>
00407   ExecStatus
00408   MaxElement<View>::post(Home home, View x0,
00409                               Gecode::Int::IntView x1) {
00410     GECODE_ME_CHECK(x0.cardMin(home,1));
00411     (void) new (home) MaxElement(home,x0,x1);
00412     return ES_OK;
00413   }
00414 
00415   template<class View>
00416   Actor*
00417   MaxElement<View>::copy(Space& home) {
00418     return new (home) MaxElement(home,*this);
00419   }
00420 
00421   template<class View>
00422   ExecStatus
00423   MaxElement<View>::propagate(Space& home, const ModEventDelta&) {
00424     LubRanges<View> ub(x0);
00425     GECODE_ME_CHECK(x1.inter_r(home,ub,false));
00426     GECODE_ME_CHECK(x1.gq(home,x0.glbMax()));
00427     assert(x0.cardMin()>=1);
00428     GECODE_ME_CHECK(x1.gq(home,x0.lubMinN(x0.cardMin()-1)));
00429     GECODE_ME_CHECK(x0.exclude(home,
00430                                x1.max()+1,Limits::max) );
00431 
00432     if (x1.assigned()) {
00433       GECODE_ME_CHECK(x0.include(home,x1.val()));
00434       GECODE_ME_CHECK( x0.exclude(home,
00435                                   x1.val()+1,Limits::max) );
00436       return home.ES_SUBSUMED(*this);
00437     }
00438 
00439     return ES_FIX;
00440   }
00441 
00442   template<class View>
00443   forceinline
00444   NotMaxElement<View>::NotMaxElement(Home home, View y0,
00445                                      Gecode::Int::IntView y1)
00446     : MixBinaryPropagator<View,PC_SET_ANY,
00447       Gecode::Int::IntView,Gecode::Int::PC_INT_DOM> (home, y0, y1) {}
00448 
00449   template<class View>
00450   forceinline
00451   NotMaxElement<View>::NotMaxElement(Space& home, NotMaxElement& p)
00452     : MixBinaryPropagator<View,PC_SET_ANY,
00453       Gecode::Int::IntView,Gecode::Int::PC_INT_DOM> (home, p) {}
00454 
00455   template<class View>
00456   ExecStatus
00457   NotMaxElement<View>::post(Home home, View x0, Gecode::Int::IntView x1) {
00458     (void) new (home) NotMaxElement(home,x0,x1);
00459     return ES_OK;
00460   }
00461 
00462   template<class View>
00463   Actor*
00464   NotMaxElement<View>::copy(Space& home) {
00465     return new (home) NotMaxElement(home,*this);
00466   }
00467 
00468   template<class View>
00469   ExecStatus
00470   NotMaxElement<View>::propagate(Space& home, const ModEventDelta&) {
00471     // cheap tests for entailment:
00472     // if x0 is empty, then entailed
00473     // if max(x1) < min(x0.lub) or min(x1) > max(x0.lub), then entailed
00474     // if max(x0.glb) > max(x1), then entailed
00475     if ((x0.cardMax() == 0) ||
00476         ((x1.max() < x0.lubMin()) || (x1.min() > x0.lubMax())) ||
00477         ((x0.glbSize() > 0) && (x0.glbMax() > x1.max())))
00478       return home.ES_SUBSUMED(*this);
00479     // if x1 is determined and = max(x0.lub): remove it from x0,
00480     // then entailed
00481     if (x1.assigned() && x1.val()==x0.lubMax()) {
00482       GECODE_ME_CHECK(x0.exclude(home,x1.val()));
00483       return home.ES_SUBSUMED(*this);
00484     }
00485     // if max(x0) is decided: remove max(x0) from the domain of x1
00486     // then entailed
00487     if (x0.glbMax() == x0.lubMax()) {
00488       GECODE_ME_CHECK(x1.nq(home,x0.glbMax()));
00489       return home.ES_SUBSUMED(*this);
00490     }
00491     // if x1 is determined and = max(x0.glb), then we need at least
00492     // one more element; if there is only one above, then we must
00493     // take it.
00494     if (x1.assigned() && x0.glbSize() > 0 && x1.val()==x0.glbMax()) {
00495       unsigned int oldGlbSize = x0.glbSize();
00496       // if there is only 1 unknown above x1, then we must take it
00497       UnknownRanges<View> ur(x0);
00498       // there is at least one unknown above x1 otherwise it would
00499       // have been caught by the if for x1=max(x0.lub)
00500       while (ur.max() < x1.val()) {
00501         assert(ur());
00502         ++ur;
00503       };
00504       // if the first range above x1 contains just 1 element,
00505       // and is the last range, then take that element
00506       if (ur.width() == 1) {
00507         int i = ur.min();
00508         ++ur;
00509         if (!ur()) {
00510           // last range
00511           GECODE_ME_CHECK(x0.include(home,i));
00512           return home.ES_SUBSUMED(*this);
00513         }
00514       }
00515       GECODE_ME_CHECK(x0.cardMin(home, oldGlbSize+1));
00516     }
00517     // if dom(x1) and lub(x0) are disjoint, then entailed
00518     {
00519       LubRanges<View> ub(x0);
00520       Gecode::Int::ViewRanges<Gecode::Int::IntView> d(x1);
00521       Gecode::Iter::Ranges::Inter<LubRanges<View>,
00522         Gecode::Int::ViewRanges<Gecode::Int::IntView> > ir(ub,d);
00523       if (!ir()) return home.ES_SUBSUMED(*this);
00524     }
00525     // x0 is fated to eventually contain at least x0.cardMin elements.
00526     // therefore max(x0) >= x0.cardMin-th smallest element of x0.lub.
00527     // if x1 < than that, then entailed.
00528     {
00529       unsigned int n = x0.cardMin();
00530       int nth_smallest = BndSet::MIN_OF_EMPTY;
00531       for (LubRanges<View> ur(x0); ur(); ++ur) {
00532         if (ur.width() >= n) {
00533           // record it and exit the loop
00534           nth_smallest = static_cast<int>(ur.min() + n - 1);
00535           break;
00536         }
00537         // otherwise, we skipped ur.width() values
00538         n -= ur.width();
00539       }
00540       // if x1.max < nth_smallest, then entailed
00541       if (x1.max() < nth_smallest)
00542         return home.ES_SUBSUMED(*this);
00543     }
00544     return ES_FIX;
00545   }
00546 
00547   template<class View, ReifyMode rm>
00548   forceinline
00549   ReMaxElement<View,rm>::ReMaxElement(Home home, View y0,
00550                                       Gecode::Int::IntView y1,
00551                                       Gecode::Int::BoolView b2)
00552     : Gecode::Int::ReMixBinaryPropagator<View,PC_SET_ANY,
00553       Gecode::Int::IntView,Gecode::Int::PC_INT_DOM,
00554       Gecode::Int::BoolView> (home, y0, y1, b2) {}
00555 
00556   template<class View, ReifyMode rm>
00557   forceinline
00558   ReMaxElement<View,rm>::ReMaxElement(Space& home, ReMaxElement& p)
00559     : Gecode::Int::ReMixBinaryPropagator<View,PC_SET_ANY,
00560       Gecode::Int::IntView,Gecode::Int::PC_INT_DOM,
00561       Gecode::Int::BoolView> (home, p) {}
00562 
00563   template<class View, ReifyMode rm>
00564   ExecStatus
00565   ReMaxElement<View,rm>::post(Home home, View x0,
00566                               Gecode::Int::IntView x1,
00567                               Gecode::Int::BoolView b2) {
00568     (void) new (home) ReMaxElement(home,x0,x1,b2);
00569     return ES_OK;
00570   }
00571 
00572   template<class View, ReifyMode rm>
00573   Actor*
00574   ReMaxElement<View,rm>::copy(Space& home) {
00575     return new (home) ReMaxElement(home,*this);
00576   }
00577 
00578   template<class View, ReifyMode rm>
00579   ExecStatus
00580   ReMaxElement<View,rm>::propagate(Space& home, const ModEventDelta&) {
00581     // check if b is determined
00582     if (b.one()) {
00583       if (rm == RM_PMI)
00584         return home.ES_SUBSUMED(*this);
00585       GECODE_REWRITE(*this, (MaxElement<View>::post(home(*this),x0,x1)));
00586     }
00587     if (b.zero()) {
00588       if (rm == RM_IMP)
00589         return home.ES_SUBSUMED(*this);
00590       GECODE_REWRITE(*this, (NotMaxElement<View>::post(home(*this),x0,x1)));
00591     }
00592     // cheap tests for => b=0
00593     // if x0 is empty, then b=0 and entailed
00594     // if max(x1) < min(x0.lub) or min(x1) > max(x0.lub), then b=0 and entailed
00595     // if max(x0.glb) > max(x1), then b=0 and entailed
00596     if ((x0.cardMax() == 0) ||
00597         ((x1.max() < x0.lubMin()) || (x1.min() > x0.lubMax())) ||
00598         ((x0.glbSize() > 0) && (x0.glbMax() > x1.max())))
00599       {
00600         if (rm != RM_PMI)
00601           GECODE_ME_CHECK(b.zero(home));
00602         return home.ES_SUBSUMED(*this);
00603       }
00604     // if max(x0) is decided
00605     if (x0.glbMax() == x0.lubMax()) {
00606       // if x1 is det: check if = max(x0), assign b, entailed
00607       if (x1.assigned()) {
00608         if (x1.val() == x0.glbMax()) {
00609           if (rm != RM_IMP)
00610             GECODE_ME_CHECK(b.one(home));
00611         } else {
00612           if (rm != RM_PMI)
00613             GECODE_ME_CHECK(b.zero(home));
00614         }
00615         return home.ES_SUBSUMED(*this);
00616       }
00617       // if max(x0) not in dom(x1): b=0, entailed
00618       else if ((x0.glbMax() < x1.min()) ||
00619                (x0.glbMax() > x1.max()) ||
00620                !x1.in(x0.glbMax()))
00621         {
00622           if (rm != RM_PMI)
00623             GECODE_ME_CHECK(b.zero(home));
00624           return home.ES_SUBSUMED(*this);
00625         }
00626     }
00627     // if dom(x1) and lub(x0) are disjoint, then b=0, entailed
00628     {
00629       LubRanges<View> ub(x0);
00630       Gecode::Int::ViewRanges<Gecode::Int::IntView> d(x1);
00631       Gecode::Iter::Ranges::Inter<LubRanges<View>,
00632         Gecode::Int::ViewRanges<Gecode::Int::IntView> > ir(ub,d);
00633       if (!ir()) {
00634         if (rm != RM_PMI)
00635           GECODE_ME_CHECK(b.zero(home));
00636         return home.ES_SUBSUMED(*this);
00637       }
00638     }
00639     // x0 is fated to eventually contain at least x0.cardMin elements.
00640     // therefore max(x0) >= x0.cardMin-th smallest element of x0.lub.
00641     // if x1 < than that, then b=0, entailed.
00642     {
00643       unsigned int n = x0.cardMin();
00644       int nth_smallest = BndSet::MIN_OF_EMPTY;
00645       for (LubRanges<View> ur(x0); ur(); ++ur) {
00646         if (ur.width() >= n)
00647           {
00648             // record it and exit the loop
00649             nth_smallest = static_cast<int>(ur.min() + n - 1);
00650             break;
00651           }
00652         // otherwise, we skipped ur.width() values
00653         n -= ur.width();
00654       }
00655       // if x1.max < nth_smallest, then entailed
00656       if (x1.max() < nth_smallest) {
00657         if (rm != RM_PMI)
00658           GECODE_ME_CHECK(b.zero(home));
00659         return home.ES_SUBSUMED(*this);
00660       }
00661     }
00662     return ES_FIX;
00663   }
00664 
00665 }}}
00666 
00667 // STATISTICS: set-prop