Generated on Sat Feb 7 2015 02:01:25 for Gecode by doxygen 1.8.9.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 11:58:02 +0200 (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
LexLqLe(Space &home, bool share, LexLqLe< View > &p)
Constructor for cloning p.
Definition: lex.hpp:54
View x0
Views currently subscribed to.
Definition: rel.hh:631
#define GECODE_REWRITE(prop, post)
Rewrite propagator by executing post function.
Definition: macros.hpp:109
Relation may hold or not.
Definition: view.hpp:1616
static ExecStatus post(Home home, ViewArray< View > &x, ViewArray< View > &y)
Post propagator .
Definition: lex.hpp:322
static PropCost linear(PropCost::Mod m, unsigned int n)
Linear complexity for modifier pcm and size measure n.
Definition: core.hpp:4041
ExecStatus ES_SUBSUMED(Propagator &p)
Definition: core.hpp:2973
ViewArray< View > y
Definition: rel.hh:600
ExecStatus resubscribe(Space &home, Propagator &p, VX &x0, ViewArray< VX > &x, VY &x1, ViewArray< VY > &y)
Definition: clause.hpp:142
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:57
Base-class for propagators.
Definition: core.hpp:755
Expensive.
Definition: core.hpp:564
Lexical disequality propagator.
Definition: rel.hh:628
Propagation has computed fixpoint.
Definition: core.hpp:528
ExecStatus resubscribe(Space &home, RelTest rt, View &x0, View &y0, View x1, View y1)
Update subscription.
Definition: lex.hpp:366
static ExecStatus post(Home home, View x0, View x1)
Post propagator .
Definition: lq-le.hpp:54
Computation spaces.
Definition: core.hpp:1362
virtual size_t dispose(Space &home)
Delete propagator and return its size.
Definition: lex.hpp:74
bool failed(void) const
Check whether space is failed.
Definition: core.hpp:3442
Base-class for both propagators and branchers.
Definition: core.hpp:666
#define GECODE_ES_CHECK(es)
Check whether execution status es is failed or subsumed, and forward failure or subsumption.
Definition: macros.hpp:84
LexNq(Home home, ViewArray< View > &x, ViewArray< View > &y)
Constructor for posting.
Definition: lex.hpp:263
ViewArray< View > x
View arrays.
Definition: rel.hh:600
bool same(const CachedView< View > &x, const CachedView< View > &y)
Definition: cached.hpp:389
int p
Number of positive literals for node type.
Definition: bool-expr.cpp:236
ViewArray< View > y
Definition: rel.hh:633
Gecode::IntArgs i(4, 1, 2, 3, 4)
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: lex.hpp:293
Execution has resulted in failure.
Definition: core.hpp:525
Relation does not hold.
Definition: view.hpp:1615
RelTest
Result of testing relation.
Definition: view.hpp:1614
static ExecStatus post(Home home, ViewArray< View > &x, ViewArray< View > &y, bool strict)
Post propagator for lexical order between x and y.
Definition: lex.hpp:238
const Gecode::PropCond PC_INT_BND
Propagate when minimum or maximum of a view changes.
Definition: var-type.hpp:91
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: lex.hpp:399
unsigned int size(I &i)
Size of all ranges of range iterator i.
Less or equal propagator.
Definition: rel.hh:465
static ExecStatus post(Home home, View x0, View x1)
Post propagator .
Definition: lq-le.hpp:95
View arrays.
Definition: array.hpp:234
#define GECODE_ME_CHECK(me)
Check whether modification event me is failed, and forward failure.
Definition: macros.hpp:45
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: lex.hpp:84
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:75
virtual PropCost cost(const Space &home, const ModEventDelta &med) const
Cost function.
Definition: lex.hpp:278
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:253
virtual PropCost cost(const Space &home, const ModEventDelta &med) const
Cost function (defined as low linear)
Definition: lex.hpp:68
Lexical ordering propagator.
Definition: rel.hh:597
virtual size_t dispose(Space &home)
Delete actor and return its size.
Definition: core.hpp:2877
Propagation cost.
Definition: core.hpp:537
ExecStatus
Definition: core.hpp:523
bool assigned(View x, int v)
Whether x is assigned to value v.
Definition: single.hpp:47
#define forceinline
Definition: config.hpp:132
virtual size_t dispose(Space &home)
Delete propagator and return its size.
Definition: lex.hpp:357
Binary disequality propagator.
Definition: rel.hh:432
Execution is okay.
Definition: core.hpp:527
RelTest rtest_eq_bnd(View x, View y)
Test whether views x and y are equal (use bounds information)
Definition: rel-test.hpp:47
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:1215
ViewArray< View > x
Views not yet subscribed to.
Definition: rel.hh:633
Gecode toplevel namespace
static ExecStatus post(Home home, View x0, View x1)
Post propagator .
Definition: nq.hpp:53
Less propagator.
Definition: rel.hh:490
int ModEventDelta
Modification event deltas.
Definition: core.hpp:173
Home class for posting propagators
Definition: core.hpp:717
static PropCost binary(PropCost::Mod m)
Two variables for modifier pcm.
Definition: core.hpp:4054
#define GECODE_NEVER
Assert that this command is never executed.
Definition: macros.hpp:60
Relation does hold.
Definition: view.hpp:1617
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: lex.hpp:62
const Gecode::PropCond PC_INT_VAL
Propagate when a view becomes assigned (single value)
Definition: var-type.hpp:82