Generated on Sat Apr 10 2021 00:00:00 for Gecode by doxygen 1.9.1
bnd.hpp
Go to the documentation of this file.
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 Distinct {
35 
36  template<class View>
39  : Propagator(home), x(x0), y(home,x0) {
40  // Both x and y initially contain the same variables
41  // - x is used for bounds propagation
42  // - y is used for performing singleton propagation
43  // They can not be shared as singleton propagation removes
44  // determined variables still required for bounds propagation.
45  y.subscribe(home,*this,PC_INT_BND);
46  int min = x[0].min(), max = x[0].max();
47  for (int i=1; i<x.size(); i++) {
48  min = std::min(min,x[i].min());
49  max = std::max(max,x[i].max());
50  }
51  min_x = min; max_x = max;
52  }
53 
54  template<class View>
55  forceinline size_t
57  y.cancel(home,*this,PC_INT_BND);
58  (void) Propagator::dispose(home);
59  return sizeof(*this);
60  }
61 
62  template<class View>
65  : Propagator(home,p), min_x(p.min_x), max_x(p.max_x) {
66  x.update(home,p.x);
67  y.update(home,p.y);
68  }
69 
70  template<class View>
71  Actor*
73  return new (home) Bnd<View>(home,*this);
74  }
75 
76  template<class View>
77  PropCost
78  Bnd<View>::cost(const Space&, const ModEventDelta& med) const {
79  if (View::me(med) == ME_INT_VAL)
80  return PropCost::linear(PropCost::LO, y.size());
81  else
82  return PropCost::quadratic(PropCost::LO, x.size());
83  }
84 
85  template<class View>
86  void
88  y.reschedule(home,*this,PC_INT_BND);
89  }
90 
91 
93  class Rank {
94  public:
95  int min, max;
96  };
97 
99  template<class View>
100  class MaxIncIdx {
101  protected:
103  public:
105  MaxIncIdx(const ViewArray<View>& x0) : x(x0) {}
106  forceinline bool
107  operator ()(const int i, const int j) {
108  return x[i].max() < x[j].max();
109  }
110  };
111 
113  template<class View>
114  class MinIncIdx {
115  protected:
117  public:
119  MinIncIdx(const ViewArray<View>& x0) : x(x0) {}
120  forceinline bool
121  operator ()(const int i, const int j) {
122  return x[i].min() < x[j].min();
123  }
124  };
125 
127  template<class View>
128  class MinInc {
129  public:
130  forceinline bool
131  operator ()(const View& x, const View& y) {
132  return x.min() < y.min();
133  }
134  };
135 
137  template<class IntType>
138  class HallInfo {
139  public:
141  };
142 
143  template<class IntType>
144  forceinline void
146  IntType start, IntType end, IntType to) {
147  IntType k, l;
148  for (l=start; (k=l) != end; hall[k].t=to) {
149  l = hall[k].t;
150  }
151  }
152 
153  template<class IntType>
154  forceinline void
156  IntType start, IntType end, IntType to) {
157  IntType k, l;
158  for (l=start; (k=l) != end; hall[k].h=to) {
159  l = hall[k].h;
160  }
161  }
162 
163  template<class IntType>
166  while (hall[i].h < i)
167  i = hall[i].h;
168  return i;
169  }
170 
171  template<class IntType>
174  while (hall[i].t < i)
175  i = hall[i].t;
176  return i;
177  }
178 
179  template<class IntType>
182  while (hall[i].h > i)
183  i = hall[i].h;
184  return i;
185  }
186 
187  template<class IntType>
190  while (hall[i].t > i)
191  i = hall[i].t;
192  return i;
193  }
194 
195  template<class View, class IntType>
198  int* minsorted, int* maxsorted) {
199  const int n = x.size();
200 
201  Region r;
202 
203  // Setup rank and bounds info
204  HallInfo<IntType>* hall = r.alloc<HallInfo<IntType> >(2*n+2);
205  Rank* rank = r.alloc<Rank>(n);
206 
207  int nb = 0;
208  {
209  IntType min = x[minsorted[0]].min();
210  IntType max = x[maxsorted[0]].max() + 1;
211  IntType last = min - 2;
212 
213  hall[0].bounds = last;
214 
215  int i = 0;
216  int j = 0;
217  while (true) {
218  if ((i < n) && (min < max)) {
219  if (min != last)
220  hall[++nb].bounds = last = min;
221  rank[minsorted[i]].min = nb;
222  if (++i < n)
223  min = x[minsorted[i]].min();
224  } else {
225  if (max != last)
226  hall[++nb].bounds = last = max;
227  rank[maxsorted[j]].max = nb;
228  if (++j == n)
229  break;
230  max = x[maxsorted[j]].max() + 1;
231  }
232  }
233  hall[nb+1].bounds = hall[nb].bounds + 2;
234  }
235 
236  // If tells cross holes, we do not compute a fixpoint
237  ExecStatus es = ES_FIX;
238 
239  // Propagate lower bounds
240  for (int i=nb+2; --i;) {
241  hall[i].t = hall[i].h = i-1;
242  hall[i].d = hall[i].bounds - hall[i-1].bounds;
243  }
244  for (int i=0; i<n; i++) { // visit intervals in increasing max order
245  IntType x0 = rank[maxsorted[i]].min;
246  IntType z = pathmax_t(hall, x0+1);
247  IntType j = hall[z].t;
248  if (--hall[z].d == 0)
249  hall[z = pathmax_t(hall, hall[z].t=z+1)].t = j;
250  pathset_t(hall, x0+1, z, z); // path compression
251  IntType y = rank[maxsorted[i]].max;
252  if (hall[z].d < hall[z].bounds-hall[y].bounds)
253  return ES_FAILED;
254  if (hall[x0].h > x0) {
255  IntType w = pathmax_h(hall, hall[x0].h);
256  IntType m = hall[w].bounds;
257  ModEvent me = x[maxsorted[i]].gq(home,m);
258  if (me_failed(me))
259  return ES_FAILED;
260  if ((me == ME_INT_VAL) ||
261  ((me == ME_INT_BND) && (m != x[maxsorted[i]].min())))
262  es = ES_NOFIX;
263  pathset_h(hall, x0, w, w); // path compression
264  }
265  if (hall[z].d == hall[z].bounds-hall[y].bounds) {
266  pathset_h(hall, hall[y].h, j-1, y); // mark hall interval
267  hall[y].h = j-1;
268  }
269  }
270 
271  // Propagate upper bounds
272  for (int i=nb+1; i--;) {
273  hall[i].t = hall[i].h = i+1;
274  hall[i].d = hall[i+1].bounds - hall[i].bounds;
275  }
276  for (int i=n; --i>=0; ) { // visit intervals in decreasing min order
277  IntType x0 = rank[minsorted[i]].max;
278  IntType z = pathmin_t(hall, x0-1);
279  IntType j = hall[z].t;
280  if (--hall[z].d == 0)
281  hall[z = pathmin_t(hall, hall[z].t=z-1)].t = j;
282  pathset_t(hall, x0-1, z, z);
283  IntType y = rank[minsorted[i]].min;
284  if (hall[z].d < hall[y].bounds-hall[z].bounds)
285  return ES_FAILED;
286  if (hall[x0].h < x0) {
287  IntType w = pathmin_h(hall, hall[x0].h);
288  IntType m = hall[w].bounds - 1;
289  ModEvent me = x[minsorted[i]].lq(home,m);
290  if (me_failed(me))
291  return ES_FAILED;
292  if ((me == ME_INT_VAL) ||
293  ((me == ME_INT_BND) && (m != x[maxsorted[i]].min())))
294  es = ES_NOFIX;
295  pathset_h(hall, x0, w, w);
296  }
297  if (hall[z].d == hall[y].bounds-hall[z].bounds) {
298  pathset_h(hall, hall[y].h, j+1, y);
299  hall[y].h = j+1;
300  }
301  }
302 
303  return es;
304  }
305 
306  template<class View>
308  prop_bnd(Space& home, ViewArray<View>& x, int& min_x, int& max_x) {
309 
310  const int n = x.size();
311 
312  Region r;
313 
314  int* minsorted = r.alloc<int>(n);
315  int* maxsorted = r.alloc<int>(n);
316 
317  unsigned int d = static_cast<unsigned int>(max_x - min_x) + 1;
318 
319  if (d < static_cast<unsigned int>(n))
320  return ES_FAILED;
321 
322  if (d > 2*static_cast<unsigned int>(n)) {
323  for (int i=0; i<n; i++)
324  minsorted[i]=maxsorted[i]=i;
325 
326  MinIncIdx<View> min_inc(x);
327  Support::quicksort<int,MinIncIdx<View> >(minsorted, n, min_inc);
328  MaxIncIdx<View> max_inc(x);
329  Support::quicksort<int,MaxIncIdx<View> >(maxsorted, n, max_inc);
330  } else {
331 
332  int* minbucket = r.alloc<int>(d);
333  int* maxbucket = r.alloc<int>(d);
334  for (unsigned int i=0; i<d; i++)
335  minbucket[i]=maxbucket[i]=0;
336 
337  for (int i=0; i<n; i++) {
338  minbucket[x[i].min() - min_x]++;
339  maxbucket[x[i].max() - min_x]++;
340  }
341 
342  int c_min = 0, c_max = 0;
343  for (unsigned int i=0; i<d; i++) {
344  int t_min = minbucket[i];
345  int t_max = maxbucket[i];
346  minbucket[i] = c_min; c_min += t_min;
347  maxbucket[i] = c_max; c_max += t_max;
348  }
349  assert((c_min == n) && (c_max == n));
350 
351  for (int i=n; i--; ) {
352  minsorted[minbucket[x[i].min() - min_x]++] = i;
353  maxsorted[maxbucket[x[i].max() - min_x]++] = i;
354  }
355  }
356 
357  // Update minimum and maximum information
358  min_x = x[minsorted[0]].min();
359  max_x = x[maxsorted[n-1]].max();
360 
361 
362  if (d > (static_cast<unsigned int>(Int::Limits::max) / 2U))
363  return prop_bnd<View,long long int>(home,x,minsorted,maxsorted);
364  else
365  return prop_bnd<View,int>(home,x,minsorted,maxsorted);
366  }
367 
368  template<class View>
369  ExecStatus
371  int min = x[0].min(), max = x[0].max();
372  for (int i=1; i<x.size(); i++) {
373  min = std::min(min,x[i].min());
374  max = std::max(max,x[i].max());
375  }
376  return prop_bnd(home, x, min, max);
377  }
378 
379  template<class View>
380  ExecStatus
382  assert(x.size() > 1);
383 
384  if (View::me(med) == ME_INT_VAL) {
385  ExecStatus es = prop_val<View,false>(home,y);
386  GECODE_ES_CHECK(es);
387  if (y.size() < 2)
388  return home.ES_SUBSUMED(*this);
389  if (es == ES_FIX)
390  return home.ES_FIX_PARTIAL(*this,View::med(ME_INT_BND));
391  }
392 
393  if (y.size() == 2)
394  GECODE_REWRITE(*this,(Rel::Nq<View,View>::post(home(*this),y[0],y[1])));
395 
396  ExecStatus es = prop_bnd<View>(home,x,min_x,max_x);
397 
398  GECODE_ES_CHECK(es);
399  if (es == ES_NOFIX && View::me(modeventdelta()) == ME_INT_VAL)
400  return es;
401 
402  const int n = x.size();
403 
404  if ((n > 2*y.size()) && (n > 6)) {
405  // If there are many assigned views, try to eliminate them
406  unsigned int d = static_cast<unsigned int>(max_x - min_x) + 1;
407  if (d > 2*static_cast<unsigned int>(n)) {
408  MinInc<View> min_inc;
409  Support::quicksort<View,MinInc<View> >(&x[0], n, min_inc);
410  } else {
411  Region r;
412  int* minbucket = r.alloc<int>(d);
413  View* minsorted = r.alloc<View>(n);
414 
415  for (unsigned int i=0; i<d; i++)
416  minbucket[i]=0;
417  for (int i=0; i<n; i++)
418  minbucket[x[i].min() - min_x]++;
419 
420  int c_min = 0;
421  for (unsigned int i=0; i<d; i++) {
422  int t_min = minbucket[i];
423  minbucket[i] = c_min; c_min += t_min;
424  }
425  assert(c_min == n);
426 
427  for (int i=0; i<n; i++)
428  minsorted[minbucket[x[i].min() - min_x]++] = x[i];
429  for (int i=0; i<n; i++)
430  x[i] = minsorted[i];
431  }
432 
433  int i = 0;
434  int j = 0;
435  int max = x[0].max()-1;
436  while (i < n-1) {
437  if (!x[i].assigned() ||
438  (x[i].val() <= max) || (x[i].val() > x[i+1].min())) {
439  // Keep view x[i]
440  max = std::max(max,x[i].max());
441  x[j++]=x[i];
442  }
443  i++;
444  }
445  if (!x[i].assigned() || (x[i].val() <= max))
446  x[j++]=x[i];
447  x.size(j);
448  }
449 
450  if (x.size() < 2)
451  return home.ES_SUBSUMED(*this);
452 
453  if (x.size() == 2)
454  GECODE_REWRITE(*this,(Rel::Nq<View,View>::post(home(*this),x[0],x[1])));
455 
456  return es;
457  }
458 
459 #ifdef GECODE_HAS_CBS
460  template<class View>
461  void
462  Bnd<View>::solndistrib(Space& home, Propagator::SendMarginal send) const {
463  cbsdistinct(home,this->id(),x,send);
464  }
465 
466  template<class View>
467  void
468  Bnd<View>::domainsizesum(Propagator::InDecision in, unsigned int& size,
469  unsigned int& size_b) const {
470  cbssize(x,in,size,size_b);
471  }
472 #endif
473 
474  template<class View>
475  ExecStatus
477  if (x.size() == 2)
478  return Rel::Nq<View,View>::post(home,x[0],x[1]);
479  if (x.size() > 2)
480  (void) new (home) Bnd<View>(home,x);
481  return ES_OK;
482  }
483 
484 }}}
485 
486 // STATISTICS: int-prop
487 
NNF * l
Left subtree.
Definition: bool-expr.cpp:240
NodeType t
Type of node.
Definition: bool-expr.cpp:230
int p
Number of positive literals for node type.
Definition: bool-expr.cpp:232
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:234
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:249
NNF * r
Right subtree.
Definition: bool-expr.cpp:242
Base-class for both propagators and branchers.
Definition: core.hpp:628
virtual size_t dispose(Space &home)
Delete actor and return its size.
Definition: core.hpp:3252
Home class for posting propagators
Definition: core.hpp:856
Bounds consistent distinct propagator.
Definition: distinct.hh:152
int max_x
Maximum (approximation) of view in x.
Definition: distinct.hh:161
static ExecStatus post(Home home, ViewArray< View > &x)
Post propagator for view array x.
Definition: bnd.hpp:476
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: bnd.hpp:381
virtual void reschedule(Space &home)
Schedule function.
Definition: bnd.hpp:87
virtual Actor * copy(Space &home)
Copy propagator during cloning.
Definition: bnd.hpp:72
ViewArray< View > y
Views on which to perform value-propagation (subset of x)
Definition: distinct.hh:157
virtual PropCost cost(const Space &home, const ModEventDelta &med) const
Cost function.
Definition: bnd.hpp:78
Bnd(Home home, ViewArray< View > &x)
Constructor for posting.
Definition: bnd.hpp:38
virtual size_t dispose(Space &home)
Destructor.
Definition: bnd.hpp:56
ViewArray< View > x
Views on which to perform bounds-propagation.
Definition: distinct.hh:155
int min_x
Minimum (approximation) of view in x.
Definition: distinct.hh:159
Information on Hall intervals.
Definition: bnd.hpp:138
Sort-order by increasing maximum (by index)
Definition: bnd.hpp:100
MaxIncIdx(const ViewArray< View > &x0)
Definition: bnd.hpp:105
ViewArray< View > x
Definition: bnd.hpp:102
bool operator()(const int i, const int j)
Definition: bnd.hpp:107
Sort-order by increasing minimum (by index)
Definition: bnd.hpp:114
MinIncIdx(const ViewArray< View > &x0)
Definition: bnd.hpp:119
bool operator()(const int i, const int j)
Definition: bnd.hpp:121
ViewArray< View > x
Definition: bnd.hpp:116
Sort-order by increasing minimum (direct)
Definition: bnd.hpp:128
bool operator()(const View &x, const View &y)
Definition: bnd.hpp:131
Rank information
Definition: bnd.hpp:93
Binary disequality propagator.
Definition: rel.hh:460
static ExecStatus post(Home home, V0 x0, V1 x1)
Post propagator .
Definition: nq.hpp:49
Propagation cost.
Definition: core.hpp:486
static PropCost quadratic(PropCost::Mod m, unsigned int n)
Quadratic complexity for modifier m and size measure n.
Definition: core.hpp:4787
static PropCost linear(PropCost::Mod m, unsigned int n)
Linear complexity for modifier pcm and size measure n.
Definition: core.hpp:4796
@ LO
Cheap.
Definition: core.hpp:513
Base-class for propagators.
Definition: core.hpp:1064
Handle to region.
Definition: region.hpp:55
Propagator for negated equality
Definition: rel.hh:268
Computation spaces.
Definition: core.hpp:1742
View arrays.
Definition: array.hpp:253
ExecStatus
Definition: core.hpp:472
@ ES_OK
Execution is okay.
Definition: core.hpp:476
@ ES_FIX
Propagation has computed fixpoint.
Definition: core.hpp:477
@ ES_FAILED
Execution has resulted in failure.
Definition: core.hpp:474
@ ES_NOFIX
Propagation has not computed fixpoint.
Definition: core.hpp:475
int ModEvent
Type for modification events.
Definition: core.hpp:62
Post propagator for SetVar SetOpType SetVar SetRelType SetVar z
Definition: set.hh:767
Post propagator for SetVar SetOpType SetVar y
Definition: set.hh:767
ExecStatus ES_FIX_PARTIAL(Propagator &p, const ModEventDelta &med)
Propagator p has computed partial fixpoint
Definition: core.hpp:3569
ExecStatus ES_SUBSUMED(Propagator &p)
Definition: core.hpp:3563
int ModEventDelta
Modification event deltas.
Definition: core.hpp:89
#define GECODE_REWRITE(prop, post)
Rewrite propagator by executing post function.
Definition: macros.hpp:116
bool me_failed(ModEvent me)
Check whether modification event me is failed.
Definition: modevent.hpp:54
#define GECODE_ES_CHECK(es)
Check whether execution status es is failed or subsumed, and forward failure or subsumption.
Definition: macros.hpp:91
const FloatNum max
Largest allowed float value.
Definition: float.hh:844
const FloatNum min
Smallest allowed float value.
Definition: float.hh:846
void pathset_h(HallInfo< IntType > hall[], IntType start, IntType end, IntType to)
Definition: bnd.hpp:155
IntType pathmin_t(const HallInfo< IntType > hall[], IntType i)
Definition: bnd.hpp:173
IntType pathmax_t(const HallInfo< IntType > hall[], IntType i)
Definition: bnd.hpp:189
IntType pathmax_h(const HallInfo< IntType > hall[], IntType i)
Definition: bnd.hpp:181
IntType pathmin_h(const HallInfo< IntType > hall[], IntType i)
Definition: bnd.hpp:165
void pathset_t(HallInfo< IntType > hall[], IntType start, IntType end, IntType to)
Definition: bnd.hpp:145
ExecStatus prop_bnd(Space &home, ViewArray< View > &x, int *minsorted, int *maxsorted)
Definition: bnd.hpp:197
const int max
Largest allowed integer value.
Definition: int.hh:116
bool assigned(View x, int v)
Whether x is assigned to value v.
Definition: single.hpp:43
const Gecode::ModEvent ME_INT_BND
Domain operation has changed the minimum or maximum of the domain.
Definition: var-type.hpp:65
const Gecode::PropCond PC_INT_BND
Propagate when minimum or maximum of a view changes.
Definition: var-type.hpp:91
const Gecode::ModEvent ME_INT_VAL
Domain operation has resulted in a value (assigned variable)
Definition: var-type.hpp:56
unsigned int size(I &i)
Size of all ranges of range iterator i.
IntType
Description of integer types.
Definition: int-type.hpp:39
Gecode::IntArgs i({1, 2, 3, 4})
Gecode::IntSet d(v, 7)
#define forceinline
Definition: config.hpp:192