00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034 #include <gecode/int/linear.hh>
00035
00036 namespace Gecode { namespace Int { namespace Arithmetic {
00037
00038
00039
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
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
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
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
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