Generated on Tue Feb 11 2025 17:33:26 for Gecode by doxygen 1.12.0
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
34namespace 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>
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>
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>
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:
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:
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:
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>
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
int p
Number of positive literals for node type.
int n
Number of negative literals for node type.
Base-class for both propagators and branchers.
Definition core.hpp:628
virtual size_t dispose(Space &home)
Delete actor and return its size.
Definition core.hpp:3252
Home class for posting propagators
Definition core.hpp:856
Less propagator.
Definition rel.hh:517
static ExecStatus post(Home home, V0 x0, V1 x1)
Post propagator .
Definition lq-le.hpp:91
Lexical ordering propagator.
Definition rel.hh:623
virtual size_t dispose(Space &home)
Delete propagator and return its size.
Definition lex.hpp:77
ViewArray< VY > y
Definition rel.hh:627
ViewArray< VX > x
View arrays.
Definition rel.hh:626
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
virtual PropCost cost(const Space &home, const ModEventDelta &med) const
Cost function (defined as low linear)
Definition lex.hpp:64
LexLqLe(Space &home, LexLqLe< VX, VY > &p)
Constructor for cloning p.
Definition lex.hpp:50
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition lex.hpp:87
virtual Actor * copy(Space &home)
Copy propagator during cloning.
Definition lex.hpp:58
virtual void reschedule(Space &home)
Schedule function.
Definition lex.hpp:70
Lexical disequality propagator.
Definition rel.hh:657
VY y0
View currently subscribed to.
Definition rel.hh:662
ExecStatus resubscribe(Space &home, RelTest rt, VX &x0, VY &y0, VX x1, VY y1)
Update subscription.
Definition lex.hpp:376
virtual size_t dispose(Space &home)
Delete propagator and return its size.
Definition lex.hpp:367
VX x0
View currently subscribed to.
Definition rel.hh:660
virtual Actor * copy(Space &home)
Copy propagator during cloning.
Definition lex.hpp:305
virtual void reschedule(Space &home)
Schedule function.
Definition lex.hpp:287
VX x1
View currently subscribed to.
Definition rel.hh:664
ViewArray< VX > x
Views not yet subscribed to.
Definition rel.hh:668
LexNq(Home home, ViewArray< VX > &x, ViewArray< VY > &y)
Constructor for posting.
Definition lex.hpp:266
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition lex.hpp:409
virtual PropCost cost(const Space &home, const ModEventDelta &med) const
Cost function.
Definition lex.hpp:281
VY y1
View currently subscribed to.
Definition rel.hh:666
static ExecStatus post(Home home, ViewArray< VX > &x, ViewArray< VY > &y)
Post propagator .
Definition lex.hpp:332
ViewArray< VY > y
Views not yet subscribed to.
Definition rel.hh:670
Less or equal propagator.
Definition rel.hh:493
static ExecStatus post(Home home, V0 x0, V1 x1)
Post propagator .
Definition lq-le.hpp:50
Binary disequality propagator.
Definition rel.hh:460
static ExecStatus post(Home home, V0 x0, V1 x1)
Post propagator .
Definition nq.hpp:49
Propagation cost.
Definition core.hpp:486
static PropCost linear(PropCost::Mod m, unsigned int n)
Linear complexity for modifier pcm and size measure n.
Definition core.hpp:4796
static PropCost binary(PropCost::Mod m)
Two variables for modifier pcm.
Definition core.hpp:4809
@ HI
Expensive.
Definition core.hpp:514
Base-class for propagators.
Definition core.hpp:1064
Computation spaces.
Definition core.hpp:1742
View arrays.
Definition array.hpp:253
void update(Space &home, ViewArray< View > &a)
Update array to be a clone of array a.
Definition array.hpp:1328
void subscribe(Space &home, Propagator &p, PropCond pc, bool schedule=true)
Subscribe propagator p with propagation condition pc to variable.
Definition array.hpp:1341
int size(void) const
Return size of array (number of elements)
Definition array.hpp:1156
ExecStatus ES_SUBSUMED(Propagator &p)
Definition core.hpp:3563
int ModEventDelta
Modification event deltas.
Definition core.hpp:89
bool failed(void) const
Check whether space is failed.
Definition core.hpp:4044
#define GECODE_ME_CHECK(me)
Check whether modification event me is failed, and forward failure.
Definition macros.hpp:52
#define GECODE_REWRITE(prop, post)
Rewrite propagator by executing post function.
Definition macros.hpp:116
#define GECODE_ES_CHECK(es)
Check whether execution status es is failed or subsumed, and forward failure or subsumption.
Definition macros.hpp:91
const Gecode::PropCond PC_INT_VAL
Propagate when a view becomes assigned (single value)
Definition var-type.hpp:82
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
const Gecode::PropCond PC_INT_BND
Propagate when minimum or maximum of a view changes.
Definition var-type.hpp:91
RelTest rtest_eq_bnd(VX x, VY y)
Test whether views x and y are equal (use bounds information)
Definition rel-test.hpp:43
RelTest
Result of testing relation.
Definition view.hpp:1734
@ RT_TRUE
Relation does hold.
Definition view.hpp:1737
@ RT_MAYBE
Relation may hold or not.
Definition view.hpp:1736
@ RT_FALSE
Relation does not hold.
Definition view.hpp:1735
Gecode toplevel namespace
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Post propagator for SetVar SetOpType SetVar y
Definition set.hh:767
ExecStatus
Definition core.hpp:472
@ ES_OK
Execution is okay.
Definition core.hpp:476
@ ES_FIX
Propagation has computed fixpoint.
Definition core.hpp:477
@ ES_FAILED
Execution has resulted in failure.
Definition core.hpp:474
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Post propagator for SetVar x
Definition set.hh:767
#define forceinline
Definition config.hpp:187
#define GECODE_NEVER
Assert that this command is never executed.
Definition macros.hpp:56