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