Generated on Tue Jan 26 2021 00:00:00 for Gecode by doxygen 1.9.1
bool.cpp
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, 2002
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/bool.hh>
35 #include <gecode/int/rel.hh>
36 
37 namespace Gecode {
38 
39  void
41  using namespace Int;
43  switch (irt) {
44  case IRT_EQ:
46  ::post(home,x0,x1)));
47  break;
48  case IRT_NQ:
49  {
50  NegBoolView n1(x1);
52  ::post(home,x0,n1)));
53  }
54  break;
55  case IRT_GQ:
57  break;
58  case IRT_LQ:
60  break;
61  case IRT_GR:
63  break;
64  case IRT_LE:
66  break;
67  default:
68  throw UnknownRelation("Int::rel");
69  }
70  }
71 
72  void
73  rel(Home home, BoolVar x0, IntRelType irt, int n, IntPropLevel) {
74  using namespace Int;
76  BoolView x(x0);
77  if (n == 0) {
78  switch (irt) {
79  case IRT_LQ:
80  case IRT_EQ:
81  GECODE_ME_FAIL(x.zero(home)); break;
82  case IRT_NQ:
83  case IRT_GR:
84  GECODE_ME_FAIL(x.one(home)); break;
85  case IRT_LE:
86  home.fail(); break;
87  case IRT_GQ:
88  break;
89  default:
90  throw UnknownRelation("Int::rel");
91  }
92  } else if (n == 1) {
93  switch (irt) {
94  case IRT_GQ:
95  case IRT_EQ:
96  GECODE_ME_FAIL(x.one(home)); break;
97  case IRT_NQ:
98  case IRT_LE:
99  GECODE_ME_FAIL(x.zero(home)); break;
100  case IRT_GR:
101  home.fail(); break;
102  case IRT_LQ:
103  break;
104  default:
105  throw UnknownRelation("Int::rel");
106  }
107  } else {
108  throw NotZeroOne("Int::rel");
109  }
110  }
111 
112  void
113  rel(Home home, BoolVar x0, IntRelType irt, BoolVar x1, Reify r,
114  IntPropLevel) {
115  using namespace Int;
116  GECODE_POST;
117  switch (irt) {
118  case IRT_EQ:
119  switch (r.mode()) {
120  case RM_EQV:
122  ::post(home,x0,x1,r.var())));
123  break;
124  case RM_IMP:
126  ::post(home,x0,x1,r.var())));
127  break;
128  case RM_PMI:
130  ::post(home,x0,x1,r.var())));
131  break;
132  default: throw UnknownReifyMode("Int::rel");
133  }
134  break;
135  case IRT_NQ:
136  {
137  NegBoolView nr(r.var());
138  switch (r.mode()) {
139  case RM_EQV:
141  ::post(home,x0,x1,nr)));
142  break;
143  case RM_IMP:
145  ::post(home,x0,x1,nr)));
146  break;
147  case RM_PMI:
149  ::post(home,x0,x1,nr)));
150  break;
151  default: throw UnknownReifyMode("Int::rel");
152  }
153  }
154  break;
155  case IRT_GQ:
156  std::swap(x0,x1); // Fall through
157  case IRT_LQ:
158  switch (r.mode()) {
159  case RM_EQV:
160  {
161  NegBoolView n0(x0);
163  ::post(home,n0,x1,r.var())));
164  }
165  break;
166  case RM_IMP:
168  ::post(home,x0,x1,r.var())));
169  break;
170  case RM_PMI:
172  ::post(home,x0,x1,r.var())));
173  break;
174  default: throw UnknownReifyMode("Int::rel");
175  }
176  break;
177  case IRT_LE:
178  std::swap(x0,x1); // Fall through
179  case IRT_GR:
180  {
181  NegBoolView nr(r.var());
182  switch (r.mode()) {
183  case RM_EQV:
184  {
185  NegBoolView n0(x0);
187  ::post(home,n0,x1,nr)));
188  }
189  break;
190  case RM_IMP:
192  ::post(home,x0,x1,nr)));
193  break;
194  case RM_PMI:
196  ::post(home,x0,x1,nr)));
197  break;
198  default: throw UnknownReifyMode("Int::rel");
199  }
200  }
201  break;
202  default:
203  throw UnknownRelation("Int::rel");
204  }
205  }
206 
207  void
208  rel(Home home, BoolVar x0, IntRelType irt, int n, Reify r,
209  IntPropLevel) {
210  using namespace Int;
211  GECODE_POST;
212  BoolView x(x0);
213  BoolView y(r.var());
214  if (n == 0) {
215  switch (irt) {
216  case IRT_LQ:
217  case IRT_EQ:
218  switch (r.mode()) {
219  case RM_EQV:
220  {
221  NegBoolView ny(y);
223  ::post(home,x,ny)));
224  }
225  break;
226  case RM_IMP:
227  {
228  NegBoolView nx(x); NegBoolView ny(y);
230  ::post(home,nx,ny)));
231  }
232  break;
233  case RM_PMI:
235  ::post(home,x,y)));
236  break;
237  default: throw UnknownReifyMode("Int::rel");
238  }
239  break;
240  case IRT_NQ:
241  case IRT_GR:
242  switch (r.mode()) {
243  case RM_EQV:
245  ::post(home,x,y)));
246  break;
247  case RM_IMP:
248  {
249  NegBoolView ny(y);
251  ::post(home,x,ny)));
252  }
253  break;
254  case RM_PMI:
255  {
256  NegBoolView nx(x);
258  ::post(home,nx,y)));
259  }
260  break;
261  default: throw UnknownReifyMode("Int::rel");
262  }
263  break;
264  case IRT_LE:
265  switch (r.mode()) {
266  case RM_EQV:
267  case RM_IMP:
268  GECODE_ME_FAIL(y.zero(home));
269  break;
270  case RM_PMI:
271  break;
272  default: throw UnknownReifyMode("Int::rel");
273  }
274  break;
275  case IRT_GQ:
276  switch (r.mode()) {
277  case RM_EQV:
278  case RM_PMI:
279  GECODE_ME_FAIL(y.one(home));
280  break;
281  case RM_IMP:
282  break;
283  default: throw UnknownReifyMode("Int::rel");
284  }
285  break;
286  default:
287  throw UnknownRelation("Int::rel");
288  }
289  } else if (n == 1) {
290  switch (irt) {
291  case IRT_NQ:
292  case IRT_LE:
293  switch (r.mode()) {
294  case RM_EQV:
295  {
296  NegBoolView ny(y);
298  ::post(home,x,ny)));
299  }
300  break;
301  case RM_IMP:
302  {
303  NegBoolView nx(x); NegBoolView ny(y);
305  ::post(home,nx,ny)));
306  }
307  break;
308  case RM_PMI:
310  ::post(home,x,y)));
311  break;
312  default: throw UnknownReifyMode("Int::rel");
313  }
314  break;
315  case IRT_EQ:
316  case IRT_GQ:
317  switch (r.mode()) {
318  case RM_EQV:
320  ::post(home,x,y)));
321  break;
322  case RM_IMP:
323  {
324  NegBoolView ny(y);
326  ::post(home,x,ny)));
327  }
328  break;
329  case RM_PMI:
330  {
331  NegBoolView nx(x);
333  ::post(home,nx,y)));
334  }
335  break;
336  default: throw UnknownReifyMode("Int::rel");
337  }
338  break;
339  case IRT_GR:
340  switch (r.mode()) {
341  case RM_EQV:
342  case RM_IMP:
343  GECODE_ME_FAIL(y.zero(home));
344  break;
345  case RM_PMI:
346  break;
347  default: throw UnknownReifyMode("Int::rel");
348  }
349  break;
350  case IRT_LQ:
351  switch (r.mode()) {
352  case RM_EQV:
353  case RM_PMI:
354  GECODE_ME_FAIL(y.one(home));
355  break;
356  case RM_IMP:
357  break;
358  default: throw UnknownReifyMode("Int::rel");
359  }
360  break;
361  default:
362  throw UnknownRelation("Int::rel");
363  }
364  } else {
365  throw NotZeroOne("Int::rel");
366  }
367  }
368 
369  void
370  rel(Home home, const BoolVarArgs& x, IntRelType irt, BoolVar y,
371  IntPropLevel) {
372  using namespace Int;
373  GECODE_POST;
374  switch (irt) {
375  case IRT_EQ:
376  for (int i=0; i<x.size(); i++) {
378  ::post(home,x[i],y)));
379  }
380  break;
381  case IRT_NQ:
382  {
383  NegBoolView n(y);
384  for (int i=0; i<x.size(); i++) {
386  ::post(home,x[i],n)));
387  }
388  }
389  break;
390  case IRT_GQ:
391  for (int i=0; i<x.size(); i++) {
393  }
394  break;
395  case IRT_LQ:
396  for (int i=0; i<x.size(); i++) {
398  }
399  break;
400  case IRT_GR:
401  for (int i=0; i<x.size(); i++) {
403  }
404  break;
405  case IRT_LE:
406  for (int i=0; i<x.size(); i++) {
408  }
409  break;
410  default:
411  throw UnknownRelation("Int::rel");
412  }
413  }
414 
415  void
416  rel(Home home, const BoolVarArgs& x, IntRelType irt, int n,
417  IntPropLevel) {
418  using namespace Int;
419  GECODE_POST;
420  if (n == 0) {
421  switch (irt) {
422  case IRT_LQ:
423  case IRT_EQ:
424  for (int i=0; i<x.size(); i++) {
425  BoolView xi(x[i]); GECODE_ME_FAIL(xi.zero(home));
426  }
427  break;
428  case IRT_NQ:
429  case IRT_GR:
430  for (int i=0; i<x.size(); i++) {
431  BoolView xi(x[i]); GECODE_ME_FAIL(xi.one(home));
432  }
433  break;
434  case IRT_LE:
435  home.fail(); break;
436  case IRT_GQ:
437  break;
438  default:
439  throw UnknownRelation("Int::rel");
440  }
441  } else if (n == 1) {
442  switch (irt) {
443  case IRT_GQ:
444  case IRT_EQ:
445  for (int i=0; i<x.size(); i++) {
446  BoolView xi(x[i]); GECODE_ME_FAIL(xi.one(home));
447  }
448  break;
449  case IRT_NQ:
450  case IRT_LE:
451  for (int i=0; i<x.size(); i++) {
452  BoolView xi(x[i]); GECODE_ME_FAIL(xi.zero(home));
453  }
454  break;
455  case IRT_GR:
456  home.fail(); break;
457  case IRT_LQ:
458  break;
459  default:
460  throw UnknownRelation("Int::rel");
461  }
462  } else {
463  throw NotZeroOne("Int::rel");
464  }
465  }
466 
467  void
468  rel(Home home, const BoolVarArgs& x, IntRelType irt, IntPropLevel) {
469  using namespace Int;
470  GECODE_POST;
471  if ((irt != IRT_NQ) && (x.size() < 2))
472  return;
473 
474  switch (irt) {
475  case IRT_EQ:
476  {
477  ViewArray<BoolView> y(home,x);
479  }
480  break;
481  case IRT_NQ:
482  {
483  ViewArray<BoolView> y(home,x);
485  }
486  break;
487  case IRT_LE:
488  if (x.size() == 2) {
490  } else {
491  home.fail();
492  }
493  break;
494  case IRT_LQ:
495  {
496  ViewArray<BoolView> y(home,x);
498  }
499  break;
500  case IRT_GR:
501  if (x.size() == 2) {
503  } else {
504  home.fail();
505  }
506  break;
507  case IRT_GQ:
508  {
509  ViewArray<BoolView> y(home,x.size());
510  for (int i=0; i<x.size(); i++)
511  y[i] = x[x.size()-1-i];
513  }
514  break;
515  default:
516  throw UnknownRelation("Int::rel");
517  }
518  }
519 
520  void
521  rel(Home home, const BoolVarArgs& x, IntRelType irt, const BoolVarArgs& y,
522  IntPropLevel) {
523  using namespace Int;
524  GECODE_POST;
525 
526  switch (irt) {
527  case IRT_GR:
528  {
529  ViewArray<BoolView> xv(home,x), yv(home,y);
531  ::post(home,yv,xv,true)));
532  }
533  break;
534  case IRT_LE:
535  {
536  ViewArray<BoolView> xv(home,x), yv(home,y);
538  ::post(home,xv,yv,true)));
539  }
540  break;
541  case IRT_GQ:
542  {
543  ViewArray<BoolView> xv(home,x), yv(home,y);
545  ::post(home,yv,xv,false)));
546  }
547  break;
548  case IRT_LQ:
549  {
550  ViewArray<BoolView> xv(home,x), yv(home,y);
552  ::post(home,xv,yv,false)));
553  }
554  break;
555  case IRT_EQ:
556  for (int i=0; i<x.size(); i++) {
558  ::post(home,x[i],y[i])));
559  }
560  break;
561  case IRT_NQ:
562  {
563  ViewArray<BoolView> xv(home,x), yv(home,y);
565  ::post(home,xv,yv)));
566  }
567  break;
568  default:
569  throw UnknownRelation("Int::rel");
570  }
571  }
572 
573  namespace {
574 
576  ViewArray<Int::ConstIntView>
577  viewarray(Space& home, const IntArgs& x) {
578  ViewArray<Int::ConstIntView> xv(home, x.size());
579  for (int i=0; i<x.size(); i++) {
580  if ((x[i] != 0) && (x[i] != 1))
581  throw Int::NotZeroOne("Int::rel");
582  xv[i] = Int::ConstIntView(x[i]);
583  }
584  return xv;
585  }
586 
587  }
588 
589  void
590  rel(Home home, const BoolVarArgs& x, IntRelType irt, const IntArgs& y,
591  IntPropLevel) {
592  using namespace Int;
593  GECODE_POST;
594 
595  switch (irt) {
596  case IRT_GR:
597  {
598  ViewArray<BoolView> xv(home,x);
599  ViewArray<ConstIntView> yv(viewarray(home,y));
601  ::post(home,yv,xv,true)));
602  }
603  break;
604  case IRT_LE:
605  {
606  ViewArray<BoolView> xv(home,x);
607  ViewArray<ConstIntView> yv(viewarray(home,y));
609  ::post(home,xv,yv,true)));
610  }
611  break;
612  case IRT_GQ:
613  {
614  ViewArray<BoolView> xv(home,x);
615  ViewArray<ConstIntView> yv(viewarray(home,y));
617  ::post(home,yv,xv,false)));
618  }
619  break;
620  case IRT_LQ:
621  {
622  ViewArray<BoolView> xv(home,x);
623  ViewArray<ConstIntView> yv(viewarray(home,y));
625  ::post(home,xv,yv,false)));
626  }
627  break;
628  case IRT_EQ:
629  if (x.size() != y.size()) {
630  home.fail();
631  } else {
632  for (int i=0; i<x.size(); i++)
633  GECODE_ME_FAIL(BoolView(x[i]).eq(home,y[i]));
634  }
635  break;
636  case IRT_NQ:
637  {
638  ViewArray<BoolView> xv(home,x);
639  ViewArray<ConstIntView> yv(viewarray(home,y));
641  ::post(home,xv,yv)));
642  }
643  break;
644  default:
645  throw UnknownRelation("Int::rel");
646  }
647  }
648 
649  void
650  rel(Home home, const IntArgs& x, IntRelType irt, const BoolVarArgs& y,
651  IntPropLevel ipl) {
652  rel(home,y,irt,x,ipl);
653  }
654 
655  void
656  rel(Home home, BoolVar x0, BoolOpType o, BoolVar x1, BoolVar x2,
657  IntPropLevel) {
658  using namespace Int;
659  GECODE_POST;
660  switch (o) {
661  case BOT_AND:
662  {
663  NegBoolView n0(x0); NegBoolView n1(x1); NegBoolView n2(x2);
665  ::post(home,n0,n1,n2)));
666  }
667  break;
668  case BOT_OR:
670  ::post(home,x0,x1,x2)));
671  break;
672  case BOT_IMP:
673  {
674  NegBoolView n0(x0);
676  ::post(home,n0,x1,x2)));
677  }
678  break;
679  case BOT_EQV:
681  ::post(home,x0,x1,x2)));
682  break;
683  case BOT_XOR:
684  {
685  NegBoolView n2(x2);
687  ::post(home,x0,x1,n2)));
688  }
689  break;
690  default:
691  throw UnknownOperation("Int::rel");
692  }
693  }
694 
695  void
696  rel(Home home, BoolVar x0, BoolOpType o, BoolVar x1, int n,
697  IntPropLevel) {
698  using namespace Int;
699  GECODE_POST;
700  if (n == 0) {
701  switch (o) {
702  case BOT_AND:
703  {
704  NegBoolView n0(x0); NegBoolView n1(x1);
706  ::post(home,n0,n1)));
707  }
708  break;
709  case BOT_OR:
710  {
711  BoolView b0(x0); BoolView b1(x1);
712  GECODE_ME_FAIL(b0.zero(home));
713  GECODE_ME_FAIL(b1.zero(home));
714  }
715  break;
716  case BOT_IMP:
717  {
718  BoolView b0(x0); BoolView b1(x1);
719  GECODE_ME_FAIL(b0.one(home));
720  GECODE_ME_FAIL(b1.zero(home));
721  }
722  break;
723  case BOT_EQV:
724  {
725  NegBoolView n0(x0);
727  }
728  break;
729  case BOT_XOR:
731  break;
732  default:
733  throw UnknownOperation("Int::rel");
734  }
735  } else if (n == 1) {
736  switch (o) {
737  case BOT_AND:
738  {
739  BoolView b0(x0); BoolView b1(x1);
740  GECODE_ME_FAIL(b0.one(home));
741  GECODE_ME_FAIL(b1.one(home));
742  }
743  break;
744  case BOT_OR:
746  break;
747  case BOT_IMP:
748  {
749  NegBoolView n0(x0);
751  ::post(home,n0,x1)));
752  }
753  break;
754  case BOT_EQV:
756  break;
757  case BOT_XOR:
758  {
759  NegBoolView n0(x0);
761  }
762  break;
763  default:
764  throw UnknownOperation("Int::rel");
765  }
766  } else {
767  throw NotZeroOne("Int::rel");
768  }
769  }
770 
771  void
772  rel(Home home, BoolOpType o, const BoolVarArgs& x, BoolVar y,
773  IntPropLevel) {
774  using namespace Int;
775  GECODE_POST;
776  int m = x.size();
777  Region r;
778  switch (o) {
779  case BOT_AND:
780  {
781  ViewArray<NegBoolView> b(home,m);
782  for (int i=0; i<m; i++) {
783  NegBoolView nb(x[i]); b[i]=nb;
784  }
785  NegBoolView ny(y);
786  b.unique();
788  ::post(home,b,ny)));
789  }
790  break;
791  case BOT_OR:
792  {
793  ViewArray<BoolView> b(home,x);
794  b.unique();
796  }
797  break;
798  case BOT_IMP:
799  if (m < 2) {
800  throw TooFewArguments("Int::rel");
801  } else {
802  ViewArray<NegBoolView> a(home,x.size()-1);
803  for (int i=x.size()-1; i--; )
804  a[i]=NegBoolView(x[i]);
805  ViewArray<BoolView> b(home,1);
806  b[0]=x[x.size()-1];
808  ::post(home,b,a,y)));
809  }
810  break;
811  case BOT_EQV:
812  {
813  ViewArray<BoolView> xy(home, x.size() + 1);
814  for (int i=0; i<x.size(); i++)
815  xy[i] = x[i];
816  xy[x.size()] = y;
818  }
819  break;
820  case BOT_XOR:
821  {
822  ViewArray<BoolView> xy(home, x.size() + 1);
823  for (int i=0; i<x.size(); i++)
824  xy[i] = x[i];
825  xy[x.size()] = y;
827  }
828  break;
829  default:
830  throw UnknownOperation("Int::rel");
831  }
832  }
833 
834  void
835  rel(Home home, BoolOpType o, const BoolVarArgs& x, int n,
836  IntPropLevel) {
837  using namespace Int;
838  if ((n < 0) || (n > 1))
839  throw NotZeroOne("Int::rel");
840  GECODE_POST;
841  int m = x.size();
842  Region r;
843  switch (o) {
844  case BOT_AND:
845  if (n == 0) {
846  ViewArray<NegBoolView> b(home,m);
847  for (int i=0; i<m; i++) {
848  NegBoolView nb(x[i]); b[i]=nb;
849  }
850  b.unique();
852  } else {
853  for (int i=0; i<m; i++) {
854  BoolView b(x[i]); GECODE_ME_FAIL(b.one(home));
855  }
856  }
857  break;
858  case BOT_OR:
859  if (n == 0) {
860  for (int i=0; i<m; i++) {
861  BoolView b(x[i]); GECODE_ME_FAIL(b.zero(home));
862  }
863  } else {
864  ViewArray<BoolView> b(home,x);
865  b.unique();
867  }
868  break;
869  case BOT_IMP:
870  if (m < 2) {
871  throw TooFewArguments("Int::rel");
872  } else if (n == 0) {
873  for (int i=m-1; i--; )
874  GECODE_ME_FAIL(BoolView(x[i]).one(home));
875  GECODE_ME_FAIL(BoolView(x[m-1]).zero(home));
876  } else {
877  ViewArray<NegBoolView> a(home,x.size()-1);
878  for (int i=x.size()-1; i--; )
879  a[i]=NegBoolView(x[i]);
880  ViewArray<BoolView> b(home,1);
881  b[0]=x[x.size()-1];
883  ::post(home,b,a)));
884  }
885  break;
886  case BOT_EQV:
887  {
888  ViewArray<BoolView> b(home,x);
890  }
891  break;
892  case BOT_XOR:
893  {
894  ViewArray<BoolView> b(home,x);
896  }
897  break;
898  default:
899  throw UnknownOperation("Int::rel");
900  }
901  }
902 
903  void
904  clause(Home home, BoolOpType o, const BoolVarArgs& x, const BoolVarArgs& y,
905  int n, IntPropLevel) {
906  using namespace Int;
907  if ((n < 0) || (n > 1))
908  throw NotZeroOne("Int::rel");
909  GECODE_POST;
910  switch (o) {
911  case BOT_AND:
912  if (n == 0) {
913  ViewArray<NegBoolView> xv(home,x.size());
914  for (int i=0; i<x.size(); i++) {
915  NegBoolView nxi(x[i]); xv[i]=nxi;
916  }
917  ViewArray<BoolView> yv(home,y);
918  xv.unique(); yv.unique();
920  ::post(home,xv,yv)));
921  } else {
922  for (int i=0; i<x.size(); i++) {
923  BoolView b(x[i]); GECODE_ME_FAIL(b.one(home));
924  }
925  for (int i=0; i<y.size(); i++) {
926  BoolView b(y[i]); GECODE_ME_FAIL(b.zero(home));
927  }
928  }
929  break;
930  case BOT_OR:
931  if (n == 0) {
932  for (int i=0; i<x.size(); i++) {
933  BoolView b(x[i]); GECODE_ME_FAIL(b.zero(home));
934  }
935  for (int i=0; i<y.size(); i++) {
936  BoolView b(y[i]); GECODE_ME_FAIL(b.one(home));
937  }
938  } else {
939  ViewArray<BoolView> xv(home,x);
940  ViewArray<NegBoolView> yv(home,y.size());
941  for (int i=0; i<y.size(); i++) {
942  NegBoolView nyi(y[i]); yv[i]=nyi;
943  }
944  xv.unique(); yv.unique();
946  ::post(home,xv,yv)));
947  }
948  break;
949  default:
950  throw IllegalOperation("Int::clause");
951  }
952  }
953 
954  void
955  clause(Home home, BoolOpType o, const BoolVarArgs& x, const BoolVarArgs& y,
956  BoolVar z, IntPropLevel) {
957  using namespace Int;
958  GECODE_POST;
959  switch (o) {
960  case BOT_AND:
961  {
962  ViewArray<NegBoolView> xv(home,x.size());
963  for (int i=0; i<x.size(); i++) {
964  NegBoolView n(x[i]); xv[i]=n;
965  }
966  ViewArray<BoolView> yv(home,y);
967  xv.unique(); yv.unique();
968  NegBoolView nz(z);
970  ::post(home,xv,yv,nz)));
971  }
972  break;
973  case BOT_OR:
974  {
975  ViewArray<BoolView> xv(home,x);
976  ViewArray<NegBoolView> yv(home,y.size());
977  for (int i=0; i<y.size(); i++) {
978  NegBoolView n(y[i]); yv[i]=n;
979  }
980  xv.unique(); yv.unique();
982  ::post(home,xv,yv,z)));
983  }
984  break;
985  default:
986  throw IllegalOperation("Int::clause");
987  }
988  }
989 
990  void
992  IntPropLevel ipl) {
993  using namespace Int;
994  GECODE_POST;
995  if (vbd(ipl) == IPL_BND) {
997  ::post(home,b,x,y,z)));
998  } else {
1000  ::post(home,b,x,y,z)));
1001  }
1002  }
1003 
1004  void
1006  IntPropLevel) {
1007  using namespace Int;
1008  GECODE_POST;
1010  ::post(home,b,x,y,z)));
1011  }
1012 
1013 }
1014 
1015 // STATISTICS: int-post
struct Gecode::@602::NNF::@65::@66 b
For binary nodes (and, or, eqv)
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:234
Node * x
Pointer to corresponding Boolean expression node.
Definition: bool-expr.cpp:249
struct Gecode::@602::NNF::@65::@67 a
For atomic nodes.
NNF * r
Right subtree.
Definition: bool-expr.cpp:242
Passing Boolean variables.
Definition: int.hh:712
Boolean integer variables.
Definition: int.hh:512
Home class for posting propagators
Definition: core.hpp:856
void fail(void)
Mark space as failed.
Definition: core.hpp:4039
Passing integer arguments.
Definition: int.hh:628
Integer variables.
Definition: int.hh:371
Boolean view for Boolean variables.
Definition: view.hpp:1380
bool zero(void) const
Test whether view is assigned to be zero.
Definition: bool.hpp:220
bool one(void) const
Test whether view is assigned to be one.
Definition: bool.hpp:224
Binary Boolean disjunction propagator (true)
Definition: bool.hh:237
Boolean clause propagator (disjunctive, true)
Definition: bool.hh:547
Boolean clause propagator (disjunctive)
Definition: bool.hh:492
Boolean equality propagator.
Definition: bool.hh:105
Boolean equivalence propagator.
Definition: bool.hh:426
If-then-else bounds-consistent propagator.
Definition: bool.hh:606
If-then-else domain-consistent propagator.
Definition: bool.hh:632
Boolean less propagator.
Definition: bool.hh:223
Boolean less or equal propagator.
Definition: bool.hh:159
n-ary Boolean equality propagator
Definition: bool.hh:133
static ExecStatus post(Home home, ViewArray< BoolView > &x, int pm2)
Post propagator .
Definition: eqv.cpp:54
Nary Boolean less or equal propagator.
Definition: bool.hh:183
Boolean n-ary disjunction propagator (true)
Definition: bool.hh:393
Boolean n-ary disjunction propagator.
Definition: bool.hh:356
Boolean disjunction propagator.
Definition: bool.hh:328
Exception: Illegal operation passed as argument
Definition: exception.hpp:101
Negated Boolean view.
Definition: view.hpp:1574
Exception: Not 0/1 integer
Definition: exception.hpp:51
Lexical ordering propagator.
Definition: rel.hh:623
Lexical disequality propagator.
Definition: rel.hh:657
Nary disequality propagator.
Definition: rel.hh:318
Reified binary bounds consistent equality propagator.
Definition: rel.hh:372
Reified less or equal propagator.
Definition: rel.hh:548
Exception: Too few arguments available in argument array
Definition: exception.hpp:66
Exception: Unknown operation passed as argument
Definition: exception.hpp:94
Exception: Unknown reification mode passed as argument
Definition: exception.hpp:115
Exception: Unknown relation passed as argument
Definition: exception.hpp:87
Handle to region.
Definition: region.hpp:55
Reification specification.
Definition: int.hh:876
View arrays.
Definition: array.hpp:253
void unique(void)
Remove all duplicate views from array (changes element order)
Definition: array.hpp:1417
Post propagator for SetVar SetOpType SetVar SetRelType SetVar z
Definition: set.hh:767
Post propagator for SetVar SetOpType SetVar y
Definition: set.hh:767
void post(Home home, Term *t, int n, FloatRelType frt, FloatVal c)
Post propagator for linear constraint over floats.
Definition: post.cpp:238
#define GECODE_POST
Check for failure in a constraint post function.
Definition: macros.hpp:40
#define GECODE_ES_FAIL(es)
Check whether execution status es is failed, and fail space home.
Definition: macros.hpp:103
#define GECODE_ME_FAIL(me)
Check whether modification event me is failed, and fail space home.
Definition: macros.hpp:77
void ite(Home home, BoolVar b, FloatVar x, FloatVar y, FloatVar z)
Post propagator for if-then-else constraint.
Definition: bool.cpp:39
void rel(Home home, BoolOpType o, const BoolVarArgs &x, int n, IntPropLevel)
Post domain consistent propagator for Boolean operation on x.
Definition: bool.cpp:835
void clause(Home home, BoolOpType o, const BoolVarArgs &x, const BoolVarArgs &y, BoolVar z, IntPropLevel)
Post domain consistent propagator for Boolean clause with positive variables x and negative variables...
Definition: bool.cpp:955
IntRelType
Relation types for integers.
Definition: int.hh:925
BoolOpType
Operation types for Booleans.
Definition: int.hh:950
IntPropLevel
Propagation levels for integer propagators.
Definition: int.hh:974
@ IRT_EQ
Equality ( )
Definition: int.hh:926
@ IRT_NQ
Disequality ( )
Definition: int.hh:927
@ IRT_GQ
Greater or equal ( )
Definition: int.hh:930
@ IRT_LE
Less ( )
Definition: int.hh:929
@ IRT_GR
Greater ( )
Definition: int.hh:931
@ IRT_LQ
Less or equal ( )
Definition: int.hh:928
@ RM_IMP
Implication for reification.
Definition: int.hh:862
@ RM_PMI
Inverse implication for reification.
Definition: int.hh:869
@ RM_EQV
Equivalence for reification (default)
Definition: int.hh:855
@ BOT_OR
Disjunction.
Definition: int.hh:952
@ BOT_EQV
Equivalence.
Definition: int.hh:954
@ BOT_IMP
Implication.
Definition: int.hh:953
@ BOT_XOR
Exclusive or.
Definition: int.hh:955
@ BOT_AND
Conjunction.
Definition: int.hh:951
@ IPL_BND
Bounds propagation.
Definition: int.hh:978
IntPropLevel vbd(IntPropLevel ipl)
Extract value, bounds, or domain propagation from propagation level.
Definition: ipl.hpp:37
bool one(const Gecode::FloatValArgs &a)
Check whether has only one coefficients.
Definition: linear.cpp:46
Gecode::IntArgs i({1, 2, 3, 4})