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 Linear {
35 
36   /*
37    * Binary linear propagators
38    *
39    */
40   template<class Val, class A, class B, PropCond pc>
41   forceinline
LinBin(Home home,A y0,B y1,Val c0)42   LinBin<Val,A,B,pc>::LinBin(Home home, A y0, B y1, Val c0)
43     : Propagator(home), x0(y0), x1(y1), c(c0) {
44     x0.subscribe(home,*this,pc);
45     x1.subscribe(home,*this,pc);
46   }
47 
48   template<class Val, class A, class B, PropCond pc>
49   forceinline
LinBin(Space & home,LinBin<Val,A,B,pc> & p)50   LinBin<Val,A,B,pc>::LinBin(Space& home, LinBin<Val,A,B,pc>& p)
51     : Propagator(home,p), c(p.c) {
52     x0.update(home,p.x0);
53     x1.update(home,p.x1);
54   }
55 
56   template<class Val, class A, class B, PropCond pc>
57   forceinline
LinBin(Space & home,Propagator & p,A y0,B y1,Val c0)58   LinBin<Val,A,B,pc>::LinBin(Space& home, Propagator& p,
59                              A y0, B y1, Val c0)
60     : Propagator(home,p), c(c0) {
61     x0.update(home,y0);
62     x1.update(home,y1);
63   }
64 
65   template<class Val, class A, class B, PropCond pc>
66   PropCost
cost(const Space &,const ModEventDelta &) const67   LinBin<Val,A,B,pc>::cost(const Space&, const ModEventDelta&) const {
68     return PropCost::binary(PropCost::LO);
69   }
70 
71   template<class Val, class A, class B, PropCond pc>
72   void
reschedule(Space & home)73   LinBin<Val,A,B,pc>::reschedule(Space& home) {
74     x0.reschedule(home,*this,pc);
75     x1.reschedule(home,*this,pc);
76   }
77 
78   template<class Val, class A, class B, PropCond pc>
79   forceinline size_t
dispose(Space & home)80   LinBin<Val,A,B,pc>::dispose(Space& home) {
81     x0.cancel(home,*this,pc);
82     x1.cancel(home,*this,pc);
83     (void) Propagator::dispose(home);
84     return sizeof(*this);
85   }
86 
87 
88   /*
89    * Binary reified linear propagators
90    *
91    */
92   template<class Val, class A, class B, PropCond pc, class Ctrl>
93   forceinline
ReLinBin(Home home,A y0,B y1,Val c0,Ctrl b0)94   ReLinBin<Val,A,B,pc,Ctrl>::ReLinBin(Home home, A y0, B y1, Val c0, Ctrl b0)
95     : Propagator(home), x0(y0), x1(y1), c(c0), b(b0) {
96     x0.subscribe(home,*this,pc);
97     x1.subscribe(home,*this,pc);
98     b.subscribe(home,*this,PC_INT_VAL);
99   }
100 
101   template<class Val, class A, class B, PropCond pc, class Ctrl>
102   forceinline
ReLinBin(Space & home,ReLinBin<Val,A,B,pc,Ctrl> & p)103   ReLinBin<Val,A,B,pc,Ctrl>::ReLinBin(Space& home,
104                                       ReLinBin<Val,A,B,pc,Ctrl>& p)
105     : Propagator(home,p), c(p.c) {
106     x0.update(home,p.x0);
107     x1.update(home,p.x1);
108     b.update(home,p.b);
109   }
110 
111   template<class Val, class A, class B, PropCond pc, class Ctrl>
112   PropCost
cost(const Space &,const ModEventDelta &) const113   ReLinBin<Val,A,B,pc,Ctrl>::cost(const Space&, const ModEventDelta&) const {
114     return PropCost::binary(PropCost::LO);
115   }
116 
117   template<class Val, class A, class B, PropCond pc, class Ctrl>
118   void
reschedule(Space & home)119   ReLinBin<Val,A,B,pc,Ctrl>::reschedule(Space& home) {
120     x0.reschedule(home,*this,pc);
121     x1.reschedule(home,*this,pc);
122     b.reschedule(home,*this,PC_INT_VAL);
123   }
124 
125   template<class Val, class A, class B, PropCond pc, class Ctrl>
126   forceinline size_t
dispose(Space & home)127   ReLinBin<Val,A,B,pc,Ctrl>::dispose(Space& home) {
128     x0.cancel(home,*this,pc);
129     x1.cancel(home,*this,pc);
130     b.cancel(home,*this,PC_BOOL_VAL);
131     (void) Propagator::dispose(home);
132     return sizeof(*this);
133   }
134 
135   /*
136    * Binary bounds consistent linear equality
137    *
138    */
139 
140   template<class Val, class A, class B>
141   forceinline
EqBin(Home home,A x0,B x1,Val c)142   EqBin<Val,A,B>::EqBin(Home home, A x0, B x1, Val c)
143     : LinBin<Val,A,B,PC_INT_BND>(home,x0,x1,c) {}
144 
145   template<class Val, class A, class B>
146   ExecStatus
post(Home home,A x0,B x1,Val c)147   EqBin<Val,A,B>::post(Home home, A x0, B x1, Val c) {
148     (void) new (home) EqBin<Val,A,B>(home,x0,x1,c);
149     return ES_OK;
150   }
151 
152 
153   template<class Val, class A, class B>
154   forceinline
EqBin(Space & home,EqBin<Val,A,B> & p)155   EqBin<Val,A,B>::EqBin(Space& home, EqBin<Val,A,B>& p)
156     : LinBin<Val,A,B,PC_INT_BND>(home,p) {}
157 
158   template<class Val, class A, class B>
159   forceinline
EqBin(Space & home,Propagator & p,A x0,B x1,Val c)160   EqBin<Val,A,B>::EqBin(Space& home, Propagator& p,
161                         A x0, B x1, Val c)
162     : LinBin<Val,A,B,PC_INT_BND>(home,p,x0,x1,c) {}
163 
164   template<class Val, class A, class B>
165   Actor*
copy(Space & home)166   EqBin<Val,A,B>::copy(Space& home) {
167     return new (home) EqBin<Val,A,B>(home,*this);
168   }
169 
170   /// Describe which view has been modified how
171   enum BinMod {
172     BM_X0_MIN = 1<<0,
173     BM_X0_MAX = 1<<1,
174     BM_X1_MIN = 1<<2,
175     BM_X1_MAX = 1<<3,
176     BM_ALL    = BM_X0_MIN|BM_X0_MAX|BM_X1_MIN|BM_X1_MAX
177   };
178 
179 #define GECODE_INT_PV(CASE,TELL,UPDATE)         \
180   if (bm & (CASE)) {                            \
181     bm -= (CASE); ModEvent me = (TELL);         \
182     if (me_failed(me))   return ES_FAILED;      \
183     if (me_modified(me)) bm |= (UPDATE);        \
184   }
185 
186   template<class Val, class A, class B>
187   ExecStatus
propagate(Space & home,const ModEventDelta &)188   EqBin<Val,A,B>::propagate(Space& home, const ModEventDelta&) {
189     int bm = BM_ALL;
190     do {
191       GECODE_INT_PV(BM_X0_MIN, x0.gq(home,c-x1.max()), BM_X1_MAX);
192       GECODE_INT_PV(BM_X1_MIN, x1.gq(home,c-x0.max()), BM_X0_MAX);
193       GECODE_INT_PV(BM_X0_MAX, x0.lq(home,c-x1.min()), BM_X1_MIN);
194       GECODE_INT_PV(BM_X1_MAX, x1.lq(home,c-x0.min()), BM_X0_MIN);
195     } while (bm);
196     return x0.assigned() ? home.ES_SUBSUMED(*this) : ES_FIX;
197   }
198 
199 #undef GECODE_INT_PV
200 
201 
202 
203 
204 
205   /*
206    * Reified binary bounds consistent linear equality
207    *
208    */
209 
210   template<class Val, class A, class B, class Ctrl, ReifyMode rm>
211   forceinline
ReEqBin(Home home,A x0,B x1,Val c,Ctrl b)212   ReEqBin<Val,A,B,Ctrl,rm>::ReEqBin(Home home, A x0, B x1, Val c, Ctrl b)
213     : ReLinBin<Val,A,B,PC_INT_BND,Ctrl>(home,x0,x1,c,b) {}
214 
215   template<class Val, class A, class B, class Ctrl, ReifyMode rm>
216   ExecStatus
post(Home home,A x0,B x1,Val c,Ctrl b)217   ReEqBin<Val,A,B,Ctrl,rm>::post(Home home, A x0, B x1, Val c, Ctrl b) {
218     (void) new (home) ReEqBin<Val,A,B,Ctrl,rm>(home,x0,x1,c,b);
219     return ES_OK;
220   }
221 
222 
223   template<class Val, class A, class B, class Ctrl, ReifyMode rm>
224   forceinline
ReEqBin(Space & home,ReEqBin<Val,A,B,Ctrl,rm> & p)225   ReEqBin<Val,A,B,Ctrl,rm>::ReEqBin(Space& home,
226                                     ReEqBin<Val,A,B,Ctrl,rm>& p)
227     : ReLinBin<Val,A,B,PC_INT_BND,Ctrl>(home,p) {}
228 
229   template<class Val, class A, class B, class Ctrl, ReifyMode rm>
230   Actor*
copy(Space & home)231   ReEqBin<Val,A,B,Ctrl,rm>::copy(Space& home) {
232     return new (home) ReEqBin<Val,A,B,Ctrl,rm>(home,*this);
233   }
234 
235   template<class Val, class A, class B, class Ctrl, ReifyMode rm>
236   ExecStatus
propagate(Space & home,const ModEventDelta &)237   ReEqBin<Val,A,B,Ctrl,rm>::propagate(Space& home, const ModEventDelta&) {
238     if (b.zero()) {
239       if (rm == RM_IMP)
240         return home.ES_SUBSUMED(*this);
241       GECODE_REWRITE(*this,(NqBin<Val,A,B>::post(home(*this),x0,x1,c)));
242     }
243     if (b.one()) {
244       if (rm == RM_PMI)
245         return home.ES_SUBSUMED(*this);
246       GECODE_REWRITE(*this,(EqBin<Val,A,B>::post(home(*this),x0,x1,c)));
247     }
248     if ((x0.min() + x1.min() > c) || (x0.max() + x1.max() < c)) {
249       if (rm != RM_PMI)
250         GECODE_ME_CHECK(b.zero_none(home));
251       return home.ES_SUBSUMED(*this);
252     }
253     if (x0.assigned() && x1.assigned()) {
254       assert(x0.val() + x1.val() == c);
255       if (rm != RM_IMP)
256         GECODE_ME_CHECK(b.one_none(home));
257       return home.ES_SUBSUMED(*this);
258     }
259     return ES_FIX;
260   }
261 
262 
263 
264 
265   /*
266    * Binary domain consistent linear disequality
267    *
268    */
269   template<class Val, class A, class B>
270   forceinline
NqBin(Home home,A x0,B x1,Val c)271   NqBin<Val,A,B>::NqBin(Home home, A x0, B x1, Val c)
272     : LinBin<Val,A,B,PC_INT_VAL>(home,x0,x1,c) {}
273 
274   template<class Val, class A, class B>
275   ExecStatus
post(Home home,A x0,B x1,Val c)276   NqBin<Val,A,B>::post(Home home, A x0, B x1, Val c) {
277     (void) new (home) NqBin<Val,A,B>(home,x0,x1,c);
278     return ES_OK;
279   }
280 
281 
282   template<class Val, class A, class B>
283   forceinline
NqBin(Space & home,NqBin<Val,A,B> & p)284   NqBin<Val,A,B>::NqBin(Space& home, NqBin<Val,A,B>& p)
285     : LinBin<Val,A,B,PC_INT_VAL>(home,p) {}
286 
287   template<class Val, class A, class B>
288   Actor*
copy(Space & home)289   NqBin<Val,A,B>::copy(Space& home) {
290     return new (home) NqBin<Val,A,B>(home,*this);
291   }
292 
293   template<class Val, class A, class B>
294   forceinline
NqBin(Space & home,Propagator & p,A x0,B x1,Val c)295   NqBin<Val,A,B>::NqBin(Space& home, Propagator& p,
296                         A x0, B x1, Val c)
297     : LinBin<Val,A,B,PC_INT_VAL>(home,p,x0,x1,c) {}
298 
299 
300 
301   template<class Val, class A, class B>
302   PropCost
cost(const Space &,const ModEventDelta &) const303   NqBin<Val,A,B>::cost(const Space&, const ModEventDelta&) const {
304     return PropCost::unary(PropCost::LO);
305   }
306 
307   template<class Val, class A, class B>
308   ExecStatus
propagate(Space & home,const ModEventDelta &)309   NqBin<Val,A,B>::propagate(Space& home, const ModEventDelta&) {
310     if (x0.assigned()) {
311       GECODE_ME_CHECK(x1.nq(home,c-x0.val()));
312     } else {
313       assert(x1.assigned());
314       GECODE_ME_CHECK(x0.nq(home,c-x1.val()));
315     }
316     return home.ES_SUBSUMED(*this);
317   }
318 
319 
320   /*
321    * Binary domain consistent less equal
322    *
323    */
324 
325   template<class Val, class A, class B>
326   forceinline
LqBin(Home home,A x0,B x1,Val c)327   LqBin<Val,A,B>::LqBin(Home home, A x0, B x1, Val c)
328     : LinBin<Val,A,B,PC_INT_BND>(home,x0,x1,c) {}
329 
330   template<class Val, class A, class B>
331   ExecStatus
post(Home home,A x0,B x1,Val c)332   LqBin<Val,A,B>::post(Home home, A x0, B x1, Val c) {
333     (void) new (home) LqBin<Val,A,B>(home,x0,x1,c);
334     return ES_OK;
335   }
336 
337 
338   template<class Val, class A, class B>
339   forceinline
LqBin(Space & home,LqBin<Val,A,B> & p)340   LqBin<Val,A,B>::LqBin(Space& home, LqBin<Val,A,B>& p)
341     : LinBin<Val,A,B,PC_INT_BND>(home,p) {}
342 
343   template<class Val, class A, class B>
344   Actor*
copy(Space & home)345   LqBin<Val,A,B>::copy(Space& home) {
346     return new (home) LqBin<Val,A,B>(home,*this);
347   }
348 
349   template<class Val, class A, class B>
350   forceinline
LqBin(Space & home,Propagator & p,A x0,B x1,Val c)351   LqBin<Val,A,B>::LqBin(Space& home, Propagator& p,
352                         A x0, B x1, Val c)
353     : LinBin<Val,A,B,PC_INT_BND>(home,p,x0,x1,c) {}
354 
355   template<class Val, class A, class B>
356   ExecStatus
propagate(Space & home,const ModEventDelta &)357   LqBin<Val,A,B>::propagate(Space& home, const ModEventDelta&) {
358     GECODE_ME_CHECK(x0.lq(home,c-x1.min()));
359     GECODE_ME_CHECK(x1.lq(home,c-x0.min()));
360     return (x0.max()+x1.max() <= c) ? home.ES_SUBSUMED(*this) : ES_FIX;
361   }
362 
363 
364 
365 
366   /*
367    * Binary domain consistent greater equal
368    *
369    */
370 
371   template<class Val, class A, class B>
372   forceinline
GqBin(Home home,A x0,B x1,Val c)373   GqBin<Val,A,B>::GqBin(Home home, A x0, B x1, Val c)
374     : LinBin<Val,A,B,PC_INT_BND>(home,x0,x1,c) {}
375 
376   template<class Val, class A, class B>
377   ExecStatus
post(Home home,A x0,B x1,Val c)378   GqBin<Val,A,B>::post(Home home, A x0, B x1, Val c) {
379     (void) new (home) GqBin<Val,A,B>(home,x0,x1,c);
380     return ES_OK;
381   }
382 
383 
384   template<class Val, class A, class B>
385   forceinline
GqBin(Space & home,GqBin<Val,A,B> & p)386   GqBin<Val,A,B>::GqBin(Space& home, GqBin<Val,A,B>& p)
387     : LinBin<Val,A,B,PC_INT_BND>(home,p) {}
388 
389   template<class Val, class A, class B>
390   Actor*
copy(Space & home)391   GqBin<Val,A,B>::copy(Space& home) {
392     return new (home) GqBin<Val,A,B>(home,*this);
393   }
394 
395   template<class Val, class A, class B>
396   forceinline
GqBin(Space & home,Propagator & p,A x0,B x1,Val c)397   GqBin<Val,A,B>::GqBin(Space& home, Propagator& p,
398                         A x0, B x1, Val c)
399     : LinBin<Val,A,B,PC_INT_BND>(home,p,x0,x1,c) {}
400 
401   template<class Val, class A, class B>
402   ExecStatus
propagate(Space & home,const ModEventDelta &)403   GqBin<Val,A,B>::propagate(Space& home, const ModEventDelta&) {
404     GECODE_ME_CHECK(x0.gq(home,c-x1.max()));
405     GECODE_ME_CHECK(x1.gq(home,c-x0.max()));
406     return (x0.min()+x1.min() >= c) ? home.ES_SUBSUMED(*this) : ES_FIX;
407   }
408 
409 
410 
411 
412   /*
413    * Reified binary domain consistent less equal
414    *
415    */
416 
417   template<class Val, class A, class B, ReifyMode rm>
418   forceinline
ReLqBin(Home home,A x0,B x1,Val c,BoolView b)419   ReLqBin<Val,A,B,rm>::ReLqBin(Home home, A x0, B x1, Val c, BoolView b)
420     : ReLinBin<Val,A,B,PC_INT_BND,BoolView>(home,x0,x1,c,b) {}
421 
422   template<class Val, class A, class B, ReifyMode rm>
423   ExecStatus
post(Home home,A x0,B x1,Val c,BoolView b)424   ReLqBin<Val,A,B,rm>::post(Home home, A x0, B x1, Val c, BoolView b) {
425     (void) new (home) ReLqBin<Val,A,B,rm>(home,x0,x1,c,b);
426     return ES_OK;
427   }
428 
429 
430   template<class Val, class A, class B, ReifyMode rm>
431   forceinline
ReLqBin(Space & home,ReLqBin<Val,A,B,rm> & p)432   ReLqBin<Val,A,B,rm>::ReLqBin(Space& home, ReLqBin<Val,A,B,rm>& p)
433     : ReLinBin<Val,A,B,PC_INT_BND,BoolView>(home,p) {}
434 
435   template<class Val, class A, class B, ReifyMode rm>
436   Actor*
copy(Space & home)437   ReLqBin<Val,A,B,rm>::copy(Space& home) {
438     return new (home) ReLqBin<Val,A,B,rm>(home,*this);
439   }
440 
441   template<class Val, class A, class B, ReifyMode rm>
442   ExecStatus
propagate(Space & home,const ModEventDelta &)443   ReLqBin<Val,A,B,rm>::propagate(Space& home, const ModEventDelta&) {
444     if (b.one()) {
445       if (rm == RM_PMI)
446         return home.ES_SUBSUMED(*this);
447       GECODE_REWRITE(*this,(LqBin<Val,A,B>::post(home(*this),x0,x1,c)));
448     }
449     if (b.zero()) {
450       if (rm == RM_IMP)
451         return home.ES_SUBSUMED(*this);
452       GECODE_REWRITE(*this,(GqBin<Val,A,B>::post(home(*this),x0,x1,c+1)));
453     }
454     if (x0.max() + x1.max() <= c) {
455       if (rm != RM_IMP)
456         GECODE_ME_CHECK(b.one_none(home));
457       return home.ES_SUBSUMED(*this);
458     }
459     if (x0.min() + x1.min() > c) {
460       if (rm != RM_PMI)
461         GECODE_ME_CHECK(b.zero_none(home));
462       return home.ES_SUBSUMED(*this);
463     }
464     return ES_FIX;
465   }
466 
467 }}}
468 
469 // STATISTICS: int-prop
470 
471