Generated on Sun Aug 9 2020 05:34:08 for Gecode by doxygen 1.8.18
lq.hpp
Go to the documentation of this file.
1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2 /*
3  * Main authors:
4  * Guido Tack <tack@gecode.org>
5  *
6  * Copyright:
7  * Guido Tack, 2011
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 Set { namespace Rel {
35 
40  protected:
42  unsigned int xsize;
46  int* ub;
48  bool xlm;
50  bool xum;
52  bool ylm;
54  bool yum;
56  bool get(unsigned int i) const;
58  void set(unsigned int i, bool j);
59 
61  class CSIter {
62  public:
66  unsigned int i;
68  unsigned int xoff;
70  unsigned int yoff;
72  void operator++ (void);
74  CSIter(void);
76  CSIter(CharacteristicSets& cs0, unsigned int xoff0, unsigned int yoff0);
78  bool operator() (void) const;
80  int val(void) const;
81  };
82 
83  public:
85  template<class View0, class View1>
86  CharacteristicSets(Region& re, View0 x, View1 y);
87 
89  bool xmin(unsigned int i) const;
91  bool xmax(unsigned int i) const;
93  bool ymin(unsigned int i) const;
95  bool ymax(unsigned int i) const;
96 
98  void xmin(unsigned int i, bool j);
100  void xmax(unsigned int i, bool j);
102  void ymin(unsigned int i, bool j);
104  void ymax(unsigned int i, bool j);
105 
107  ModEvent xlq(unsigned int i, bool j);
109  ModEvent xgq(unsigned int i, bool j);
111  ModEvent ylq(unsigned int i, bool j);
113  ModEvent ygq(unsigned int i, bool j);
114 
116  unsigned int size(void) const;
117 
119  template<class View0, class View1>
120  ExecStatus prune(Space& home, View0 x, View1 y);
121 
122  };
123 
124 
125  forceinline bool
126  CharacteristicSets::get(unsigned int i) const {
127  return b.get(i);
128  }
129  forceinline void
130  CharacteristicSets::set(unsigned int i, bool j) {
131  if (j)
132  b.set(i);
133  else
134  b.clear(i);
135  }
136  forceinline unsigned int
138  return xsize;
139  }
140 
145  unsigned int xoff0, unsigned int yoff0)
146  : cs(&cs0), i(0), xoff(xoff0), yoff(yoff0) {
147  while ((i < cs->xsize) && !cs->get(xoff+2*i+yoff))
148  i++;
149  }
150  forceinline void
152  i++;
153  while ((i < cs->xsize) && !cs->get(xoff+2*i+yoff))
154  i++;
155  }
156  forceinline bool
158  return i<cs->xsize;
159  }
160  forceinline int
162  return cs->ub[i];
163  }
164 
165 
166  forceinline bool
167  CharacteristicSets::xmin(unsigned int i) const {
168  return get(2*i);
169  }
170  forceinline bool
171  CharacteristicSets::xmax(unsigned int i) const {
172  return get(2*i+1);
173  }
174  forceinline bool
175  CharacteristicSets::ymin(unsigned int i) const {
176  return get(2*xsize+2*i);
177  }
178  forceinline bool
179  CharacteristicSets::ymax(unsigned int i) const {
180  return get(2*xsize+2*i+1);
181  }
182 
183  forceinline void
184  CharacteristicSets::xmin(unsigned int i, bool j) {
185  set(2*i,j);
186  }
187  forceinline void
188  CharacteristicSets::xmax(unsigned int i, bool j) {
189  set(2*i+1,j);
190  }
191  forceinline void
192  CharacteristicSets::ymin(unsigned int i, bool j) {
193  set(2*xsize+2*i,j);
194  }
195  forceinline void
196  CharacteristicSets::ymax(unsigned int i, bool j) {
197  set(2*xsize+2*i+1,j);
198  }
199 
201  CharacteristicSets::xlq(unsigned int i, bool j) {
202  if (!j) {
203  if (xmin(i)) return ME_SET_FAILED;
204  if (xmax(i)) {
205  xmax(i,false);
206  xum=true;
207  }
208  }
209  return ME_SET_NONE;
210  }
212  CharacteristicSets::xgq(unsigned int i, bool j) {
213  if (j) {
214  if (!xmax(i)) return ME_SET_FAILED;
215  if (!xmin(i)) {
216  xmin(i,true);
217  xlm=true;
218  }
219  }
220  return ME_SET_NONE;
221  }
223  CharacteristicSets::ylq(unsigned int i, bool j) {
224  if (!j) {
225  if (ymin(i)) return ME_SET_FAILED;
226  if (ymax(i)) {
227  ymax(i,false);
228  yum=true;
229  }
230  }
231  return ME_SET_NONE;
232  }
234  CharacteristicSets::ygq(unsigned int i, bool j) {
235  if (j) {
236  if (!ymax(i)) return ME_SET_FAILED;
237  if (!ymin(i)) {
238  ymin(i,true);
239  ylm=true;
240  }
241  }
242  return ME_SET_NONE;
243  }
244 
245  template<class View0, class View1>
247  CharacteristicSets::prune(Space& home, View0 x, View1 y) {
248  if (xlm) {
249  CSIter i(*this,0,0);
251  GECODE_ME_CHECK(x.includeI(home,ir));
252  }
253  if (xum) {
254  CSIter i(*this,0,1);
256  GECODE_ME_CHECK(x.intersectI(home,ir));
257  }
258  if (ylm) {
259  CSIter i(*this,2*xsize,0);
261  GECODE_ME_CHECK(y.includeI(home,ir));
262  }
263  if (yum) {
264  CSIter i(*this,2*xsize,1);
266  GECODE_ME_CHECK(y.intersectI(home,ir));
267  }
268  return ES_OK;
269  }
270 
271  template<class View0, class View1>
274  : xlm(false), xum(false), ylm(false), yum(false) {
275  LubRanges<View0> xlub(x);
276  LubRanges<View1> ylub(y);
278  Iter::Ranges::Cache xylubc(re,xylub);
279  xsize = Iter::Ranges::size(xylubc);
280  b.init(re,4*xsize);
281  ub = re.alloc<int>(xsize);
282  xylubc.reset();
284  LubRanges<View0> xur(x);
285  GlbRanges<View0> xlr(x);
286  LubRanges<View1> yur(y);
287  GlbRanges<View1> ylr(y);
292  for (unsigned int i=0; xylubv(); ++xylubv, ++i) {
293  ub[i] = xylubv.val();
294  if (xlv() && xylubv.val()==xlv.val()) {
295  b.set(2*i);
296  ++xlv;
297  }
298  if (xuv() && xylubv.val()==xuv.val()) {
299  b.set(2*i+1);
300  ++xuv;
301  }
302  if (ylv() && xylubv.val()==ylv.val()) {
303  b.set(2*xsize+2*i);
304  ++ylv;
305  }
306  if (yuv() && xylubv.val()==yuv.val()) {
307  b.set(2*xsize+2*i+1);
308  ++yuv;
309  }
310  }
311  }
312 
313  template<class View0, class View1, bool strict>
315  Lq<View0,View1,strict>::Lq(Home home, View0 x, View1 y)
316  : MixBinaryPropagator<View0,PC_SET_ANY,View1,PC_SET_ANY>(home,x,y) {}
317 
318  template<class View0, class View1, bool strict>
321  : MixBinaryPropagator<View0,PC_SET_ANY,View1,PC_SET_ANY>(home,p) {}
322 
323  template<class View0, class View1, bool strict>
324  ExecStatus
325  Lq<View0,View1,strict>::post(Home home, View0 x, View1 y) {
326  if (strict)
327  GECODE_ME_CHECK(y.cardMin(home,1));
328  if (same(x,y))
329  return strict ? ES_FAILED : ES_OK;
330  (void) new (home) Lq(home,x,y);
331  return ES_OK;
332  }
333 
334  template<class View0, class View1, bool strict>
335  Actor*
337  return new (home) Lq(home,*this);
338  }
339 
340  template<class View0, class View1, bool strict>
341  ExecStatus
343  if ( (!strict) && x1.cardMax()==0) {
344  GECODE_ME_CHECK(x0.cardMax(home,0));
345  }
346 
347  if (x0.cardMax()==0) {
348  return home.ES_SUBSUMED(*this);
349  }
350 
351  if (x0.glbMin() < x1.lubMin())
352  return ES_FAILED;
353  if (x1.glbMin() < x0.lubMin())
354  return home.ES_SUBSUMED(*this);
355 
356  bool assigned = x0.assigned() && x1.assigned();
357 
358  Region re;
359  CharacteristicSets cs(re,x0,x1);
360 
361  /*
362  * State 1
363  *
364  */
365  unsigned int i=0;
366  unsigned int firsti=0;
367  unsigned int n=cs.size();
368  while ((i<n) && (cs.xmin(i) == cs.ymax(i))) {
369  // case: =, >=
370  GECODE_ME_CHECK(cs.xlq(i,cs.ymax(i)));
371  GECODE_ME_CHECK(cs.ygq(i,cs.xmin(i)));
372  i++;
373  }
374 
375  if (i == n) {// case: $
376  if (strict) {
377  return ES_FAILED;
378  } else {
379  GECODE_ES_CHECK(cs.prune(home,x0,x1));
380  return home.ES_SUBSUMED(*this);
381  }
382  }
383 
384  // Possible cases left: <, <=, > (yields failure), ?
385  GECODE_ME_CHECK(cs.xlq(i,cs.ymax(i)));
386  GECODE_ME_CHECK(cs.ygq(i,cs.xmin(i)));
387 
388  if (cs.xmax(i) < cs.ymin(i)) { // case: < (after tell)
389  GECODE_ES_CHECK(cs.prune(home,x0,x1));
390  return home.ES_SUBSUMED(*this);
391  }
392 
393  firsti=i;
394 
395  /*
396  * State 2
397  * prefix: (?|<=)
398  *
399  */
400  i++;
401 
402  while ((i < n) &&
403  (cs.xmin(i) == cs.ymax(i)) &&
404  (cs.xmax(i) == cs.ymin(i))) { // case: =
405  i++;
406  }
407 
408  if (i == n) { // case: $
409  if (strict)
410  goto rewrite_le;
411  else
412  goto rewrite_lq;
413  }
414 
415  if (cs.xmax(i) < cs.ymin(i)) // case: <
416  goto rewrite_lq;
417 
418  if (cs.xmin(i) > cs.ymax(i)) // case: >
419  goto rewrite_le;
420 
421  if (cs.xmax(i) <= cs.ymin(i)) {
422  // case: <= (invariant: not =, <)
423  /*
424  * State 3
425  * prefix: (?|<=),<=
426  *
427  */
428  i++;
429 
430  while ((i < n) && (cs.xmax(i) == cs.ymin(i))) {// case: <=, =
431  i++;
432  }
433 
434  if (i == n) { // case: $
435  if (strict) {
436  GECODE_ES_CHECK(cs.prune(home,x0,x1));
437  return assigned ? home.ES_SUBSUMED(*this) : ES_NOFIX;
438  } else {
439  goto rewrite_lq;
440  }
441  }
442 
443  if (cs.xmax(i) < cs.ymin(i)) // case: <
444  goto rewrite_lq;
445 
446  GECODE_ES_CHECK(cs.prune(home,x0,x1));
447  return assigned ? home.ES_SUBSUMED(*this) : ES_NOFIX;
448  }
449 
450  if (cs.xmin(i) >= cs.ymax(i)) {
451  // case: >= (invariant: not =, >)
452  /*
453  * State 4
454  * prefix: (?|<=) >=
455  *
456  */
457  i++;
458 
459  while ((i < n) && (cs.xmin(i) == cs.ymax(i))) {
460  // case: >=, =
461  i++;
462  }
463 
464  if (i == n) { // case: $
465  if (strict) {
466  goto rewrite_le;
467  } else {
468  GECODE_ES_CHECK(cs.prune(home,x0,x1));
469  return assigned ? home.ES_SUBSUMED(*this) : ES_NOFIX;
470  }
471  }
472 
473  if (cs.xmin(i) > cs.ymax(i)) // case: >
474  goto rewrite_le;
475 
476  GECODE_ES_CHECK(cs.prune(home,x0,x1));
477  return assigned ? home.ES_SUBSUMED(*this) : ES_NOFIX;
478  }
479 
480  GECODE_ES_CHECK(cs.prune(home,x0,x1));
481  return assigned ? home.ES_SUBSUMED(*this) : ES_NOFIX;
482 
483  rewrite_le:
484  GECODE_ME_CHECK(cs.xlq(firsti,false));
485  GECODE_ME_CHECK(cs.ygq(firsti,true));
486  GECODE_ES_CHECK(cs.prune(home,x0,x1));
487  return home.ES_SUBSUMED(*this);
488  rewrite_lq:
489  GECODE_ES_CHECK(cs.prune(home,x0,x1));
490  return assigned ? home.ES_SUBSUMED(*this) : ES_NOFIX;
491  }
492 
493 }}}
494 
495 // STATISTICS: set-prop
unsigned int xoff
Offset from start of bitset.
Definition: lq.hpp:68
Post propagator for SetVar x
Definition: set.hh:767
Post propagator for SetVar SetOpType SetVar y
Definition: set.hh:767
ModEvent xgq(unsigned int i, bool j)
Update lower bound of to j.
Definition: lq.hpp:212
void init(A &a, unsigned int s, bool setbits=false)
Initialize for s bits and allocator a (only after default constructor)
void set(unsigned int i)
Set bit i.
bool get(unsigned int i) const
Get bit i.
Definition: lq.hpp:126
void operator++(void)
Move iterator to next element.
Definition: lq.hpp:151
ExecStatus prune(Space &home, View0 x, View1 y)
Prune x and y using computed bounds.
Definition: lq.hpp:247
ExecStatus ES_SUBSUMED(Propagator &p)
Definition: core.hpp:3563
unsigned int size(I &i)
Size of all ranges of range iterator i.
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: lq.hpp:342
bool xum
Whether upper bound of x was updated.
Definition: lq.hpp:50
bool assigned(View x, int v)
Whether x is assigned to value v.
Definition: single.hpp:43
static ExecStatus post(Home home, View0 x, View1 y)
Post propagator .
Definition: lq.hpp:325
unsigned int size(void) const
Return size of combined upper bounds.
Definition: lq.hpp:137
unsigned int cardMin(void) const
Return cardinality minimum.
Definition: set.hpp:78
T * alloc(long unsigned int n)
Allocate block of n objects of type T from region.
Definition: region.hpp:386
CharacteristicSets * cs
Pointer to the underlying set.
Definition: lq.hpp:64
unsigned int yoff
Offset for each element (0=lower bound, 1=upper bound)
Definition: lq.hpp:70
Computation spaces.
Definition: core.hpp:1742
Base-class for both propagators and branchers.
Definition: core.hpp:628
int val(void) const
Return current value.
unsigned int i
Current position.
Definition: lq.hpp:66
void reset(void)
Reset iterator to start.
Gecode toplevel namespace
Mixed binary propagator.
Definition: pattern.hpp:204
Support::BitSetBase b
Storage for the characteristic functions.
Definition: lq.hpp:44
#define GECODE_ES_CHECK(es)
Check whether execution status es is failed or subsumed, and forward failure or subsumption.
Definition: macros.hpp:91
bool operator()(void) const
Test if iterator is finished.
Definition: lq.hpp:157
CharacteristicSets(Region &re, View0 x, View1 y)
Constructor.
Definition: lq.hpp:273
ModEvent ylq(unsigned int i, bool j)
Update upper bound of to j.
Definition: lq.hpp:223
void clear(unsigned int i)
Clear bit i.
Home class for posting propagators
Definition: core.hpp:856
bool same(VX, VY)
Test whether two views are in fact the same.
Definition: common.hpp:57
Representation of the characteristic functions of two sets.
Definition: lq.hpp:39
Value iterator from range iterator.
Range iterator from value iterator.
Handle to region.
Definition: region.hpp:55
Basic bitset support.
bool yum
Whether upper bound of y was updated.
Definition: lq.hpp:54
Range iterator for the greatest lower bound.
Definition: var-imp.hpp:359
bool xmin(unsigned int i) const
Return minimum of element i for variable x.
Definition: lq.hpp:167
const Gecode::ModEvent ME_SET_NONE
Domain operation has not changed domain.
Definition: var-type.hpp:140
const Gecode::ModEvent ME_SET_FAILED
Domain operation has resulted in failure.
Definition: var-type.hpp:138
unsigned int xsize
Size of the combined upper bounds.
Definition: lq.hpp:42
bool ymin(unsigned int i) const
Return minimum of element i for variable y.
Definition: lq.hpp:175
int ModEvent
Type for modification events.
Definition: core.hpp:62
virtual Actor * copy(Space &home)
Copy propagator during cloning.
Definition: lq.hpp:336
Range iterator cache
Range iterator for computing union (binary)
void set(unsigned int i, bool j)
Set bit i to value j.
Definition: lq.hpp:130
Lq(Space &home, Lq &p)
Constructor for cloning p.
Definition: lq.hpp:320
bool get(unsigned int i) const
Access value at bit i.
bool ylm
Whether lower bound of y was updated.
Definition: lq.hpp:52
ModEvent xlq(unsigned int i, bool j)
Update upper bound of to j.
Definition: lq.hpp:201
Range iterator for the least upper bound.
Definition: var-imp.hpp:317
#define forceinline
Definition: config.hpp:185
bool xmax(unsigned int i) const
Return maximum of element i for variable x.
Definition: lq.hpp:171
const Gecode::PropCond PC_SET_ANY
Propagate when any bound or the cardinality of a view changes.
Definition: var-type.hpp:248
int val(void) const
Value of current iterator position.
Definition: lq.hpp:161
#define GECODE_ME_CHECK(me)
Check whether modification event me is failed, and forward failure.
Definition: macros.hpp:52
Propagator for set less than or equal
Definition: rel.hh:208
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:234
@ ES_FAILED
Execution has resulted in failure.
Definition: core.hpp:474
int ModEventDelta
Modification event deltas.
Definition: core.hpp:89
CSIter(void)
Default constructor.
Definition: lq.hpp:142
@ ES_NOFIX
Propagation has not computed fixpoint.
Definition: core.hpp:475
Gecode::IntArgs i({1, 2, 3, 4})
bool xlm
Whether lower bound of x was updated.
Definition: lq.hpp:48
bool ymax(unsigned int i) const
Return maximum of element i for variable y.
Definition: lq.hpp:179
ModEvent ygq(unsigned int i, bool j)
Update lower bound of to j.
Definition: lq.hpp:234
@ ES_OK
Execution is okay.
Definition: core.hpp:476
int p
Number of positive literals for node type.
Definition: bool-expr.cpp:232
int * ub
Elements in the combined upper bounds.
Definition: lq.hpp:46
Value iterator for characteristic function.
Definition: lq.hpp:61
ExecStatus
Definition: core.hpp:472