Generated on Thu Mar 7 2013 10:21:33 for Gecode by doxygen 1.8.3.1
lex.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  * Last modified:
10  * $Date: 2011-07-08 19:58:02 +1000 (Fri, 08 Jul 2011) $ by $Author: schulte $
11  * $Revision: 12163 $
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 Int { namespace Rel {
39 
40  /*
41  * Lexical order propagator
42  */
43  template<class View>
44  inline
46  ViewArray<View>& x0, ViewArray<View>& y0, bool s)
47  : Propagator(home), x(x0), y(y0), strict(s) {
48  x.subscribe(home, *this, PC_INT_BND);
49  y.subscribe(home, *this, PC_INT_BND);
50  }
51 
52  template<class View>
55  : Propagator(home,share,p), strict(p.strict) {
56  x.update(home,share,p.x);
57  y.update(home,share,p.y);
58  }
59 
60  template<class View>
61  Actor*
62  LexLqLe<View>::copy(Space& home, bool share) {
63  return new (home) LexLqLe<View>(home,share,*this);
64  }
65 
66  template<class View>
67  PropCost
68  LexLqLe<View>::cost(const Space&, const ModEventDelta&) const {
69  return PropCost::linear(PropCost::LO, x.size());
70  }
71 
72  template<class View>
73  forceinline size_t
75  assert(!home.failed());
76  x.cancel(home,*this,PC_INT_BND);
77  y.cancel(home,*this,PC_INT_BND);
78  (void) Propagator::dispose(home);
79  return sizeof(*this);
80  }
81 
82  template<class View>
85  /*
86  * State 1
87  *
88  */
89  {
90  int i = 0;
91  int n = x.size();
92 
93  while ((i < n) && (x[i].min() == y[i].max())) {
94  // case: =, >=
95  GECODE_ME_CHECK(x[i].lq(home,y[i].max()));
96  GECODE_ME_CHECK(y[i].gq(home,x[i].min()));
97  i++;
98  }
99 
100  if (i == n) // case: $
101  return strict ? ES_FAILED : home.ES_SUBSUMED(*this);
102 
103  // Possible cases left: <, <=, > (yields failure), ?
104  GECODE_ME_CHECK(x[i].lq(home,y[i].max()));
105  GECODE_ME_CHECK(y[i].gq(home,x[i].min()));
106 
107  if (x[i].max() < y[i].min()) // case: < (after tell)
108  return home.ES_SUBSUMED(*this);
109 
110  // x[i] can never be equal to y[i] (otherwise: >=)
111  assert(!(x[i].assigned() && y[i].assigned() &&
112  x[i].val() == y[i].val()));
113  // Remove all elements between 0...i-1 as they are assigned and equal
114  x.drop_fst(i); y.drop_fst(i);
115  // After this, execution continues at [1]
116  }
117 
118  /*
119  * State 2
120  * prefix: (?|<=)
121  *
122  */
123  {
124  int i = 1;
125  int n = x.size();
126 
127  while ((i < n) &&
128  (x[i].min() == y[i].max()) &&
129  (x[i].max() == y[i].min())) { // case: =
130  assert(x[i].assigned() && y[i].assigned() &&
131  (x[i].val() == y[i].val()));
132  i++;
133  }
134 
135  if (i == n) { // case: $
136  if (strict)
137  goto rewrite_le;
138  else
139  goto rewrite_lq;
140  }
141 
142  if (x[i].max() < y[i].min()) // case: <
143  goto rewrite_lq;
144 
145  if (x[i].min() > y[i].max()) // case: >
146  goto rewrite_le;
147 
148  if (i > 1) {
149  // Remove equal elements [1...i-1], keep element [0]
150  x[i-1]=x[0]; x.drop_fst(i-1);
151  y[i-1]=y[0]; y.drop_fst(i-1);
152  }
153  }
154 
155  if (x[1].max() <= y[1].min()) {
156  // case: <= (invariant: not =, <)
157  /*
158  * State 3
159  * prefix: (?|<=),<=
160  *
161  */
162  int i = 2;
163  int n = x.size();
164 
165  while ((i < n) && (x[i].max() == y[i].min())) // case: <=, =
166  i++;
167 
168  if (i == n) { // case: $
169  if (strict)
170  return ES_FIX;
171  else
172  goto rewrite_lq;
173  }
174 
175  if (x[i].max() < y[i].min()) // case: <
176  goto rewrite_lq;
177 
178  if (x[i].min() > y[i].max()) { // case: >
179  // Eliminate [i]...[n-1]
180  for (int j=i; j<n; j++) {
181  x[j].cancel(home,*this,PC_INT_BND);
182  y[j].cancel(home,*this,PC_INT_BND);
183  }
184  x.size(i); y.size(i);
185  strict = true;
186  }
187 
188  return ES_FIX;
189  }
190 
191  if (x[1].min() >= y[1].max()) {
192  // case: >= (invariant: not =, >)
193  /*
194  * State 4
195  * prefix: (?|<=) >=
196  *
197  */
198  int i = 2;
199  int n = x.size();
200 
201  while ((i < n) && (x[i].min() == y[i].max()))
202  // case: >=, =
203  i++;
204 
205  if (i == n) { // case: $
206  if (strict)
207  goto rewrite_le;
208  else
209  return ES_FIX;
210  }
211 
212  if (x[i].min() > y[i].max()) // case: >
213  goto rewrite_le;
214 
215  if (x[i].max() < y[i].min()) { // case: <
216  // Eliminate [i]...[n-1]
217  for (int j=i; j<n; j++) {
218  x[j].cancel(home,*this,PC_INT_BND);
219  y[j].cancel(home,*this,PC_INT_BND);
220  }
221  x.size(i); y.size(i);
222  strict = false;
223  }
224 
225  return ES_FIX;
226  }
227 
228  return ES_FIX;
229 
230  rewrite_le:
231  GECODE_REWRITE(*this,Le<View>::post(home(*this),x[0],y[0]));
232  rewrite_lq:
233  GECODE_REWRITE(*this,Lq<View>::post(home(*this),x[0],y[0]));
234  }
235 
236  template<class View>
237  ExecStatus
239  ViewArray<View>& x, ViewArray<View>& y, bool strict) {
240  if (x.size() < y.size()) {
241  y.size(x.size()); strict=false;
242  } else if (x.size() > y.size()) {
243  x.size(y.size()); strict=true;
244  }
245  if (x.size() == 0)
246  return strict ? ES_FAILED : ES_OK;
247  if (x.size() == 1) {
248  if (strict)
249  return Le<View>::post(home,x[0],y[0]);
250  else
251  return Lq<View>::post(home,x[0],y[0]);
252  }
253  (void) new (home) LexLqLe<View>(home,x,y,strict);
254  return ES_OK;
255  }
256 
257 
258  /*
259  * Lexical disequality propagator
260  */
261  template<class View>
264  : Propagator(home),
265  x0(xv[xv.size()-2]), y0(yv[xv.size()-2]),
266  x1(xv[xv.size()-1]), y1(yv[xv.size()-1]),
267  x(xv), y(yv) {
268  int n = x.size();
269  assert(n > 1);
270  assert(n == y.size());
271  x.size(n-2); y.size(n-2);
272  x0.subscribe(home,*this,PC_INT_VAL); y0.subscribe(home,*this,PC_INT_VAL);
273  x1.subscribe(home,*this,PC_INT_VAL); y1.subscribe(home,*this,PC_INT_VAL);
274  }
275 
276  template<class View>
277  PropCost
278  LexNq<View>::cost(const Space&, const ModEventDelta&) const {
280  }
281 
282  template<class View>
284  LexNq<View>::LexNq(Space& home, bool share, LexNq<View>& p)
285  : Propagator(home,share,p) {
286  x0.update(home,share,p.x0); y0.update(home,share,p.y0);
287  x1.update(home,share,p.x1); y1.update(home,share,p.y1);
288  x.update(home,share,p.x); y.update(home,share,p.y);
289  }
290 
291  template<class View>
292  Actor*
293  LexNq<View>::copy(Space& home, bool share) {
294  /*
295  int n = x.size();
296  if (n > 0) {
297  // Eliminate all equal views and keep one disequal pair
298  for (int i=n; i--; )
299  switch (rtest_eq_bnd(x[i],y[i])) {
300  case RT_TRUE:
301  // Eliminate equal pair
302  n--; x[i]=x[n]; y[i]=y[n];
303  break;
304  case RT_FALSE:
305  // Just keep a single disequal pair
306  n=1; x[0]=x[i]; y[0]=y[i];
307  goto done;
308  case RT_MAYBE:
309  break;
310  default:
311  GECODE_NEVER;
312  }
313  done:
314  x.size(n); y.size(n);
315  }
316  */
317  return new (home) LexNq<View>(home,share,*this);
318  }
319 
320  template<class View>
321  inline ExecStatus
323  if (x.size() != y.size())
324  return ES_OK;
325  int n = x.size();
326  if (n > 0) {
327  // Eliminate all equal views
328  for (int i=n; i--; )
329  switch (rtest_eq_bnd(x[i],y[i])) {
330  case RT_TRUE:
331  // Eliminate equal pair
332  n--; x[i]=x[n]; y[i]=y[n];
333  break;
334  case RT_FALSE:
335  return ES_OK;
336  case RT_MAYBE:
337  if (same(x[i],y[i])) {
338  // Eliminate equal pair
339  n--; x[i]=x[n]; y[i]=y[n];
340  }
341  break;
342  default:
343  GECODE_NEVER;
344  }
345  x.size(n); y.size(n);
346  }
347  if (n == 0)
348  return ES_FAILED;
349  if (n == 1)
350  return Nq<View>::post(home,x[0],y[0]);
351  (void) new (home) LexNq(home,x,y);
352  return ES_OK;
353  }
354 
355  template<class View>
356  forceinline size_t
358  x0.cancel(home,*this,PC_INT_VAL); y0.cancel(home,*this,PC_INT_VAL);
359  x1.cancel(home,*this,PC_INT_VAL); y1.cancel(home,*this,PC_INT_VAL);
360  (void) Propagator::dispose(home);
361  return sizeof(*this);
362  }
363 
364  template<class View>
367  RelTest rt, View& x0, View& y0, View x1, View y1) {
368  if (rt == RT_TRUE) {
369  assert(x0.assigned() && y0.assigned());
370  assert(x0.val() == y0.val());
371  int n = x.size();
372  for (int i=n; i--; )
373  switch (rtest_eq_bnd(x[i],y[i])) {
374  case RT_TRUE:
375  // Eliminate equal pair
376  n--; x[i]=x[n]; y[i]=y[n];
377  break;
378  case RT_FALSE:
379  return home.ES_SUBSUMED(*this);
380  case RT_MAYBE:
381  // Move to x0, y0 and subscribe
382  x0=x[i]; y0=y[i];
383  n--; x[i]=x[n]; y[i]=y[n];
384  x.size(n); y.size(n);
385  x0.subscribe(home,*this,PC_INT_VAL,false);
386  y0.subscribe(home,*this,PC_INT_VAL,false);
387  return ES_FIX;
388  default:
389  GECODE_NEVER;
390  }
391  // No more views to subscribe to left
392  GECODE_REWRITE(*this,Nq<View>::post(home,x1,y1));
393  }
394  return ES_FIX;
395  }
396 
397  template<class View>
398  ExecStatus
400  RelTest rt0 = rtest_eq_bnd(x0,y0);
401  if (rt0 == RT_FALSE)
402  return home.ES_SUBSUMED(*this);
403  RelTest rt1 = rtest_eq_bnd(x1,y1);
404  if (rt1 == RT_FALSE)
405  return home.ES_SUBSUMED(*this);
406  GECODE_ES_CHECK(resubscribe(home,rt0,x0,y0,x1,y1));
407  GECODE_ES_CHECK(resubscribe(home,rt1,x1,y1,x0,y0));
408  return ES_FIX;
409  }
410 
411 
412 }}}
413 
414 // STATISTICS: int-prop