Generated on Tue Feb 11 2025 17:33:26 for Gecode by doxygen 1.12.0
bnd-sup.hpp
Go to the documentation of this file.
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
40namespace Gecode { namespace Int { namespace GCC {
41
54 public:
56 int minb;
58 int maxb;
60 int eq;
62 int le;
64 int gr;
65 };
66
72 template<class Card>
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
137 template<class Card>
138 forceinline bool
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
154 class Rank {
155 public:
160 int min;
165 int max;
166 };
167
175 template<class View>
176 class MaxInc {
177 protected:
180 public:
182 MaxInc(const ViewArray<View>& x0) : x(x0) {}
184 forceinline bool
185 operator ()(const int i, const int j) {
186 return x[i].max() < x[j].max();
187 }
188 };
189
190
198 template<class View>
199 class MinInc {
200 protected:
203 public:
205 MinInc(const ViewArray<View>& x0) : x(x0) {}
207 forceinline bool
208 operator ()(const int i, const int j) {
209 return x[i].min() < x[j].min();
210 }
211 };
212
213
220 template<class Card>
221 class MinIdx {
222 public:
224 forceinline bool
225 operator ()(const Card& x, const Card& y) {
226 return x.card() < y.card();
227 }
228 };
229
236 template<class Card>
238 private:
240 int* sum;
242 int size;
243 public:
247
248
249 PartialSum(void);
251 void init(Space& home, ViewArray<Card>& k, bool up);
253 void reinit(void);
255 operator bool(void) const;
257
259
260 int sumup(int from, int to) const;
262 int minValue(void) const;
264 int maxValue(void) const;
266 int skipNonNullElementsRight(int v) const;
268 int skipNonNullElementsLeft(int v) const;
270
272
289 };
290
291
292 template<class Card>
294 PartialSum<Card>::PartialSum(void) : sum(NULL), size(-1) {}
295
296 template<class Card>
298 PartialSum<Card>::operator bool(void) const {
299 return size != -1;
300 }
301 template<class Card>
302 inline void
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 == NULL) {
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
371 size = -1;
372 }
373
374
375 template<class Card>
376 forceinline int
377 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
392 return firstValue + 3;
393 }
394 template<class Card>
395 forceinline int
397 return lastValue - 2;
398 }
399
400
401 template<class Card>
402 forceinline int
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
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
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
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
456 class HallInfo {
457 public:
465 int t;
473 int d;
482 int h;
484 int s;
486 int ps;
494 };
495
496
506 forceinline void
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 }
514 forceinline void
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 }
522 forceinline void
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 }
530 forceinline void
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 }
539
548 forceinline int
549 pathmin_h(const HallInfo hall[], int i) {
550 while (hall[i].h < i)
551 i = hall[i].h;
552 return i;
553 }
555 forceinline int
556 pathmin_t(const HallInfo hall[], int i) {
557 while (hall[i].t < i)
558 i = hall[i].t;
559 return i;
560 }
562
571 forceinline int
572 pathmax_h(const HallInfo hall[], int i) {
573 while (hall[i].h > i)
574 i = hall[i].h;
575 return i;
576 }
578 forceinline int
579 pathmax_t(const HallInfo hall[], int i) {
580 while (hall[i].t > i) {
581 i = hall[i].t;
582 }
583 return i;
584 }
586 forceinline int
587 pathmax_s(const HallInfo hall[], int i) {
588 while (hall[i].s > i)
589 i = hall[i].s;
590 return i;
591 }
593 forceinline int
594 pathmax_ps(const HallInfo hall[], int i) {
595 while (hall[i].ps > i)
596 i = hall[i].ps;
597 return i;
598 }
600
601}}}
602
603// STATISTICS: int-prop
604
NNF * l
Left subtree.
NodeType t
Type of node.
int n
Number of negative literals for node type.
Container class provding information about the Hall structure of the problem variables.
Definition bnd-sup.hpp:456
int t
Critical capacity pointer t represents a predecessor function where denotes the predecessor of i in ...
Definition bnd-sup.hpp:465
int newBound
Bound update.
Definition bnd-sup.hpp:493
int h
Hall set pointer.
Definition bnd-sup.hpp:482
int bounds
Represents the union of all lower and upper domain bounds.
Definition bnd-sup.hpp:459
int s
Stable Set pointer.
Definition bnd-sup.hpp:484
int ps
Potentially Stable Set pointer.
Definition bnd-sup.hpp:486
int d
Difference between critical capacities.
Definition bnd-sup.hpp:473
Compares two indices i, j of two views according to the ascending order of the views upper bounds.
Definition bnd-sup.hpp:176
ViewArray< View > x
View array for comparison.
Definition bnd-sup.hpp:179
MaxInc(const ViewArray< View > &x0)
Constructor.
Definition bnd-sup.hpp:182
bool operator()(const int i, const int j)
Order.
Definition bnd-sup.hpp:185
Compares two cardinality views according to the index.
Definition bnd-sup.hpp:221
bool operator()(const Card &x, const Card &y)
Comparison.
Definition bnd-sup.hpp:225
Compares two indices i, j of two views according to the ascending order of the views lower bounds.
Definition bnd-sup.hpp:199
MinInc(const ViewArray< View > &x0)
Constructor.
Definition bnd-sup.hpp:205
ViewArray< View > x
View array for comparison.
Definition bnd-sup.hpp:202
bool operator()(const int i, const int j)
Comparison.
Definition bnd-sup.hpp:208
Partial sum structure for constant time computation of the maximal capacity of an interval.
Definition bnd-sup.hpp:237
int firstValue
Sentinels indicating whether an end of sum is reached.
Definition bnd-sup.hpp:245
int skipNonNullElementsLeft(int v) const
Skip neigbouring array entries if their values do not differ.
Definition bnd-sup.hpp:410
int maxValue(void) const
Return largest bound of variables.
Definition bnd-sup.hpp:396
void reinit(void)
Mark datstructure as requiring reinitialization.
Definition bnd-sup.hpp:370
bool check_update_max(ViewArray< Card > &k)
Check whether the values in the partial sum structure containting the upper cardinality bounds differ...
Definition bnd-sup.hpp:418
int minValue(void) const
Return smallest bound of variables.
Definition bnd-sup.hpp:391
PartialSum(void)
Constructor.
Definition bnd-sup.hpp:294
bool check_update_min(ViewArray< Card > &k)
Check whether the values in the partial sum structure containting the lower cardinality bounds differ...
Definition bnd-sup.hpp:432
void init(Space &home, ViewArray< Card > &k, bool up)
Initialization.
Definition bnd-sup.hpp:303
int sumup(int from, int to) const
Compute the maximum capacity of an interval.
Definition bnd-sup.hpp:377
int skipNonNullElementsRight(int v) const
Skip neigbouring array entries if their values do not differ.
Definition bnd-sup.hpp:403
Maps domain bounds to their position in hall[].bounds.
Definition bnd-sup.hpp:154
Class for computing unreachable values in the value GCC propagator.
Definition bnd-sup.hpp:53
int maxb
Number of variables with upper bound.
Definition bnd-sup.hpp:58
int gr
Number of greater variables.
Definition bnd-sup.hpp:64
int minb
Number of variables with lower bound.
Definition bnd-sup.hpp:56
int eq
Number of equal variables.
Definition bnd-sup.hpp:60
int le
Number of smaller variables.
Definition bnd-sup.hpp:62
Handle to region.
Definition region.hpp:55
Computation spaces.
Definition core.hpp:1742
T * alloc(long unsigned int n)
Allocate block of n objects of type T from space heap.
Definition core.hpp:2837
View arrays.
Definition array.hpp:253
int size(void) const
Return size of array (number of elements)
Definition array.hpp:1156
bool card_consistent(ViewArray< IntView > &x, ViewArray< Card > &k)
Consistency check, whether the cardinality values are feasible.
Definition bnd-sup.hpp:139
ExecStatus prop_card(Space &home, ViewArray< IntView > &x, ViewArray< Card > &k)
Bounds consistency check for cardinality variables.
Definition bnd-sup.hpp:74
#define GECODE_ME_CHECK(me)
Check whether modification event me is failed, and forward failure.
Definition macros.hpp:52
int pathmin_h(const HallInfo hall[], int i)
Path minimum for hall pointer structure.
Definition bnd-sup.hpp:549
int pathmax_t(const HallInfo hall[], int i)
Path maximum for capacity pointer structure.
Definition bnd-sup.hpp:579
void pathset_ps(HallInfo hall[], int start, int end, int to)
Path compression for potentially stable set structure.
Definition bnd-sup.hpp:507
int pathmax_s(const HallInfo hall[], int i)
Path maximum for stable set pointer structure.
Definition bnd-sup.hpp:587
void pathset_t(HallInfo hall[], int start, int end, int to)
Path compression for capacity pointer structure.
Definition bnd-sup.hpp:523
int pathmin_t(const HallInfo hall[], int i)
Path minimum for capacity pointer structure.
Definition bnd-sup.hpp:556
void pathset_h(HallInfo hall[], int start, int end, int to)
Path compression for hall pointer structure.
Definition bnd-sup.hpp:531
void pathset_s(HallInfo hall[], int start, int end, int to)
Path compression for stable set structure.
Definition bnd-sup.hpp:515
bool lookupValue(T &a, int v, int &i)
Return index of v in array a.
Definition view.hpp:45
int pathmax_h(const HallInfo hall[], int i)
Path maximum for hall pointer structure.
Definition bnd-sup.hpp:572
int pathmax_ps(const HallInfo hall[], int i)
Path maximum for potentially stable set pointer structure.
Definition bnd-sup.hpp:594
Gecode toplevel namespace
Post propagator for SetVar SetOpType SetVar SetRelType r
Definition set.hh:767
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Post propagator for SetVar SetOpType SetVar y
Definition set.hh:767
LinIntExpr sum(const IntVarArgs &x)
Construct linear expression as sum of integer variables.
Definition int-expr.cpp:880
ExecStatus
Definition core.hpp:472
@ ES_OK
Execution is okay.
Definition core.hpp:476
@ ES_FAILED
Execution has resulted in failure.
Definition core.hpp:474
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Post propagator for SetVar x
Definition set.hh:767
#define forceinline
Definition config.hpp:187