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: 2010-03-03 17:32:21 +0100 (Wed, 03 Mar 2010) $ by $Author: schulte $
00011  *     $Revision: 10364 $
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 
00047   template<class Val, class VA, class VB, class VC>
00048   forceinline
00049   DivPlusBnd<Val,VA,VB,VC>
00050   ::DivPlusBnd(Home home, VA x0, VB x1, VC x2)
00051     : MixTernaryPropagator<VA,PC_INT_BND,VB,PC_INT_BND,VC,PC_INT_BND>
00052   (home,x0,x1,x2) {}
00053 
00054   template<class Val, class VA, class VB, class VC>
00055   forceinline
00056   DivPlusBnd<Val,VA,VB,VC>
00057   ::DivPlusBnd(Space& home, bool share,
00058                DivPlusBnd<Val,VA,VB,VC>& p)
00059     : MixTernaryPropagator<VA,PC_INT_BND,VB,PC_INT_BND,VC,PC_INT_BND>
00060   (home,share,p) {}
00061 
00062   template<class Val, class VA, class VB, class VC>
00063   Actor*
00064   DivPlusBnd<Val,VA,VB,VC>::copy(Space& home, bool share) {
00065     return new (home) DivPlusBnd<Val,VA,VB,VC>(home,share,*this);
00066   }
00067 
00068   template<class Val, class VA, class VB, class VC>
00069   ExecStatus
00070   DivPlusBnd<Val,VA,VB,VC>
00071   ::propagate(Space& home, const ModEventDelta&) {
00072     assert(pos(x0) && pos(x1) && !neg(x2));
00073     bool mod;
00074     do {
00075       mod = false;
00076       GECODE_ME_CHECK_MODIFIED(mod,x2.lq(home,f_d_p<Val>(x0.max(),x1.min())));
00077       GECODE_ME_CHECK_MODIFIED(mod,x2.gq(home,f_d_p<Val>(x0.min(),x1.max())));
00078       GECODE_ME_CHECK_MODIFIED(mod,x0.le(home,m<Val>(x1.max(),
00079                                               static_cast<Val>(x2.max())+
00080                                               static_cast<Val>(1))));
00081       GECODE_ME_CHECK_MODIFIED(mod,x0.gq(home,m<Val>(x1.min(),x2.min())));
00082       if (x2.min() > 0) {
00083           GECODE_ME_CHECK_MODIFIED(mod,
00084             x1.lq(home,f_d_p<Val>(x0.max(),x2.min())));
00085       }
00086       GECODE_ME_CHECK_MODIFIED(mod,x1.gq(home,c_d_p<Val>(x0.min(),
00087           static_cast<Val>(x2.max())+static_cast<Val>(1))));
00088     } while (mod);
00089     return x0.assigned() && x1.assigned() ?
00090       home.ES_SUBSUMED(*this) : ES_FIX;
00091   }
00092 
00093   template<class Val, class VA, class VB, class VC>
00094   forceinline ExecStatus
00095   DivPlusBnd<Val,VA,VB,VC>
00096   ::post(Home home, VA x0, VB x1, VC x2) {
00097     GECODE_ME_CHECK(x0.gr(home,0));
00098     GECODE_ME_CHECK(x1.gr(home,0));
00099     GECODE_ME_CHECK(x2.gq(home,floor(static_cast<double>(x0.min()) /
00100                                      static_cast<double>(x1.max()))));
00101     (void)
00102       new (home) DivPlusBnd<double,VA,VB,VC>(home,x0,x1,x2);
00103     return ES_OK;
00104   }
00105 
00106 
00107   /*
00108    * Bounds consistent division
00109    *
00110    */
00111   template<class View>
00112   forceinline
00113   DivBnd<View>::DivBnd(Home home, View x0, View x1, View x2)
00114     : TernaryPropagator<View,PC_INT_BND>(home,x0,x1,x2) {}
00115 
00116   template<class View>
00117   forceinline
00118   DivBnd<View>::DivBnd(Space& home, bool share, DivBnd<View>& p)
00119     : TernaryPropagator<View,PC_INT_BND>(home,share,p) {}
00120 
00121   template<class View>
00122   Actor*
00123   DivBnd<View>::copy(Space& home, bool share) {
00124     return new (home) DivBnd<View>(home,share,*this);
00125   }
00126 
00127   template<class View>
00128   ExecStatus
00129   DivBnd<View>::propagate(Space& home, const ModEventDelta&) {
00130     if (pos(x1)) {
00131       if (pos(x2) || pos(x0)) goto rewrite_ppp;
00132       if (neg(x2) || neg(x0)) goto rewrite_npn;
00133       goto prop_xpx;
00134     }
00135     if (neg(x1)) {
00136       if (neg(x2) || pos(x0)) goto rewrite_pnn;
00137       if (pos(x2) || neg(x0)) goto rewrite_nnp;
00138       goto prop_xnx;
00139     }
00140     if (pos(x2)) {
00141       if (pos(x0)) goto rewrite_ppp;
00142       if (neg(x0)) goto rewrite_nnp;
00143       goto prop_xxp;
00144     }
00145     if (neg(x2)) {
00146       if (pos(x0)) goto rewrite_pnn;
00147       if (neg(x0)) goto rewrite_npn;
00148       goto prop_xxn;
00149     }
00150     assert(any(x1) && any(x2));
00151     GECODE_ME_CHECK(x0.lq(home,std::max(m<double>(x1.max(),x2.max()+1)-1,
00152                                         m<double>(x1.min(),x2.min()-1)-1)));
00153     GECODE_ME_CHECK(x0.gq(home,std::min(m<double>(x1.min(),x2.max()+1),
00154                                         m<double>(x1.max(),x2.min()-1))));
00155     return ES_NOFIX;
00156 
00157   prop_xxp:
00158     assert(any(x0) && any(x1) && pos(x2));
00159 
00160     GECODE_ME_CHECK(x0.le(home, m<double>(x1.max(),x2.max()+1)));
00161     GECODE_ME_CHECK(x0.gq(home, m<double>(x1.min(),x2.max()+1)));
00162 
00163     if (pos(x0)) goto rewrite_ppp;
00164     if (neg(x0)) goto rewrite_nnp;
00165 
00166     GECODE_ME_CHECK(x1.lq(home,f_d_p<double>(x0.max(),x2.min())));
00167     GECODE_ME_CHECK(x1.gq(home,c_d(x0.min(),x2.min())));
00168 
00169     if (x0.assigned() && x1.assigned())
00170       goto subsumed;
00171     return ES_NOFIX;
00172 
00173   prop_xpx:
00174     assert(any(x0) && pos(x1) && any(x2));
00175 
00176     GECODE_ME_CHECK(x0.le(home, m<double>(x1.max(),x2.max()+1)));
00177     GECODE_ME_CHECK(x0.gq(home, m<double>(x1.max(),x2.min()-1)));
00178 
00179     if (pos(x0)) goto rewrite_ppp;
00180     if (neg(x0)) goto rewrite_npn;
00181 
00182     GECODE_ME_CHECK(x2.lq(home,f_d(x0.max(),x1.min())));
00183     GECODE_ME_CHECK(x2.gq(home,f_d(x0.min(),x1.min())));
00184 
00185     if (x0.assigned() && x1.assigned())
00186       goto subsumed;
00187     return ES_NOFIX;
00188 
00189   prop_xxn:
00190     assert(any(x0) && any(x1) && neg(x2));
00191 
00192     GECODE_ME_CHECK(x0.lq(home, m<double>(x1.min(),x2.min()-1)));
00193     GECODE_ME_CHECK(x0.gq(home, m<double>(x1.max(),x2.min()-1)));
00194 
00195     if (pos(x0)) goto rewrite_pnn;
00196     if (neg(x0)) goto rewrite_npn;
00197 
00198     if (x2.max() != -1)
00199       GECODE_ME_CHECK(x1.lq(home,c_d(x0.min(),x2.max()+1)));
00200     if (x2.max() != -1)
00201       GECODE_ME_CHECK(x1.gq(home,c_d(x0.max(),x2.max()+1)));
00202 
00203     if (x0.assigned() && x1.assigned())
00204       goto subsumed;
00205     return ES_NOFIX;
00206 
00207   prop_xnx:
00208     assert(any(x0) && neg(x1) && any(x2));
00209 
00210     GECODE_ME_CHECK(x0.lq(home, m<double>(x1.min(),x2.min()-1)));
00211     GECODE_ME_CHECK(x0.gq(home, m<double>(x1.min(),x2.max()+1)));
00212 
00213     if (pos(x0)) goto rewrite_pnn;
00214     if (neg(x0)) goto rewrite_nnp;
00215 
00216     GECODE_ME_CHECK(x2.lq(home,f_d(x0.min(),x1.max())));
00217     GECODE_ME_CHECK(x2.gq(home,f_d(x0.max(),x1.max())));
00218 
00219     if (x0.assigned() && x1.assigned())
00220       goto subsumed;
00221     return ES_NOFIX;
00222 
00223   rewrite_ppp:
00224     GECODE_REWRITE(*this,(DivPlusBnd<double,IntView,IntView,IntView>
00225                          ::post(home(*this),x0,x1,x2)));
00226   rewrite_nnp:
00227     GECODE_REWRITE(*this,(DivPlusBnd<double,MinusView,MinusView,IntView>
00228                          ::post(home(*this),MinusView(x0),MinusView(x1),x2)));
00229   rewrite_pnn:
00230     GECODE_REWRITE(*this,(DivPlusBnd<double,IntView,MinusView,MinusView>
00231                          ::post(home(*this),x0,MinusView(x1),MinusView(x2))));
00232   rewrite_npn:
00233     GECODE_REWRITE(*this,(DivPlusBnd<double,MinusView,IntView,MinusView>
00234                          ::post(home(*this),MinusView(x0),x1,MinusView(x2))));
00235   subsumed:
00236     assert(x0.assigned() && x1.assigned());
00237     int result = std::abs(x0.val()) / std::abs(x1.val());
00238     if (x0.val()/x1.val() < 0)
00239       result = -result;
00240     GECODE_ME_CHECK(x2.eq(home,result));
00241     return home.ES_SUBSUMED(*this);
00242   }
00243 
00244   template<class View>
00245   ExecStatus
00246   DivBnd<View>::post(Home home, View x0, View x1, View x2) {
00247     GECODE_ME_CHECK(x1.nq(home, 0));
00248     if (pos(x0)) {
00249       if (pos(x1) || pos(x2)) goto post_ppp;
00250       if (neg(x1) || neg(x2)) goto post_pnn;
00251     } else if (neg(x0)) {
00252       if (neg(x1) || pos(x2)) goto post_nnp;
00253       if (pos(x1) || neg(x2)) goto post_npn;
00254     } else if (pos(x1)) {
00255       if (pos(x2)) goto post_ppp;
00256       if (neg(x2)) goto post_npn;
00257     } else if (neg(x1)) {
00258       if (pos(x2)) goto post_nnp;
00259       if (neg(x2)) goto post_pnn;
00260     }
00261     (void) new (home) DivBnd<View>(home,x0,x1,x2);
00262     return ES_OK;
00263 
00264   post_ppp:
00265     return DivPlusBnd<double,IntView,IntView,IntView>::post(home,x0,x1,x2);
00266   post_nnp:
00267     return DivPlusBnd<double,MinusView,MinusView,IntView>::post(home,
00268       MinusView(x0),MinusView(x1),x2);
00269   post_pnn:
00270     return DivPlusBnd<double,IntView,MinusView,MinusView>::post(home,
00271       x0,MinusView(x1),MinusView(x2));
00272   post_npn:
00273     return DivPlusBnd<double,MinusView,IntView,MinusView>::post(home,
00274       MinusView(x0),x1,MinusView(x2));
00275   }
00276 
00277 
00278   /*
00279    * Propagator for x0 != 0 /\ (x1 != 0 => x0*x1>0) /\ abs(x1)<abs(x0)
00280    *
00281    */
00282 
00283   template<class View>
00284   forceinline
00285   DivMod<View>::DivMod(Home home, View x0, View x1, View x2)
00286     : TernaryPropagator<View,PC_INT_BND>(home,x0,x1,x2) {}
00287 
00288   template<class View>
00289   forceinline ExecStatus
00290   DivMod<View>::post(Home home, View x0, View x1, View x2) {
00291     GECODE_ME_CHECK(x1.nq(home,0));
00292     (void) new (home) DivMod<View>(home,x0,x1,x2);
00293     return ES_OK;
00294   }
00295 
00296   template<class View>
00297   forceinline
00298   DivMod<View>::DivMod(Space& home, bool share, DivMod<View>& p)
00299   : TernaryPropagator<View,PC_INT_BND>(home,share,p) {}
00300 
00301   template<class View>
00302   Actor*
00303   DivMod<View>::copy(Space& home, bool share) {
00304     return new (home) DivMod<View>(home,share,*this);
00305   }
00306 
00307   template<class View>
00308   ExecStatus
00309   DivMod<View>::propagate(Space& home, const ModEventDelta&) {
00310     bool signIsSame;
00311     do {
00312       signIsSame = true;
00313       // The sign of x0 and x2 is the same
00314       if (x0.min() >= 0) {
00315         GECODE_ME_CHECK(x2.gq(home, 0));
00316       } else if (x0.max() <= 0) {
00317         GECODE_ME_CHECK(x2.lq(home, 0));
00318       } else if (x2.min() > 0) {
00319         GECODE_ME_CHECK(x0.gq(home, 0));
00320       } else if (x2.max() < 0) {
00321         GECODE_ME_CHECK(x0.lq(home, 0));
00322       } else {
00323         signIsSame = false;
00324       }
00325 
00326       // abs(x2) is less than abs(x1)
00327       int x1max = std::max(x1.max(),std::max(-x1.max(),
00328                            std::max(x1.min(),-x1.min())));
00329       GECODE_ME_CHECK(x2.le(home, x1max));
00330       GECODE_ME_CHECK(x2.gr(home, -x1max));
00331 
00332       int x2absmin = any(x2) ? 0 : (pos(x2) ? x2.min() : -x2.max());
00333       Iter::Ranges::Singleton sr(-x2absmin,x2absmin);
00334       GECODE_ME_CHECK(x1.minus_r(home,sr,false));
00335     } while (!signIsSame &&
00336              (x0.min() > 0 || x0.max() < 0 || x2.min() > 0 || x2.max() < 0));
00337 
00338     if (signIsSame) {
00339       int x2max = std::max(x2.max(),std::max(-x2.max(),
00340                            std::max(x2.min(),-x2.min())));
00341       int x1absmin = any(x1) ? 0 : (pos(x1) ? x1.min() : -x1.max());
00342       if (x2max < x1absmin)
00343         return home.ES_SUBSUMED(*this);
00344     }
00345     return ES_FIX;
00346   }
00347 
00348 }}}
00349 
00350 // STATISTICS: int-prop