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

lex.hpp

Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
00002 /*
00003  *  Main authors:
00004  *     Christian Schulte <schulte@gecode.org>
00005  *
00006  *  Copyright:
00007  *     Christian Schulte, 2003
00008  *
00009  *  This file is part of Gecode, the generic constraint
00010  *  development environment:
00011  *     http://www.gecode.org
00012  *
00013  *  Permission is hereby granted, free of charge, to any person obtaining
00014  *  a copy of this software and associated documentation files (the
00015  *  "Software"), to deal in the Software without restriction, including
00016  *  without limitation the rights to use, copy, modify, merge, publish,
00017  *  distribute, sublicense, and/or sell copies of the Software, and to
00018  *  permit persons to whom the Software is furnished to do so, subject to
00019  *  the following conditions:
00020  *
00021  *  The above copyright notice and this permission notice shall be
00022  *  included in all copies or substantial portions of the Software.
00023  *
00024  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00025  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00026  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00027  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00028  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00029  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00030  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00031  *
00032  */
00033 
00034 namespace Gecode { namespace Int { namespace Rel {
00035 
00036   /*
00037    * Lexical order propagator
00038    */
00039   template<class VX, class VY>
00040   inline
00041   LexLqLe<VX,VY>::LexLqLe(Home home,
00042                           ViewArray<VX>& x0, ViewArray<VY>& y0, bool s)
00043     : Propagator(home), x(x0), y(y0), strict(s) {
00044     x.subscribe(home, *this, PC_INT_BND);
00045     y.subscribe(home, *this, PC_INT_BND);
00046   }
00047 
00048   template<class VX, class VY>
00049   forceinline
00050   LexLqLe<VX,VY>::LexLqLe(Space& home, LexLqLe<VX,VY>& p)
00051     : Propagator(home,p), strict(p.strict) {
00052     x.update(home,p.x);
00053     y.update(home,p.y);
00054   }
00055 
00056   template<class VX, class VY>
00057   Actor*
00058   LexLqLe<VX,VY>::copy(Space& home) {
00059     return new (home) LexLqLe<VX,VY>(home,*this);
00060   }
00061 
00062   template<class VX, class VY>
00063   PropCost
00064   LexLqLe<VX,VY>::cost(const Space&, const ModEventDelta&) const {
00065     return PropCost::linear(PropCost::LO, x.size());
00066   }
00067 
00068   template<class VX, class VY>
00069   void
00070   LexLqLe<VX,VY>::reschedule(Space& home) {
00071     x.reschedule(home,*this,PC_INT_BND);
00072     y.reschedule(home,*this,PC_INT_BND);
00073   }
00074 
00075   template<class VX, class VY>
00076   forceinline size_t
00077   LexLqLe<VX,VY>::dispose(Space& home) {
00078     assert(!home.failed());
00079     x.cancel(home,*this,PC_INT_BND);
00080     y.cancel(home,*this,PC_INT_BND);
00081     (void) Propagator::dispose(home);
00082     return sizeof(*this);
00083   }
00084 
00085   template<class VX, class VY>
00086   ExecStatus
00087   LexLqLe<VX,VY>::propagate(Space& home, const ModEventDelta&) {
00088     /*
00089      * State 1
00090      *
00091      */
00092     {
00093       int i = 0;
00094       int n = x.size();
00095 
00096       while ((i < n) && (x[i].min() == y[i].max())) {
00097         // case: =, >=
00098         GECODE_ME_CHECK(x[i].lq(home,y[i].max()));
00099         GECODE_ME_CHECK(y[i].gq(home,x[i].min()));
00100         i++;
00101       }
00102 
00103       if (i == n) // case: $
00104         return strict ? ES_FAILED : home.ES_SUBSUMED(*this);
00105 
00106       // Possible cases left: <, <=, > (yields failure), ?
00107       GECODE_ME_CHECK(x[i].lq(home,y[i].max()));
00108       GECODE_ME_CHECK(y[i].gq(home,x[i].min()));
00109 
00110       if (x[i].max() < y[i].min()) // case: < (after tell)
00111         return home.ES_SUBSUMED(*this);
00112 
00113       // x[i] can never be equal to y[i] (otherwise: >=)
00114       assert(!(x[i].assigned() && y[i].assigned() &&
00115                x[i].val() == y[i].val()));
00116       // Remove all elements between 0...i-1 as they are assigned and equal
00117       x.drop_fst(i); y.drop_fst(i);
00118       // After this, execution continues at [1]
00119     }
00120 
00121     /*
00122      * State 2
00123      *   prefix: (?|<=)
00124      *
00125      */
00126     {
00127       int i = 1;
00128       int n = x.size();
00129 
00130       while ((i < n) &&
00131              (x[i].min() == y[i].max()) &&
00132              (x[i].max() == y[i].min())) { // case: =
00133         assert(x[i].assigned() && y[i].assigned() &&
00134                (x[i].val() == y[i].val()));
00135         i++;
00136       }
00137 
00138       if (i == n) { // case: $
00139         if (strict)
00140           goto rewrite_le;
00141         else
00142           goto rewrite_lq;
00143       }
00144 
00145       if (x[i].max() < y[i].min()) // case: <
00146         goto rewrite_lq;
00147 
00148       if (x[i].min() > y[i].max()) // case: >
00149         goto rewrite_le;
00150 
00151       if (i > 1) {
00152         // Remove equal elements [1...i-1], keep element [0]
00153         x[i-1]=x[0]; x.drop_fst(i-1);
00154         y[i-1]=y[0]; y.drop_fst(i-1);
00155       }
00156     }
00157 
00158     if (x[1].max() <= y[1].min()) {
00159       // case: <= (invariant: not =, <)
00160       /*
00161        * State 3
00162        *   prefix: (?|<=),<=
00163        *
00164        */
00165       int i = 2;
00166       int n = x.size();
00167 
00168       while ((i < n) && (x[i].max() == y[i].min())) // case: <=, =
00169         i++;
00170 
00171       if (i == n) { // case: $
00172         if (strict)
00173           return ES_FIX;
00174         else
00175           goto rewrite_lq;
00176       }
00177 
00178       if (x[i].max() < y[i].min()) // case: <
00179         goto rewrite_lq;
00180 
00181       if (x[i].min() > y[i].max()) { // case: >
00182         // Eliminate [i]...[n-1]
00183         for (int j=i; j<n; j++) {
00184           x[j].cancel(home,*this,PC_INT_BND);
00185           y[j].cancel(home,*this,PC_INT_BND);
00186         }
00187         x.size(i); y.size(i);
00188         strict = true;
00189       }
00190 
00191       return ES_FIX;
00192     }
00193 
00194     if (x[1].min() >= y[1].max()) {
00195       // case: >= (invariant: not =, >)
00196       /*
00197        * State 4
00198        *   prefix: (?|<=) >=
00199        *
00200        */
00201       int i = 2;
00202       int n = x.size();
00203 
00204       while ((i < n) && (x[i].min() == y[i].max()))
00205         // case: >=, =
00206         i++;
00207 
00208       if (i == n) { // case: $
00209         if (strict)
00210           goto rewrite_le;
00211         else
00212           return ES_FIX;
00213       }
00214 
00215       if (x[i].min() > y[i].max()) // case: >
00216         goto rewrite_le;
00217 
00218       if (x[i].max() < y[i].min()) { // case: <
00219         // Eliminate [i]...[n-1]
00220         for (int j=i; j<n; j++) {
00221           x[j].cancel(home,*this,PC_INT_BND);
00222           y[j].cancel(home,*this,PC_INT_BND);
00223         }
00224         x.size(i); y.size(i);
00225         strict = false;
00226       }
00227 
00228       return ES_FIX;
00229     }
00230 
00231     return ES_FIX;
00232 
00233   rewrite_le:
00234     GECODE_REWRITE(*this,(Le<VX,VY>::post(home(*this),x[0],y[0])));
00235   rewrite_lq:
00236     GECODE_REWRITE(*this,(Lq<VX,VY>::post(home(*this),x[0],y[0])));
00237   }
00238 
00239   template<class VX, class VY>
00240   ExecStatus
00241   LexLqLe<VX,VY>::post(Home home,
00242                       ViewArray<VX>& x, ViewArray<VY>& y, bool strict) {
00243     if (x.size() < y.size()) {
00244       y.size(x.size()); strict=false;
00245     } else if (x.size() > y.size()) {
00246       x.size(y.size()); strict=true;
00247     }
00248     if (x.size() == 0)
00249       return strict ? ES_FAILED : ES_OK;
00250     if (x.size() == 1) {
00251       if (strict)
00252         return Le<VX,VY>::post(home,x[0],y[0]);
00253       else
00254         return Lq<VX,VY>::post(home,x[0],y[0]);
00255     }
00256     (void) new (home) LexLqLe<VX,VY>(home,x,y,strict);
00257     return ES_OK;
00258   }
00259 
00260 
00261   /*
00262    * Lexical disequality propagator
00263    */
00264   template<class VX, class VY>
00265   forceinline
00266   LexNq<VX,VY>::LexNq(Home home, ViewArray<VX>& xv, ViewArray<VY>& yv)
00267     : Propagator(home),
00268       x0(xv[xv.size()-2]), y0(yv[xv.size()-2]),
00269       x1(xv[xv.size()-1]), y1(yv[xv.size()-1]),
00270       x(xv), y(yv) {
00271     int n = x.size();
00272     assert(n > 1);
00273     assert(n == y.size());
00274     x.size(n-2); y.size(n-2);
00275     x0.subscribe(home,*this,PC_INT_VAL); y0.subscribe(home,*this,PC_INT_VAL);
00276     x1.subscribe(home,*this,PC_INT_VAL); y1.subscribe(home,*this,PC_INT_VAL);
00277   }
00278 
00279   template<class VX, class VY>
00280   PropCost
00281   LexNq<VX,VY>::cost(const Space&, const ModEventDelta&) const {
00282     return PropCost::binary(PropCost::HI);
00283   }
00284 
00285   template<class VX, class VY>
00286   void
00287   LexNq<VX,VY>::reschedule(Space& home) {
00288     x0.reschedule(home,*this,PC_INT_VAL);
00289     y0.reschedule(home,*this,PC_INT_VAL);
00290     x1.reschedule(home,*this,PC_INT_VAL);
00291     y1.reschedule(home,*this,PC_INT_VAL);
00292   }
00293 
00294   template<class VX, class VY>
00295   forceinline
00296   LexNq<VX,VY>::LexNq(Space& home, LexNq<VX,VY>& p)
00297     : Propagator(home,p) {
00298     x0.update(home,p.x0); y0.update(home,p.y0);
00299     x1.update(home,p.x1); y1.update(home,p.y1);
00300     x.update(home,p.x); y.update(home,p.y);
00301   }
00302 
00303   template<class VX, class VY>
00304   Actor*
00305   LexNq<VX,VY>::copy(Space& home) {
00306     int n = x.size();
00307     if (n > 0) {
00308       // Eliminate all equal views and keep one disequal pair
00309       for (int i=n; i--; )
00310         switch (rtest_eq_bnd(x[i],y[i])) {
00311         case RT_TRUE:
00312           // Eliminate equal pair
00313           n--; x[i]=x[n]; y[i]=y[n];
00314           break;
00315         case RT_FALSE:
00316           // Just keep a single disequal pair
00317           n=1; x[0]=x[i]; y[0]=y[i];
00318           goto done;
00319         case RT_MAYBE:
00320           break;
00321         default:
00322           GECODE_NEVER;
00323         }
00324     done:
00325       x.size(n); y.size(n);
00326     }
00327     return new (home) LexNq<VX,VY>(home,*this);
00328   }
00329 
00330   template<class VX, class VY>
00331   inline ExecStatus
00332   LexNq<VX,VY>::post(Home home, ViewArray<VX>& x, ViewArray<VY>& y) {
00333     if (x.size() != y.size())
00334       return ES_OK;
00335     int n = x.size();
00336     if (n > 0) {
00337       // Eliminate all equal views
00338       for (int i=n; i--; )
00339         switch (rtest_eq_dom(x[i],y[i])) {
00340         case RT_TRUE:
00341           // Eliminate equal pair
00342           n--; x[i]=x[n]; y[i]=y[n];
00343           break;
00344         case RT_FALSE:
00345           return ES_OK;
00346         case RT_MAYBE:
00347           if (x[i] == y[i]) {
00348             // Eliminate equal pair
00349             n--; x[i]=x[n]; y[i]=y[n];
00350           }
00351           break;
00352         default:
00353           GECODE_NEVER;
00354         }
00355       x.size(n); y.size(n);
00356     }
00357     if (n == 0)
00358       return ES_FAILED;
00359     if (n == 1)
00360       return Nq<VX,VY>::post(home,x[0],y[0]);
00361     (void) new (home) LexNq<VX,VY>(home,x,y);
00362     return ES_OK;
00363   }
00364 
00365   template<class VX, class VY>
00366   forceinline size_t
00367   LexNq<VX,VY>::dispose(Space& home) {
00368     x0.cancel(home,*this,PC_INT_VAL); y0.cancel(home,*this,PC_INT_VAL);
00369     x1.cancel(home,*this,PC_INT_VAL); y1.cancel(home,*this,PC_INT_VAL);
00370     (void) Propagator::dispose(home);
00371     return sizeof(*this);
00372   }
00373 
00374   template<class VX, class VY>
00375   forceinline ExecStatus
00376   LexNq<VX,VY>::resubscribe(Space& home,
00377                             RelTest rt, VX& x0, VY& y0, VX x1, VY y1) {
00378     if (rt == RT_TRUE) {
00379       assert(x0.assigned() && y0.assigned());
00380       assert(x0.val() == y0.val());
00381       int n = x.size();
00382       for (int i=n; i--; )
00383         switch (rtest_eq_dom(x[i],y[i])) {
00384         case RT_TRUE:
00385           // Eliminate equal pair
00386           n--; x[i]=x[n]; y[i]=y[n];
00387           break;
00388         case RT_FALSE:
00389           return home.ES_SUBSUMED(*this);
00390         case RT_MAYBE:
00391           // Move to x0, y0 and subscribe
00392           x0=x[i]; y0=y[i];
00393           n--; x[i]=x[n]; y[i]=y[n];
00394           x.size(n); y.size(n);
00395           x0.subscribe(home,*this,PC_INT_VAL,false);
00396           y0.subscribe(home,*this,PC_INT_VAL,false);
00397           return ES_FIX;
00398         default:
00399           GECODE_NEVER;
00400         }
00401       // No more views to subscribe to left
00402       GECODE_REWRITE(*this,(Nq<VX,VY>::post(home(*this),x1,y1)));
00403     }
00404     return ES_FIX;
00405   }
00406 
00407   template<class VX, class VY>
00408   ExecStatus
00409   LexNq<VX,VY>::propagate(Space& home, const ModEventDelta&) {
00410     RelTest rt0 = rtest_eq_dom(x0,y0);
00411     if (rt0 == RT_FALSE)
00412       return home.ES_SUBSUMED(*this);
00413     RelTest rt1 = rtest_eq_dom(x1,y1);
00414     if (rt1 == RT_FALSE)
00415       return home.ES_SUBSUMED(*this);
00416     GECODE_ES_CHECK(resubscribe(home,rt0,x0,y0,x1,y1));
00417     GECODE_ES_CHECK(resubscribe(home,rt1,x1,y1,x0,y0));
00418     return ES_FIX;
00419   }
00420 
00421 
00422 }}}
00423 
00424 // STATISTICS: int-prop