1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ 2 /* 3 * Main authors: 4 * Christian Schulte <schulte@gecode.org> 5 * 6 * Copyright: 7 * Christian Schulte, 2003 8 * 9 * This file is part of Gecode, the generic constraint 10 * development environment: 11 * http://www.gecode.org 12 * 13 * Permission is hereby granted, free of charge, to any person obtaining 14 * a copy of this software and associated documentation files (the 15 * "Software"), to deal in the Software without restriction, including 16 * without limitation the rights to use, copy, modify, merge, publish, 17 * distribute, sublicense, and/or sell copies of the Software, and to 18 * permit persons to whom the Software is furnished to do so, subject to 19 * the following conditions: 20 * 21 * The above copyright notice and this permission notice shall be 22 * included in all copies or substantial portions of the Software. 23 * 24 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 25 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 26 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 27 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE 28 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION 29 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION 30 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 31 * 32 */ 33 34 namespace Gecode { namespace Int { namespace Linear { 35 36 /* 37 * Binary linear propagators 38 * 39 */ 40 template<class Val, class A, class B, PropCond pc> 41 forceinline LinBin(Home home,A y0,B y1,Val c0)42 LinBin<Val,A,B,pc>::LinBin(Home home, A y0, B y1, Val c0) 43 : Propagator(home), x0(y0), x1(y1), c(c0) { 44 x0.subscribe(home,*this,pc); 45 x1.subscribe(home,*this,pc); 46 } 47 48 template<class Val, class A, class B, PropCond pc> 49 forceinline LinBin(Space & home,LinBin<Val,A,B,pc> & p)50 LinBin<Val,A,B,pc>::LinBin(Space& home, LinBin<Val,A,B,pc>& p) 51 : Propagator(home,p), c(p.c) { 52 x0.update(home,p.x0); 53 x1.update(home,p.x1); 54 } 55 56 template<class Val, class A, class B, PropCond pc> 57 forceinline LinBin(Space & home,Propagator & p,A y0,B y1,Val c0)58 LinBin<Val,A,B,pc>::LinBin(Space& home, Propagator& p, 59 A y0, B y1, Val c0) 60 : Propagator(home,p), c(c0) { 61 x0.update(home,y0); 62 x1.update(home,y1); 63 } 64 65 template<class Val, class A, class B, PropCond pc> 66 PropCost cost(const Space &,const ModEventDelta &) const67 LinBin<Val,A,B,pc>::cost(const Space&, const ModEventDelta&) const { 68 return PropCost::binary(PropCost::LO); 69 } 70 71 template<class Val, class A, class B, PropCond pc> 72 void reschedule(Space & home)73 LinBin<Val,A,B,pc>::reschedule(Space& home) { 74 x0.reschedule(home,*this,pc); 75 x1.reschedule(home,*this,pc); 76 } 77 78 template<class Val, class A, class B, PropCond pc> 79 forceinline size_t dispose(Space & home)80 LinBin<Val,A,B,pc>::dispose(Space& home) { 81 x0.cancel(home,*this,pc); 82 x1.cancel(home,*this,pc); 83 (void) Propagator::dispose(home); 84 return sizeof(*this); 85 } 86 87 88 /* 89 * Binary reified linear propagators 90 * 91 */ 92 template<class Val, class A, class B, PropCond pc, class Ctrl> 93 forceinline ReLinBin(Home home,A y0,B y1,Val c0,Ctrl b0)94 ReLinBin<Val,A,B,pc,Ctrl>::ReLinBin(Home home, A y0, B y1, Val c0, Ctrl b0) 95 : Propagator(home), x0(y0), x1(y1), c(c0), b(b0) { 96 x0.subscribe(home,*this,pc); 97 x1.subscribe(home,*this,pc); 98 b.subscribe(home,*this,PC_INT_VAL); 99 } 100 101 template<class Val, class A, class B, PropCond pc, class Ctrl> 102 forceinline ReLinBin(Space & home,ReLinBin<Val,A,B,pc,Ctrl> & p)103 ReLinBin<Val,A,B,pc,Ctrl>::ReLinBin(Space& home, 104 ReLinBin<Val,A,B,pc,Ctrl>& p) 105 : Propagator(home,p), c(p.c) { 106 x0.update(home,p.x0); 107 x1.update(home,p.x1); 108 b.update(home,p.b); 109 } 110 111 template<class Val, class A, class B, PropCond pc, class Ctrl> 112 PropCost cost(const Space &,const ModEventDelta &) const113 ReLinBin<Val,A,B,pc,Ctrl>::cost(const Space&, const ModEventDelta&) const { 114 return PropCost::binary(PropCost::LO); 115 } 116 117 template<class Val, class A, class B, PropCond pc, class Ctrl> 118 void reschedule(Space & home)119 ReLinBin<Val,A,B,pc,Ctrl>::reschedule(Space& home) { 120 x0.reschedule(home,*this,pc); 121 x1.reschedule(home,*this,pc); 122 b.reschedule(home,*this,PC_INT_VAL); 123 } 124 125 template<class Val, class A, class B, PropCond pc, class Ctrl> 126 forceinline size_t dispose(Space & home)127 ReLinBin<Val,A,B,pc,Ctrl>::dispose(Space& home) { 128 x0.cancel(home,*this,pc); 129 x1.cancel(home,*this,pc); 130 b.cancel(home,*this,PC_BOOL_VAL); 131 (void) Propagator::dispose(home); 132 return sizeof(*this); 133 } 134 135 /* 136 * Binary bounds consistent linear equality 137 * 138 */ 139 140 template<class Val, class A, class B> 141 forceinline EqBin(Home home,A x0,B x1,Val c)142 EqBin<Val,A,B>::EqBin(Home home, A x0, B x1, Val c) 143 : LinBin<Val,A,B,PC_INT_BND>(home,x0,x1,c) {} 144 145 template<class Val, class A, class B> 146 ExecStatus post(Home home,A x0,B x1,Val c)147 EqBin<Val,A,B>::post(Home home, A x0, B x1, Val c) { 148 (void) new (home) EqBin<Val,A,B>(home,x0,x1,c); 149 return ES_OK; 150 } 151 152 153 template<class Val, class A, class B> 154 forceinline EqBin(Space & home,EqBin<Val,A,B> & p)155 EqBin<Val,A,B>::EqBin(Space& home, EqBin<Val,A,B>& p) 156 : LinBin<Val,A,B,PC_INT_BND>(home,p) {} 157 158 template<class Val, class A, class B> 159 forceinline EqBin(Space & home,Propagator & p,A x0,B x1,Val c)160 EqBin<Val,A,B>::EqBin(Space& home, Propagator& p, 161 A x0, B x1, Val c) 162 : LinBin<Val,A,B,PC_INT_BND>(home,p,x0,x1,c) {} 163 164 template<class Val, class A, class B> 165 Actor* copy(Space & home)166 EqBin<Val,A,B>::copy(Space& home) { 167 return new (home) EqBin<Val,A,B>(home,*this); 168 } 169 170 /// Describe which view has been modified how 171 enum BinMod { 172 BM_X0_MIN = 1<<0, 173 BM_X0_MAX = 1<<1, 174 BM_X1_MIN = 1<<2, 175 BM_X1_MAX = 1<<3, 176 BM_ALL = BM_X0_MIN|BM_X0_MAX|BM_X1_MIN|BM_X1_MAX 177 }; 178 179 #define GECODE_INT_PV(CASE,TELL,UPDATE) \ 180 if (bm & (CASE)) { \ 181 bm -= (CASE); ModEvent me = (TELL); \ 182 if (me_failed(me)) return ES_FAILED; \ 183 if (me_modified(me)) bm |= (UPDATE); \ 184 } 185 186 template<class Val, class A, class B> 187 ExecStatus propagate(Space & home,const ModEventDelta &)188 EqBin<Val,A,B>::propagate(Space& home, const ModEventDelta&) { 189 int bm = BM_ALL; 190 do { 191 GECODE_INT_PV(BM_X0_MIN, x0.gq(home,c-x1.max()), BM_X1_MAX); 192 GECODE_INT_PV(BM_X1_MIN, x1.gq(home,c-x0.max()), BM_X0_MAX); 193 GECODE_INT_PV(BM_X0_MAX, x0.lq(home,c-x1.min()), BM_X1_MIN); 194 GECODE_INT_PV(BM_X1_MAX, x1.lq(home,c-x0.min()), BM_X0_MIN); 195 } while (bm); 196 return x0.assigned() ? home.ES_SUBSUMED(*this) : ES_FIX; 197 } 198 199 #undef GECODE_INT_PV 200 201 202 203 204 205 /* 206 * Reified binary bounds consistent linear equality 207 * 208 */ 209 210 template<class Val, class A, class B, class Ctrl, ReifyMode rm> 211 forceinline ReEqBin(Home home,A x0,B x1,Val c,Ctrl b)212 ReEqBin<Val,A,B,Ctrl,rm>::ReEqBin(Home home, A x0, B x1, Val c, Ctrl b) 213 : ReLinBin<Val,A,B,PC_INT_BND,Ctrl>(home,x0,x1,c,b) {} 214 215 template<class Val, class A, class B, class Ctrl, ReifyMode rm> 216 ExecStatus post(Home home,A x0,B x1,Val c,Ctrl b)217 ReEqBin<Val,A,B,Ctrl,rm>::post(Home home, A x0, B x1, Val c, Ctrl b) { 218 (void) new (home) ReEqBin<Val,A,B,Ctrl,rm>(home,x0,x1,c,b); 219 return ES_OK; 220 } 221 222 223 template<class Val, class A, class B, class Ctrl, ReifyMode rm> 224 forceinline ReEqBin(Space & home,ReEqBin<Val,A,B,Ctrl,rm> & p)225 ReEqBin<Val,A,B,Ctrl,rm>::ReEqBin(Space& home, 226 ReEqBin<Val,A,B,Ctrl,rm>& p) 227 : ReLinBin<Val,A,B,PC_INT_BND,Ctrl>(home,p) {} 228 229 template<class Val, class A, class B, class Ctrl, ReifyMode rm> 230 Actor* copy(Space & home)231 ReEqBin<Val,A,B,Ctrl,rm>::copy(Space& home) { 232 return new (home) ReEqBin<Val,A,B,Ctrl,rm>(home,*this); 233 } 234 235 template<class Val, class A, class B, class Ctrl, ReifyMode rm> 236 ExecStatus propagate(Space & home,const ModEventDelta &)237 ReEqBin<Val,A,B,Ctrl,rm>::propagate(Space& home, const ModEventDelta&) { 238 if (b.zero()) { 239 if (rm == RM_IMP) 240 return home.ES_SUBSUMED(*this); 241 GECODE_REWRITE(*this,(NqBin<Val,A,B>::post(home(*this),x0,x1,c))); 242 } 243 if (b.one()) { 244 if (rm == RM_PMI) 245 return home.ES_SUBSUMED(*this); 246 GECODE_REWRITE(*this,(EqBin<Val,A,B>::post(home(*this),x0,x1,c))); 247 } 248 if ((x0.min() + x1.min() > c) || (x0.max() + x1.max() < c)) { 249 if (rm != RM_PMI) 250 GECODE_ME_CHECK(b.zero_none(home)); 251 return home.ES_SUBSUMED(*this); 252 } 253 if (x0.assigned() && x1.assigned()) { 254 assert(x0.val() + x1.val() == c); 255 if (rm != RM_IMP) 256 GECODE_ME_CHECK(b.one_none(home)); 257 return home.ES_SUBSUMED(*this); 258 } 259 return ES_FIX; 260 } 261 262 263 264 265 /* 266 * Binary domain consistent linear disequality 267 * 268 */ 269 template<class Val, class A, class B> 270 forceinline NqBin(Home home,A x0,B x1,Val c)271 NqBin<Val,A,B>::NqBin(Home home, A x0, B x1, Val c) 272 : LinBin<Val,A,B,PC_INT_VAL>(home,x0,x1,c) {} 273 274 template<class Val, class A, class B> 275 ExecStatus post(Home home,A x0,B x1,Val c)276 NqBin<Val,A,B>::post(Home home, A x0, B x1, Val c) { 277 (void) new (home) NqBin<Val,A,B>(home,x0,x1,c); 278 return ES_OK; 279 } 280 281 282 template<class Val, class A, class B> 283 forceinline NqBin(Space & home,NqBin<Val,A,B> & p)284 NqBin<Val,A,B>::NqBin(Space& home, NqBin<Val,A,B>& p) 285 : LinBin<Val,A,B,PC_INT_VAL>(home,p) {} 286 287 template<class Val, class A, class B> 288 Actor* copy(Space & home)289 NqBin<Val,A,B>::copy(Space& home) { 290 return new (home) NqBin<Val,A,B>(home,*this); 291 } 292 293 template<class Val, class A, class B> 294 forceinline NqBin(Space & home,Propagator & p,A x0,B x1,Val c)295 NqBin<Val,A,B>::NqBin(Space& home, Propagator& p, 296 A x0, B x1, Val c) 297 : LinBin<Val,A,B,PC_INT_VAL>(home,p,x0,x1,c) {} 298 299 300 301 template<class Val, class A, class B> 302 PropCost cost(const Space &,const ModEventDelta &) const303 NqBin<Val,A,B>::cost(const Space&, const ModEventDelta&) const { 304 return PropCost::unary(PropCost::LO); 305 } 306 307 template<class Val, class A, class B> 308 ExecStatus propagate(Space & home,const ModEventDelta &)309 NqBin<Val,A,B>::propagate(Space& home, const ModEventDelta&) { 310 if (x0.assigned()) { 311 GECODE_ME_CHECK(x1.nq(home,c-x0.val())); 312 } else { 313 assert(x1.assigned()); 314 GECODE_ME_CHECK(x0.nq(home,c-x1.val())); 315 } 316 return home.ES_SUBSUMED(*this); 317 } 318 319 320 /* 321 * Binary domain consistent less equal 322 * 323 */ 324 325 template<class Val, class A, class B> 326 forceinline LqBin(Home home,A x0,B x1,Val c)327 LqBin<Val,A,B>::LqBin(Home home, A x0, B x1, Val c) 328 : LinBin<Val,A,B,PC_INT_BND>(home,x0,x1,c) {} 329 330 template<class Val, class A, class B> 331 ExecStatus post(Home home,A x0,B x1,Val c)332 LqBin<Val,A,B>::post(Home home, A x0, B x1, Val c) { 333 (void) new (home) LqBin<Val,A,B>(home,x0,x1,c); 334 return ES_OK; 335 } 336 337 338 template<class Val, class A, class B> 339 forceinline LqBin(Space & home,LqBin<Val,A,B> & p)340 LqBin<Val,A,B>::LqBin(Space& home, LqBin<Val,A,B>& p) 341 : LinBin<Val,A,B,PC_INT_BND>(home,p) {} 342 343 template<class Val, class A, class B> 344 Actor* copy(Space & home)345 LqBin<Val,A,B>::copy(Space& home) { 346 return new (home) LqBin<Val,A,B>(home,*this); 347 } 348 349 template<class Val, class A, class B> 350 forceinline LqBin(Space & home,Propagator & p,A x0,B x1,Val c)351 LqBin<Val,A,B>::LqBin(Space& home, Propagator& p, 352 A x0, B x1, Val c) 353 : LinBin<Val,A,B,PC_INT_BND>(home,p,x0,x1,c) {} 354 355 template<class Val, class A, class B> 356 ExecStatus propagate(Space & home,const ModEventDelta &)357 LqBin<Val,A,B>::propagate(Space& home, const ModEventDelta&) { 358 GECODE_ME_CHECK(x0.lq(home,c-x1.min())); 359 GECODE_ME_CHECK(x1.lq(home,c-x0.min())); 360 return (x0.max()+x1.max() <= c) ? home.ES_SUBSUMED(*this) : ES_FIX; 361 } 362 363 364 365 366 /* 367 * Binary domain consistent greater equal 368 * 369 */ 370 371 template<class Val, class A, class B> 372 forceinline GqBin(Home home,A x0,B x1,Val c)373 GqBin<Val,A,B>::GqBin(Home home, A x0, B x1, Val c) 374 : LinBin<Val,A,B,PC_INT_BND>(home,x0,x1,c) {} 375 376 template<class Val, class A, class B> 377 ExecStatus post(Home home,A x0,B x1,Val c)378 GqBin<Val,A,B>::post(Home home, A x0, B x1, Val c) { 379 (void) new (home) GqBin<Val,A,B>(home,x0,x1,c); 380 return ES_OK; 381 } 382 383 384 template<class Val, class A, class B> 385 forceinline GqBin(Space & home,GqBin<Val,A,B> & p)386 GqBin<Val,A,B>::GqBin(Space& home, GqBin<Val,A,B>& p) 387 : LinBin<Val,A,B,PC_INT_BND>(home,p) {} 388 389 template<class Val, class A, class B> 390 Actor* copy(Space & home)391 GqBin<Val,A,B>::copy(Space& home) { 392 return new (home) GqBin<Val,A,B>(home,*this); 393 } 394 395 template<class Val, class A, class B> 396 forceinline GqBin(Space & home,Propagator & p,A x0,B x1,Val c)397 GqBin<Val,A,B>::GqBin(Space& home, Propagator& p, 398 A x0, B x1, Val c) 399 : LinBin<Val,A,B,PC_INT_BND>(home,p,x0,x1,c) {} 400 401 template<class Val, class A, class B> 402 ExecStatus propagate(Space & home,const ModEventDelta &)403 GqBin<Val,A,B>::propagate(Space& home, const ModEventDelta&) { 404 GECODE_ME_CHECK(x0.gq(home,c-x1.max())); 405 GECODE_ME_CHECK(x1.gq(home,c-x0.max())); 406 return (x0.min()+x1.min() >= c) ? home.ES_SUBSUMED(*this) : ES_FIX; 407 } 408 409 410 411 412 /* 413 * Reified binary domain consistent less equal 414 * 415 */ 416 417 template<class Val, class A, class B, ReifyMode rm> 418 forceinline ReLqBin(Home home,A x0,B x1,Val c,BoolView b)419 ReLqBin<Val,A,B,rm>::ReLqBin(Home home, A x0, B x1, Val c, BoolView b) 420 : ReLinBin<Val,A,B,PC_INT_BND,BoolView>(home,x0,x1,c,b) {} 421 422 template<class Val, class A, class B, ReifyMode rm> 423 ExecStatus post(Home home,A x0,B x1,Val c,BoolView b)424 ReLqBin<Val,A,B,rm>::post(Home home, A x0, B x1, Val c, BoolView b) { 425 (void) new (home) ReLqBin<Val,A,B,rm>(home,x0,x1,c,b); 426 return ES_OK; 427 } 428 429 430 template<class Val, class A, class B, ReifyMode rm> 431 forceinline ReLqBin(Space & home,ReLqBin<Val,A,B,rm> & p)432 ReLqBin<Val,A,B,rm>::ReLqBin(Space& home, ReLqBin<Val,A,B,rm>& p) 433 : ReLinBin<Val,A,B,PC_INT_BND,BoolView>(home,p) {} 434 435 template<class Val, class A, class B, ReifyMode rm> 436 Actor* copy(Space & home)437 ReLqBin<Val,A,B,rm>::copy(Space& home) { 438 return new (home) ReLqBin<Val,A,B,rm>(home,*this); 439 } 440 441 template<class Val, class A, class B, ReifyMode rm> 442 ExecStatus propagate(Space & home,const ModEventDelta &)443 ReLqBin<Val,A,B,rm>::propagate(Space& home, const ModEventDelta&) { 444 if (b.one()) { 445 if (rm == RM_PMI) 446 return home.ES_SUBSUMED(*this); 447 GECODE_REWRITE(*this,(LqBin<Val,A,B>::post(home(*this),x0,x1,c))); 448 } 449 if (b.zero()) { 450 if (rm == RM_IMP) 451 return home.ES_SUBSUMED(*this); 452 GECODE_REWRITE(*this,(GqBin<Val,A,B>::post(home(*this),x0,x1,c+1))); 453 } 454 if (x0.max() + x1.max() <= c) { 455 if (rm != RM_IMP) 456 GECODE_ME_CHECK(b.one_none(home)); 457 return home.ES_SUBSUMED(*this); 458 } 459 if (x0.min() + x1.min() > c) { 460 if (rm != RM_PMI) 461 GECODE_ME_CHECK(b.zero_none(home)); 462 return home.ES_SUBSUMED(*this); 463 } 464 return ES_FIX; 465 } 466 467 }}} 468 469 // STATISTICS: int-prop 470 471