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