Generated on Tue Mar 5 2013 22:37:22 for Gecode by doxygen 1.8.3.1
bool-int.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  * Tias Guns <tias.guns@cs.kuleuven.be>
6  *
7  * Copyright:
8  * Christian Schulte, 2006
9  * Tias Guns, 2009
10  *
11  * Last modified:
12  * $Date: 2010-04-08 20:35:31 +1000 (Thu, 08 Apr 2010) $ by $Author: schulte $
13  * $Revision: 10684 $
14  *
15  * This file is part of Gecode, the generic constraint
16  * development environment:
17  * http://www.gecode.org
18  *
19  * Permission is hereby granted, free of charge, to any person obtaining
20  * a copy of this software and associated documentation files (the
21  * "Software"), to deal in the Software without restriction, including
22  * without limitation the rights to use, copy, modify, merge, publish,
23  * distribute, sublicense, and/or sell copies of the Software, and to
24  * permit persons to whom the Software is furnished to do so, subject to
25  * the following conditions:
26  *
27  * The above copyright notice and this permission notice shall be
28  * included in all copies or substantial portions of the Software.
29  *
30  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
31  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
32  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
33  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
34  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
35  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
36  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
37  *
38  */
39 
40 #include <algorithm>
41 
42 #include <gecode/int/bool.hh>
43 
44 namespace Gecode { namespace Int { namespace Linear {
45 
46  /*
47  * Baseclass for integer Boolean sum using dependencies
48  *
49  */
50  template<class VX>
53  int n_s, int c0)
54  : Propagator(home), co(home), x(x0), n_as(n_s), n_hs(n_s), c(c0) {
55  Advisor* a = new (home) Advisor(home,*this,co);
56  for (int i=n_as; i--; )
57  x[i].subscribe(home,*a);
58  }
59 
60  template<class VX>
61  forceinline void
63  if (n_as != n_hs) {
64  // Remove views for which no more subscriptions exist
65  int n_x = x.size();
66  for (int i=n_hs; i--; )
67  if (!x[i].none()) {
68  x[i]=x[--n_hs]; x[n_hs]=x[--n_x];
69  }
70  x.size(n_x);
71  }
72  assert(n_as == n_hs);
73  // Remove assigned yet unsubscribed views
74  {
75  int n_x = x.size();
76  for (int i=n_x-1; i>=n_hs; i--)
77  if (x[i].one()) {
78  c--; x[i]=x[--n_x];
79  } else if (x[i].zero()) {
80  x[i]=x[--n_x];
81  }
82  x.size(n_x);
83  }
84  }
85 
86  template<class VX>
89  : Propagator(home,share,p), n_as(p.n_as), n_hs(n_as) {
90  p.normalize();
91  c=p.c;
92  co.update(home,share,p.co);
93  x.update(home,share,p.x);
94  }
95 
96  template<class VX>
97  PropCost
98  LinBoolInt<VX>::cost(const Space&, const ModEventDelta&) const {
100  }
101 
102  template<class VX>
103  forceinline size_t
105  Advisors<Advisor> as(co);
106  for (int i=n_hs; i--; )
107  x[i].cancel(home,as.advisor());
108  co.dispose(home);
109  (void) Propagator::dispose(home);
110  return sizeof(*this);
111  }
112 
113  /*
114  * Greater or equal propagator (integer rhs)
115  *
116  */
117  template<class VX>
120  : LinBoolInt<VX>(home,x,c+1,c) {}
121 
122  template<class VX>
125  : LinBoolInt<VX>(home,share,p) {}
126 
127  template<class VX>
128  Actor*
129  GqBoolInt<VX>::copy(Space& home, bool share) {
130  return new (home) GqBoolInt<VX>(home,share,*this);
131  }
132 
133  template<class VX>
134  ExecStatus
136  // Check whether propagator is running
137  if (n_as == 0)
138  return ES_FIX;
139 
140  if (VX::one(d)) {
141  c--; goto check;
142  }
143  if (c+1 < n_as)
144  goto check;
145  // Find a new subscription
146  for (int i = x.size()-1; i>=n_hs; i--)
147  if (x[i].none()) {
148  std::swap(x[i],x[n_hs]);
149  x[n_hs++].subscribe(home,a);
150  x.size(i+1);
151  return ES_FIX;
152  } else if (x[i].one()) {
153  c--;
154  if (c+1 < n_as) {
155  x.size(i);
156  assert(n_hs <= x.size());
157  goto check;
158  }
159  }
160  // No view left for subscription
161  x.size(n_hs);
162  check:
163  // Do not update subscription
164  n_as--;
165  int n = x.size()-n_hs+n_as;
166  if (n < c)
167  return ES_FAILED;
168  if ((c <= 0) || (c == n))
169  return ES_NOFIX;
170  else
171  return ES_FIX;
172  }
173 
174  template<class VX>
175  ExecStatus
177  if (c > 0) {
178  assert((n_as == c) && (x.size() == n_hs));
179  // Signal that propagator is running
180  n_as = 0;
181  // All views must be one to satisfy inequality
182  for (int i=n_hs; i--; )
183  if (x[i].none())
184  GECODE_ME_CHECK(x[i].one_none(home));
185  }
186  return home.ES_SUBSUMED(*this);
187  }
188 
189  template<class VX>
190  ExecStatus
192  // Eliminate assigned views
193  int n_x = x.size();
194  for (int i=n_x; i--; )
195  if (x[i].zero()) {
196  x[i] = x[--n_x];
197  } else if (x[i].one()) {
198  x[i] = x[--n_x]; c--;
199  }
200  x.size(n_x);
201  // RHS too large
202  if (n_x < c)
203  return ES_FAILED;
204  // Whatever the x[i] take for values, the inequality is subsumed
205  if (c <= 0)
206  return ES_OK;
207  // Use Boolean disjunction for this special case
208  if (c == 1)
209  return Bool::NaryOrTrue<VX>::post(home,x);
210  // All views must be one to satisfy inequality
211  if (c == n_x) {
212  for (int i=n_x; i--; )
213  GECODE_ME_CHECK(x[i].one_none(home));
214  return ES_OK;
215  }
216  // This is the needed invariant as c+1 subscriptions must be created
217  assert(n_x > c);
218  (void) new (home) GqBoolInt<VX>(home,x,c);
219  return ES_OK;
220  }
221 
222 
223 
224 
225  /*
226  * Equal propagator (integer rhs)
227  *
228  */
229  template<class VX>
232  : LinBoolInt<VX>(home,x,std::max(c,x.size()-c)+1,c) {}
233 
234  template<class VX>
237  : LinBoolInt<VX>(home,share,p) {}
238 
239  template<class VX>
240  Actor*
241  EqBoolInt<VX>::copy(Space& home, bool share) {
242  return new (home) EqBoolInt<VX>(home,share,*this);
243  }
244 
245  template<class VX>
246  ExecStatus
248  // Check whether propagator is running
249  if (n_as == 0)
250  return ES_FIX;
251 
252  if (VX::one(d))
253  c--;
254  if ((c+1 < n_as) && (x.size()-n_hs < c))
255  goto check;
256  // Find a new subscription
257  for (int i = x.size()-1; i>=n_hs; i--)
258  if (x[i].none()) {
259  std::swap(x[i],x[n_hs]);
260  x[n_hs++].subscribe(home,a);
261  x.size(i+1);
262  return ES_FIX;
263  } else if (x[i].one()) {
264  c--;
265  }
266  // No view left for subscription
267  x.size(n_hs);
268  check:
269  // Do not update subscription
270  n_as--;
271  int n = x.size()-n_hs+n_as;
272  if ((c < 0) || (c > n))
273  return ES_FAILED;
274  if ((c == 0) || (c == n))
275  return ES_NOFIX;
276  else
277  return ES_FIX;
278  }
279 
280  template<class VX>
281  ExecStatus
283  assert(x.size() == n_hs);
284  // Signal that propagator is running
285  n_as = 0;
286  if (c == 0) {
287  // All views must be zero to satisfy equality
288  for (int i=n_hs; i--; )
289  if (x[i].none())
290  GECODE_ME_CHECK(x[i].zero_none(home));
291  } else {
292  // All views must be one to satisfy equality
293  for (int i=n_hs; i--; )
294  if (x[i].none())
295  GECODE_ME_CHECK(x[i].one_none(home));
296  }
297  return home.ES_SUBSUMED(*this);
298  }
299 
300  template<class VX>
301  ExecStatus
303  // Eliminate assigned views
304  int n_x = x.size();
305  for (int i=n_x; i--; )
306  if (x[i].zero()) {
307  x[i] = x[--n_x];
308  } else if (x[i].one()) {
309  x[i] = x[--n_x]; c--;
310  }
311  x.size(n_x);
312  // RHS too small or too large
313  if ((c < 0) || (c > n_x))
314  return ES_FAILED;
315  // All views must be zero to satisfy equality
316  if (c == 0) {
317  for (int i=n_x; i--; )
318  GECODE_ME_CHECK(x[i].zero_none(home));
319  return ES_OK;
320  }
321  // All views must be one to satisfy equality
322  if (c == n_x) {
323  for (int i=n_x; i--; )
324  GECODE_ME_CHECK(x[i].one_none(home));
325  return ES_OK;
326  }
327  (void) new (home) EqBoolInt<VX>(home,x,c);
328  return ES_OK;
329  }
330 
331 
332  /*
333  * Integer disequal to Boolean sum
334  *
335  */
336 
337  template<class VX>
340  : BinaryPropagator<VX,PC_INT_VAL>(home,
341  b[b.size()-2],
342  b[b.size()-1]), x(b), c(c0) {
343  assert(x.size() >= 2);
344  x.size(x.size()-2);
345  }
346 
347  template<class VX>
348  forceinline size_t
351  return sizeof(*this);
352  }
353 
354  template<class VX>
357  : BinaryPropagator<VX,PC_INT_VAL>(home,share,p), x(home,p.x.size()) {
358  // Eliminate all zeros and ones in original and update
359  int n = p.x.size();
360  int p_c = p.c;
361  for (int i=n; i--; )
362  if (p.x[i].zero()) {
363  n--; p.x[i]=p.x[n]; x[i]=x[n];
364  } else if (p.x[i].one()) {
365  n--; p_c--; p.x[i]=p.x[n]; x[i]=x[n];
366  } else {
367  x[i].update(home,share,p.x[i]);
368  }
369  c = p_c; p.c = p_c;
370  x.size(n); p.x.size(n);
371  }
372 
373  template<class VX>
376  int n = x.size();
377  for (int i=n; i--; )
378  if (x[i].one()) {
379  x[i]=x[--n]; c--;
380  } else if (x[i].zero()) {
381  x[i]=x[--n];
382  }
383  x.size(n);
384  if ((n < c) || (c < 0))
385  return ES_OK;
386  if (n == 0)
387  return (c == 0) ? ES_FAILED : ES_OK;
388  if (n == 1) {
389  if (c == 1) {
390  GECODE_ME_CHECK(x[0].zero_none(home));
391  } else {
392  GECODE_ME_CHECK(x[0].one_none(home));
393  }
394  return ES_OK;
395  }
396  (void) new (home) NqBoolInt(home,x,c);
397  return ES_OK;
398  }
399 
400  template<class VX>
401  Actor*
402  NqBoolInt<VX>::copy(Space& home, bool share) {
403  return new (home) NqBoolInt<VX>(home,share,*this);
404  }
405 
406  template<class VX>
407  PropCost
408  NqBoolInt<VX>::cost(const Space&, const ModEventDelta&) const {
409  return PropCost::linear(PropCost::LO, x.size());
410  }
411 
412  template<class VX>
413  forceinline bool
415  if (y.one())
416  c--;
417  int n = x.size();
418  for (int i=n; i--; )
419  if (x[i].one()) {
420  c--; x[i]=x[--n];
421  } else if (x[i].zero()) {
422  x[i] = x[--n];
423  } else {
424  // New unassigned view found
425  assert(!x[i].zero() && !x[i].one());
426  // Move to y and subscribe
427  y=x[i]; x[i]=x[--n];
428  x.size(n);
429  y.subscribe(home,*this,PC_INT_VAL,false);
430  return true;
431  }
432  // All views have been assigned!
433  x.size(0);
434  return false;
435  }
436 
437  template<class VX>
438  ExecStatus
440  bool s0 = true;
441  if (x0.zero() || x0.one())
442  s0 = resubscribe(home,x0);
443  bool s1 = true;
444  if (x1.zero() || x1.one())
445  s1 = resubscribe(home,x1);
446  int n = x.size() + s0 + s1;
447  if ((n < c) || (c < 0))
448  return home.ES_SUBSUMED(*this);
449  if (n == 0)
450  return (c == 0) ? ES_FAILED : home.ES_SUBSUMED(*this);
451  if (n == 1) {
452  if (s0) {
453  if (c == 1) {
454  GECODE_ME_CHECK(x0.zero_none(home));
455  } else {
456  GECODE_ME_CHECK(x0.one_none(home));
457  }
458  } else {
459  assert(s1);
460  if (c == 1) {
461  GECODE_ME_CHECK(x1.zero_none(home));
462  } else {
463  GECODE_ME_CHECK(x1.one_none(home));
464  }
465  }
466  return home.ES_SUBSUMED(*this);
467  }
468  return ES_FIX;
469  }
470 
471  /*
472  * Baseclass for reified integer Boolean sum
473  *
474  */
475  template<class VX, class VB>
478  int c0, VB b0)
479  : Propagator(home), co(home), x(x0), n_s(x.size()), c(c0), b(b0) {
480  x.subscribe(home,*new (home) Advisor(home,*this,co));
481  b.subscribe(home,*this,PC_BOOL_VAL);
482  }
483 
484  template<class VX, class VB>
485  forceinline void
487  if (n_s != x.size()) {
488  int n_x = x.size();
489  for (int i=n_x; i--; )
490  if (!x[i].none())
491  x[i] = x[--n_x];
492  x.size(n_x);
493  assert(x.size() == n_s);
494  }
495  }
496 
497  template<class VX, class VB>
501  : Propagator(home,share,p), n_s(p.n_s), c(p.c) {
502  p.normalize();
503  co.update(home,share,p.co);
504  x.update(home,share,p.x);
505  b.update(home,share,p.b);
506  }
507 
508  template<class VX, class VB>
509  forceinline size_t
511  Advisors<Advisor> as(co);
512  x.cancel(home,as.advisor());
513  co.dispose(home);
514  b.cancel(home,*this,PC_BOOL_VAL);
515  (void) Propagator::dispose(home);
516  return sizeof(*this);
517  }
518 
519  template<class VX, class VB>
520  PropCost
523  }
524 
525 
526  template<>
529  public:
534  NegBoolView y(x); return y;
535  }
536  };
537 
538  template<>
541  public:
543  typedef BoolView NegView;
546  return x.base();
547  }
548  };
549 
550 
551  /*
552  * Reified greater or equal propagator (integer rhs)
553  *
554  */
555  template<class VX, class VB>
558  : ReLinBoolInt<VX,VB>(home,x,c,b) {}
559 
560  template<class VX, class VB>
564  : ReLinBoolInt<VX,VB>(home,share,p) {}
565 
566  template<class VX, class VB>
567  Actor*
568  ReGqBoolInt<VX,VB>::copy(Space& home, bool share) {
569  return new (home) ReGqBoolInt<VX,VB>(home,share,*this);
570  }
571 
572  template<class VX, class VB>
573  ExecStatus
575  if (VX::one(d))
576  c--;
577  n_s--;
578  if ((n_s < c) || (c <= 0))
579  return ES_NOFIX;
580  else
581  return ES_FIX;
582  }
583 
584  template<class VX, class VB>
585  ExecStatus
587  if (b.none()) {
588  if (c <= 0) {
589  GECODE_ME_CHECK(b.one_none(home));
590  } else {
591  GECODE_ME_CHECK(b.zero_none(home));
592  }
593  } else {
594  normalize();
595  if (b.one()) {
596  GECODE_REWRITE(*this,(GqBoolInt<VX>::post(home(*this),x,c)));
597  } else {
599  for (int i=x.size(); i--; )
600  nx[i]=BoolNegTraits<VX>::neg(x[i]);
602  ::post(home(*this),nx,x.size()-c+1));
603  }
604  }
605  return home.ES_SUBSUMED(*this);
606  }
607 
608  template<class VX, class VB>
609  ExecStatus
611  assert(!b.assigned()); // checked before posting
612 
613  // Eliminate assigned views
614  int n_x = x.size();
615  for (int i=n_x; i--; )
616  if (x[i].zero()) {
617  x[i] = x[--n_x];
618  } else if (x[i].one()) {
619  x[i] = x[--n_x]; c--;
620  }
621  x.size(n_x);
622  if (n_x < c) {
623  // RHS too large
624  GECODE_ME_CHECK(b.zero_none(home));
625  } else if (c <= 0) {
626  // Whatever the x[i] take for values, the inequality is subsumed
627  GECODE_ME_CHECK(b.one_none(home));
628  } else if (c == 1) {
629  // Equivalent to Boolean disjunction
630  return Bool::NaryOr<VX,VB>::post(home,x,b);
631  } else if (c == n_x) {
632  // Equivalent to Boolean conjunction, transform to Boolean disjunction
634  for (int i=n_x; i--; )
635  nx[i]=BoolNegTraits<VX>::neg(x[i]);
636  return Bool::NaryOr
637  <typename BoolNegTraits<VX>::NegView,
639  ::post(home,nx,BoolNegTraits<VB>::neg(b));
640  } else {
641  (void) new (home) ReGqBoolInt<VX,VB>(home,x,c,b);
642  }
643  return ES_OK;
644  }
645 
646  /*
647  * Reified equal propagator (integer rhs)
648  *
649  */
650  template<class VX, class VB>
653  : ReLinBoolInt<VX,VB>(home,x,c,b) {}
654 
655  template<class VX, class VB>
659  : ReLinBoolInt<VX,VB>(home,share,p) {}
660 
661  template<class VX, class VB>
662  Actor*
663  ReEqBoolInt<VX,VB>::copy(Space& home, bool share) {
664  return new (home) ReEqBoolInt<VX,VB>(home,share,*this);
665  }
666 
667  template<class VX, class VB>
668  ExecStatus
670  if (VX::one(d))
671  c--;
672  n_s--;
673 
674  if ((c < 0) || (c > n_s) || (n_s == 0))
675  return ES_NOFIX;
676  else
677  return ES_FIX;
678  }
679 
680  template<class VX, class VB>
681  ExecStatus
683  if (b.none()) {
684  if ((c == 0) && (n_s == 0)) {
685  GECODE_ME_CHECK(b.one_none(home));
686  } else {
687  GECODE_ME_CHECK(b.zero_none(home));
688  }
689  } else {
690  normalize();
691  if (b.one()) {
692  GECODE_REWRITE(*this,(EqBoolInt<VX>::post(home(*this),x,c)));
693  } else {
694  GECODE_REWRITE(*this,(NqBoolInt<VX>::post(home(*this),x,c)));
695  }
696  }
697  return home.ES_SUBSUMED(*this);
698  }
699 
700  template<class VX, class VB>
701  ExecStatus
703  assert(!b.assigned()); // checked before posting
704 
705  // Eliminate assigned views
706  int n_x = x.size();
707  for (int i=n_x; i--; )
708  if (x[i].zero()) {
709  x[i] = x[--n_x];
710  } else if (x[i].one()) {
711  x[i] = x[--n_x]; c--;
712  }
713  x.size(n_x);
714  if ((n_x < c) || (c < 0)) {
715  // RHS too large
716  GECODE_ME_CHECK(b.zero_none(home));
717  } else if ((c == 0) && (n_x == 0)) {
718  // all variables set, and c == 0: equality
719  GECODE_ME_CHECK(b.one_none(home));
720  } else if (c == 0) {
721  // Equivalent to Boolean disjunction
723  ::post(home,x,BoolNegTraits<VB>::neg(b));
724  } else if (c == n_x) {
725  // Equivalent to Boolean conjunction, transform to Boolean disjunction
727  for (int i=n_x; i--; )
728  nx[i]=BoolNegTraits<VX>::neg(x[i]);
729  return Bool::NaryOr
730  <typename BoolNegTraits<VX>::NegView,
732  ::post(home,nx,BoolNegTraits<VB>::neg(b));
733  } else {
734  (void) new (home) ReEqBoolInt<VX,VB>(home,x,c,b);
735  }
736  return ES_OK;
737  }
738 
739 
740 }}}
741 
742 // STATISTICS: int-prop
743