Generated on Fri Jul 13 2018 06:08:28 for Gecode by doxygen 1.8.14
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: 2016-11-08 17:23:24 +0100 (Tue, 08 Nov 2016) $ by $Author: schulte $
11  * $Revision: 15253 $
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 VX, class VY>
44  inline
46  ViewArray<VX>& x0, ViewArray<VY>& 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 VX, class VY>
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 VX, class VY>
61  Actor*
62  LexLqLe<VX,VY>::copy(Space& home, bool share) {
63  return new (home) LexLqLe<VX,VY>(home,share,*this);
64  }
65 
66  template<class VX, class VY>
67  PropCost
68  LexLqLe<VX,VY>::cost(const Space&, const ModEventDelta&) const {
69  return PropCost::linear(PropCost::LO, x.size());
70  }
71 
72  template<class VX, class VY>
73  void
75  x.reschedule(home,*this,PC_INT_BND);
76  y.reschedule(home,*this,PC_INT_BND);
77  }
78 
79  template<class VX, class VY>
80  forceinline size_t
82  assert(!home.failed());
83  x.cancel(home,*this,PC_INT_BND);
84  y.cancel(home,*this,PC_INT_BND);
85  (void) Propagator::dispose(home);
86  return sizeof(*this);
87  }
88 
89  template<class VX, class VY>
92  /*
93  * State 1
94  *
95  */
96  {
97  int i = 0;
98  int n = x.size();
99 
100  while ((i < n) && (x[i].min() == y[i].max())) {
101  // case: =, >=
102  GECODE_ME_CHECK(x[i].lq(home,y[i].max()));
103  GECODE_ME_CHECK(y[i].gq(home,x[i].min()));
104  i++;
105  }
106 
107  if (i == n) // case: $
108  return strict ? ES_FAILED : home.ES_SUBSUMED(*this);
109 
110  // Possible cases left: <, <=, > (yields failure), ?
111  GECODE_ME_CHECK(x[i].lq(home,y[i].max()));
112  GECODE_ME_CHECK(y[i].gq(home,x[i].min()));
113 
114  if (x[i].max() < y[i].min()) // case: < (after tell)
115  return home.ES_SUBSUMED(*this);
116 
117  // x[i] can never be equal to y[i] (otherwise: >=)
118  assert(!(x[i].assigned() && y[i].assigned() &&
119  x[i].val() == y[i].val()));
120  // Remove all elements between 0...i-1 as they are assigned and equal
121  x.drop_fst(i); y.drop_fst(i);
122  // After this, execution continues at [1]
123  }
124 
125  /*
126  * State 2
127  * prefix: (?|<=)
128  *
129  */
130  {
131  int i = 1;
132  int n = x.size();
133 
134  while ((i < n) &&
135  (x[i].min() == y[i].max()) &&
136  (x[i].max() == y[i].min())) { // case: =
137  assert(x[i].assigned() && y[i].assigned() &&
138  (x[i].val() == y[i].val()));
139  i++;
140  }
141 
142  if (i == n) { // case: $
143  if (strict)
144  goto rewrite_le;
145  else
146  goto rewrite_lq;
147  }
148 
149  if (x[i].max() < y[i].min()) // case: <
150  goto rewrite_lq;
151 
152  if (x[i].min() > y[i].max()) // case: >
153  goto rewrite_le;
154 
155  if (i > 1) {
156  // Remove equal elements [1...i-1], keep element [0]
157  x[i-1]=x[0]; x.drop_fst(i-1);
158  y[i-1]=y[0]; y.drop_fst(i-1);
159  }
160  }
161 
162  if (x[1].max() <= y[1].min()) {
163  // case: <= (invariant: not =, <)
164  /*
165  * State 3
166  * prefix: (?|<=),<=
167  *
168  */
169  int i = 2;
170  int n = x.size();
171 
172  while ((i < n) && (x[i].max() == y[i].min())) // case: <=, =
173  i++;
174 
175  if (i == n) { // case: $
176  if (strict)
177  return ES_FIX;
178  else
179  goto rewrite_lq;
180  }
181 
182  if (x[i].max() < y[i].min()) // case: <
183  goto rewrite_lq;
184 
185  if (x[i].min() > y[i].max()) { // case: >
186  // Eliminate [i]...[n-1]
187  for (int j=i; j<n; j++) {
188  x[j].cancel(home,*this,PC_INT_BND);
189  y[j].cancel(home,*this,PC_INT_BND);
190  }
191  x.size(i); y.size(i);
192  strict = true;
193  }
194 
195  return ES_FIX;
196  }
197 
198  if (x[1].min() >= y[1].max()) {
199  // case: >= (invariant: not =, >)
200  /*
201  * State 4
202  * prefix: (?|<=) >=
203  *
204  */
205  int i = 2;
206  int n = x.size();
207 
208  while ((i < n) && (x[i].min() == y[i].max()))
209  // case: >=, =
210  i++;
211 
212  if (i == n) { // case: $
213  if (strict)
214  goto rewrite_le;
215  else
216  return ES_FIX;
217  }
218 
219  if (x[i].min() > y[i].max()) // case: >
220  goto rewrite_le;
221 
222  if (x[i].max() < y[i].min()) { // case: <
223  // Eliminate [i]...[n-1]
224  for (int j=i; j<n; j++) {
225  x[j].cancel(home,*this,PC_INT_BND);
226  y[j].cancel(home,*this,PC_INT_BND);
227  }
228  x.size(i); y.size(i);
229  strict = false;
230  }
231 
232  return ES_FIX;
233  }
234 
235  return ES_FIX;
236 
237  rewrite_le:
238  GECODE_REWRITE(*this,(Le<VX,VY>::post(home(*this),x[0],y[0])));
239  rewrite_lq:
240  GECODE_REWRITE(*this,(Lq<VX,VY>::post(home(*this),x[0],y[0])));
241  }
242 
243  template<class VX, class VY>
244  ExecStatus
246  ViewArray<VX>& x, ViewArray<VY>& y, bool strict) {
247  if (x.size() < y.size()) {
248  y.size(x.size()); strict=false;
249  } else if (x.size() > y.size()) {
250  x.size(y.size()); strict=true;
251  }
252  if (x.size() == 0)
253  return strict ? ES_FAILED : ES_OK;
254  if (x.size() == 1) {
255  if (strict)
256  return Le<VX,VY>::post(home,x[0],y[0]);
257  else
258  return Lq<VX,VY>::post(home,x[0],y[0]);
259  }
260  (void) new (home) LexLqLe<VX,VY>(home,x,y,strict);
261  return ES_OK;
262  }
263 
264 
265  /*
266  * Lexical disequality propagator
267  */
268  template<class VX, class VY>
271  : Propagator(home),
272  x0(xv[xv.size()-2]), y0(yv[xv.size()-2]),
273  x1(xv[xv.size()-1]), y1(yv[xv.size()-1]),
274  x(xv), y(yv) {
275  int n = x.size();
276  assert(n > 1);
277  assert(n == y.size());
278  x.size(n-2); y.size(n-2);
279  x0.subscribe(home,*this,PC_INT_VAL); y0.subscribe(home,*this,PC_INT_VAL);
280  x1.subscribe(home,*this,PC_INT_VAL); y1.subscribe(home,*this,PC_INT_VAL);
281  }
282 
283  template<class VX, class VY>
284  PropCost
285  LexNq<VX,VY>::cost(const Space&, const ModEventDelta&) const {
287  }
288 
289  template<class VX, class VY>
290  void
292  x0.reschedule(home,*this,PC_INT_VAL);
293  y0.reschedule(home,*this,PC_INT_VAL);
294  x1.reschedule(home,*this,PC_INT_VAL);
295  y1.reschedule(home,*this,PC_INT_VAL);
296  }
297 
298  template<class VX, class VY>
301  : Propagator(home,share,p) {
302  x0.update(home,share,p.x0); y0.update(home,share,p.y0);
303  x1.update(home,share,p.x1); y1.update(home,share,p.y1);
304  x.update(home,share,p.x); y.update(home,share,p.y);
305  }
306 
307  template<class VX, class VY>
308  Actor*
309  LexNq<VX,VY>::copy(Space& home, bool share) {
310  int n = x.size();
311  if (n > 0) {
312  // Eliminate all equal views and keep one disequal pair
313  for (int i=n; i--; )
314  switch (rtest_eq_bnd(x[i],y[i])) {
315  case RT_TRUE:
316  // Eliminate equal pair
317  n--; x[i]=x[n]; y[i]=y[n];
318  break;
319  case RT_FALSE:
320  // Just keep a single disequal pair
321  n=1; x[0]=x[i]; y[0]=y[i];
322  goto done;
323  case RT_MAYBE:
324  break;
325  default:
326  GECODE_NEVER;
327  }
328  done:
329  x.size(n); y.size(n);
330  }
331  return new (home) LexNq<VX,VY>(home,share,*this);
332  }
333 
334  template<class VX, class VY>
335  inline ExecStatus
337  if (x.size() != y.size())
338  return ES_OK;
339  int n = x.size();
340  if (n > 0) {
341  // Eliminate all equal views
342  for (int i=n; i--; )
343  switch (rtest_eq_dom(x[i],y[i])) {
344  case RT_TRUE:
345  // Eliminate equal pair
346  n--; x[i]=x[n]; y[i]=y[n];
347  break;
348  case RT_FALSE:
349  return ES_OK;
350  case RT_MAYBE:
351  if (same(x[i],y[i])) {
352  // Eliminate equal pair
353  n--; x[i]=x[n]; y[i]=y[n];
354  }
355  break;
356  default:
357  GECODE_NEVER;
358  }
359  x.size(n); y.size(n);
360  }
361  if (n == 0)
362  return ES_FAILED;
363  if (n == 1)
364  return Nq<VX,VY>::post(home,x[0],y[0]);
365  (void) new (home) LexNq<VX,VY>(home,x,y);
366  return ES_OK;
367  }
368 
369  template<class VX, class VY>
370  forceinline size_t
372  x0.cancel(home,*this,PC_INT_VAL); y0.cancel(home,*this,PC_INT_VAL);
373  x1.cancel(home,*this,PC_INT_VAL); y1.cancel(home,*this,PC_INT_VAL);
374  (void) Propagator::dispose(home);
375  return sizeof(*this);
376  }
377 
378  template<class VX, class VY>
381  RelTest rt, VX& x0, VY& y0, VX x1, VY y1) {
382  if (rt == RT_TRUE) {
383  assert(x0.assigned() && y0.assigned());
384  assert(x0.val() == y0.val());
385  int n = x.size();
386  for (int i=n; i--; )
387  switch (rtest_eq_dom(x[i],y[i])) {
388  case RT_TRUE:
389  // Eliminate equal pair
390  n--; x[i]=x[n]; y[i]=y[n];
391  break;
392  case RT_FALSE:
393  return home.ES_SUBSUMED(*this);
394  case RT_MAYBE:
395  // Move to x0, y0 and subscribe
396  x0=x[i]; y0=y[i];
397  n--; x[i]=x[n]; y[i]=y[n];
398  x.size(n); y.size(n);
399  x0.subscribe(home,*this,PC_INT_VAL,false);
400  y0.subscribe(home,*this,PC_INT_VAL,false);
401  return ES_FIX;
402  default:
403  GECODE_NEVER;
404  }
405  // No more views to subscribe to left
406  GECODE_REWRITE(*this,(Nq<VX,VY>::post(home(*this),x1,y1)));
407  }
408  return ES_FIX;
409  }
410 
411  template<class VX, class VY>
412  ExecStatus
414  RelTest rt0 = rtest_eq_dom(x0,y0);
415  if (rt0 == RT_FALSE)
416  return home.ES_SUBSUMED(*this);
417  RelTest rt1 = rtest_eq_dom(x1,y1);
418  if (rt1 == RT_FALSE)
419  return home.ES_SUBSUMED(*this);
420  GECODE_ES_CHECK(resubscribe(home,rt0,x0,y0,x1,y1));
421  GECODE_ES_CHECK(resubscribe(home,rt1,x1,y1,x0,y0));
422  return ES_FIX;
423  }
424 
425 
426 }}}
427 
428 // STATISTICS: int-prop
VX x1
View currently subscribed to.
Definition: rel.hh:672
#define GECODE_REWRITE(prop, post)
Rewrite propagator by executing post function.
Definition: macros.hpp:120
void update(Space &, bool share, ViewArray< View > &a)
Update array to be a clone of array a.
Definition: array.hpp:1387
Relation may hold or not.
Definition: view.hpp:1616
static ExecStatus post(Home home, V0 x0, V1 x1)
Post propagator .
Definition: nq.hpp:53
VX x0
View currently subscribed to.
Definition: rel.hh:668
ViewArray< VY > y
Definition: rel.hh:635
static PropCost linear(PropCost::Mod m, unsigned int n)
Linear complexity for modifier pcm and size measure n.
Definition: core.hpp:4841
ExecStatus ES_SUBSUMED(Propagator &p)
Definition: core.hpp:3614
virtual size_t dispose(Space &home)
Delete propagator and return its size.
Definition: lex.hpp:81
RelTest rtest_eq_dom(VX x, VY y)
Test whether views x and y are equal (use full domain information)
Definition: rel-test.hpp:69
static ExecStatus post(Home home, V0 x0, V1 x1)
Post propagator .
Definition: lq-le.hpp:73
ExecStatus resubscribe(Space &home, Propagator &p, VX &x0, ViewArray< VX > &x, VY &x1, ViewArray< VY > &y)
Definition: clause.hpp:142
ViewArray< VX > x
Views not yet subscribed to.
Definition: rel.hh:676
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:53
LexLqLe(Space &home, bool share, LexLqLe< VX, VY > &p)
Constructor for cloning p.
Definition: lex.hpp:54
virtual PropCost cost(const Space &home, const ModEventDelta &med) const
Cost function.
Definition: lex.hpp:285
VY y1
View currently subscribed to.
Definition: rel.hh:674
virtual PropCost cost(const Space &home, const ModEventDelta &med) const
Cost function (defined as low linear)
Definition: lex.hpp:68
Base-class for propagators.
Definition: core.hpp:1092
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: lex.hpp:309
Lexical disequality propagator.
Definition: rel.hh:665
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: lex.hpp:413
void subscribe(Space &home, Propagator &p, PropCond pc, bool schedule=true)
Subscribe propagator p with propagation condition pc to variable.
Definition: array.hpp:1400
Propagation has computed fixpoint.
Definition: core.hpp:545
Computation spaces.
Definition: core.hpp:1748
Base-class for both propagators and branchers.
Definition: core.hpp:696
#define GECODE_ES_CHECK(es)
Check whether execution status es is failed or subsumed, and forward failure or subsumption.
Definition: macros.hpp:95
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
static ExecStatus post(Home home, ViewArray< VX > &x, ViewArray< VY > &y)
Post propagator .
Definition: lex.hpp:336
Gecode::IntArgs i(4, 1, 2, 3, 4)
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
Execution has resulted in failure.
Definition: core.hpp:542
Relation does not hold.
Definition: view.hpp:1615
RelTest
Result of testing relation.
Definition: view.hpp:1614
const Gecode::PropCond PC_INT_BND
Propagate when minimum or maximum of a view changes.
Definition: var-type.hpp:91
virtual void reschedule(Space &home)
Schedule function.
Definition: lex.hpp:74
bool failed(void) const
Check whether space is failed.
Definition: core.hpp:4095
unsigned int size(I &i)
Size of all ranges of range iterator i.
Less or equal propagator.
Definition: rel.hh:497
virtual size_t dispose(Space &home)
Delete propagator and return its size.
Definition: lex.hpp:371
Expensive.
Definition: core.hpp:582
#define GECODE_ME_CHECK(me)
Check whether modification event me is failed, and forward failure.
Definition: macros.hpp:56
ViewArray< VY > y
Views not yet subscribed to.
Definition: rel.hh:678
LexNq(Home home, ViewArray< VX > &x, ViewArray< VY > &y)
Constructor for posting.
Definition: lex.hpp:270
ExecStatus resubscribe(Space &home, RelTest rt, VX &x0, VY &y0, VX x1, VY y1)
Update subscription.
Definition: lex.hpp:380
RelTest rtest_eq_bnd(VX x, VY y)
Test whether views x and y are equal (use bounds information)
Definition: rel-test.hpp:47
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:71
Post propagator for SetVar SetOpType SetVar y
Definition: set.hh:784
static ExecStatus post(Home home, ViewArray< VX > &x, ViewArray< VY > &y, bool strict)
Post propagator for lexical order between x and y.
Definition: lex.hpp:245
virtual void reschedule(Space &home)
Schedule function.
Definition: lex.hpp:291
Lexical ordering propagator.
Definition: rel.hh:631
static ExecStatus post(Home home, V0 x0, V1 x1)
Post propagator .
Definition: lq-le.hpp:139
virtual size_t dispose(Space &home)
Delete actor and return its size.
Definition: core.hpp:3354
Propagation cost.
Definition: core.hpp:554
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
virtual Actor * copy(Space &home, bool share)
Copy propagator during cloning.
Definition: lex.hpp:62
Binary disequality propagator.
Definition: rel.hh:464
Post propagator for SetVar x
Definition: set.hh:784
Execution is okay.
Definition: core.hpp:544
ViewArray< VX > x
View arrays.
Definition: rel.hh:634
Gecode toplevel namespace
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: lex.hpp:91
Less propagator.
Definition: rel.hh:523
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:1215
int ModEventDelta
Modification event deltas.
Definition: core.hpp:169
Home class for posting propagators
Definition: core.hpp:922
static PropCost binary(PropCost::Mod m)
Two variables for modifier pcm.
Definition: core.hpp:4854
VY y0
View currently subscribed to.
Definition: rel.hh:670
#define GECODE_NEVER
Assert that this command is never executed.
Definition: macros.hpp:60
Relation does hold.
Definition: view.hpp:1617
const Gecode::PropCond PC_INT_VAL
Propagate when a view becomes assigned (single value)
Definition: var-type.hpp:82