1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ 2 /* 3 * Main authors: 4 * Patrick Pekczynski <pekczynski@ps.uni-sb.de> 5 * 6 * Contributing authors: 7 * Christian Schulte <schulte@gecode.org> 8 * Guido Tack <tack@gecode.org> 9 * 10 * Copyright: 11 * Patrick Pekczynski, 2004 12 * Christian Schulte, 2009 13 * Guido Tack, 2009 14 * 15 * This file is part of Gecode, the generic constraint 16 * development environment: 17 * http://www.gecode.org 18 * 19 * Permission is hereby granted, free of charge, to any person obtaining 20 * a copy of this software and associated documentation files (the 21 * "Software"), to deal in the Software without restriction, including 22 * without limitation the rights to use, copy, modify, merge, publish, 23 * distribute, sublicense, and/or sell copies of the Software, and to 24 * permit persons to whom the Software is furnished to do so, subject to 25 * the following conditions: 26 * 27 * The above copyright notice and this permission notice shall be 28 * included in all copies or substantial portions of the Software. 29 * 30 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 31 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 32 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 33 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE 34 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION 35 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION 36 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 37 * 38 */ 39 40 namespace Gecode { namespace Int { namespace GCC { 41 42 /** 43 * \defgroup GCCBndSup Support for GCC bounds propagation 44 * 45 * \ingroup FuncIntProp 46 */ 47 48 /** 49 * \brief Class for computing unreachable values in the value %GCC propagator 50 * 51 * \ingroup GCCBndSup 52 */ 53 class UnReachable { 54 public: 55 /// Number of variables with lower bound 56 int minb; 57 /// Number of variables with upper bound 58 int maxb; 59 /// Number of equal variables 60 int eq; 61 /// Number of smaller variables 62 int le; 63 /// Number of greater variables 64 int gr; 65 }; 66 67 /** 68 * \brief Bounds consistency check for cardinality variables. 69 * \ingroup GCCBndSup 70 */ 71 72 template<class Card> 73 ExecStatus prop_card(Space & home,ViewArray<IntView> & x,ViewArray<Card> & k)74 prop_card(Space& home, 75 ViewArray<IntView>& x, ViewArray<Card>& k) { 76 int n = x.size(); 77 int m = k.size(); 78 Region r; 79 UnReachable* rv = r.alloc<UnReachable>(m); 80 for(int i = m; i--; ) 81 rv[i].minb=rv[i].maxb=rv[i].le=rv[i].gr=rv[i].eq=0; 82 83 for (int i = n; i--; ) { 84 int min_idx; 85 if (!lookupValue(k,x[i].min(),min_idx)) 86 return ES_FAILED; 87 if (x[i].assigned()) { 88 rv[min_idx].minb++; 89 rv[min_idx].maxb++; 90 rv[min_idx].eq++; 91 } else { 92 // count the number of variables 93 // with lower bound k[min_idx].card() 94 rv[min_idx].minb++; 95 int max_idx; 96 if (!lookupValue(k,x[i].max(),max_idx)) 97 return ES_FAILED; 98 // count the number of variables 99 // with upper bound k[max_idx].card() 100 rv[max_idx].maxb++; 101 } 102 } 103 104 rv[0].le = 0; 105 int c_min = 0; 106 for (int i = 1; i < m; i++) { 107 rv[i].le = c_min + rv[i - 1].maxb; 108 c_min += rv[i - 1].maxb; 109 } 110 111 rv[m-1].gr = 0; 112 int c_max = 0; 113 for (int i = m-1; i--; ) { 114 rv[i].gr = c_max + rv[i + 1].minb; 115 c_max += rv[i + 1].minb; 116 } 117 118 for (int i = m; i--; ) { 119 int reachable = x.size() - rv[i].le - rv[i].gr; 120 if (!k[i].assigned()) { 121 GECODE_ME_CHECK(k[i].lq(home, reachable)); 122 GECODE_ME_CHECK(k[i].gq(home, rv[i].eq)); 123 } else { 124 // check validity of the cardinality value 125 if ((rv[i].eq > k[i].max()) || (k[i].max() > reachable)) 126 return ES_FAILED; 127 } 128 } 129 130 return ES_OK; 131 } 132 133 134 /** \brief Consistency check, whether the cardinality values are feasible. 135 * \ingroup GCCBndSup 136 */ 137 template<class Card> 138 forceinline bool card_consistent(ViewArray<IntView> & x,ViewArray<Card> & k)139 card_consistent(ViewArray<IntView>& x, ViewArray<Card>& k) { 140 int smin = 0; 141 int smax = 0; 142 for (int i = k.size(); i--; ) { 143 smax += k[i].max(); 144 smin += k[i].min(); 145 } 146 // Consistent if number of variables within cardinality bounds 147 return (smin <= x.size()) && (x.size() <= smax); 148 } 149 150 /** 151 * \brief Maps domain bounds to their position in hall[].bounds. 152 * \ingroup GCCBndSup 153 */ 154 class Rank { 155 public: 156 /** 157 * \brief \f$ rank[i].min = z 158 * \Leftrightarrow min(x_i) = hall[z].bounds \f$ 159 */ 160 int min; 161 /** 162 * \brief \f$ rank[i].max = z 163 * \Leftrightarrow max(x_i) = hall[z].bounds \f$ 164 */ 165 int max; 166 }; 167 168 /** 169 * \brief Compares two indices \a i, \a j of two views 170 * \a \f$ x_i \f$ \f$ x_j\f$ according to the 171 * ascending order of the views upper bounds 172 * 173 * \ingroup GCCBndSup 174 */ 175 template<class View> 176 class MaxInc { 177 protected: 178 /// View array for comparison 179 ViewArray<View> x; 180 public: 181 /// Constructor MaxInc(const ViewArray<View> & x0)182 MaxInc(const ViewArray<View>& x0) : x(x0) {} 183 /// Order 184 forceinline bool operator ()(const int i,const int j)185 operator ()(const int i, const int j) { 186 return x[i].max() < x[j].max(); 187 } 188 }; 189 190 191 /** 192 * \brief Compares two indices \a i, \a j of two views 193 * \a \f$ x_i \f$ \f$ x_j\f$ according to the 194 * ascending order of the views lower bounds 195 * 196 * \ingroup GCCBndSup 197 */ 198 template<class View> 199 class MinInc { 200 protected: 201 /// View array for comparison 202 ViewArray<View> x; 203 public: 204 /// Constructor MinInc(const ViewArray<View> & x0)205 MinInc(const ViewArray<View>& x0) : x(x0) {} 206 /// Comparison 207 forceinline bool operator ()(const int i,const int j)208 operator ()(const int i, const int j) { 209 return x[i].min() < x[j].min(); 210 } 211 }; 212 213 214 /** 215 * \brief Compares two cardinality views 216 * \a \f$ x_i \f$ \f$ x_j\f$ according to the index 217 * 218 * \ingroup GCCBndSup 219 */ 220 template<class Card> 221 class MinIdx { 222 public: 223 /// Comparison 224 forceinline bool operator ()(const Card & x,const Card & y)225 operator ()(const Card& x, const Card& y) { 226 return x.card() < y.card(); 227 } 228 }; 229 230 /** 231 * \brief Partial sum structure for constant 232 * time computation of the maximal capacity of an interval. 233 * 234 * \ingroup GCCBndSup 235 */ 236 template<class Card> 237 class PartialSum { 238 private: 239 /// sum[i] contains the partial sum from 0 to i 240 int* sum; 241 /// the size of the sum 242 int size; 243 public: 244 /// Sentinels indicating whether an end of sum is reached 245 int firstValue, lastValue; 246 /// \name Initialization 247 //@{ 248 /// Constructor 249 PartialSum(void); 250 /// Initialization 251 void init(Space& home, ViewArray<Card>& k, bool up); 252 /// Mark datstructure as requiring reinitialization 253 void reinit(void); 254 /// Test whether already initialized 255 operator bool(void) const; 256 //@} 257 /// \name Access 258 //@{ 259 /// Compute the maximum capacity of an interval 260 int sumup(int from, int to) const; 261 /// Return smallest bound of variables 262 int minValue(void) const; 263 /// Return largest bound of variables 264 int maxValue(void) const; 265 /// Skip neigbouring array entries if their values do not differ 266 int skipNonNullElementsRight(int v) const; 267 /// Skip neigbouring array entries if their values do not differ 268 int skipNonNullElementsLeft(int v) const; 269 //@} 270 /// \name Update 271 //@{ 272 /** 273 * \brief Check whether the values in the 274 * partial sum structure containting 275 * the lower cardinality bounds differ 276 * from the actual lower bounds of the 277 * cardinalities. 278 */ 279 bool check_update_min(ViewArray<Card>& k); 280 /** 281 * \brief Check whether the values in the 282 * partial sum structure containting 283 * the upper cardinality bounds differ 284 * from the actual upper bounds of the 285 * cardinalities. 286 */ 287 bool check_update_max(ViewArray<Card>& k); 288 //@} 289 }; 290 291 292 template<class Card> 293 forceinline PartialSum(void)294 PartialSum<Card>::PartialSum(void) : sum(nullptr), size(-1) {} 295 296 template<class Card> 297 forceinline operator bool(void) const298 PartialSum<Card>::operator bool(void) const { 299 return size != -1; 300 } 301 template<class Card> 302 inline void init(Space & home,ViewArray<Card> & elements,bool up)303 PartialSum<Card>::init(Space& home, ViewArray<Card>& elements, bool up) { 304 int i = 0; 305 int j = 0; 306 307 // Determine number of holes in the index set 308 int holes = 0; 309 for (i = 1; i < elements.size(); i++) { 310 if (elements[i].card() != elements[i-1].card() + 1) 311 holes += elements[i].card()-elements[i-1].card()-1; 312 } 313 314 // we add three elements at the beginning and two at the end 315 size = elements.size() + holes + 5; 316 317 // memory allocation 318 if (sum == nullptr) { 319 sum = home.alloc<int>(2*size); 320 } 321 int* ds = &sum[size]; 322 323 int first = elements[0].card(); 324 325 firstValue = first - 3; 326 lastValue = first + elements.size() + holes + 1; 327 328 // the first three elements 329 for (i = 3; i--; ) 330 sum[i] = i; 331 332 /* 333 * copy the bounds into sum, filling up holes with zeroes 334 */ 335 int prevCard = elements[0].card()-1; 336 i = 0; 337 for (j = 2; j < elements.size() + holes + 2; j++) { 338 if (elements[i].card() != prevCard + 1) { 339 sum[j + 1] = sum[j]; 340 } else if (up) { 341 sum[j + 1] = sum[j] + elements[i].max(); 342 i++; 343 } else { 344 sum[j + 1] = sum[j] + elements[i].min(); 345 i++; 346 } 347 prevCard++; 348 } 349 sum[j + 1] = sum[j] + 1; 350 sum[j + 2] = sum[j + 1] + 1; 351 352 // Compute distances, eliminating zeroes 353 i = elements.size() + holes + 3; 354 j = i + 1; 355 for ( ; i > 0; ) { 356 while(sum[i] == sum[i - 1]) { 357 ds[i] = j; 358 i--; 359 } 360 ds[j] = i; 361 i--; 362 j = ds[j]; 363 } 364 ds[j] = 0; 365 ds[0] = 0; 366 } 367 368 template<class Card> 369 forceinline void reinit(void)370 PartialSum<Card>::reinit(void) { 371 size = -1; 372 } 373 374 375 template<class Card> 376 forceinline int sumup(int from,int to) const377 PartialSum<Card>::sumup(int from, int to) const { 378 if (from <= to) { 379 return sum[to - firstValue] - sum[from - firstValue - 1]; 380 } else { 381 assert(to - firstValue - 1 >= 0); 382 assert(to - firstValue - 1 < size); 383 assert(from - firstValue >= 0); 384 assert(from - firstValue < size); 385 return sum[to - firstValue - 1] - sum[from - firstValue]; 386 } 387 } 388 389 template<class Card> 390 forceinline int minValue(void) const391 PartialSum<Card>::minValue(void) const { 392 return firstValue + 3; 393 } 394 template<class Card> 395 forceinline int maxValue(void) const396 PartialSum<Card>::maxValue(void) const { 397 return lastValue - 2; 398 } 399 400 401 template<class Card> 402 forceinline int skipNonNullElementsRight(int value) const403 PartialSum<Card>::skipNonNullElementsRight(int value) const { 404 value -= firstValue; 405 int* ds = &sum[size]; 406 return (ds[value] < value ? value : ds[value]) + firstValue; 407 } 408 template<class Card> 409 forceinline int skipNonNullElementsLeft(int value) const410 PartialSum<Card>::skipNonNullElementsLeft(int value) const { 411 value -= firstValue; 412 int* ds = &sum[size]; 413 return (ds[value] > value ? ds[ds[value]] : value) + firstValue; 414 } 415 416 template<class Card> 417 inline bool check_update_max(ViewArray<Card> & k)418 PartialSum<Card>::check_update_max(ViewArray<Card>& k) { 419 int j = 0; 420 for (int i = 3; i < size - 2; i++) { 421 int max = 0; 422 if (k[j].card() == i+firstValue) 423 max = k[j++].max(); 424 if ((sum[i] - sum[i - 1]) != max) 425 return true; 426 } 427 return false; 428 } 429 430 template<class Card> 431 inline bool check_update_min(ViewArray<Card> & k)432 PartialSum<Card>::check_update_min(ViewArray<Card>& k) { 433 int j = 0; 434 for (int i = 3; i < size - 2; i++) { 435 int min = 0; 436 if (k[j].card() == i+firstValue) 437 min = k[j++].min(); 438 if ((sum[i] - sum[i - 1]) != min) 439 return true; 440 } 441 return false; 442 } 443 444 445 /** 446 * \brief Container class provding information about the Hall 447 * structure of the problem variables. 448 * 449 * This class is used to 450 * keep the number of different arrays small, that is 451 * an array of type %HallInfo replaces integer arrays for each 452 * of the class members. 453 * 454 * \ingroup GCCBndSup 455 */ 456 class HallInfo { 457 public: 458 /// Represents the union of all lower and upper domain bounds 459 int bounds; 460 /** 461 * \brief Critical capacity pointer 462 * \a t represents a predecessor function where \f$ t_i \f$ denotes the 463 * predecessor of i in bounds 464 */ 465 int t; 466 /** 467 * \brief Difference between critical capacities 468 * 469 * \a d_i is the difference between the capacities of hall[i].bounds 470 * and its predecessor in bounds hall[t[i]].bounds 471 * 472 */ 473 int d; 474 /** 475 * \brief Hall set pointer 476 * 477 * If hall[i].h < i then the half-open interval 478 * [hall[h[i]].bounds,hall[i].bounds) is containd in a Hall 479 * set. 480 * Otherwise holds a pointer to the Hall intervall it belongs to. 481 */ 482 int h; 483 /// Stable Set pointer 484 int s; 485 /// Potentially Stable Set pointer 486 int ps; 487 /** 488 * \brief Bound update 489 * 490 * \a newBound contains either a narrowed domain bound 491 * or is stores the old domain bound of a variable. 492 */ 493 int newBound; 494 }; 495 496 497 /** 498 * \name Path compression 499 * 500 * Each of the nodes on the path from \a start to \a end 501 * becomes a direct child of \a to. 502 * \ingroup GCCBndSup 503 */ 504 //@{ 505 /// Path compression for potentially stable set structure 506 forceinline void pathset_ps(HallInfo hall[],int start,int end,int to)507 pathset_ps(HallInfo hall[], int start, int end, int to) { 508 int k, l; 509 for (l=start; (k=l) != end; hall[k].ps=to) { 510 l = hall[k].ps; 511 } 512 } 513 /// Path compression for stable set structure 514 forceinline void pathset_s(HallInfo hall[],int start,int end,int to)515 pathset_s(HallInfo hall[], int start, int end, int to) { 516 int k, l; 517 for (l=start; (k=l) != end; hall[k].s=to) { 518 l = hall[k].s; 519 } 520 } 521 /// Path compression for capacity pointer structure 522 forceinline void pathset_t(HallInfo hall[],int start,int end,int to)523 pathset_t(HallInfo hall[], int start, int end, int to) { 524 int k, l; 525 for (l=start; (k=l) != end; hall[k].t=to) { 526 l = hall[k].t; 527 } 528 } 529 /// Path compression for hall pointer structure 530 forceinline void pathset_h(HallInfo hall[],int start,int end,int to)531 pathset_h(HallInfo hall[], int start, int end, int to) { 532 int k, l; 533 for (l=start; (k=l) != end; hall[k].h=to) { 534 l = hall[k].h; 535 assert(l != k); 536 } 537 } 538 //@} 539 540 /** 541 * \name Path minimum 542 * 543 * Returns the smalles reachable index starting from \a i. 544 * \ingroup GCCBndSup 545 */ 546 //@{ 547 /// Path minimum for hall pointer structure 548 forceinline int pathmin_h(const HallInfo hall[],int i)549 pathmin_h(const HallInfo hall[], int i) { 550 while (hall[i].h < i) 551 i = hall[i].h; 552 return i; 553 } 554 /// Path minimum for capacity pointer structure 555 forceinline int pathmin_t(const HallInfo hall[],int i)556 pathmin_t(const HallInfo hall[], int i) { 557 while (hall[i].t < i) 558 i = hall[i].t; 559 return i; 560 } 561 //@} 562 563 /** 564 * \name Path maximum 565 * 566 * Returns the greatest reachable index starting from \a i. 567 * \ingroup GCCBndSup 568 */ 569 //@{ 570 /// Path maximum for hall pointer structure 571 forceinline int pathmax_h(const HallInfo hall[],int i)572 pathmax_h(const HallInfo hall[], int i) { 573 while (hall[i].h > i) 574 i = hall[i].h; 575 return i; 576 } 577 /// Path maximum for capacity pointer structure 578 forceinline int pathmax_t(const HallInfo hall[],int i)579 pathmax_t(const HallInfo hall[], int i) { 580 while (hall[i].t > i) { 581 i = hall[i].t; 582 } 583 return i; 584 } 585 /// Path maximum for stable set pointer structure 586 forceinline int pathmax_s(const HallInfo hall[],int i)587 pathmax_s(const HallInfo hall[], int i) { 588 while (hall[i].s > i) 589 i = hall[i].s; 590 return i; 591 } 592 /// Path maximum for potentially stable set pointer structure 593 forceinline int pathmax_ps(const HallInfo hall[],int i)594 pathmax_ps(const HallInfo hall[], int i) { 595 while (hall[i].ps > i) 596 i = hall[i].ps; 597 return i; 598 } 599 //@} 600 601 }}} 602 603 // STATISTICS: int-prop 604 605