Generated on Thu Jan 20 2022 00:00:00 for Gecode by doxygen 1.9.1
int-bin.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 Linear {
35 
36  /*
37  * Binary linear propagators
38  *
39  */
40  template<class Val, class A, class B, PropCond pc>
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>
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>
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
69  }
70 
71  template<class Val, class A, class B, PropCond pc>
72  void
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
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>
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>
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
115  }
116 
117  template<class Val, class A, class B, PropCond pc, class Ctrl>
118  void
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
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>
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
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>
156  : LinBin<Val,A,B,PC_INT_BND>(home,p) {}
157 
158  template<class Val, class A, class B>
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*
167  return new (home) EqBin<Val,A,B>(home,*this);
168  }
169 
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,
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
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>
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
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>
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*
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
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>
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
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>
285  : LinBin<Val,A,B,PC_INT_VAL>(home,p) {}
286 
287  template<class Val, class A, class B>
288  Actor*
290  return new (home) NqBin<Val,A,B>(home,*this);
291  }
292 
293  template<class Val, class A, class B>
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
303  NqBin<Val,A,B>::cost(const Space&, const ModEventDelta&) const {
305  }
306 
307  template<class Val, class A, class B>
308  ExecStatus
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>
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
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>
341  : LinBin<Val,A,B,PC_INT_BND>(home,p) {}
342 
343  template<class Val, class A, class B>
344  Actor*
346  return new (home) LqBin<Val,A,B>(home,*this);
347  }
348 
349  template<class Val, class A, class B>
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
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>
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
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>
387  : LinBin<Val,A,B,PC_INT_BND>(home,p) {}
388 
389  template<class Val, class A, class B>
390  Actor*
392  return new (home) GqBin<Val,A,B>(home,*this);
393  }
394 
395  template<class Val, class A, class B>
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
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>
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
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>
433  : ReLinBin<Val,A,B,PC_INT_BND,BoolView>(home,p) {}
434 
435  template<class Val, class A, class B, ReifyMode rm>
436  Actor*
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
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 
struct Gecode::@602::NNF::@65::@66 b
For binary nodes (and, or, eqv)
int p
Number of positive literals for node type.
Definition: bool-expr.cpp:232
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
friend FloatVal max(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:386
friend FloatVal min(const FloatVal &x, const FloatVal &y)
Definition: val.hpp:398
Home class for posting propagators
Definition: core.hpp:856
Boolean view for Boolean variables.
Definition: view.hpp:1380
Propagator for bounds consistent binary linear equality
Definition: linear.hh:134
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: int-bin.hpp:188
EqBin(Space &home, EqBin &p)
Constructor for cloning p.
Definition: int-bin.hpp:155
static ExecStatus post(Home home, A x0, B x1, Val c)
Post propagator for .
Definition: int-bin.hpp:147
virtual Actor * copy(Space &home)
Create copy during cloning.
Definition: int-bin.hpp:166
Propagator for bounds consistent binary linear greater or equal
Definition: linear.hh:271
static ExecStatus post(Home home, A x0, B x1, Val c)
Post propagator for .
Definition: int-bin.hpp:378
virtual Actor * copy(Space &home)
Create copy during cloning.
Definition: int-bin.hpp:391
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: int-bin.hpp:403
GqBin(Space &home, GqBin &p)
Constructor for cloning p.
Definition: int-bin.hpp:386
Base-class for binary linear propagators.
Definition: linear.hh:65
virtual size_t dispose(Space &home)
Delete propagator and return its size.
Definition: int-bin.hpp:80
B x1
View of type B.
Definition: linear.hh:70
A x0
View of type A.
Definition: linear.hh:68
virtual void reschedule(Space &home)
Schedule function.
Definition: int-bin.hpp:73
virtual PropCost cost(const Space &home, const ModEventDelta &med) const
Cost function (defined as low binary)
Definition: int-bin.hpp:67
LinBin(Space &home, LinBin &p)
Constructor for cloning p.
Definition: int-bin.hpp:50
Propagator for bounds consistent binary linear less or equal
Definition: linear.hh:237
static ExecStatus post(Home home, A x0, B x1, Val c)
Post propagator for .
Definition: int-bin.hpp:332
LqBin(Space &home, LqBin &p)
Constructor for cloning p.
Definition: int-bin.hpp:340
virtual Actor * copy(Space &home)
Create copy during cloning.
Definition: int-bin.hpp:345
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: int-bin.hpp:357
Propagator for bounds consistent binary linear disequality
Definition: linear.hh:201
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: int-bin.hpp:309
NqBin(Space &home, NqBin &p)
Constructor for cloning p.
Definition: int-bin.hpp:284
virtual PropCost cost(const Space &home, const ModEventDelta &med) const
Cost function (defined as low unary)
Definition: int-bin.hpp:303
static ExecStatus post(Home home, A x0, B x1, Val c)
Post propagator for .
Definition: int-bin.hpp:276
virtual Actor * copy(Space &home)
Create copy during cloning.
Definition: int-bin.hpp:289
Propagator for reified bounds consistent binary linear equality
Definition: linear.hh:168
static ExecStatus post(Home home, A x0, B x1, Val c, Ctrl b)
Post propagator for .
Definition: int-bin.hpp:217
ReEqBin(Space &home, ReEqBin &p)
Constructor for cloning p.
Definition: int-bin.hpp:225
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: int-bin.hpp:237
virtual Actor * copy(Space &home)
Create copy during cloning.
Definition: int-bin.hpp:231
Base-class for reified binary linear propagators.
Definition: linear.hh:98
Ctrl b
Control view for reification.
Definition: linear.hh:107
virtual size_t dispose(Space &home)
Delete propagator and return its size.
Definition: int-bin.hpp:127
B x1
View of type B.
Definition: linear.hh:103
virtual PropCost cost(const Space &home, const ModEventDelta &med) const
Cost function (defined as low binary)
Definition: int-bin.hpp:113
ReLinBin(Space &home, ReLinBin &p)
Constructor for cloning p.
Definition: int-bin.hpp:103
virtual void reschedule(Space &home)
Schedule function.
Definition: int-bin.hpp:119
A x0
View of type A.
Definition: linear.hh:101
Propagator for reified bounds consistent binary linear less or equal
Definition: linear.hh:305
static ExecStatus post(Home home, A x0, B x1, Val c, BoolView b)
Post propagator for .
Definition: int-bin.hpp:424
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: int-bin.hpp:443
virtual Actor * copy(Space &home)
Create copy during cloning.
Definition: int-bin.hpp:437
ReLqBin(Space &home, ReLqBin &p)
Constructor for cloning p.
Definition: int-bin.hpp:432
Propagation cost.
Definition: core.hpp:486
static PropCost unary(PropCost::Mod m)
Single variable for modifier pcm.
Definition: core.hpp:4813
static PropCost binary(PropCost::Mod m)
Two variables for modifier pcm.
Definition: core.hpp:4809
@ LO
Cheap.
Definition: core.hpp:513
Base-class for propagators.
Definition: core.hpp:1064
Computation spaces.
Definition: core.hpp:1742
ExecStatus
Definition: core.hpp:472
@ ES_OK
Execution is okay.
Definition: core.hpp:476
@ ES_FIX
Propagation has computed fixpoint.
Definition: core.hpp:477
ExecStatus ES_SUBSUMED(Propagator &p)
Definition: core.hpp:3563
int ModEventDelta
Modification event deltas.
Definition: core.hpp:89
#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
@ RM_IMP
Implication for reification.
Definition: int.hh:862
@ RM_PMI
Inverse implication for reification.
Definition: int.hh:869
#define GECODE_INT_PV(CASE, TELL, UPDATE)
Definition: int-bin.hpp:179
BinMod
Describe which view has been modified how.
Definition: int-bin.hpp:171
const Gecode::PropCond PC_INT_VAL
Propagate when a view becomes assigned (single value)
Definition: var-type.hpp:82
const Gecode::PropCond PC_INT_BND
Propagate when minimum or maximum of a view changes.
Definition: var-type.hpp:91
const Gecode::PropCond PC_BOOL_VAL
Propagate when a view becomes assigned (single value)
Definition: var-type.hpp:126
Gecode::FloatVal c(-8, 8)
#define forceinline
Definition: config.hpp:194