Generated on Thu Jan 31 2019 20:56:35 for Gecode by doxygen 1.8.15
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  * Last modified:
10  * $Date: 2016-06-27 14:37:04 +0200 (Mon, 27 Jun 2016) $ by $Author: schulte $
11  * $Revision: 15129 $
12  *
13  * This file is part of Gecode, the generic constraint
14  * development environment:
15  * http://www.gecode.org
16  *
17  * Permission is hereby granted, free of charge, to any person obtaining
18  * a copy of this software and associated documentation files (the
19  * "Software"), to deal in the Software without restriction, including
20  * without limitation the rights to use, copy, modify, merge, publish,
21  * distribute, sublicense, and/or sell copies of the Software, and to
22  * permit persons to whom the Software is furnished to do so, subject to
23  * the following conditions:
24  *
25  * The above copyright notice and this permission notice shall be
26  * included in all copies or substantial portions of the Software.
27  *
28  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
29  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
30  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
31  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
32  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
33  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
34  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
35  *
36  */
37 
38 namespace Gecode { namespace Set { namespace Rel {
39 
44  protected:
46  unsigned int xsize;
50  int* ub;
52  bool xlm;
54  bool xum;
56  bool ylm;
58  bool yum;
60  bool get(unsigned int i) const;
62  void set(unsigned int i, bool j);
63 
65  class CSIter {
66  public:
70  unsigned int i;
72  unsigned int xoff;
74  unsigned int yoff;
76  void operator++ (void);
78  CSIter(void);
80  CSIter(CharacteristicSets& cs0, unsigned int xoff0, unsigned int yoff0);
82  bool operator() (void) const;
84  int val(void) const;
85  };
86 
87  public:
89  template<class View0, class View1>
90  CharacteristicSets(Region& re, View0 x, View1 y);
91 
93  bool xmin(unsigned int i) const;
95  bool xmax(unsigned int i) const;
97  bool ymin(unsigned int i) const;
99  bool ymax(unsigned int i) const;
100 
102  void xmin(unsigned int i, bool j);
104  void xmax(unsigned int i, bool j);
106  void ymin(unsigned int i, bool j);
108  void ymax(unsigned int i, bool j);
109 
111  ModEvent xlq(unsigned int i, bool j);
113  ModEvent xgq(unsigned int i, bool j);
115  ModEvent ylq(unsigned int i, bool j);
117  ModEvent ygq(unsigned int i, bool j);
118 
120  unsigned int size(void) const;
121 
123  template<class View0, class View1>
124  ExecStatus prune(Space& home, View0 x, View1 y);
125 
126  };
127 
128 
129  forceinline bool
130  CharacteristicSets::get(unsigned int i) const {
131  return b.get(i);
132  }
133  forceinline void
134  CharacteristicSets::set(unsigned int i, bool j) {
135  if (j)
136  b.set(i);
137  else
138  b.clear(i);
139  }
140  forceinline unsigned int
142  return xsize;
143  }
144 
149  unsigned int xoff0, unsigned int yoff0)
150  : cs(&cs0), i(0), xoff(xoff0), yoff(yoff0) {
151  while ((i < cs->xsize) && !cs->get(xoff+2*i+yoff))
152  i++;
153  }
154  forceinline void
156  i++;
157  while ((i < cs->xsize) && !cs->get(xoff+2*i+yoff))
158  i++;
159  }
160  forceinline bool
162  return i<cs->xsize;
163  }
164  forceinline int
166  return cs->ub[i];
167  }
168 
169 
170  forceinline bool
171  CharacteristicSets::xmin(unsigned int i) const {
172  return get(2*i);
173  }
174  forceinline bool
175  CharacteristicSets::xmax(unsigned int i) const {
176  return get(2*i+1);
177  }
178  forceinline bool
179  CharacteristicSets::ymin(unsigned int i) const {
180  return get(2*xsize+2*i);
181  }
182  forceinline bool
183  CharacteristicSets::ymax(unsigned int i) const {
184  return get(2*xsize+2*i+1);
185  }
186 
187  forceinline void
188  CharacteristicSets::xmin(unsigned int i, bool j) {
189  set(2*i,j);
190  }
191  forceinline void
192  CharacteristicSets::xmax(unsigned int i, bool j) {
193  set(2*i+1,j);
194  }
195  forceinline void
196  CharacteristicSets::ymin(unsigned int i, bool j) {
197  set(2*xsize+2*i,j);
198  }
199  forceinline void
200  CharacteristicSets::ymax(unsigned int i, bool j) {
201  set(2*xsize+2*i+1,j);
202  }
203 
205  CharacteristicSets::xlq(unsigned int i, bool j) {
206  if (!j) {
207  if (xmin(i)) return ME_SET_FAILED;
208  if (xmax(i)) {
209  xmax(i,false);
210  xum=true;
211  }
212  }
213  return ME_SET_NONE;
214  }
216  CharacteristicSets::xgq(unsigned int i, bool j) {
217  if (j) {
218  if (!xmax(i)) return ME_SET_FAILED;
219  if (!xmin(i)) {
220  xmin(i,true);
221  xlm=true;
222  }
223  }
224  return ME_SET_NONE;
225  }
227  CharacteristicSets::ylq(unsigned int i, bool j) {
228  if (!j) {
229  if (ymin(i)) return ME_SET_FAILED;
230  if (ymax(i)) {
231  ymax(i,false);
232  yum=true;
233  }
234  }
235  return ME_SET_NONE;
236  }
238  CharacteristicSets::ygq(unsigned int i, bool j) {
239  if (j) {
240  if (!ymax(i)) return ME_SET_FAILED;
241  if (!ymin(i)) {
242  ymin(i,true);
243  ylm=true;
244  }
245  }
246  return ME_SET_NONE;
247  }
248 
249  template<class View0, class View1>
251  CharacteristicSets::prune(Space& home, View0 x, View1 y) {
252  if (xlm) {
253  CSIter i(*this,0,0);
255  GECODE_ME_CHECK(x.includeI(home,ir));
256  }
257  if (xum) {
258  CSIter i(*this,0,1);
260  GECODE_ME_CHECK(x.intersectI(home,ir));
261  }
262  if (ylm) {
263  CSIter i(*this,2*xsize,0);
265  GECODE_ME_CHECK(y.includeI(home,ir));
266  }
267  if (yum) {
268  CSIter i(*this,2*xsize,1);
270  GECODE_ME_CHECK(y.intersectI(home,ir));
271  }
272  return ES_OK;
273  }
274 
275  template<class View0, class View1>
278  : xlm(false), xum(false), ylm(false), yum(false) {
279  LubRanges<View0> xlub(x);
280  LubRanges<View1> ylub(y);
282  Iter::Ranges::Cache xylubc(re,xylub);
283  xsize = Iter::Ranges::size(xylubc);
284  b.init(re,4*xsize);
285  ub = re.alloc<int>(xsize);
286  xylubc.reset();
288  LubRanges<View0> xur(x);
289  GlbRanges<View0> xlr(x);
290  LubRanges<View1> yur(y);
291  GlbRanges<View1> ylr(y);
296  for (unsigned int i=0; xylubv(); ++xylubv, ++i) {
297  ub[i] = xylubv.val();
298  if (xlv() && xylubv.val()==xlv.val()) {
299  b.set(2*i);
300  ++xlv;
301  }
302  if (xuv() && xylubv.val()==xuv.val()) {
303  b.set(2*i+1);
304  ++xuv;
305  }
306  if (ylv() && xylubv.val()==ylv.val()) {
307  b.set(2*xsize+2*i);
308  ++ylv;
309  }
310  if (yuv() && xylubv.val()==yuv.val()) {
311  b.set(2*xsize+2*i+1);
312  ++yuv;
313  }
314  }
315  }
316 
317  template<class View0, class View1, bool strict>
319  Lq<View0,View1,strict>::Lq(Home home, View0 x, View1 y)
320  : MixBinaryPropagator<View0,PC_SET_ANY,View1,PC_SET_ANY>(home,x,y) {}
321 
322  template<class View0, class View1, bool strict>
324  Lq<View0,View1,strict>::Lq(Space& home, bool share, Lq& p)
325  : MixBinaryPropagator<View0,PC_SET_ANY,View1,PC_SET_ANY>(home,share,p) {}
326 
327  template<class View0, class View1, bool strict>
328  ExecStatus
329  Lq<View0,View1,strict>::post(Home home, View0 x, View1 y) {
330  if (strict)
331  GECODE_ME_CHECK(y.cardMin(home,1));
332  (void) new (home) Lq(home,x,y);
333  return ES_OK;
334  }
335 
336  template<class View0, class View1, bool strict>
337  Actor*
338  Lq<View0,View1,strict>::copy(Space& home, bool share) {
339  return new (home) Lq(home,share,*this);
340  }
341 
342  template<class View0, class View1, bool strict>
343  ExecStatus
345  if ( (!strict) && x1.cardMax()==0) {
346  GECODE_ME_CHECK(x0.cardMax(home,0));
347  }
348 
349  if (x0.cardMax()==0) {
350  return home.ES_SUBSUMED(*this);
351  }
352 
353  if (x0.glbMin() < x1.lubMin())
354  return ES_FAILED;
355  if (x1.glbMin() < x0.lubMin())
356  return home.ES_SUBSUMED(*this);
357 
358  bool assigned = x0.assigned() && x1.assigned();
359 
360  Region re(home);
361  CharacteristicSets cs(re,x0,x1);
362 
363  /*
364  * State 1
365  *
366  */
367  unsigned int i=0;
368  unsigned int firsti=0;
369  unsigned int n=cs.size();
370  while ((i<n) && (cs.xmin(i) == cs.ymax(i))) {
371  // case: =, >=
372  GECODE_ME_CHECK(cs.xlq(i,cs.ymax(i)));
373  GECODE_ME_CHECK(cs.ygq(i,cs.xmin(i)));
374  i++;
375  }
376 
377  if (i == n) {// case: $
378  if (strict) {
379  return ES_FAILED;
380  } else {
381  GECODE_ES_CHECK(cs.prune(home,x0,x1));
382  return home.ES_SUBSUMED(*this);
383  }
384  }
385 
386  // Possible cases left: <, <=, > (yields failure), ?
387  GECODE_ME_CHECK(cs.xlq(i,cs.ymax(i)));
388  GECODE_ME_CHECK(cs.ygq(i,cs.xmin(i)));
389 
390  if (cs.xmax(i) < cs.ymin(i)) { // case: < (after tell)
391  GECODE_ES_CHECK(cs.prune(home,x0,x1));
392  return home.ES_SUBSUMED(*this);
393  }
394 
395  firsti=i;
396 
397  /*
398  * State 2
399  * prefix: (?|<=)
400  *
401  */
402  i++;
403 
404  while ((i < n) &&
405  (cs.xmin(i) == cs.ymax(i)) &&
406  (cs.xmax(i) == cs.ymin(i))) { // case: =
407  i++;
408  }
409 
410  if (i == n) { // case: $
411  if (strict)
412  goto rewrite_le;
413  else
414  goto rewrite_lq;
415  }
416 
417  if (cs.xmax(i) < cs.ymin(i)) // case: <
418  goto rewrite_lq;
419 
420  if (cs.xmin(i) > cs.ymax(i)) // case: >
421  goto rewrite_le;
422 
423  if (cs.xmax(i) <= cs.ymin(i)) {
424  // case: <= (invariant: not =, <)
425  /*
426  * State 3
427  * prefix: (?|<=),<=
428  *
429  */
430  i++;
431 
432  while ((i < n) && (cs.xmax(i) == cs.ymin(i))) {// case: <=, =
433  i++;
434  }
435 
436  if (i == n) { // case: $
437  if (strict) {
438  GECODE_ES_CHECK(cs.prune(home,x0,x1));
439  return assigned ? home.ES_SUBSUMED(*this) : ES_NOFIX;
440  } else {
441  goto rewrite_lq;
442  }
443  }
444 
445  if (cs.xmax(i) < cs.ymin(i)) // case: <
446  goto rewrite_lq;
447 
448  GECODE_ES_CHECK(cs.prune(home,x0,x1));
449  return assigned ? home.ES_SUBSUMED(*this) : ES_NOFIX;
450  }
451 
452  if (cs.xmin(i) >= cs.ymax(i)) {
453  // case: >= (invariant: not =, >)
454  /*
455  * State 4
456  * prefix: (?|<=) >=
457  *
458  */
459  i++;
460 
461  while ((i < n) && (cs.xmin(i) == cs.ymax(i))) {
462  // case: >=, =
463  i++;
464  }
465 
466  if (i == n) { // case: $
467  if (strict) {
468  goto rewrite_le;
469  } else {
470  GECODE_ES_CHECK(cs.prune(home,x0,x1));
471  return assigned ? home.ES_SUBSUMED(*this) : ES_NOFIX;
472  }
473  }
474 
475  if (cs.xmin(i) > cs.ymax(i)) // case: >
476  goto rewrite_le;
477 
478  GECODE_ES_CHECK(cs.prune(home,x0,x1));
479  return assigned ? home.ES_SUBSUMED(*this) : ES_NOFIX;
480  }
481 
482  GECODE_ES_CHECK(cs.prune(home,x0,x1));
483  return assigned ? home.ES_SUBSUMED(*this) : ES_NOFIX;
484 
485  rewrite_le:
486  GECODE_ME_CHECK(cs.xlq(firsti,false));
487  GECODE_ME_CHECK(cs.ygq(firsti,true));
488  GECODE_ES_CHECK(cs.prune(home,x0,x1));
489  return home.ES_SUBSUMED(*this);
490  rewrite_lq:
491  GECODE_ES_CHECK(cs.prune(home,x0,x1));
492  return assigned ? home.ES_SUBSUMED(*this) : ES_NOFIX;
493  }
494 
495 }}}
496 
497 // STATISTICS: set-prop
bool get(unsigned int i) const
Access value at bit i.
CSIter(void)
Default constructor.
Definition: lq.hpp:146
const Gecode::ModEvent ME_SET_FAILED
Domain operation has resulted in failure.
Definition: var-type.hpp:138
Value iterator for characteristic function.
Definition: lq.hpp:65
ExecStatus ES_SUBSUMED(Propagator &p)
Definition: core.hpp:3614
unsigned int yoff
Offset for each element (0=lower bound, 1=upper bound)
Definition: lq.hpp:74
void clear(unsigned int i)
Clear bit i.
T * alloc(long unsigned int n)
Allocate block of n objects of type T from region.
Definition: region.hpp:326
Support::BitSetBase b
Storage for the characteristic functions.
Definition: lq.hpp:48
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: lq.hpp:344
Basic bitset support.
int ModEvent
Type for modification events.
Definition: core.hpp:142
Propagator for set less than or equal
Definition: rel.hh:208
bool yum
Whether upper bound of y was updated.
Definition: lq.hpp:58
ModEvent xgq(unsigned int i, bool j)
Update lower bound of to j.
Definition: lq.hpp:216
Range iterator for the greatest lower bound.
Definition: var-imp.hpp:363
unsigned int size(void) const
Return size of combined upper bounds.
Definition: lq.hpp:141
bool operator()(void) const
Test if iterator is finished.
Definition: lq.hpp:161
Handle to region.
Definition: region.hpp:61
bool get(unsigned int i) const
Get bit i.
Definition: lq.hpp:130
CharacteristicSets * cs
Pointer to the underlying set.
Definition: lq.hpp:68
Computation spaces.
Definition: core.hpp:1748
int val(void) const
Return current value.
Range iterator for the least upper bound.
Definition: var-imp.hpp:321
Base-class for both propagators and branchers.
Definition: core.hpp:696
bool xmax(unsigned int i) const
Return maximum of element i for variable x.
Definition: lq.hpp:175
#define GECODE_ES_CHECK(es)
Check whether execution status es is failed or subsumed, and forward failure or subsumption.
Definition: macros.hpp:95
int val(void) const
Value of current iterator position.
Definition: lq.hpp:165
int p
Number of positive literals for node type.
Definition: bool-expr.cpp:236
void set(unsigned int i, bool j)
Set bit i to value j.
Definition: lq.hpp:134
Gecode::IntArgs i(4, 1, 2, 3, 4)
bool ymin(unsigned int i) const
Return minimum of element i for variable y.
Definition: lq.hpp:179
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
void reset(void)
Reset iterator to start.
Execution has resulted in failure.
Definition: core.hpp:542
bool xmin(unsigned int i) const
Return minimum of element i for variable x.
Definition: lq.hpp:171
void operator++(void)
Move iterator to next element.
Definition: lq.hpp:155
unsigned int cardMin(void) const
Return cardinality minimum.
Definition: set.hpp:82
Representation of the characteristic functions of two sets.
Definition: lq.hpp:43
Value iterator from range iterator.
Range iterator from value iterator.
unsigned int size(I &i)
Size of all ranges of range iterator i.
Lq(Space &home, bool share, Lq &p)
Constructor for cloning p.
Definition: lq.hpp:324
virtual Actor * copy(Space &home, bool)
Copy propagator during cloning.
Definition: lq.hpp:338
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.
ModEvent xlq(unsigned int i, bool j)
Update upper bound of to j.
Definition: lq.hpp:205
const Gecode::ModEvent ME_SET_NONE
Domain operation has not changed domain.
Definition: var-type.hpp:140
unsigned int i
Current position.
Definition: lq.hpp:70
CharacteristicSets(Region &re, View0 x, View1 y)
Constructor.
Definition: lq.hpp:277
#define GECODE_ME_CHECK(me)
Check whether modification event me is failed, and forward failure.
Definition: macros.hpp:56
const Gecode::PropCond PC_SET_ANY
Propagate when any bound or the cardinality of a view changes.
Definition: var-type.hpp:248
ExecStatus prune(Space &home, View0 x, View1 y)
Prune x and y using computed bounds.
Definition: lq.hpp:251
Range iterator for computing union (binary)
ModEvent ylq(unsigned int i, bool j)
Update upper bound of to j.
Definition: lq.hpp:227
Post propagator for SetVar SetOpType SetVar y
Definition: set.hh:784
bool xlm
Whether lower bound of x was updated.
Definition: lq.hpp:52
Mixed binary propagator.
Definition: propagator.hpp:213
Range iterator cache
ExecStatus
Definition: core.hpp:540
bool assigned(View x, int v)
Whether x is assigned to value v.
Definition: single.hpp:47
#define forceinline
Definition: config.hpp:173
static ExecStatus post(Home home, View0 x, View1 y)
Post propagator .
Definition: lq.hpp:329
int * ub
Elements in the combined upper bounds.
Definition: lq.hpp:50
Post propagator for SetVar x
Definition: set.hh:784
Execution is okay.
Definition: core.hpp:544
Propagation has not computed fixpoint.
Definition: core.hpp:543
unsigned int xsize
Size of the combined upper bounds.
Definition: lq.hpp:46
Gecode toplevel namespace
bool ymax(unsigned int i) const
Return maximum of element i for variable y.
Definition: lq.hpp:183
ModEvent ygq(unsigned int i, bool j)
Update lower bound of to j.
Definition: lq.hpp:238
int ModEventDelta
Modification event deltas.
Definition: core.hpp:169
unsigned int xoff
Offset from start of bitset.
Definition: lq.hpp:72
Home class for posting propagators
Definition: core.hpp:922
bool xum
Whether upper bound of x was updated.
Definition: lq.hpp:54
bool ylm
Whether lower bound of y was updated.
Definition: lq.hpp:56