this repo has no description
dekker.one
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#include <gecode/int/linear/int-noview.hpp>
35
36namespace Gecode { namespace Int { namespace Linear {
37
38 /**
39 * \brief Test if only unit-coefficient arrays used
40 *
41 */
42 template<class P, class N>
43 forceinline bool
44 isunit(ViewArray<P>&, ViewArray<N>&) { return false; }
45 template<>
46 forceinline bool
47 isunit(ViewArray<IntView>&, ViewArray<IntView>&) { return true; }
48 template<>
49 forceinline bool
50 isunit(ViewArray<IntView>&, ViewArray<NoView>&) { return true; }
51 template<>
52 forceinline bool
53 isunit(ViewArray<NoView>&, ViewArray<IntView>&) { return true; }
54
55 /*
56 * Linear propagators
57 *
58 */
59 template<class Val, class P, class N, PropCond pc>
60 forceinline
61 Lin<Val,P,N,pc>::Lin(Home home, ViewArray<P>& x0, ViewArray<N>& y0, Val c0)
62 : Propagator(home), x(x0), y(y0), c(c0) {
63 x.subscribe(home,*this,pc);
64 y.subscribe(home,*this,pc);
65 }
66
67 template<class Val, class P, class N, PropCond pc>
68 forceinline
69 Lin<Val,P,N,pc>::Lin(Space& home, Lin<Val,P,N,pc>& p)
70 : Propagator(home,p), c(p.c) {
71 x.update(home,p.x);
72 y.update(home,p.y);
73 }
74
75 template<class Val, class P, class N, PropCond pc>
76 PropCost
77 Lin<Val,P,N,pc>::cost(const Space&, const ModEventDelta&) const {
78 return PropCost::linear(PropCost::LO, x.size()+y.size());
79 }
80
81 template<class Val, class P, class N, PropCond pc>
82 void
83 Lin<Val,P,N,pc>::reschedule(Space& home) {
84 x.reschedule(home,*this,pc);
85 y.reschedule(home,*this,pc);
86 }
87
88 template<class Val, class P, class N, PropCond pc>
89 forceinline size_t
90 Lin<Val,P,N,pc>::dispose(Space& home) {
91 x.cancel(home,*this,pc);
92 y.cancel(home,*this,pc);
93 (void) Propagator::dispose(home);
94 return sizeof(*this);
95 }
96
97 /*
98 * Reified linear propagators
99 *
100 */
101 template<class Val, class P, class N, PropCond pc, class Ctrl>
102 forceinline
103 ReLin<Val,P,N,pc,Ctrl>::ReLin
104 (Home home, ViewArray<P>& x, ViewArray<N>& y, Val c, Ctrl b0)
105 : Lin<Val,P,N,pc>(home,x,y,c), b(b0) {
106 b.subscribe(home,*this,PC_INT_VAL);
107 }
108
109 template<class Val, class P, class N, PropCond pc, class Ctrl>
110 forceinline
111 ReLin<Val,P,N,pc,Ctrl>::ReLin
112 (Space& home, ReLin<Val,P,N,pc,Ctrl>& p)
113 : Lin<Val,P,N,pc>(home,p) {
114 b.update(home,p.b);
115 }
116
117 template<class Val, class P, class N, PropCond pc, class Ctrl>
118 void
119 ReLin<Val,P,N,pc,Ctrl>::reschedule(Space& home) {
120 x.reschedule(home,*this,pc);
121 y.reschedule(home,*this,pc);
122 b.reschedule(home,*this,PC_INT_VAL);
123 }
124
125 template<class Val, class P, class N, PropCond pc, class Ctrl>
126 forceinline size_t
127 ReLin<Val,P,N,pc,Ctrl>::dispose(Space& home) {
128 b.cancel(home,*this,PC_BOOL_VAL);
129 (void) Lin<Val,P,N,pc>::dispose(home);
130 return sizeof(*this);
131 }
132
133 /*
134 * Computing bounds
135 *
136 */
137
138 template<class Val, class View>
139 void
140 bounds_p(ModEventDelta med, ViewArray<View>& x, Val& c, Val& sl, Val& su) {
141 int n = x.size();
142 if (IntView::me(med) == ME_INT_VAL) {
143 for (int i=n; i--; ) {
144 Val m = x[i].min();
145 if (x[i].assigned()) {
146 c -= m; x[i] = x[--n];
147 } else {
148 sl -= m; su -= x[i].max();
149 }
150 }
151 x.size(n);
152 } else {
153 for (int i=0; i<n; i++) {
154 sl -= x[i].min(); su -= x[i].max();
155 }
156 }
157 }
158
159 template<class Val, class View>
160 void
161 bounds_n(ModEventDelta med, ViewArray<View>& y, Val& c, Val& sl, Val& su) {
162 int n = y.size();
163 if (IntView::me(med) == ME_INT_VAL) {
164 for (int i=n; i--; ) {
165 Val m = y[i].max();
166 if (y[i].assigned()) {
167 c += m; y[i] = y[--n];
168 } else {
169 sl += m; su += y[i].min();
170 }
171 }
172 y.size(n);
173 } else {
174 for (int i=0; i<n; i++) {
175 sl += y[i].max(); su += y[i].min();
176 }
177 }
178 }
179
180
181 template<class Val, class P, class N>
182 ExecStatus
183 prop_bnd(Space& home, ModEventDelta med, Propagator& p,
184 ViewArray<P>& x, ViewArray<N>& y, Val& c) {
185 // Eliminate singletons
186 Val sl = 0;
187 Val su = 0;
188
189 bounds_p<Val,P>(med, x, c, sl, su);
190 bounds_n<Val,N>(med, y, c, sl, su);
191
192 if ((IntView::me(med) == ME_INT_VAL) && ((x.size() + y.size()) <= 1)) {
193 if (x.size() == 1) {
194 GECODE_ME_CHECK(x[0].eq(home,c));
195 return home.ES_SUBSUMED(p);
196 }
197 if (y.size() == 1) {
198 GECODE_ME_CHECK(y[0].eq(home,-c));
199 return home.ES_SUBSUMED(p);
200 }
201 return (c == static_cast<Val>(0)) ?
202 home.ES_SUBSUMED(p) : ES_FAILED;
203 }
204
205 sl += c; su += c;
206
207 const int mod_sl = 1;
208 const int mod_su = 2;
209
210 int mod = mod_sl | mod_su;
211
212 do {
213 if (mod & mod_sl) {
214 mod -= mod_sl;
215 // Propagate upper bound for positive variables
216 for (int i=0; i<x.size(); i++) {
217 const Val xi_max = x[i].max();
218 ModEvent me = x[i].lq(home,sl + x[i].min());
219 if (me_failed(me))
220 return ES_FAILED;
221 if (me_modified(me)) {
222 su += xi_max - x[i].max();
223 mod |= mod_su;
224 }
225 }
226 // Propagate lower bound for negative variables
227 for (int i=0; i<y.size(); i++) {
228 const Val yi_min = y[i].min();
229 ModEvent me = y[i].gq(home,y[i].max() - sl);
230 if (me_failed(me))
231 return ES_FAILED;
232 if (me_modified(me)) {
233 su += y[i].min() - yi_min;
234 mod |= mod_su;
235 }
236 }
237 }
238 if (mod & mod_su) {
239 mod -= mod_su;
240 // Propagate lower bound for positive variables
241 for (int i=0; i<x.size(); i++) {
242 const Val xi_min = x[i].min();
243 ModEvent me = x[i].gq(home,su + x[i].max());
244 if (me_failed(me))
245 return ES_FAILED;
246 if (me_modified(me)) {
247 sl += xi_min - x[i].min();
248 mod |= mod_sl;
249 }
250 }
251 // Propagate upper bound for negative variables
252 for (int i=0; i<y.size(); i++) {
253 const Val yi_max = y[i].max();
254 ModEvent me = y[i].lq(home,y[i].min() - su);
255 if (me_failed(me))
256 return ES_FAILED;
257 if (me_modified(me)) {
258 sl += y[i].max() - yi_max;
259 mod |= mod_sl;
260 }
261 }
262 }
263 } while (mod);
264
265 return (sl == su) ? home.ES_SUBSUMED(p) : ES_FIX;
266 }
267
268 /*
269 * Bound consistent linear equation
270 *
271 */
272
273 template<class Val, class P, class N>
274 forceinline
275 Eq<Val,P,N>::Eq(Home home, ViewArray<P>& x, ViewArray<N>& y, Val c)
276 : Lin<Val,P,N,PC_INT_BND>(home,x,y,c) {}
277
278 template<class Val, class P, class N>
279 ExecStatus
280 Eq<Val,P,N>::post(Home home, ViewArray<P>& x, ViewArray<N>& y, Val c) {
281 ViewArray<NoView> nva;
282 if (y.size() == 0) {
283 (void) new (home) Eq<Val,P,NoView>(home,x,nva,c);
284 } else if (x.size() == 0) {
285 (void) new (home) Eq<Val,N,NoView>(home,y,nva,-c);
286 } else {
287 (void) new (home) Eq<Val,P,N>(home,x,y,c);
288 }
289 return ES_OK;
290 }
291
292
293 template<class Val, class P, class N>
294 forceinline
295 Eq<Val,P,N>::Eq(Space& home, Eq<Val,P,N>& p)
296 : Lin<Val,P,N,PC_INT_BND>(home,p) {}
297
298 /**
299 * \brief Rewriting of equality to binary propagators
300 *
301 */
302 template<class Val, class P, class N>
303 forceinline Actor*
304 eqtobin(Space&, Propagator&, ViewArray<P>&, ViewArray<N>&, Val) {
305 return nullptr;
306 }
307 template<class Val>
308 forceinline Actor*
309 eqtobin(Space& home, Propagator& p,
310 ViewArray<IntView>& x, ViewArray<NoView>&, Val c) {
311 assert(x.size() == 2);
312 return new (home) EqBin<Val,IntView,IntView>
313 (home,p,x[0],x[1],c);
314 }
315 template<class Val>
316 forceinline Actor*
317 eqtobin(Space& home, Propagator& p,
318 ViewArray<NoView>&, ViewArray<IntView>& y, Val c) {
319 assert(y.size() == 2);
320 return new (home) EqBin<Val,IntView,IntView>
321 (home,p,y[0],y[1],-c);
322 }
323 template<class Val>
324 forceinline Actor*
325 eqtobin(Space& home, Propagator& p,
326 ViewArray<IntView>& x, ViewArray<IntView>& y, Val c) {
327 if (x.size() == 2)
328 return new (home) EqBin<Val,IntView,IntView>
329 (home,p,x[0],x[1],c);
330 if (x.size() == 1)
331 return new (home) EqBin<Val,IntView,MinusView>
332 (home,p,x[0],MinusView(y[0]),c);
333 return new (home) EqBin<Val,IntView,IntView>
334 (home,p,y[0],y[1],-c);
335 }
336
337 /**
338 * \brief Rewriting of equality to ternary propagators
339 *
340 */
341 template<class Val, class P, class N>
342 forceinline Actor*
343 eqtoter(Space&, Propagator&, ViewArray<P>&, ViewArray<N>&, Val) {
344 return nullptr;
345 }
346 template<class Val>
347 forceinline Actor*
348 eqtoter(Space& home, Propagator& p,
349 ViewArray<IntView>& x, ViewArray<NoView>&, Val c) {
350 assert(x.size() == 3);
351 return new (home) EqTer<Val,IntView,IntView,IntView>
352 (home,p,x[0],x[1],x[2],c);
353 }
354 template<class Val>
355 forceinline Actor*
356 eqtoter(Space& home, Propagator& p,
357 ViewArray<NoView>&, ViewArray<IntView>& y, Val c) {
358 assert(y.size() == 3);
359 return new (home) EqTer<Val,IntView,IntView,IntView>
360 (home,p,y[0],y[1],y[2],-c);
361 }
362 template<class Val>
363 forceinline Actor*
364 eqtoter(Space& home, Propagator& p,
365 ViewArray<IntView>& x, ViewArray<IntView>& y, Val c) {
366 if (x.size() == 3)
367 return new (home) EqTer<Val,IntView,IntView,IntView>
368 (home,p,x[0],x[1],x[2],c);
369 if (x.size() == 2)
370 return new (home) EqTer<Val,IntView,IntView,MinusView>
371 (home,p,x[0],x[1],MinusView(y[0]),c);
372 if (x.size() == 1)
373 return new (home) EqTer<Val,IntView,IntView,MinusView>
374 (home,p,y[0],y[1],MinusView(x[0]),-c);
375 return new (home) EqTer<Val,IntView,IntView,IntView>
376 (home,p,y[0],y[1],y[2],-c);
377 }
378
379 template<class Val, class P, class N>
380 Actor*
381 Eq<Val,P,N>::copy(Space& home) {
382 if (isunit(x,y)) {
383 // Check whether rewriting is possible
384 if (x.size() + y.size() == 2)
385 return eqtobin(home,*this,x,y,c);
386 if (x.size() + y.size() == 3)
387 return eqtoter(home,*this,x,y,c);
388 }
389 return new (home) Eq<Val,P,N>(home,*this);
390 }
391
392 template<class Val, class P, class N>
393 ExecStatus
394 Eq<Val,P,N>::propagate(Space& home, const ModEventDelta& med) {
395 return prop_bnd<Val,P,N>(home,med,*this,x,y,c);
396 }
397
398 /*
399 * Reified bound consistent linear equation
400 *
401 */
402
403 template<class Val, class P, class N, class Ctrl, ReifyMode rm>
404 forceinline
405 ReEq<Val,P,N,Ctrl,rm>::ReEq(Home home,
406 ViewArray<P>& x, ViewArray<N>& y, Val c, Ctrl b)
407 : ReLin<Val,P,N,PC_INT_BND,Ctrl>(home,x,y,c,b) {}
408
409 template<class Val, class P, class N, class Ctrl, ReifyMode rm>
410 ExecStatus
411 ReEq<Val,P,N,Ctrl,rm>::post(Home home,
412 ViewArray<P>& x, ViewArray<N>& y, Val c, Ctrl b) {
413 ViewArray<NoView> nva;
414 if (y.size() == 0) {
415 (void) new (home) ReEq<Val,P,NoView,Ctrl,rm>(home,x,nva,c,b);
416 } else if (x.size() == 0) {
417 (void) new (home) ReEq<Val,N,NoView,Ctrl,rm>(home,y,nva,-c,b);
418 } else {
419 (void) new (home) ReEq<Val,P,N,Ctrl,rm>(home,x,y,c,b);
420 }
421 return ES_OK;
422 }
423
424
425 template<class Val, class P, class N, class Ctrl, ReifyMode rm>
426 forceinline
427 ReEq<Val,P,N,Ctrl,rm>::ReEq(Space& home, ReEq<Val,P,N,Ctrl,rm>& p)
428 : ReLin<Val,P,N,PC_INT_BND,Ctrl>(home,p) {}
429
430 template<class Val, class P, class N, class Ctrl, ReifyMode rm>
431 Actor*
432 ReEq<Val,P,N,Ctrl,rm>::copy(Space& home) {
433 return new (home) ReEq<Val,P,N,Ctrl,rm>(home,*this);
434 }
435
436 template<class Val, class P, class N, class Ctrl, ReifyMode rm>
437 ExecStatus
438 ReEq<Val,P,N,Ctrl,rm>::propagate(Space& home, const ModEventDelta& med) {
439 if (b.zero()) {
440 if (rm == RM_IMP)
441 return home.ES_SUBSUMED(*this);
442 GECODE_REWRITE(*this,(Nq<Val,P,N>::post(home(*this),x,y,c)));
443 }
444 if (b.one()) {
445 if (rm == RM_PMI)
446 return home.ES_SUBSUMED(*this);
447 GECODE_REWRITE(*this,(Eq<Val,P,N>::post(home(*this),x,y,c)));
448 }
449
450 Val sl = 0;
451 Val su = 0;
452
453 bounds_p<Val,P>(med, x, c, sl, su);
454 bounds_n<Val,N>(med, y, c, sl, su);
455
456 if ((-sl == c) && (-su == c)) {
457 if (rm != RM_IMP)
458 GECODE_ME_CHECK(b.one_none(home));
459 return home.ES_SUBSUMED(*this);
460 }
461 if ((-sl > c) || (-su < c)) {
462 if (rm != RM_PMI)
463 GECODE_ME_CHECK(b.zero_none(home));
464 return home.ES_SUBSUMED(*this);
465 }
466 return ES_FIX;
467 }
468
469
470 /*
471 * Domain consistent linear disequation
472 *
473 */
474
475 template<class Val, class P, class N>
476 forceinline
477 Nq<Val,P,N>::Nq(Home home, ViewArray<P>& x, ViewArray<N>& y, Val c)
478 : Lin<Val,P,N,PC_INT_VAL>(home,x,y,c) {}
479
480 template<class Val, class P, class N>
481 ExecStatus
482 Nq<Val,P,N>::post(Home home, ViewArray<P>& x, ViewArray<N>& y, Val c) {
483 ViewArray<NoView> nva;
484 if (y.size() == 0) {
485 (void) new (home) Nq<Val,P,NoView>(home,x,nva,c);
486 } else if (x.size() == 0) {
487 (void) new (home) Nq<Val,N,NoView>(home,y,nva,-c);
488 } else {
489 (void) new (home) Nq<Val,P,N>(home,x,y,c);
490 }
491 return ES_OK;
492 }
493
494
495 template<class Val, class P, class N>
496 forceinline
497 Nq<Val,P,N>::Nq(Space& home, Nq<Val,P,N>& p)
498 : Lin<Val,P,N,PC_INT_VAL>(home,p) {}
499
500 /**
501 * \brief Rewriting of disequality to binary propagators
502 *
503 */
504 template<class Val, class P, class N>
505 forceinline Actor*
506 nqtobin(Space&, Propagator&, ViewArray<P>&, ViewArray<N>&, Val) {
507 return nullptr;
508 }
509 template<class Val>
510 forceinline Actor*
511 nqtobin(Space& home, Propagator& p,
512 ViewArray<IntView>& x, ViewArray<NoView>&, Val c) {
513 assert(x.size() == 2);
514 return new (home) NqBin<Val,IntView,IntView>
515 (home,p,x[0],x[1],c);
516 }
517 template<class Val>
518 forceinline Actor*
519 nqtobin(Space& home, Propagator& p,
520 ViewArray<NoView>&, ViewArray<IntView>& y, Val c) {
521 assert(y.size() == 2);
522 return new (home) NqBin<Val,IntView,IntView>
523 (home,p,y[0],y[1],-c);
524 }
525 template<class Val>
526 forceinline Actor*
527 nqtobin(Space& home, Propagator& p,
528 ViewArray<IntView>& x, ViewArray<IntView>& y, Val c) {
529 if (x.size() == 2)
530 return new (home) NqBin<Val,IntView,IntView>
531 (home,p,x[0],x[1],c);
532 if (x.size() == 1)
533 return new (home) NqBin<Val,IntView,MinusView>
534 (home,p,x[0],MinusView(y[0]),c);
535 return new (home) NqBin<Val,IntView,IntView>
536 (home,p,y[0],y[1],-c);
537 }
538
539 /**
540 * \brief Rewriting of disequality to ternary propagators
541 *
542 */
543 template<class Val, class P, class N>
544 forceinline Actor*
545 nqtoter(Space&, Propagator&,ViewArray<P>&, ViewArray<N>&, Val) {
546 return nullptr;
547 }
548 template<class Val>
549 forceinline Actor*
550 nqtoter(Space& home, Propagator& p,
551 ViewArray<IntView>& x, ViewArray<NoView>&, Val c) {
552 assert(x.size() == 3);
553 return new (home) NqTer<Val,IntView,IntView,IntView>
554 (home,p,x[0],x[1],x[2],c);
555 }
556 template<class Val>
557 forceinline Actor*
558 nqtoter(Space& home, Propagator& p,
559 ViewArray<NoView>&, ViewArray<IntView>& y, Val c) {
560 assert(y.size() == 3);
561 return new (home) NqTer<Val,IntView,IntView,IntView>
562 (home,p,y[0],y[1],y[2],-c);
563 }
564 template<class Val>
565 forceinline Actor*
566 nqtoter(Space& home, Propagator& p,
567 ViewArray<IntView>& x, ViewArray<IntView>& y, Val c) {
568 if (x.size() == 3)
569 return new (home) NqTer<Val,IntView,IntView,IntView>
570 (home,p,x[0],x[1],x[2],c);
571 if (x.size() == 2)
572 return new (home) NqTer<Val,IntView,IntView,MinusView>
573 (home,p,x[0],x[1],MinusView(y[0]),c);
574 if (x.size() == 1)
575 return new (home) NqTer<Val,IntView,IntView,MinusView>
576 (home,p,y[0],y[1],MinusView(x[0]),-c);
577 return new (home) NqTer<Val,IntView,IntView,IntView>
578 (home,p,y[0],y[1],y[2],-c);
579 }
580
581 template<class Val, class P, class N>
582 Actor*
583 Nq<Val,P,N>::copy(Space& home) {
584 if (isunit(x,y)) {
585 // Check whether rewriting is possible
586 if (x.size() + y.size() == 2)
587 return nqtobin(home,*this,x,y,c);
588 if (x.size() + y.size() == 3)
589 return nqtoter(home,*this,x,y,c);
590 }
591 return new (home) Nq<Val,P,N>(home,*this);
592 }
593
594 template<class Val, class P, class N>
595 ExecStatus
596 Nq<Val,P,N>::propagate(Space& home, const ModEventDelta&) {
597 for (int i=x.size(); i--; )
598 if (x[i].assigned()) {
599 c -= x[i].val(); x.move_lst(i);
600 }
601 for (int i=y.size(); i--; )
602 if (y[i].assigned()) {
603 c += y[i].val(); y.move_lst(i);
604 }
605 if (x.size() + y.size() <= 1) {
606 if (x.size() == 1) {
607 GECODE_ME_CHECK(x[0].nq(home,c)); return home.ES_SUBSUMED(*this);
608 }
609 if (y.size() == 1) {
610 GECODE_ME_CHECK(y[0].nq(home,-c)); return home.ES_SUBSUMED(*this);
611 }
612 return (c == static_cast<Val>(0)) ?
613 ES_FAILED : home.ES_SUBSUMED(*this);
614 }
615 return ES_FIX;
616 }
617
618
619 /*
620 * Bound consistent linear inequation
621 *
622 */
623
624 template<class Val, class P, class N>
625 forceinline
626 Lq<Val,P,N>::Lq(Home home, ViewArray<P>& x, ViewArray<N>& y, Val c)
627 : Lin<Val,P,N,PC_INT_BND>(home,x,y,c) {}
628
629 template<class Val, class P, class N>
630 ExecStatus
631 Lq<Val,P,N>::post(Home home, ViewArray<P>& x, ViewArray<N>& y, Val c) {
632 ViewArray<NoView> nva;
633 if (y.size() == 0) {
634 (void) new (home) Lq<Val,P,NoView>(home,x,nva,c);
635 } else if (x.size() == 0) {
636 (void) new (home) Lq<Val,NoView,N>(home,nva,y,c);
637 } else {
638 (void) new (home) Lq<Val,P,N>(home,x,y,c);
639 }
640 return ES_OK;
641 }
642
643
644 template<class Val, class P, class N>
645 forceinline
646 Lq<Val,P,N>::Lq(Space& home, Lq<Val,P,N>& p)
647 : Lin<Val,P,N,PC_INT_BND>(home,p) {}
648
649 /**
650 * \brief Rewriting of inequality to binary propagators
651 *
652 */
653 template<class Val, class P, class N>
654 forceinline Actor*
655 lqtobin(Space&, Propagator&,ViewArray<P>&, ViewArray<N>&, Val) {
656 return nullptr;
657 }
658 template<class Val>
659 forceinline Actor*
660 lqtobin(Space& home, Propagator& p,
661 ViewArray<IntView>& x, ViewArray<NoView>&, Val c) {
662 assert(x.size() == 2);
663 return new (home) LqBin<Val,IntView,IntView>
664 (home,p,x[0],x[1],c);
665 }
666 template<class Val>
667 forceinline Actor*
668 lqtobin(Space& home, Propagator& p,
669 ViewArray<NoView>&, ViewArray<IntView>& y, Val c) {
670 assert(y.size() == 2);
671 return new (home) LqBin<Val,MinusView,MinusView>
672 (home,p,MinusView(y[0]),MinusView(y[1]),c);
673 }
674 template<class Val>
675 forceinline Actor*
676 lqtobin(Space& home, Propagator& p,
677 ViewArray<IntView>& x, ViewArray<IntView>& y, Val c) {
678 if (x.size() == 2)
679 return new (home) LqBin<Val,IntView,IntView>
680 (home,p,x[0],x[1],c);
681 if (x.size() == 1)
682 return new (home) LqBin<Val,IntView,MinusView>
683 (home,p,x[0],MinusView(y[0]),c);
684 return new (home) LqBin<Val,MinusView,MinusView>
685 (home,p,MinusView(y[0]),MinusView(y[1]),c);
686 }
687
688 /**
689 * \brief Rewriting of inequality to ternary propagators
690 *
691 */
692 template<class Val, class P, class N>
693 forceinline Actor*
694 lqtoter(Space&, Propagator&, ViewArray<P>&, ViewArray<N>&, Val) {
695 return nullptr;
696 }
697 template<class Val>
698 forceinline Actor*
699 lqtoter(Space& home, Propagator& p,
700 ViewArray<IntView>& x, ViewArray<NoView>&, Val c) {
701 assert(x.size() == 3);
702 return new (home) LqTer<Val,IntView,IntView,IntView>
703 (home,p,x[0],x[1],x[2],c);
704 }
705 template<class Val>
706 forceinline Actor*
707 lqtoter(Space& home, Propagator& p,
708 ViewArray<NoView>&, ViewArray<IntView>& y, Val c) {
709 assert(y.size() == 3);
710 return new (home) LqTer<Val,MinusView,MinusView,MinusView>
711 (home,p,MinusView(y[0]),MinusView(y[1]),MinusView(y[2]),c);
712 }
713 template<class Val>
714 forceinline Actor*
715 lqtoter(Space& home, Propagator& p,
716 ViewArray<IntView>& x, ViewArray<IntView>& y, Val c) {
717 if (x.size() == 3)
718 return new (home) LqTer<Val,IntView,IntView,IntView>
719 (home,p,x[0],x[1],x[2],c);
720 if (x.size() == 2)
721 return new (home) LqTer<Val,IntView,IntView,MinusView>
722 (home,p,x[0],x[1],MinusView(y[0]),c);
723 if (x.size() == 1)
724 return new (home) LqTer<Val,IntView,MinusView,MinusView>
725 (home,p,x[0],MinusView(y[0]),MinusView(y[1]),c);
726 return new (home) LqTer<Val,MinusView,MinusView,MinusView>
727 (home,p,MinusView(y[0]),MinusView(y[1]),MinusView(y[2]),c);
728 }
729
730 template<class Val, class P, class N>
731 Actor*
732 Lq<Val,P,N>::copy(Space& home) {
733 if (isunit(x,y)) {
734 // Check whether rewriting is possible
735 if (x.size() + y.size() == 2)
736 return lqtobin(home,*this,x,y,c);
737 if (x.size() + y.size() == 3)
738 return lqtoter(home,*this,x,y,c);
739 }
740 return new (home) Lq<Val,P,N>(home,*this);
741 }
742
743 template<class Val, class P, class N>
744 ExecStatus
745 Lq<Val,P,N>::propagate(Space& home, const ModEventDelta& med) {
746 // Eliminate singletons
747 Val sl = 0;
748
749 if (IntView::me(med) == ME_INT_VAL) {
750 for (int i=x.size(); i--; ) {
751 Val m = x[i].min();
752 if (x[i].assigned()) {
753 c -= m; x.move_lst(i);
754 } else {
755 sl -= m;
756 }
757 }
758 for (int i=y.size(); i--; ) {
759 Val m = y[i].max();
760 if (y[i].assigned()) {
761 c += m; y.move_lst(i);
762 } else {
763 sl += m;
764 }
765 }
766 if ((x.size() + y.size()) <= 1) {
767 if (x.size() == 1) {
768 GECODE_ME_CHECK(x[0].lq(home,c));
769 return home.ES_SUBSUMED(*this);
770 }
771 if (y.size() == 1) {
772 GECODE_ME_CHECK(y[0].gq(home,-c));
773 return home.ES_SUBSUMED(*this);
774 }
775 return (c >= static_cast<Val>(0)) ?
776 home.ES_SUBSUMED(*this) : ES_FAILED;
777 }
778 } else {
779 for (int i=0; i<x.size(); i++)
780 sl -= x[i].min();
781 for (int i=0; i<y.size(); i++)
782 sl += y[i].max();
783 }
784
785 sl += c;
786
787 ExecStatus es = ES_FIX;
788 bool assigned = true;
789 for (int i=0; i<x.size(); i++) {
790 assert(!x[i].assigned());
791 Val slx = sl + x[i].min();
792 ModEvent me = x[i].lq(home,slx);
793 if (me == ME_INT_FAILED)
794 return ES_FAILED;
795 if (me != ME_INT_VAL)
796 assigned = false;
797 if (me_modified(me) && (slx != x[i].max()))
798 es = ES_NOFIX;
799 }
800
801 for (int i=0; i<y.size(); i++) {
802 assert(!y[i].assigned());
803 Val sly = y[i].max() - sl;
804 ModEvent me = y[i].gq(home,sly);
805 if (me == ME_INT_FAILED)
806 return ES_FAILED;
807 if (me != ME_INT_VAL)
808 assigned = false;
809 if (me_modified(me) && (sly != y[i].min()))
810 es = ES_NOFIX;
811 }
812 return assigned ? home.ES_SUBSUMED(*this) : es;
813 }
814
815 /*
816 * Reified bound consistent linear inequation
817 *
818 */
819
820 template<class Val, class P, class N, ReifyMode rm>
821 forceinline
822 ReLq<Val,P,N,rm>::ReLq(Home home,
823 ViewArray<P>& x, ViewArray<N>& y, Val c, BoolView b)
824 : ReLin<Val,P,N,PC_INT_BND,BoolView>(home,x,y,c,b) {}
825
826 template<class Val, class P, class N, ReifyMode rm>
827 ExecStatus
828 ReLq<Val,P,N,rm>::post(Home home,
829 ViewArray<P>& x, ViewArray<N>& y, Val c, BoolView b) {
830 ViewArray<NoView> nva;
831 if (y.size() == 0) {
832 (void) new (home) ReLq<Val,P,NoView,rm>(home,x,nva,c,b);
833 } else if (x.size() == 0) {
834 (void) new (home) ReLq<Val,NoView,N,rm>(home,nva,y,c,b);
835 } else {
836 (void) new (home) ReLq<Val,P,N,rm>(home,x,y,c,b);
837 }
838 return ES_OK;
839 }
840
841
842 template<class Val, class P, class N, ReifyMode rm>
843 forceinline
844 ReLq<Val,P,N,rm>::ReLq(Space& home, ReLq<Val,P,N,rm>& p)
845 : ReLin<Val,P,N,PC_INT_BND,BoolView>(home,p) {}
846
847 template<class Val, class P, class N, ReifyMode rm>
848 Actor*
849 ReLq<Val,P,N,rm>::copy(Space& home) {
850 return new (home) ReLq<Val,P,N,rm>(home,*this);
851 }
852
853 template<class Val, class P, class N, ReifyMode rm>
854 ExecStatus
855 ReLq<Val,P,N,rm>::propagate(Space& home, const ModEventDelta& med) {
856 if (b.zero()) {
857 if (rm == RM_IMP)
858 return home.ES_SUBSUMED(*this);
859 GECODE_REWRITE(*this,(Lq<Val,N,P>::post(home(*this),y,x,-c-1)));
860 }
861 if (b.one()) {
862 if (rm == RM_PMI)
863 return home.ES_SUBSUMED(*this);
864 GECODE_REWRITE(*this,(Lq<Val,P,N>::post(home(*this),x,y,c)));
865 }
866
867 // Eliminate singletons
868 Val sl = 0;
869 Val su = 0;
870
871 bounds_p<Val,P>(med,x,c,sl,su);
872 bounds_n<Val,N>(med,y,c,sl,su);
873
874 if (-sl > c) {
875 if (rm != RM_PMI)
876 GECODE_ME_CHECK(b.zero_none(home));
877 return home.ES_SUBSUMED(*this);
878 }
879 if (-su <= c) {
880 if (rm != RM_IMP)
881 GECODE_ME_CHECK(b.one_none(home));
882 return home.ES_SUBSUMED(*this);
883 }
884
885 return ES_FIX;
886 }
887
888}}}
889
890// STATISTICS: int-prop
891