divmod.hpp

00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
00002 /*
00003  *  Main authors:
00004  *     Guido Tack <tack@gecode.org>
00005  *
00006  *  Copyright:
00007  *     Guido Tack, 2008
00008  *
00009  *  Last modified:
00010  *     $Date: 2009-01-20 23:44:27 +0100 (Tue, 20 Jan 2009) $ by $Author: schulte $
00011  *     $Revision: 8082 $
00012  *
00013  *  This file is part of Gecode, the generic constraint
00014  *  development environment:
00015  *     http://www.gecode.org
00016  *
00017  *  Permission is hereby granted, free of charge, to any person obtaining
00018  *  a copy of this software and associated documentation files (the
00019  *  "Software"), to deal in the Software without restriction, including
00020  *  without limitation the rights to use, copy, modify, merge, publish,
00021  *  distribute, sublicense, and/or sell copies of the Software, and to
00022  *  permit persons to whom the Software is furnished to do so, subject to
00023  *  the following conditions:
00024  *
00025  *  The above copyright notice and this permission notice shall be
00026  *  included in all copies or substantial portions of the Software.
00027  *
00028  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00029  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00030  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00031  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00032  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00033  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00034  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00035  *
00036  */
00037 
00038 #include <gecode/int/linear.hh>
00039 
00040 namespace Gecode { namespace Int { namespace Arithmetic {
00041 
00042   /*
00043    * Positive bounds consistent division
00044    *
00045    */
00046   template <class Val, class VA, class VB, class VC, bool towardsMinInf>
00047   forceinline ExecStatus
00048   prop_div_plus_bnd(Space& home, Propagator& p, VA x0, VB x1, VC x2) {
00049     assert(pos(x0) && pos(x1) && !neg(x2));
00050     bool mod;
00051     do {
00052       mod = false;
00053       {
00054         ModEvent me;
00055         if (towardsMinInf)
00056           me = x2.lq(home,f_d_p<Val>(x0.max(),x1.min()));
00057         else
00058           me = x2.lq(home,c_d_p<Val>(x0.max(),x1.min()));
00059         if (me_failed(me)) return ES_FAILED;
00060         mod |= me_modified(me);
00061       }
00062       {
00063         ModEvent me;
00064         if (towardsMinInf)
00065           me = x2.gq(home,f_d_p<Val>(x0.min(),x1.max()));
00066         else
00067           me = x2.gq(home,c_d_p<Val>(x0.min(),x1.max()));
00068         if (me_failed(me)) return ES_FAILED;
00069         mod |= me_modified(me);
00070       }
00071       {
00072         ModEvent me;
00073         if (towardsMinInf)
00074           me = x0.le(home,m<Val>(x1.max(),
00075                                  static_cast<Val>(x2.max())+
00076                                  static_cast<Val>(1)));
00077         else
00078           me = x0.lq(home,m<Val>(x1.max(),x2.max()));
00079         if (me_failed(me)) return ES_FAILED;
00080         mod |= me_modified(me);
00081       }
00082       {
00083         ModEvent me;
00084         if (towardsMinInf)
00085           me = x0.gq(home,m<Val>(x1.min(),x2.min()));
00086         else
00087           me = x0.gr(home,m<Val>(x1.min(),
00088                                  static_cast<Val>(x2.min())-
00089                                  static_cast<Val>(1)));
00090         if (me_failed(me)) return ES_FAILED;
00091         mod |= me_modified(me);
00092       }
00093       {
00094         if (x2.min() > 0) {
00095           ModEvent me;
00096           if (towardsMinInf)
00097             me = x1.lq(home,f_d_p<Val>(x0.max(),x2.min()));
00098           else if (x2.min() != 1) {
00099             me = x1.lq(home,c_d_p<Val>(x0.max(),
00100                                        static_cast<Val>(x2.min())-
00101                                        static_cast<Val>(1)));
00102           } else
00103             me = ME_INT_NONE;
00104           if (me_failed(me)) return ES_FAILED;
00105           mod |= me_modified(me);
00106         }
00107       }
00108       {
00109         ModEvent me;
00110         if (towardsMinInf)
00111           me = x1.gq(home,c_d_p<Val>(x0.min(),
00112             static_cast<Val>(x2.max())+static_cast<Val>(1)));
00113         else
00114           me = x1.gq(home,f_d_p<Val>(x0.min(),
00115             static_cast<Val>(x2.max())+static_cast<Val>(1)));
00116         if (me_failed(me)) return ES_FAILED;
00117         mod |= me_modified(me);
00118       }
00119     } while (mod);
00120     return x0.assigned() && x1.assigned() ?
00121       ES_SUBSUMED(p,sizeof(p)) : ES_FIX;
00122   }
00123 
00124   template <class Val, class VA, class VB, class VC, bool towardsMinInf>
00125   forceinline
00126   DivPlusBnd<Val,VA,VB,VC,towardsMinInf>
00127   ::DivPlusBnd(Space& home, VA x0, VB x1, VC x2)
00128     : MixTernaryPropagator<VA,PC_INT_BND,VB,PC_INT_BND,VC,PC_INT_BND>
00129   (home,x0,x1,x2) {}
00130 
00131   template <class Val, class VA, class VB, class VC, bool towardsMinInf>
00132   forceinline
00133   DivPlusBnd<Val,VA,VB,VC,towardsMinInf>
00134   ::DivPlusBnd(Space& home, bool share,
00135                DivPlusBnd<Val,VA,VB,VC,towardsMinInf>& p)
00136     : MixTernaryPropagator<VA,PC_INT_BND,VB,PC_INT_BND,VC,PC_INT_BND>
00137   (home,share,p) {}
00138 
00139   template <class Val, class VA, class VB, class VC, bool towardsMinInf>
00140   Actor*
00141   DivPlusBnd<Val,VA,VB,VC,towardsMinInf>::copy(Space& home, bool share) {
00142     return new (home) DivPlusBnd<Val,VA,VB,VC,towardsMinInf>(home,
00143                                                              share,*this);
00144   }
00145 
00146   template <class Val, class VA, class VB, class VC, bool towardsMinInf>
00147   ExecStatus
00148   DivPlusBnd<Val,VA,VB,VC,towardsMinInf>
00149   ::propagate(Space& home, const ModEventDelta&) {
00150     return prop_div_plus_bnd<Val,VA,VB,VC,towardsMinInf>(home,*this,x0,x1,x2);
00151   }
00152 
00153   template <class Val, class VA, class VB, class VC, bool towardsMinInf>
00154   forceinline ExecStatus
00155   DivPlusBnd<Val,VA,VB,VC,towardsMinInf>
00156   ::post(Space& home, VA x0, VB x1, VC x2) {
00157     GECODE_ME_CHECK(x0.gr(home,0));
00158     GECODE_ME_CHECK(x1.gr(home,0));
00159     if (towardsMinInf) {
00160       GECODE_ME_CHECK(x2.gq(home,floor(static_cast<double>(x0.min()) /
00161                                        static_cast<double>(x1.max()))));
00162     } else {
00163       GECODE_ME_CHECK(x2.gq(home,ceil(static_cast<double>(x0.min()) /
00164                                       static_cast<double>(x1.max()))));
00165     }
00166     (void)
00167       new (home) DivPlusBnd<double,VA,VB,VC,towardsMinInf>(home,x0,x1,x2);
00168     return ES_OK;
00169   }
00170 
00171 
00172   /*
00173    * Bounds consistent multiplication
00174    *
00175    */
00176   template <class View>
00177   forceinline
00178   DivBnd<View>::DivBnd(Space& home, View x0, View x1, View x2)
00179     : TernaryPropagator<View,PC_INT_BND>(home,x0,x1,x2) {}
00180 
00181   template <class View>
00182   forceinline
00183   DivBnd<View>::DivBnd(Space& home, bool share, DivBnd<View>& p)
00184     : TernaryPropagator<View,PC_INT_BND>(home,share,p) {}
00185 
00186   template <class View>
00187   Actor*
00188   DivBnd<View>::copy(Space& home, bool share) {
00189     return new (home) DivBnd<View>(home,share,*this);
00190   }
00191 
00192   template <class View>
00193   ExecStatus
00194   DivBnd<View>::propagate(Space& home, const ModEventDelta&) {
00195     if (pos(x1)) {
00196       if (pos(x2) || pos(x0)) goto rewrite_ppp;
00197       if (neg(x2) || neg(x0)) goto rewrite_npn;
00198       goto prop_xpx;
00199     }
00200     if (neg(x1)) {
00201       if (neg(x2) || pos(x0)) goto rewrite_pnn;
00202       if (pos(x2) || neg(x0)) goto rewrite_nnp;
00203       goto prop_xnx;
00204     }
00205     if (pos(x2)) {
00206       if (pos(x0)) goto rewrite_ppp;
00207       if (neg(x0)) goto rewrite_nnp;
00208       goto prop_xxp;
00209     }
00210     if (neg(x2)) {
00211       if (pos(x0)) goto rewrite_pnn;
00212       if (neg(x0)) goto rewrite_npn;
00213       goto prop_xxn;
00214     }
00215     assert(any(x1) && any(x2));
00216 
00217     GECODE_ME_CHECK(x0.le(home,std::max(m<double>(x1.max(),x2.max()+1),
00218                                         m<double>(x1.min(),x2.min()-1))));
00219     GECODE_ME_CHECK(x0.gq(home,std::min(m<double>(x1.min(),x2.max()+1),
00220                                         m<double>(x1.max(),x2.min()-1))));
00221 
00222     return ES_NOFIX;
00223 
00224   prop_xxp:
00225     assert(any(x0) && any(x1) && pos(x2));
00226 
00227     GECODE_ME_CHECK(x0.le(home, m<double>(x1.max(),x2.max()+1)));
00228     GECODE_ME_CHECK(x0.gq(home, m<double>(x1.min(),x2.max()+1)));
00229 
00230     if (pos(x0)) goto rewrite_ppp;
00231     if (neg(x0)) goto rewrite_nnp;
00232 
00233     GECODE_ME_CHECK(x1.lq(home,f_d_p<double>(x0.max(),x2.min())));
00234     GECODE_ME_CHECK(x1.gq(home,c_d(x0.min(),x2.min())));
00235 
00236     if (x0.assigned() && x1.assigned()) {
00237       GECODE_ME_CHECK(x2.eq(home,f_d(x0.val(),x1.val())));
00238       return ES_SUBSUMED(*this,sizeof(*this));
00239     }
00240 
00241     return ES_NOFIX;
00242   prop_xpx:
00243     assert(any(x0) && pos(x1) && any(x2));
00244 
00245     GECODE_ME_CHECK(x0.le(home, m<double>(x1.max(),x2.max()+1)));
00246     GECODE_ME_CHECK(x0.gq(home, m<double>(x1.max(),x2.min()-1)));
00247 
00248     if (pos(x0)) goto rewrite_ppp;
00249     if (neg(x0)) goto rewrite_npn;
00250 
00251     GECODE_ME_CHECK(x2.lq(home,f_d(x0.max(),x1.min())));
00252     GECODE_ME_CHECK(x2.gq(home,f_d(x0.min(),x1.min())));
00253 
00254     if (x0.assigned() && x1.assigned()) {
00255       GECODE_ME_CHECK(x2.eq(home,f_d(x0.val(),x1.val())));
00256       return ES_SUBSUMED(*this,sizeof(*this));
00257     }
00258 
00259     return ES_NOFIX;
00260 
00261   prop_xxn:
00262     assert(any(x0) && any(x1) && neg(x2));
00263 
00264     GECODE_ME_CHECK(x0.le(home, m<double>(x1.min(),x2.min()-1)));
00265     GECODE_ME_CHECK(x0.gq(home, m<double>(x1.max(),x2.min()-1)));
00266 
00267     if (pos(x0)) goto rewrite_pnn;
00268     if (neg(x0)) goto rewrite_npn;
00269 
00270     if (x2.max() != -1)
00271       GECODE_ME_CHECK(x1.lq(home,c_d(x0.min(),x2.max()+1)));
00272     if (x2.max() != -1)
00273       GECODE_ME_CHECK(x1.gq(home,c_d(x0.max(),x2.max()+1)));
00274 
00275     if (x0.assigned() && x1.assigned()) {
00276       GECODE_ME_CHECK(x2.eq(home,f_d(x0.val(),x1.val())));
00277       return ES_SUBSUMED(*this,sizeof(*this));
00278     }
00279     return ES_NOFIX;
00280 
00281   prop_xnx:
00282     assert(any(x0) && neg(x1) && any(x2));
00283 
00284     GECODE_ME_CHECK(x0.le(home, m<double>(x1.min(),x2.min()-1)));
00285     GECODE_ME_CHECK(x0.gq(home, m<double>(x1.min(),x2.max()+1)));
00286 
00287     if (pos(x0)) goto rewrite_pnn;
00288     if (neg(x0)) goto rewrite_nnp;
00289 
00290     GECODE_ME_CHECK(x2.lq(home,f_d(x0.min(),x1.max())));
00291     GECODE_ME_CHECK(x2.gq(home,f_d(x0.max(),x1.max())));
00292 
00293     if (x0.assigned() && x1.assigned()) {
00294       GECODE_ME_CHECK(x2.eq(home,f_d(x0.val(),x1.val())));
00295       return ES_SUBSUMED(*this,sizeof(*this));
00296     }
00297     return ES_NOFIX;
00298 
00299   rewrite_ppp:
00300     GECODE_REWRITE(*this,(DivPlusBnd<double,IntView,IntView,IntView>
00301                          ::post(home,x0,x1,x2)));
00302   rewrite_nnp:
00303     GECODE_REWRITE(*this,(DivPlusBnd<double,MinusView,MinusView,IntView>
00304                          ::post(home,x0,x1,x2)));
00305   rewrite_pnn:
00306     GECODE_REWRITE(*this,(DivPlusBnd<double,IntView,MinusView,MinusView,false>
00307                          ::post(home,x0,x1,x2)));
00308   rewrite_npn:
00309     GECODE_REWRITE(*this,(DivPlusBnd<double,MinusView,IntView,MinusView,false>
00310                          ::post(home,x0,x1,x2)));
00311   }
00312 
00313   template <class View>
00314   ExecStatus
00315   DivBnd<View>::post(Space& home, View x0, View x1, View x2) {
00316     GECODE_ME_CHECK(x1.nq(home, 0));
00317     if (pos(x0)) {
00318       if (pos(x1) || pos(x2)) goto post_ppp;
00319       if (neg(x1) || neg(x2)) goto post_pnn;
00320     } else if (neg(x0)) {
00321       if (neg(x1) || pos(x2)) goto post_nnp;
00322       if (pos(x1) || neg(x2)) goto post_npn;
00323     } else if (pos(x1)) {
00324       if (pos(x2)) goto post_ppp;
00325       if (neg(x2)) goto post_npn;
00326     } else if (neg(x1)) {
00327       if (pos(x2)) goto post_nnp;
00328       if (neg(x2)) goto post_pnn;
00329     }
00330     (void) new (home) DivBnd<View>(home,x0,x1,x2);
00331     return ES_OK;
00332 
00333   post_ppp:
00334     return DivPlusBnd<double,IntView,IntView,IntView>::post(home,x0,x1,x2);
00335   post_nnp:
00336     return DivPlusBnd<double,MinusView,MinusView,IntView>::post(home,x0,x1,x2);
00337   post_pnn:
00338     return DivPlusBnd<double,IntView,MinusView,MinusView,false>::post(home,x0,x1,x2);
00339   post_npn:
00340     return DivPlusBnd<double,MinusView,IntView,MinusView,false>::post(home,x0,x1,x2);
00341   }
00342 
00343 
00344   /*
00345    * Propagator for x0 != 0 /\ (x1 != 0 => x0*x1>0) /\ abs(x1)<abs(x0)
00346    *
00347    */
00348 
00349   template <class View>
00350   forceinline
00351   DivMod<View>::DivMod(Space& home, View x0, View x1)
00352     : BinaryPropagator<View,PC_INT_BND>(home,x0,x1) {}
00353 
00354   template <class View>
00355   forceinline ExecStatus
00356   DivMod<View>::post(Space& home, View x0, View x1) {
00357     GECODE_ME_CHECK(x0.nq(home,0));
00358     (void) new (home) DivMod<View>(home,x0,x1);
00359     return ES_OK;
00360   }
00361 
00362   template <class View>
00363   forceinline
00364   DivMod<View>::DivMod(Space& home, bool share,
00365                              DivMod<View>& p)
00366   : BinaryPropagator<View,PC_INT_BND>(home,share,p) {}
00367 
00368   template <class View>
00369   Actor*
00370   DivMod<View>::copy(Space& home, bool share) {
00371     return new (home) DivMod<View>(home,share,*this);
00372   }
00373 
00374   template <class View>
00375   ExecStatus
00376   DivMod<View>::propagate(Space& home, const ModEventDelta&) {
00377     bool signIsSame;
00378     do {
00379       signIsSame = true;
00380       // The sign of x1 and x3 is the same
00381       if (x0.min() > 0) {
00382         GECODE_ME_CHECK(x1.gq(home, 0));
00383       } else if (x0.max() < 0) {
00384         GECODE_ME_CHECK(x1.lq(home, 0));
00385       } else if (x1.min() > 0) {
00386         GECODE_ME_CHECK(x0.gr(home, 0));
00387       } else if (x1.max() < 0) {
00388         GECODE_ME_CHECK(x0.le(home, 0));
00389       } else {
00390         signIsSame = false;
00391       }
00392 
00393       // abs(x1) is less than abs(x0)
00394       int x0max = std::max(x0.max(),std::max(-x0.max(),
00395                            std::max(x0.min(),-x0.min())));
00396       GECODE_ME_CHECK(x1.le(home, x0max));
00397       GECODE_ME_CHECK(x1.gr(home, -x0max));
00398 
00399       if (x0.min() > 0) {
00400         int min = std::min(x1.min() < 0 ? -x1.min():x1.min(),
00401                            x1.max() < 0 ? -x1.max():x1.max());
00402         GECODE_ME_CHECK(x0.gr(home,min));
00403       } else if (x0.max() < 0) {
00404         int min = std::min(x1.min() < 0 ? -x1.min():x1.min(),
00405                            x1.max() < 0 ? -x1.max():x1.max());
00406         GECODE_ME_CHECK(x0.le(home,-min));
00407       }
00408     } while (!signIsSame &&
00409              (x0.min() > 0 || x0.max() < 0 || x1.min() > 0 || x1.max() < 0));
00410 
00411     if (signIsSame) {
00412       int maxx1 = std::max(x1.min() < 0 ? -x1.min():x1.min(),
00413                            x1.max() < 0 ? -x1.max():x1.max());
00414       int minx0 = std::min(x0.min() < 0 ? -x0.min():x0.min(),
00415                            x0.max() < 0 ? -x0.max():x0.max());
00416       if (maxx1 < minx0) {
00417         return ES_SUBSUMED(*this,home);
00418       }
00419     }
00420     return ES_FIX;
00421   }
00422 
00423 }}}
00424 
00425 // STATISTICS: int-prop