this repo has no description
dekker.one
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
34namespace Gecode { namespace Set { namespace Rel {
35
36 /**
37 * \brief Representation of the characteristic functions of two sets
38 */
39 class CharacteristicSets {
40 protected:
41 /// Size of the combined upper bounds
42 unsigned int xsize;
43 /// Storage for the characteristic functions
44 Support::BitSetBase b;
45 /// Elements in the combined upper bounds
46 int* ub;
47 /// Whether lower bound of x was updated
48 bool xlm;
49 /// Whether upper bound of x was updated
50 bool xum;
51 /// Whether lower bound of y was updated
52 bool ylm;
53 /// Whether upper bound of y was updated
54 bool yum;
55 /// Get bit \a i
56 bool get(unsigned int i) const;
57 /// Set bit \a i to value \a j
58 void set(unsigned int i, bool j);
59
60 /// \brief Value iterator for characteristic function
61 class CSIter {
62 public:
63 /// Pointer to the underlying set
64 CharacteristicSets* cs;
65 /// Current position
66 unsigned int i;
67 /// Offset from start of bitset
68 unsigned int xoff;
69 /// Offset for each element (0=lower bound, 1=upper bound)
70 unsigned int yoff;
71 /// Move iterator to next element
72 void operator++ (void);
73 /// Default constructor
74 CSIter(void);
75 /// Constructor
76 CSIter(CharacteristicSets& cs0, unsigned int xoff0, unsigned int yoff0);
77 /// Test if iterator is finished
78 bool operator() (void) const;
79 /// Value of current iterator position
80 int val(void) const;
81 };
82
83 public:
84 /// Constructor
85 template<class View0, class View1>
86 CharacteristicSets(Region& re, View0 x, View1 y);
87
88 /// Return minimum of element \a i for variable x
89 bool xmin(unsigned int i) const;
90 /// Return maximum of element \a i for variable x
91 bool xmax(unsigned int i) const;
92 /// Return minimum of element \a i for variable y
93 bool ymin(unsigned int i) const;
94 /// Return maximum of element \a i for variable y
95 bool ymax(unsigned int i) const;
96
97 /// Set minimum of element \a i for variable x to \a j
98 void xmin(unsigned int i, bool j);
99 /// Set maximum of element \a i for variable x to \a j
100 void xmax(unsigned int i, bool j);
101 /// Set minimum of element \a i for variable y to \a j
102 void ymin(unsigned int i, bool j);
103 /// Set maximum of element \a i for variable y to \a j
104 void ymax(unsigned int i, bool j);
105
106 /// Update upper bound of \f$x_i\f$ to \a j
107 ModEvent xlq(unsigned int i, bool j);
108 /// Update lower bound of \f$x_i\f$ to \a j
109 ModEvent xgq(unsigned int i, bool j);
110 /// Update upper bound of \f$y_i\f$ to \a j
111 ModEvent ylq(unsigned int i, bool j);
112 /// Update lower bound of \f$y_i\f$ to \a j
113 ModEvent ygq(unsigned int i, bool j);
114
115 /// Return size of combined upper bounds
116 unsigned int size(void) const;
117
118 /// Prune \a x and \a y using computed bounds
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
137 CharacteristicSets::size(void) const {
138 return xsize;
139 }
140
141 forceinline
142 CharacteristicSets::CSIter::CSIter(void) {}
143 forceinline
144 CharacteristicSets::CSIter::CSIter(CharacteristicSets& cs0,
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
151 CharacteristicSets::CSIter::operator++ (void) {
152 i++;
153 while ((i < cs->xsize) && !cs->get(xoff+2*i+yoff))
154 i++;
155 }
156 forceinline bool
157 CharacteristicSets::CSIter::operator() (void) const {
158 return i<cs->xsize;
159 }
160 forceinline int
161 CharacteristicSets::CSIter::val(void) const {
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
200 forceinline ModEvent
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 }
211 forceinline ModEvent
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 }
222 forceinline ModEvent
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 }
233 forceinline ModEvent
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>
246 forceinline ExecStatus
247 CharacteristicSets::prune(Space& home, View0 x, View1 y) {
248 if (xlm) {
249 CSIter i(*this,0,0);
250 Iter::Values::ToRanges<CSIter> ir(i);
251 GECODE_ME_CHECK(x.includeI(home,ir));
252 }
253 if (xum) {
254 CSIter i(*this,0,1);
255 Iter::Values::ToRanges<CSIter> ir(i);
256 GECODE_ME_CHECK(x.intersectI(home,ir));
257 }
258 if (ylm) {
259 CSIter i(*this,2*xsize,0);
260 Iter::Values::ToRanges<CSIter> ir(i);
261 GECODE_ME_CHECK(y.includeI(home,ir));
262 }
263 if (yum) {
264 CSIter i(*this,2*xsize,1);
265 Iter::Values::ToRanges<CSIter> ir(i);
266 GECODE_ME_CHECK(y.intersectI(home,ir));
267 }
268 return ES_OK;
269 }
270
271 template<class View0, class View1>
272 forceinline
273 CharacteristicSets::CharacteristicSets(Region& re,View0 x, View1 y)
274 : xlm(false), xum(false), ylm(false), yum(false) {
275 LubRanges<View0> xlub(x);
276 LubRanges<View1> ylub(y);
277 Iter::Ranges::Union<LubRanges<View0>,LubRanges<View1> > xylub(xlub,ylub);
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();
283 Iter::Ranges::ToValues<Iter::Ranges::Cache> xylubv(xylubc);
284 LubRanges<View0> xur(x);
285 GlbRanges<View0> xlr(x);
286 LubRanges<View1> yur(y);
287 GlbRanges<View1> ylr(y);
288 Iter::Ranges::ToValues<LubRanges<View0> > xuv(xur);
289 Iter::Ranges::ToValues<GlbRanges<View0> > xlv(xlr);
290 Iter::Ranges::ToValues<LubRanges<View1> > yuv(yur);
291 Iter::Ranges::ToValues<GlbRanges<View1> > ylv(ylr);
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>
314 forceinline
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>
319 forceinline
320 Lq<View0,View1,strict>::Lq(Space& home, Lq& p)
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*
336 Lq<View0,View1,strict>::copy(Space& home) {
337 return new (home) Lq(home,*this);
338 }
339
340 template<class View0, class View1, bool strict>
341 ExecStatus
342 Lq<View0,View1,strict>::propagate(Space& home, const ModEventDelta&) {
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