Generated on Mon Feb 8 2021 00:00:00 for Gecode by doxygen 1.8.20
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 
40 namespace Gecode { namespace Int { namespace GCC {
41 
53  class UnReachable {
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>
237  class PartialSum {
238  private:
240  int* sum;
242  int size;
243  public:
247 
248  PartialSum(void);
251  void init(Space& home, ViewArray<Card>& k, bool up);
253  void reinit(void);
255  operator bool(void) const;
257 
259  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:
459  int bounds;
465  int t;
473  int d;
482  int h;
484  int s;
486  int ps;
493  int newBound;
494  };
495 
496 
505  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 
547  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 
570  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 
void reinit(void)
Mark datstructure as requiring reinitialization.
Definition: bnd-sup.hpp:370
LinFloatExpr sum(const FloatVarArgs &x)
Construct linear float expression as sum of float variables.
Definition: float-expr.cpp:546
int minb
Number of variables with lower bound.
Definition: bnd-sup.hpp:56
void pathset_h(HallInfo hall[], int start, int end, int to)
Path compression for hall pointer structure.
Definition: bnd-sup.hpp:531
Post propagator for SetVar x
Definition: set.hh:767
int t
Critical capacity pointer t represents a predecessor function where denotes the predecessor of i in ...
Definition: bnd-sup.hpp:465
Post propagator for SetVar SetOpType SetVar y
Definition: set.hh:767
int h
Hall set pointer.
Definition: bnd-sup.hpp:482
Compares two indices i, j of two views according to the ascending order of the views upper bounds.
Definition: bnd-sup.hpp:176
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:49
int firstValue
Sentinels indicating whether an end of sum is reached.
Definition: bnd-sup.hpp:245
bool operator()(const int i, const int j)
Comparison.
Definition: bnd-sup.hpp:208
int maxValue(void) const
Return largest bound of variables.
Definition: bnd-sup.hpp:396
unsigned int size(I &i)
Size of all ranges of range iterator i.
int newBound
Bound update.
Definition: bnd-sup.hpp:493
int gr
Number of greater variables.
Definition: bnd-sup.hpp:64
bool assigned(View x, int v)
Whether x is assigned to value v.
Definition: single.hpp:43
int eq
Number of equal variables.
Definition: bnd-sup.hpp:60
int pathmin_h(const HallInfo hall[], int i)
Path minimum for hall pointer structure.
Definition: bnd-sup.hpp:549
NodeType t
Type of node.
Definition: bool-expr.cpp:230
int d
Difference between critical capacities.
Definition: bnd-sup.hpp:473
int maxb
Number of variables with upper bound.
Definition: bnd-sup.hpp:58
Computation spaces.
Definition: core.hpp:1742
bool lookupValue(T &a, int v, int &i)
Return index of v in array a.
Definition: view.hpp:45
int sumup(int from, int to) const
Compute the maximum capacity of an interval.
Definition: bnd-sup.hpp:377
ExecStatus prop_card(Space &home, ViewArray< IntView > &x, ViewArray< Card > &k)
Bounds consistency check for cardinality variables.
Definition: bnd-sup.hpp:74
bool operator()(const int i, const int j)
Order.
Definition: bnd-sup.hpp:185
Gecode toplevel namespace
int pathmax_t(const HallInfo hall[], int i)
Path maximum for capacity pointer structure.
Definition: bnd-sup.hpp:579
const unsigned int card
Maximum cardinality of an integer set.
Definition: set.hh:101
MaxInc(const ViewArray< View > &x0)
Constructor.
Definition: bnd-sup.hpp:182
int pathmin_t(const HallInfo hall[], int i)
Path minimum for capacity pointer structure.
Definition: bnd-sup.hpp:556
Handle to region.
Definition: region.hpp:55
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
Post propagator for SetVar SetOpType SetVar SetRelType r
Definition: set.hh:767
T * alloc(long unsigned int n)
Allocate block of n objects of type T from space heap.
Definition: core.hpp:2837
void pathset_ps(HallInfo hall[], int start, int end, int to)
Path compression for potentially stable set structure.
Definition: bnd-sup.hpp:507
void init(Space &home, ViewArray< Card > &k, bool up)
Initialization.
Definition: bnd-sup.hpp:303
Maps domain bounds to their position in hall[].bounds.
Definition: bnd-sup.hpp:154
int pathmax_ps(const HallInfo hall[], int i)
Path maximum for potentially stable set pointer structure.
Definition: bnd-sup.hpp:594
void pathset_t(HallInfo hall[], int start, int end, int to)
Path compression for capacity pointer structure.
Definition: bnd-sup.hpp:523
int bounds
Represents the union of all lower and upper domain bounds.
Definition: bnd-sup.hpp:459
int ps
Potentially Stable Set pointer.
Definition: bnd-sup.hpp:486
void pathset_s(HallInfo hall[], int start, int end, int to)
Path compression for stable set structure.
Definition: bnd-sup.hpp:515
const int v[7]
Definition: distinct.cpp:259
Container class provding information about the Hall structure of the problem variables.
Definition: bnd-sup.hpp:456
NNF * l
Left subtree.
Definition: bool-expr.cpp:240
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
ViewArray< View > x
View array for comparison.
Definition: bnd-sup.hpp:202
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:1156
int pathmax_h(const HallInfo hall[], int i)
Path maximum for hall pointer structure.
Definition: bnd-sup.hpp:572
int lastValue
Definition: bnd-sup.hpp:245
#define forceinline
Definition: config.hpp:192
int skipNonNullElementsLeft(int v) const
Skip neigbouring array entries if their values do not differ.
Definition: bnd-sup.hpp:410
Partial sum structure for constant time computation of the maximal capacity of an interval.
Definition: bnd-sup.hpp:237
#define GECODE_ME_CHECK(me)
Check whether modification event me is failed, and forward failure.
Definition: macros.hpp:52
Compares two cardinality views according to the index.
Definition: bnd-sup.hpp:221
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:67
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:234
int s
Stable Set pointer.
Definition: bnd-sup.hpp:484
@ ES_FAILED
Execution has resulted in failure.
Definition: core.hpp:474
int le
Number of smaller variables.
Definition: bnd-sup.hpp:62
Gecode::IntArgs i({1, 2, 3, 4})
bool operator()(const Card &x, const Card &y)
Comparison.
Definition: bnd-sup.hpp:225
int pathmax_s(const HallInfo hall[], int i)
Path maximum for stable set pointer structure.
Definition: bnd-sup.hpp:587
MinInc(const ViewArray< View > &x0)
Constructor.
Definition: bnd-sup.hpp:205
@ ES_OK
Execution is okay.
Definition: core.hpp:476
bool card_consistent(ViewArray< IntView > &x, ViewArray< Card > &k)
Consistency check, whether the cardinality values are feasible.
Definition: bnd-sup.hpp:139
ViewArray< View > x
View array for comparison.
Definition: bnd-sup.hpp:179
int skipNonNullElementsRight(int v) const
Skip neigbouring array entries if their values do not differ.
Definition: bnd-sup.hpp:403
Class for computing unreachable values in the value GCC propagator.
Definition: bnd-sup.hpp:53
PartialSum(void)
Constructor.
Definition: bnd-sup.hpp:294
int max
Definition: bnd-sup.hpp:165
ExecStatus
Definition: core.hpp:472
int min
Definition: bnd-sup.hpp:160
Compares two indices i, j of two views according to the ascending order of the views lower bounds.
Definition: bnd-sup.hpp:199