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

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