Generated on Sat Feb 7 2015 02:01:23 for Gecode by doxygen 1.8.9.1
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  * Last modified:
16  * $Date: 2012-09-07 17:31:22 +0200 (Fri, 07 Sep 2012) $ by $Author: schulte $
17  * $Revision: 13068 $
18  *
19  * This file is part of Gecode, the generic constraint
20  * development environment:
21  * http://www.gecode.org
22  *
23  * Permission is hereby granted, free of charge, to any person obtaining
24  * a copy of this software and associated documentation files (the
25  * "Software"), to deal in the Software without restriction, including
26  * without limitation the rights to use, copy, modify, merge, publish,
27  * distribute, sublicense, and/or sell copies of the Software, and to
28  * permit persons to whom the Software is furnished to do so, subject to
29  * the following conditions:
30  *
31  * The above copyright notice and this permission notice shall be
32  * included in all copies or substantial portions of the Software.
33  *
34  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
35  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
36  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
37  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
38  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
39  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
40  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
41  *
42  */
43 
44 namespace Gecode { namespace Int { namespace GCC {
45 
57  class UnReachable {
58  public:
60  int minb;
62  int maxb;
64  int eq;
66  int le;
68  int gr;
69  };
70 
76  template<class Card>
78  prop_card(Space& home,
80  int n = x.size();
81  int m = k.size();
82  Region r(home);
83  UnReachable* rv = r.alloc<UnReachable>(m);
84  for(int i = m; i--; )
85  rv[i].minb=rv[i].maxb=rv[i].le=rv[i].gr=rv[i].eq=0;
86 
87  for (int i = n; i--; ) {
88  int min_idx;
89  if (!lookupValue(k,x[i].min(),min_idx))
90  return ES_FAILED;
91  if (x[i].assigned()) {
92  rv[min_idx].minb++;
93  rv[min_idx].maxb++;
94  rv[min_idx].eq++;
95  } else {
96  // count the number of variables
97  // with lower bound k[min_idx].card()
98  rv[min_idx].minb++;
99  int max_idx;
100  if (!lookupValue(k,x[i].max(),max_idx))
101  return ES_FAILED;
102  // count the number of variables
103  // with upper bound k[max_idx].card()
104  rv[max_idx].maxb++;
105  }
106  }
107 
108  rv[0].le = 0;
109  int c_min = 0;
110  for (int i = 1; i < m; i++) {
111  rv[i].le = c_min + rv[i - 1].maxb;
112  c_min += rv[i - 1].maxb;
113  }
114 
115  rv[m-1].gr = 0;
116  int c_max = 0;
117  for (int i = m-1; i--; ) {
118  rv[i].gr = c_max + rv[i + 1].minb;
119  c_max += rv[i + 1].minb;
120  }
121 
122  for (int i = m; i--; ) {
123  int reachable = x.size() - rv[i].le - rv[i].gr;
124  if (!k[i].assigned()) {
125  GECODE_ME_CHECK(k[i].lq(home, reachable));
126  GECODE_ME_CHECK(k[i].gq(home, rv[i].eq));
127  } else {
128  // check validity of the cardinality value
129  if ((rv[i].eq > k[i].max()) || (k[i].max() > reachable))
130  return ES_FAILED;
131  }
132  }
133 
134  return ES_OK;
135  }
136 
137 
141  template<class Card>
142  forceinline bool
144  int smin = 0;
145  int smax = 0;
146  for (int i = k.size(); i--; ) {
147  smax += k[i].max();
148  smin += k[i].min();
149  }
150  // Consistent if number of variables within cardinality bounds
151  return (smin <= x.size()) && (x.size() <= smax);
152  }
153 
158  class Rank {
159  public:
164  int min;
169  int max;
170  };
171 
179  template<class View>
180  class MaxInc {
181  protected:
184  public:
186  MaxInc(const ViewArray<View>& x0) : x(x0) {}
188  forceinline bool
189  operator ()(const int i, const int j) {
190  return x[i].max() < x[j].max();
191  }
192  };
193 
194 
202  template<class View>
203  class MinInc {
204  protected:
207  public:
209  MinInc(const ViewArray<View>& x0) : x(x0) {}
211  forceinline bool
212  operator ()(const int i, const int j) {
213  return x[i].min() < x[j].min();
214  }
215  };
216 
217 
224  template<class Card>
225  class MinIdx {
226  public:
228  forceinline bool
229  operator ()(const Card& x, const Card& y) {
230  return x.card() < y.card();
231  }
232  };
233 
240  template<class Card>
241  class PartialSum {
242  private:
244  int* sum;
246  int size;
247  public:
251 
252  PartialSum(void);
255  void init(Space& home, ViewArray<Card>& k, bool up);
257  void reinit(void);
259  bool initialized(void) const;
261 
263  int sumup(int from, int to) const;
266  int minValue(void) const;
268  int maxValue(void) const;
270  int skipNonNullElementsRight(int v) const;
272  int skipNonNullElementsLeft(int v) const;
274 
276 
293  };
294 
295 
296  template<class Card>
298  PartialSum<Card>::PartialSum(void) : sum(NULL), size(-1) {}
299 
300  template<class Card>
301  forceinline bool
303  return size != -1;
304  }
305  template<class Card>
306  inline void
307  PartialSum<Card>::init(Space& home, ViewArray<Card>& elements, bool up) {
308  int i = 0;
309  int j = 0;
310 
311  // Determine number of holes in the index set
312  int holes = 0;
313  for (i = 1; i < elements.size(); i++) {
314  if (elements[i].card() != elements[i-1].card() + 1)
315  holes += elements[i].card()-elements[i-1].card()-1;
316  }
317 
318  // we add three elements at the beginning and two at the end
319  size = elements.size() + holes + 5;
320 
321  // memory allocation
322  if (sum == NULL) {
323  sum = home.alloc<int>(2*size);
324  }
325  int* ds = &sum[size];
326 
327  int first = elements[0].card();
328 
329  firstValue = first - 3;
330  lastValue = first + elements.size() + holes + 1;
331 
332  // the first three elements
333  for (i = 3; i--; )
334  sum[i] = i;
335 
336  /*
337  * copy the bounds into sum, filling up holes with zeroes
338  */
339  int prevCard = elements[0].card()-1;
340  i = 0;
341  for (j = 2; j < elements.size() + holes + 2; j++) {
342  if (elements[i].card() != prevCard + 1) {
343  sum[j + 1] = sum[j];
344  } else if (up) {
345  sum[j + 1] = sum[j] + elements[i].max();
346  i++;
347  } else {
348  sum[j + 1] = sum[j] + elements[i].min();
349  i++;
350  }
351  prevCard++;
352  }
353  sum[j + 1] = sum[j] + 1;
354  sum[j + 2] = sum[j + 1] + 1;
355 
356  // Compute distances, eliminating zeroes
357  i = elements.size() + holes + 3;
358  j = i + 1;
359  for ( ; i > 0; ) {
360  while(sum[i] == sum[i - 1]) {
361  ds[i] = j;
362  i--;
363  }
364  ds[j] = i;
365  i--;
366  j = ds[j];
367  }
368  ds[j] = 0;
369  ds[0] = 0;
370  }
371 
372  template<class Card>
373  forceinline void
375  size = -1;
376  }
377 
378 
379  template<class Card>
380  forceinline int
381  PartialSum<Card>::sumup(int from, int to) const {
382  if (from <= to) {
383  return sum[to - firstValue] - sum[from - firstValue - 1];
384  } else {
385  assert(to - firstValue - 1 >= 0);
386  assert(to - firstValue - 1 < size);
387  assert(from - firstValue >= 0);
388  assert(from - firstValue < size);
389  return sum[to - firstValue - 1] - sum[from - firstValue];
390  }
391  }
392 
393  template<class Card>
394  forceinline int
396  return firstValue + 3;
397  }
398  template<class Card>
399  forceinline int
401  return lastValue - 2;
402  }
403 
404 
405  template<class Card>
406  forceinline int
408  value -= firstValue;
409  int* ds = &sum[size];
410  return (ds[value] < value ? value : ds[value]) + firstValue;
411  }
412  template<class Card>
413  forceinline int
415  value -= firstValue;
416  int* ds = &sum[size];
417  return (ds[value] > value ? ds[ds[value]] : value) + firstValue;
418  }
419 
420  template<class Card>
421  inline bool
423  int j = 0;
424  for (int i = 3; i < size - 2; i++) {
425  int max = 0;
426  if (k[j].card() == i+firstValue)
427  max = k[j++].max();
428  if ((sum[i] - sum[i - 1]) != max)
429  return true;
430  }
431  return false;
432  }
433 
434  template<class Card>
435  inline bool
437  int j = 0;
438  for (int i = 3; i < size - 2; i++) {
439  int min = 0;
440  if (k[j].card() == i+firstValue)
441  min = k[j++].min();
442  if ((sum[i] - sum[i - 1]) != min)
443  return true;
444  }
445  return false;
446  }
447 
448 
460  class HallInfo {
461  public:
463  int bounds;
469  int t;
477  int d;
486  int h;
488  int s;
490  int ps;
497  int newBound;
498  };
499 
500 
509  forceinline void
511  pathset_ps(HallInfo hall[], int start, int end, int to) {
512  int k, l;
513  for (l=start; (k=l) != end; hall[k].ps=to) {
514  l = hall[k].ps;
515  }
516  }
518  forceinline void
519  pathset_s(HallInfo hall[], int start, int end, int to) {
520  int k, l;
521  for (l=start; (k=l) != end; hall[k].s=to) {
522  l = hall[k].s;
523  }
524  }
526  forceinline void
527  pathset_t(HallInfo hall[], int start, int end, int to) {
528  int k, l;
529  for (l=start; (k=l) != end; hall[k].t=to) {
530  l = hall[k].t;
531  }
532  }
534  forceinline void
535  pathset_h(HallInfo hall[], int start, int end, int to) {
536  int k, l;
537  for (l=start; (k=l) != end; hall[k].h=to) {
538  l = hall[k].h;
539  assert(l != k);
540  }
541  }
543 
551  forceinline int
553  pathmin_h(const HallInfo hall[], int i) {
554  while (hall[i].h < i)
555  i = hall[i].h;
556  return i;
557  }
559  forceinline int
560  pathmin_t(const HallInfo hall[], int i) {
561  while (hall[i].t < i)
562  i = hall[i].t;
563  return i;
564  }
566 
574  forceinline int
576  pathmax_h(const HallInfo hall[], int i) {
577  while (hall[i].h > i)
578  i = hall[i].h;
579  return i;
580  }
582  forceinline int
583  pathmax_t(const HallInfo hall[], int i) {
584  while (hall[i].t > i) {
585  i = hall[i].t;
586  }
587  return i;
588  }
590  forceinline int
591  pathmax_s(const HallInfo hall[], int i) {
592  while (hall[i].s > i)
593  i = hall[i].s;
594  return i;
595  }
597  forceinline int
598  pathmax_ps(const HallInfo hall[], int i) {
599  while (hall[i].ps > i)
600  i = hall[i].ps;
601  return i;
602  }
604 
605 }}}
606 
607 // STATISTICS: int-prop
608 
int d
Difference between critical capacities.
Definition: bnd-sup.hpp:477
int skipNonNullElementsLeft(int v) const
Skip neigbouring array entries if their values do not differ.
Definition: bnd-sup.hpp:414
NodeType t
Type of node.
Definition: bool-expr.cpp:234
Container class provding information about the Hall structure of the problem variables.
Definition: bnd-sup.hpp:460
NNF * l
Left subtree.
Definition: bool-expr.cpp:244
int minValue(void) const
Return smallest bound of variables.
Definition: bnd-sup.hpp:395
bool operator()(const int i, const int j)
Order.
Definition: bnd-sup.hpp:189
int gr
Number of greater variables.
Definition: bnd-sup.hpp:68
bool initialized(void) const
Test whether already initialized.
Definition: bnd-sup.hpp:302
T * alloc(long unsigned int n)
Allocate block of n objects of type T from region.
Definition: region.hpp:326
int eq
Number of equal variables.
Definition: bnd-sup.hpp:64
bool lookupValue(T &a, int v, int &i)
Return index of v in array a.
Definition: view.hpp:48
void pathset_s(HallInfo hall[], int start, int end, int to)
Path compression for stable set structure.
Definition: bnd-sup.hpp:519
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:57
void pathset_h(HallInfo hall[], int start, int end, int to)
Path compression for hall pointer structure.
Definition: bnd-sup.hpp:535
int h
Hall set pointer.
Definition: bnd-sup.hpp:486
int skipNonNullElementsRight(int v) const
Skip neigbouring array entries if their values do not differ.
Definition: bnd-sup.hpp:407
Handle to region.
Definition: region.hpp:61
void reinit(void)
Mark datstructure as requiring reinitialization.
Definition: bnd-sup.hpp:374
int pathmax_t(const HallInfo hall[], int i)
Path maximum for capacity pointer structure.
Definition: bnd-sup.hpp:583
int pathmin_h(const HallInfo hall[], int i)
Path minimum for hall pointer structure.
Definition: bnd-sup.hpp:553
const unsigned int card
Maximum cardinality of an integer set.
Definition: set.hh:103
int maxb
Number of variables with upper bound.
Definition: bnd-sup.hpp:62
int pathmin_t(const HallInfo hall[], int i)
Path minimum for capacity pointer structure.
Definition: bnd-sup.hpp:560
Computation spaces.
Definition: core.hpp:1362
Compares two indices i, j of two views according to the ascending order of the views lower bounds...
Definition: bnd-sup.hpp:203
T * alloc(long unsigned int n)
Allocate block of n objects of type T from space heap.
Definition: core.hpp:2397
int pathmax_h(const HallInfo hall[], int i)
Path maximum for hall pointer structure.
Definition: bnd-sup.hpp:576
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:436
int maxValue(void) const
Return largest bound of variables.
Definition: bnd-sup.hpp:400
Gecode::IntArgs i(4, 1, 2, 3, 4)
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
int t
Critical capacity pointer t represents a predecessor function where denotes the predecessor of i in ...
Definition: bnd-sup.hpp:469
Compares two indices i, j of two views according to the ascending order of the views upper bounds...
Definition: bnd-sup.hpp:180
Execution has resulted in failure.
Definition: core.hpp:525
NNF * r
Right subtree.
Definition: bool-expr.cpp:246
Class for computing unreachable values in the value GCC propagator.
Definition: bnd-sup.hpp:57
int sumup(int from, int to) const
Compute the maximum capacity of an interval.
Definition: bnd-sup.hpp:381
int pathmax_ps(const HallInfo hall[], int i)
Path maximum for potentially stable set pointer structure.
Definition: bnd-sup.hpp:598
unsigned int size(I &i)
Size of all ranges of range iterator i.
bool operator()(const Card &x, const Card &y)
Comparison.
Definition: bnd-sup.hpp:229
MaxInc(const ViewArray< View > &x0)
Constructor.
Definition: bnd-sup.hpp:186
#define GECODE_ME_CHECK(me)
Check whether modification event me is failed, and forward failure.
Definition: macros.hpp:45
ExecStatus prop_card(Space &home, ViewArray< IntView > &x, ViewArray< Card > &k)
Bounds consistency check for cardinality variables.
Definition: bnd-sup.hpp:78
PartialSum(void)
Constructor.
Definition: bnd-sup.hpp:298
int bounds
Represents the union of all lower and upper domain bounds.
Definition: bnd-sup.hpp:463
void pathset_t(HallInfo hall[], int start, int end, int to)
Path compression for capacity pointer structure.
Definition: bnd-sup.hpp:527
bool card_consistent(ViewArray< IntView > &x, ViewArray< Card > &k)
Consistency check, whether the cardinality values are feasible.
Definition: bnd-sup.hpp:143
const int v[7]
Definition: distinct.cpp:207
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:75
int newBound
Bound update.
Definition: bnd-sup.hpp:497
Maps domain bounds to their position in hall[].bounds.
Definition: bnd-sup.hpp:158
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:253
ViewArray< View > x
View array for comparison.
Definition: bnd-sup.hpp:206
ExecStatus
Definition: core.hpp:523
int s
Stable Set pointer.
Definition: bnd-sup.hpp:488
MinInc(const ViewArray< View > &x0)
Constructor.
Definition: bnd-sup.hpp:209
bool assigned(View x, int v)
Whether x is assigned to value v.
Definition: single.hpp:47
Partial sum structure for constant time computation of the maximal capacity of an interval...
Definition: bnd-sup.hpp:241
#define forceinline
Definition: config.hpp:132
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:422
int firstValue
Sentinels indicating whether an end of sum is reached.
Definition: bnd-sup.hpp:249
int pathmax_s(const HallInfo hall[], int i)
Path maximum for stable set pointer structure.
Definition: bnd-sup.hpp:591
ViewArray< View > x
View array for comparison.
Definition: bnd-sup.hpp:183
Execution is okay.
Definition: core.hpp:527
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:1215
int ps
Potentially Stable Set pointer.
Definition: bnd-sup.hpp:490
Gecode toplevel namespace
LinFloatExpr sum(const FloatVarArgs &x)
Construct linear float expression as sum of float variables.
Definition: float-expr.cpp:548
Compares two cardinality views according to the index.
Definition: bnd-sup.hpp:225
void init(Space &home, ViewArray< Card > &k, bool up)
Initialization.
Definition: bnd-sup.hpp:307
bool operator()(const int i, const int j)
Comparison.
Definition: bnd-sup.hpp:212
void pathset_ps(HallInfo hall[], int start, int end, int to)
Path compression for potentially stable set structure.
Definition: bnd-sup.hpp:511
int minb
Number of variables with lower bound.
Definition: bnd-sup.hpp:60
int le
Number of smaller variables.
Definition: bnd-sup.hpp:66