Generated on Thu Mar 16 2017 03:24:20 for Gecode by doxygen 1.8.13
int-nary.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  * Last modified:
10  * $Date: 2016-06-29 17:28:17 +0200 (Wed, 29 Jun 2016) $ by $Author: schulte $
11  * $Revision: 15137 $
12  *
13  * This file is part of Gecode, the generic constraint
14  * development environment:
15  * http://www.gecode.org
16  *
17  * Permission is hereby granted, free of charge, to any person obtaining
18  * a copy of this software and associated documentation files (the
19  * "Software"), to deal in the Software without restriction, including
20  * without limitation the rights to use, copy, modify, merge, publish,
21  * distribute, sublicense, and/or sell copies of the Software, and to
22  * permit persons to whom the Software is furnished to do so, subject to
23  * the following conditions:
24  *
25  * The above copyright notice and this permission notice shall be
26  * included in all copies or substantial portions of the Software.
27  *
28  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
29  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
30  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
31  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
32  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
33  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
34  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
35  *
36  */
37 
39 
40 namespace Gecode { namespace Int { namespace Linear {
41 
46  template<class P, class N>
47  forceinline bool
48  isunit(ViewArray<P>&, ViewArray<N>&) { return false; }
49  template<>
50  forceinline bool
52  template<>
53  forceinline bool
55  template<>
56  forceinline bool
58 
59  /*
60  * Linear propagators
61  *
62  */
63  template<class Val, class P, class N, PropCond pc>
66  : Propagator(home), x(x0), y(y0), c(c0) {
67  x.subscribe(home,*this,pc);
68  y.subscribe(home,*this,pc);
69  }
70 
71  template<class Val, class P, class N, PropCond pc>
74  : Propagator(home,share,p), c(p.c) {
75  x.update(home,share,p.x);
76  y.update(home,share,p.y);
77  }
78 
79  template<class Val, class P, class N, PropCond pc>
80  PropCost
81  Lin<Val,P,N,pc>::cost(const Space&, const ModEventDelta&) const {
82  return PropCost::linear(PropCost::LO, x.size()+y.size());
83  }
84 
85  template<class Val, class P, class N, PropCond pc>
86  void
88  x.reschedule(home,*this,pc);
89  y.reschedule(home,*this,pc);
90  }
91 
92  template<class Val, class P, class N, PropCond pc>
93  forceinline size_t
95  x.cancel(home,*this,pc);
96  y.cancel(home,*this,pc);
97  (void) Propagator::dispose(home);
98  return sizeof(*this);
99  }
100 
101  /*
102  * Reified linear propagators
103  *
104  */
105  template<class Val, class P, class N, PropCond pc, class Ctrl>
108  (Home home, ViewArray<P>& x, ViewArray<N>& y, Val c, Ctrl b0)
109  : Lin<Val,P,N,pc>(home,x,y,c), b(b0) {
110  b.subscribe(home,*this,PC_INT_VAL);
111  }
112 
113  template<class Val, class P, class N, PropCond pc, class Ctrl>
116  (Space& home, bool share, ReLin<Val,P,N,pc,Ctrl>& p)
117  : Lin<Val,P,N,pc>(home,share,p) {
118  b.update(home,share,p.b);
119  }
120 
121  template<class Val, class P, class N, PropCond pc, class Ctrl>
122  void
124  x.reschedule(home,*this,pc);
125  y.reschedule(home,*this,pc);
126  b.reschedule(home,*this,PC_INT_VAL);
127  }
128 
129  template<class Val, class P, class N, PropCond pc, class Ctrl>
130  forceinline size_t
132  b.cancel(home,*this,PC_BOOL_VAL);
133  (void) Lin<Val,P,N,pc>::dispose(home);
134  return sizeof(*this);
135  }
136 
137  /*
138  * Computing bounds
139  *
140  */
141 
142  template<class Val, class View>
143  void
144  bounds_p(ModEventDelta med, ViewArray<View>& x, Val& c, Val& sl, Val& su) {
145  int n = x.size();
146  if (IntView::me(med) == ME_INT_VAL) {
147  for (int i = n; i--; ) {
148  Val m = x[i].min();
149  if (x[i].assigned()) {
150  c -= m; x[i] = x[--n];
151  } else {
152  sl -= m; su -= x[i].max();
153  }
154  }
155  x.size(n);
156  } else {
157  for (int i = n; i--; ) {
158  sl -= x[i].min(); su -= x[i].max();
159  }
160  }
161  }
162 
163  template<class Val, class View>
164  void
165  bounds_n(ModEventDelta med, ViewArray<View>& y, Val& c, Val& sl, Val& su) {
166  int n = y.size();
167  if (IntView::me(med) == ME_INT_VAL) {
168  for (int i = n; i--; ) {
169  Val m = y[i].max();
170  if (y[i].assigned()) {
171  c += m; y[i] = y[--n];
172  } else {
173  sl += m; su += y[i].min();
174  }
175  }
176  y.size(n);
177  } else {
178  for (int i = n; i--; ) {
179  sl += y[i].max(); su += y[i].min();
180  }
181  }
182  }
183 
184 
185  template<class Val, class P, class N>
186  ExecStatus
188  ViewArray<P>& x, ViewArray<N>& y, Val& c) {
189  // Eliminate singletons
190  Val sl = 0;
191  Val su = 0;
192 
193  bounds_p<Val,P>(med, x, c, sl, su);
194  bounds_n<Val,N>(med, y, c, sl, su);
195 
196  if ((IntView::me(med) == ME_INT_VAL) && ((x.size() + y.size()) <= 1)) {
197  if (x.size() == 1) {
198  GECODE_ME_CHECK(x[0].eq(home,c));
199  return home.ES_SUBSUMED(p);
200  }
201  if (y.size() == 1) {
202  GECODE_ME_CHECK(y[0].eq(home,-c));
203  return home.ES_SUBSUMED(p);
204  }
205  return (c == static_cast<Val>(0)) ?
206  home.ES_SUBSUMED(p) : ES_FAILED;
207  }
208 
209  sl += c; su += c;
210 
211  const int mod_sl = 1;
212  const int mod_su = 2;
213 
214  int mod = mod_sl | mod_su;
215 
216  do {
217  if (mod & mod_sl) {
218  mod -= mod_sl;
219  // Propagate upper bound for positive variables
220  for (int i = x.size(); i--; ) {
221  const Val xi_max = x[i].max();
222  ModEvent me = x[i].lq(home,sl + x[i].min());
223  if (me_failed(me))
224  return ES_FAILED;
225  if (me_modified(me)) {
226  su += xi_max - x[i].max();
227  mod |= mod_su;
228  }
229  }
230  // Propagate lower bound for negative variables
231  for (int i = y.size(); i--; ) {
232  const Val yi_min = y[i].min();
233  ModEvent me = y[i].gq(home,y[i].max() - sl);
234  if (me_failed(me))
235  return ES_FAILED;
236  if (me_modified(me)) {
237  su += y[i].min() - yi_min;
238  mod |= mod_su;
239  }
240  }
241  }
242  if (mod & mod_su) {
243  mod -= mod_su;
244  // Propagate lower bound for positive variables
245  for (int i = x.size(); i--; ) {
246  const Val xi_min = x[i].min();
247  ModEvent me = x[i].gq(home,su + x[i].max());
248  if (me_failed(me))
249  return ES_FAILED;
250  if (me_modified(me)) {
251  sl += xi_min - x[i].min();
252  mod |= mod_sl;
253  }
254  }
255  // Propagate upper bound for negative variables
256  for (int i = y.size(); i--; ) {
257  const Val yi_max = y[i].max();
258  ModEvent me = y[i].lq(home,y[i].min() - su);
259  if (me_failed(me))
260  return ES_FAILED;
261  if (me_modified(me)) {
262  sl += y[i].max() - yi_max;
263  mod |= mod_sl;
264  }
265  }
266  }
267  } while (mod);
268 
269  return (sl == su) ? home.ES_SUBSUMED(p) : ES_FIX;
270  }
271 
272  /*
273  * Bound consistent linear equation
274  *
275  */
276 
277  template<class Val, class P, class N>
280  : Lin<Val,P,N,PC_INT_BND>(home,x,y,c) {}
281 
282  template<class Val, class P, class N>
283  ExecStatus
285  ViewArray<NoView> nva;
286  if (y.size() == 0) {
287  (void) new (home) Eq<Val,P,NoView>(home,x,nva,c);
288  } else if (x.size() == 0) {
289  (void) new (home) Eq<Val,N,NoView>(home,y,nva,-c);
290  } else {
291  (void) new (home) Eq<Val,P,N>(home,x,y,c);
292  }
293  return ES_OK;
294  }
295 
296 
297  template<class Val, class P, class N>
299  Eq<Val,P,N>::Eq(Space& home, bool share, Eq<Val,P,N>& p)
300  : Lin<Val,P,N,PC_INT_BND>(home,share,p) {}
301 
306  template<class Val, class P, class N>
309  return NULL;
310  }
311  template<class Val>
313  eqtobin(Space& home, bool share, Propagator& p,
315  assert(x.size() == 2);
316  return new (home) EqBin<Val,IntView,IntView>
317  (home,share,p,x[0],x[1],c);
318  }
319  template<class Val>
321  eqtobin(Space& home, bool share, Propagator& p,
323  assert(y.size() == 2);
324  return new (home) EqBin<Val,IntView,IntView>
325  (home,share,p,y[0],y[1],-c);
326  }
327  template<class Val>
329  eqtobin(Space& home, bool share, Propagator& p,
330  ViewArray<IntView>& x, ViewArray<IntView>& y, Val c) {
331  if (x.size() == 2)
332  return new (home) EqBin<Val,IntView,IntView>
333  (home,share,p,x[0],x[1],c);
334  if (x.size() == 1)
335  return new (home) EqBin<Val,IntView,MinusView>
336  (home,share,p,x[0],MinusView(y[0]),c);
337  return new (home) EqBin<Val,IntView,IntView>
338  (home,share,p,y[0],y[1],-c);
339  }
340 
345  template<class Val, class P, class N>
348  return NULL;
349  }
350  template<class Val>
352  eqtoter(Space& home, bool share, Propagator& p,
354  assert(x.size() == 3);
355  return new (home) EqTer<Val,IntView,IntView,IntView>
356  (home,share,p,x[0],x[1],x[2],c);
357  }
358  template<class Val>
360  eqtoter(Space& home, bool share, Propagator& p,
362  assert(y.size() == 3);
363  return new (home) EqTer<Val,IntView,IntView,IntView>
364  (home,share,p,y[0],y[1],y[2],-c);
365  }
366  template<class Val>
368  eqtoter(Space& home, bool share, Propagator& p,
369  ViewArray<IntView>& x, ViewArray<IntView>& y, Val c) {
370  if (x.size() == 3)
371  return new (home) EqTer<Val,IntView,IntView,IntView>
372  (home,share,p,x[0],x[1],x[2],c);
373  if (x.size() == 2)
374  return new (home) EqTer<Val,IntView,IntView,MinusView>
375  (home,share,p,x[0],x[1],MinusView(y[0]),c);
376  if (x.size() == 1)
377  return new (home) EqTer<Val,IntView,IntView,MinusView>
378  (home,share,p,y[0],y[1],MinusView(x[0]),-c);
379  return new (home) EqTer<Val,IntView,IntView,IntView>
380  (home,share,p,y[0],y[1],y[2],-c);
381  }
382 
383  template<class Val, class P, class N>
384  Actor*
385  Eq<Val,P,N>::copy(Space& home, bool share) {
386  if (isunit(x,y)) {
387  // Check whether rewriting is possible
388  if (x.size() + y.size() == 2)
389  return eqtobin(home,share,*this,x,y,c);
390  if (x.size() + y.size() == 3)
391  return eqtoter(home,share,*this,x,y,c);
392  }
393  return new (home) Eq<Val,P,N>(home,share,*this);
394  }
395 
396  template<class Val, class P, class N>
397  ExecStatus
399  return prop_bnd<Val,P,N>(home,med,*this,x,y,c);
400  }
401 
402  /*
403  * Reified bound consistent linear equation
404  *
405  */
406 
407  template<class Val, class P, class N, class Ctrl, ReifyMode rm>
410  ViewArray<P>& x, ViewArray<N>& y, Val c, Ctrl b)
411  : ReLin<Val,P,N,PC_INT_BND,Ctrl>(home,x,y,c,b) {}
412 
413  template<class Val, class P, class N, class Ctrl, ReifyMode rm>
414  ExecStatus
416  ViewArray<P>& x, ViewArray<N>& y, Val c, Ctrl b) {
417  ViewArray<NoView> nva;
418  if (y.size() == 0) {
419  (void) new (home) ReEq<Val,P,NoView,Ctrl,rm>(home,x,nva,c,b);
420  } else if (x.size() == 0) {
421  (void) new (home) ReEq<Val,N,NoView,Ctrl,rm>(home,y,nva,-c,b);
422  } else {
423  (void) new (home) ReEq<Val,P,N,Ctrl,rm>(home,x,y,c,b);
424  }
425  return ES_OK;
426  }
427 
428 
429  template<class Val, class P, class N, class Ctrl, ReifyMode rm>
433  : ReLin<Val,P,N,PC_INT_BND,Ctrl>(home,share,p) {}
434 
435  template<class Val, class P, class N, class Ctrl, ReifyMode rm>
436  Actor*
437  ReEq<Val,P,N,Ctrl,rm>::copy(Space& home, bool share) {
438  return new (home) ReEq<Val,P,N,Ctrl,rm>(home,share,*this);
439  }
440 
441  template<class Val, class P, class N, class Ctrl, ReifyMode rm>
442  ExecStatus
444  if (b.zero()) {
445  if (rm == RM_IMP)
446  return home.ES_SUBSUMED(*this);
447  GECODE_REWRITE(*this,(Nq<Val,P,N>::post(home(*this),x,y,c)));
448  }
449  if (b.one()) {
450  if (rm == RM_PMI)
451  return home.ES_SUBSUMED(*this);
452  GECODE_REWRITE(*this,(Eq<Val,P,N>::post(home(*this),x,y,c)));
453  }
454 
455  Val sl = 0;
456  Val su = 0;
457 
458  bounds_p<Val,P>(med, x, c, sl, su);
459  bounds_n<Val,N>(med, y, c, sl, su);
460 
461  if ((-sl == c) && (-su == c)) {
462  if (rm != RM_IMP)
463  GECODE_ME_CHECK(b.one_none(home));
464  return home.ES_SUBSUMED(*this);
465  }
466  if ((-sl > c) || (-su < c)) {
467  if (rm != RM_PMI)
468  GECODE_ME_CHECK(b.zero_none(home));
469  return home.ES_SUBSUMED(*this);
470  }
471  return ES_FIX;
472  }
473 
474 
475  /*
476  * Domain consistent linear disequation
477  *
478  */
479 
480  template<class Val, class P, class N>
483  : Lin<Val,P,N,PC_INT_VAL>(home,x,y,c) {}
484 
485  template<class Val, class P, class N>
486  ExecStatus
488  ViewArray<NoView> nva;
489  if (y.size() == 0) {
490  (void) new (home) Nq<Val,P,NoView>(home,x,nva,c);
491  } else if (x.size() == 0) {
492  (void) new (home) Nq<Val,N,NoView>(home,y,nva,-c);
493  } else {
494  (void) new (home) Nq<Val,P,N>(home,x,y,c);
495  }
496  return ES_OK;
497  }
498 
499 
500  template<class Val, class P, class N>
502  Nq<Val,P,N>::Nq(Space& home, bool share, Nq<Val,P,N>& p)
503  : Lin<Val,P,N,PC_INT_VAL>(home,share,p) {}
504 
509  template<class Val, class P, class N>
512  return NULL;
513  }
514  template<class Val>
516  nqtobin(Space& home, bool share, Propagator& p,
518  assert(x.size() == 2);
519  return new (home) NqBin<Val,IntView,IntView>
520  (home,share,p,x[0],x[1],c);
521  }
522  template<class Val>
524  nqtobin(Space& home, bool share, Propagator& p,
526  assert(y.size() == 2);
527  return new (home) NqBin<Val,IntView,IntView>
528  (home,share,p,y[0],y[1],-c);
529  }
530  template<class Val>
532  nqtobin(Space& home, bool share, Propagator& p,
533  ViewArray<IntView>& x, ViewArray<IntView>& y, Val c) {
534  if (x.size() == 2)
535  return new (home) NqBin<Val,IntView,IntView>
536  (home,share,p,x[0],x[1],c);
537  if (x.size() == 1)
538  return new (home) NqBin<Val,IntView,MinusView>
539  (home,share,p,x[0],MinusView(y[0]),c);
540  return new (home) NqBin<Val,IntView,IntView>
541  (home,share,p,y[0],y[1],-c);
542  }
543 
548  template<class Val, class P, class N>
551  return NULL;
552  }
553  template<class Val>
555  nqtoter(Space& home, bool share, Propagator& p,
557  assert(x.size() == 3);
558  return new (home) NqTer<Val,IntView,IntView,IntView>
559  (home,share,p,x[0],x[1],x[2],c);
560  }
561  template<class Val>
563  nqtoter(Space& home, bool share, Propagator& p,
565  assert(y.size() == 3);
566  return new (home) NqTer<Val,IntView,IntView,IntView>
567  (home,share,p,y[0],y[1],y[2],-c);
568  }
569  template<class Val>
571  nqtoter(Space& home, bool share, Propagator& p,
572  ViewArray<IntView>& x, ViewArray<IntView>& y, Val c) {
573  if (x.size() == 3)
574  return new (home) NqTer<Val,IntView,IntView,IntView>
575  (home,share,p,x[0],x[1],x[2],c);
576  if (x.size() == 2)
577  return new (home) NqTer<Val,IntView,IntView,MinusView>
578  (home,share,p,x[0],x[1],MinusView(y[0]),c);
579  if (x.size() == 1)
580  return new (home) NqTer<Val,IntView,IntView,MinusView>
581  (home,share,p,y[0],y[1],MinusView(x[0]),-c);
582  return new (home) NqTer<Val,IntView,IntView,IntView>
583  (home,share,p,y[0],y[1],y[2],-c);
584  }
585 
586  template<class Val, class P, class N>
587  Actor*
588  Nq<Val,P,N>::copy(Space& home, bool share) {
589  if (isunit(x,y)) {
590  // Check whether rewriting is possible
591  if (x.size() + y.size() == 2)
592  return nqtobin(home,share,*this,x,y,c);
593  if (x.size() + y.size() == 3)
594  return nqtoter(home,share,*this,x,y,c);
595  }
596  return new (home) Nq<Val,P,N>(home,share,*this);
597  }
598 
599  template<class Val, class P, class N>
600  ExecStatus
602  for (int i = x.size(); i--; )
603  if (x[i].assigned()) {
604  c -= x[i].val(); x.move_lst(i);
605  }
606  for (int i = y.size(); i--; )
607  if (y[i].assigned()) {
608  c += y[i].val(); y.move_lst(i);
609  }
610  if (x.size() + y.size() <= 1) {
611  if (x.size() == 1) {
612  GECODE_ME_CHECK(x[0].nq(home,c)); return home.ES_SUBSUMED(*this);
613  }
614  if (y.size() == 1) {
615  GECODE_ME_CHECK(y[0].nq(home,-c)); return home.ES_SUBSUMED(*this);
616  }
617  return (c == static_cast<Val>(0)) ?
618  ES_FAILED : home.ES_SUBSUMED(*this);
619  }
620  return ES_FIX;
621  }
622 
623 
624  /*
625  * Bound consistent linear inequation
626  *
627  */
628 
629  template<class Val, class P, class N>
632  : Lin<Val,P,N,PC_INT_BND>(home,x,y,c) {}
633 
634  template<class Val, class P, class N>
635  ExecStatus
637  ViewArray<NoView> nva;
638  if (y.size() == 0) {
639  (void) new (home) Lq<Val,P,NoView>(home,x,nva,c);
640  } else if (x.size() == 0) {
641  (void) new (home) Lq<Val,NoView,N>(home,nva,y,c);
642  } else {
643  (void) new (home) Lq<Val,P,N>(home,x,y,c);
644  }
645  return ES_OK;
646  }
647 
648 
649  template<class Val, class P, class N>
651  Lq<Val,P,N>::Lq(Space& home, bool share, Lq<Val,P,N>& p)
652  : Lin<Val,P,N,PC_INT_BND>(home,share,p) {}
653 
658  template<class Val, class P, class N>
661  return NULL;
662  }
663  template<class Val>
665  lqtobin(Space& home, bool share, Propagator& p,
667  assert(x.size() == 2);
668  return new (home) LqBin<Val,IntView,IntView>
669  (home,share,p,x[0],x[1],c);
670  }
671  template<class Val>
673  lqtobin(Space& home, bool share, Propagator& p,
675  assert(y.size() == 2);
676  return new (home) LqBin<Val,MinusView,MinusView>
677  (home,share,p,MinusView(y[0]),MinusView(y[1]),c);
678  }
679  template<class Val>
681  lqtobin(Space& home, bool share, Propagator& p,
682  ViewArray<IntView>& x, ViewArray<IntView>& y, Val c) {
683  if (x.size() == 2)
684  return new (home) LqBin<Val,IntView,IntView>
685  (home,share,p,x[0],x[1],c);
686  if (x.size() == 1)
687  return new (home) LqBin<Val,IntView,MinusView>
688  (home,share,p,x[0],MinusView(y[0]),c);
689  return new (home) LqBin<Val,MinusView,MinusView>
690  (home,share,p,MinusView(y[0]),MinusView(y[1]),c);
691  }
692 
697  template<class Val, class P, class N>
700  return NULL;
701  }
702  template<class Val>
704  lqtoter(Space& home, bool share, Propagator& p,
706  assert(x.size() == 3);
707  return new (home) LqTer<Val,IntView,IntView,IntView>
708  (home,share,p,x[0],x[1],x[2],c);
709  }
710  template<class Val>
712  lqtoter(Space& home, bool share, Propagator& p,
714  assert(y.size() == 3);
716  (home,share,p,MinusView(y[0]),MinusView(y[1]),MinusView(y[2]),c);
717  }
718  template<class Val>
720  lqtoter(Space& home, bool share, Propagator& p,
721  ViewArray<IntView>& x, ViewArray<IntView>& y, Val c) {
722  if (x.size() == 3)
723  return new (home) LqTer<Val,IntView,IntView,IntView>
724  (home,share,p,x[0],x[1],x[2],c);
725  if (x.size() == 2)
726  return new (home) LqTer<Val,IntView,IntView,MinusView>
727  (home,share,p,x[0],x[1],MinusView(y[0]),c);
728  if (x.size() == 1)
730  (home,share,p,x[0],MinusView(y[0]),MinusView(y[1]),c);
732  (home,share,p,MinusView(y[0]),MinusView(y[1]),MinusView(y[2]),c);
733  }
734 
735  template<class Val, class P, class N>
736  Actor*
737  Lq<Val,P,N>::copy(Space& home, bool share) {
738  if (isunit(x,y)) {
739  // Check whether rewriting is possible
740  if (x.size() + y.size() == 2)
741  return lqtobin(home,share,*this,x,y,c);
742  if (x.size() + y.size() == 3)
743  return lqtoter(home,share,*this,x,y,c);
744  }
745  return new (home) Lq<Val,P,N>(home,share,*this);
746  }
747 
748  template<class Val, class P, class N>
749  ExecStatus
751  // Eliminate singletons
752  Val sl = 0;
753 
754  if (IntView::me(med) == ME_INT_VAL) {
755  for (int i = x.size(); i--; ) {
756  Val m = x[i].min();
757  if (x[i].assigned()) {
758  c -= m; x.move_lst(i);
759  } else {
760  sl -= m;
761  }
762  }
763  for (int i = y.size(); i--; ) {
764  Val m = y[i].max();
765  if (y[i].assigned()) {
766  c += m; y.move_lst(i);
767  } else {
768  sl += m;
769  }
770  }
771  if ((x.size() + y.size()) <= 1) {
772  if (x.size() == 1) {
773  GECODE_ME_CHECK(x[0].lq(home,c));
774  return home.ES_SUBSUMED(*this);
775  }
776  if (y.size() == 1) {
777  GECODE_ME_CHECK(y[0].gq(home,-c));
778  return home.ES_SUBSUMED(*this);
779  }
780  return (c >= static_cast<Val>(0)) ?
781  home.ES_SUBSUMED(*this) : ES_FAILED;
782  }
783  } else {
784  for (int i = x.size(); i--; )
785  sl -= x[i].min();
786  for (int i = y.size(); i--; )
787  sl += y[i].max();
788  }
789 
790  sl += c;
791 
792  ExecStatus es = ES_FIX;
793  bool assigned = true;
794  for (int i = x.size(); i--; ) {
795  assert(!x[i].assigned());
796  Val slx = sl + x[i].min();
797  ModEvent me = x[i].lq(home,slx);
798  if (me == ME_INT_FAILED)
799  return ES_FAILED;
800  if (me != ME_INT_VAL)
801  assigned = false;
802  if (me_modified(me) && (slx != x[i].max()))
803  es = ES_NOFIX;
804  }
805 
806  for (int i = y.size(); i--; ) {
807  assert(!y[i].assigned());
808  Val sly = y[i].max() - sl;
809  ModEvent me = y[i].gq(home,sly);
810  if (me == ME_INT_FAILED)
811  return ES_FAILED;
812  if (me != ME_INT_VAL)
813  assigned = false;
814  if (me_modified(me) && (sly != y[i].min()))
815  es = ES_NOFIX;
816  }
817  return assigned ? home.ES_SUBSUMED(*this) : es;
818  }
819 
820  /*
821  * Reified bound consistent linear inequation
822  *
823  */
824 
825  template<class Val, class P, class N, ReifyMode rm>
828  ViewArray<P>& x, ViewArray<N>& y, Val c, BoolView b)
829  : ReLin<Val,P,N,PC_INT_BND,BoolView>(home,x,y,c,b) {}
830 
831  template<class Val, class P, class N, ReifyMode rm>
832  ExecStatus
834  ViewArray<P>& x, ViewArray<N>& y, Val c, BoolView b) {
835  ViewArray<NoView> nva;
836  if (y.size() == 0) {
837  (void) new (home) ReLq<Val,P,NoView,rm>(home,x,nva,c,b);
838  } else if (x.size() == 0) {
839  (void) new (home) ReLq<Val,NoView,N,rm>(home,nva,y,c,b);
840  } else {
841  (void) new (home) ReLq<Val,P,N,rm>(home,x,y,c,b);
842  }
843  return ES_OK;
844  }
845 
846 
847  template<class Val, class P, class N, ReifyMode rm>
850  : ReLin<Val,P,N,PC_INT_BND,BoolView>(home,share,p) {}
851 
852  template<class Val, class P, class N, ReifyMode rm>
853  Actor*
854  ReLq<Val,P,N,rm>::copy(Space& home, bool share) {
855  return new (home) ReLq<Val,P,N,rm>(home,share,*this);
856  }
857 
858  template<class Val, class P, class N, ReifyMode rm>
859  ExecStatus
861  if (b.zero()) {
862  if (rm == RM_IMP)
863  return home.ES_SUBSUMED(*this);
864  GECODE_REWRITE(*this,(Lq<Val,N,P>::post(home(*this),y,x,-c-1)));
865  }
866  if (b.one()) {
867  if (rm == RM_PMI)
868  return home.ES_SUBSUMED(*this);
869  GECODE_REWRITE(*this,(Lq<Val,P,N>::post(home(*this),x,y,c)));
870  }
871 
872  // Eliminate singletons
873  Val sl = 0;
874  Val su = 0;
875 
876  bounds_p<Val,P>(med,x,c,sl,su);
877  bounds_n<Val,N>(med,y,c,sl,su);
878 
879  if (-sl > c) {
880  if (rm != RM_PMI)
881  GECODE_ME_CHECK(b.zero_none(home));
882  return home.ES_SUBSUMED(*this);
883  }
884  if (-su <= c) {
885  if (rm != RM_IMP)
886  GECODE_ME_CHECK(b.one_none(home));
887  return home.ES_SUBSUMED(*this);
888  }
889 
890  return ES_FIX;
891  }
892 
893 }}}
894 
895 // STATISTICS: int-prop
896 
Propagator for bounds consistent binary linear disequality
Definition: linear.hh:205
void mod(Home home, IntVar x0, IntVar x1, IntVar x2, IntPropLevel ipl)
Post propagator for .
Definition: arithmetic.cpp:277
ReEq(Space &home, bool share, ReEq &p)
Constructor for cloning p.
Definition: int-nary.hpp:431
#define GECODE_REWRITE(prop, post)
Rewrite propagator by executing post function.
Definition: macros.hpp:120
bool isunit(ViewArray< P > &, ViewArray< N > &)
Test if only unit-coefficient arrays used.
Definition: int-nary.hpp:48
static ExecStatus post(Home home, ViewArray< P > &x, ViewArray< N > &y, Val c)
Post propagator for .
Definition: int-nary.hpp:487
Propagator for bounds consistent n-ary linear equality
Definition: linear.hh:581
Lq(Space &home, bool share, Lq &p)
Constructor for cloning p.
Definition: int-nary.hpp:651
bool zero(void) const
Test whether view is assigned to be zero.
Definition: bool.hpp:214
void linear(Home home, const FloatVarArgs &x, FloatRelType frt, FloatNum c)
Post propagator for .
Definition: linear.cpp:45
Inverse implication for reification.
Definition: int.hh:848
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:1669
ViewArray< N > y
Array of negative views.
Definition: linear.hh:506
Propagator for reified bounds consistent n-ary linear less or equal
Definition: linear.hh:753
ExecStatus ES_SUBSUMED(Propagator &p)
Definition: core.hpp:3484
const FloatNum max
Largest allowed float value.
Definition: float.hh:846
static ExecStatus post(Home home, ViewArray< P > &x, ViewArray< N > &y, Val c)
Post propagator for .
Definition: int-nary.hpp:284
Propagator for bounds consistent n-ary linear disequality
Definition: linear.hh:687
bool one(void) const
Test whether view is assigned to be one.
Definition: bool.hpp:218
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:57
Propagator for bounds consistent ternary linear equality
Definition: linear.hh:388
ExecStatus prop_bnd(Space &home, ModEventDelta med, Propagator &p, ViewArray< P > &x, ViewArray< N > &y, Val &c)
Definition: int-nary.hpp:187
int ModEvent
Type for modification events.
Definition: core.hpp:142
Base-class for reified n-ary linear propagators.
Definition: linear.hh:533
Base-class for propagators.
Definition: core.hpp:1012
Actor * lqtobin(Space &, bool, Propagator &, ViewArray< P > &, ViewArray< N > &, Val)
Rewriting of inequality to binary propagators.
Definition: int-nary.hpp:660
Base-class for n-ary linear propagators.
Definition: linear.hh:501
Propagation has computed fixpoint.
Definition: core.hpp:541
Propagator for bounds consistent binary linear equality
Definition: linear.hh:138
Computation spaces.
Definition: core.hpp:1672
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: int-nary.hpp:601
Actor * lqtoter(Space &, bool, Propagator &, ViewArray< P > &, ViewArray< N > &, Val)
Rewriting of inequality to ternary propagators.
Definition: int-nary.hpp:699
Base-class for both propagators and branchers.
Definition: core.hpp:682
Actor * eqtoter(Space &, bool, Propagator &, ViewArray< P > &, ViewArray< N > &, Val)
Rewriting of equality to ternary propagators.
Definition: int-nary.hpp:347
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: int-nary.hpp:443
ViewArray< P > x
Array of positive views.
Definition: linear.hh:504
const Gecode::ModEvent ME_INT_FAILED
Domain operation has resulted in failure.
Definition: var-type.hpp:52
virtual Actor * copy(Space &home, bool share)
Create copy during cloning.
Definition: int-nary.hpp:385
Propagator for bounds consistent ternary linear less or equal
Definition: linear.hh:458
Gecode::FloatVal c(-8, 8)
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: int-nary.hpp:398
int p
Number of positive literals for node type.
Definition: bool-expr.cpp:236
const FloatNum min
Smallest allowed float value.
Definition: float.hh:848
Gecode::IntArgs i(4, 1, 2, 3, 4)
static ExecStatus post(Home home, ViewArray< P > &x, ViewArray< N > &y, Val c, BoolView b)
Post propagator for .
Definition: int-nary.hpp:833
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:238
Execution has resulted in failure.
Definition: core.hpp:538
ModEvent zero_none(Space &home)
Assign not yet assigned view to zero.
Definition: bool.hpp:232
void bounds_n(ModEventDelta med, ViewArray< View > &y, Val &c, Val &sl, Val &su)
Definition: int-nary.hpp:165
const Gecode::PropCond PC_INT_BND
Propagate when minimum or maximum of a view changes.
Definition: var-type.hpp:91
Actor * eqtobin(Space &, bool, Propagator &, ViewArray< P > &, ViewArray< N > &, Val)
Rewriting of equality to binary propagators.
Definition: int-nary.hpp:308
const Gecode::ModEvent ME_INT_VAL
Domain operation has resulted in a value (assigned variable)
Definition: var-type.hpp:56
ModEventDelta med
A set of modification events (used during propagation)
Definition: core.hpp:1022
Propagator for bounds consistent binary linear less or equal
Definition: linear.hh:241
virtual Actor * copy(Space &home, bool share)
Create copy during cloning.
Definition: int-nary.hpp:588
size_t size
The size of the propagator (used during subsumption)
Definition: core.hpp:1024
Propagator for reified bounds consistent n-ary linear equality
Definition: linear.hh:653
Nq(Space &home, bool share, Nq &p)
Constructor for cloning p.
Definition: int-nary.hpp:502
void bounds_p(ModEventDelta med, ViewArray< View > &x, Val &c, Val &sl, Val &su)
Definition: int-nary.hpp:144
#define GECODE_ME_CHECK(me)
Check whether modification event me is failed, and forward failure.
Definition: macros.hpp:56
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: int-nary.hpp:750
Lin(Space &home, bool share, Lin< Val, P, N, pc > &p)
Constructor for cloning p.
Definition: int-nary.hpp:73
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition: arithmetic.cpp:75
Eq(Space &home, bool share, Eq &p)
Constructor for cloning p.
Definition: int-nary.hpp:299
static ExecStatus post(Home home, ViewArray< P > &x, ViewArray< N > &y, Val c, Ctrl b)
Post propagator for .
Definition: int-nary.hpp:415
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:253
static ExecStatus post(Home home, ViewArray< P > &x, ViewArray< N > &y, Val c)
Post propagator for .
Definition: int-nary.hpp:636
Propagation cost.
Definition: core.hpp:550
virtual Actor * copy(Space &home, bool share)
Create copy during cloning.
Definition: int-nary.hpp:854
virtual ExecStatus propagate(Space &home, const ModEventDelta &med)
Perform propagation.
Definition: int-nary.hpp:860
ExecStatus
Definition: core.hpp:536
Minus integer view.
Definition: view.hpp:276
bool assigned(View x, int v)
Whether x is assigned to value v.
Definition: single.hpp:47
ReLq(Space &home, bool share, ReLq &p)
Constructor for cloning p.
Definition: int-nary.hpp:849
static ModEvent me(const ModEventDelta &med)
Return modification event for view type in med.
Definition: view.hpp:502
#define forceinline
Definition: config.hpp:173
bool me_modified(ModEvent me)
Check whether modification event me describes variable modification.
Definition: modevent.hpp:63
Execution is okay.
Definition: core.hpp:540
Propagation has not computed fixpoint.
Definition: core.hpp:539
Ctrl b
Control view for reification.
Definition: linear.hh:538
virtual Actor * copy(Space &home, bool share)
Create copy during cloning.
Definition: int-nary.hpp:737
Gecode toplevel namespace
Propagator for bounds consistent n-ary linear less or equal
Definition: linear.hh:720
Actor * nqtoter(Space &, bool, Propagator &, ViewArray< P > &, ViewArray< N > &, Val)
Rewriting of disequality to ternary propagators.
Definition: int-nary.hpp:550
Implication for reification.
Definition: int.hh:841
virtual void reschedule(Space &home)
Schedule function.
Definition: int-nary.hpp:87
ModEvent one_none(Space &home)
Assign not yet assigned view to one.
Definition: bool.hpp:236
void reschedule(Space &home, Propagator &p, IntSet &y)
Definition: rel.hpp:96
virtual Actor * copy(Space &home, bool share)
Create copy during cloning.
Definition: int-nary.hpp:437
struct Gecode::@554::NNF::@60::@61 b
For binary nodes (and, or, eqv)
Propagator for bounds consistent ternary linear disquality
Definition: linear.hh:423
int size(void) const
Return size of array (number of elements)
Definition: array.hpp:1215
int ModEventDelta
Modification event deltas.
Definition: core.hpp:169
Home class for posting propagators
Definition: core.hpp:905
bool me_failed(ModEvent me)
Check whether modification event me is failed.
Definition: modevent.hpp:58
Actor * nqtobin(Space &, bool, Propagator &, ViewArray< P > &, ViewArray< N > &, Val)
Rewriting of disequality to binary propagators.
Definition: int-nary.hpp:511
const Gecode::PropCond PC_INT_VAL
Propagate when a view becomes assigned (single value)
Definition: var-type.hpp:82
const Gecode::PropCond PC_BOOL_VAL
Propagate when a view becomes assigned (single value)
Definition: var-type.hpp:126
Boolean view for Boolean variables.
Definition: view.hpp:1315