| 54 | |
| 55 | template<class VY> |
| 56 | inline ExecStatus |
| 57 | EqBool<VY>::post(Home home, ViewArray<BoolView>& x, VY y) { |
| 58 | if (x.size() == 0) { |
| 59 | GECODE_ME_CHECK(y.eq(home,0)); |
| 60 | return ES_OK; |
| 61 | } |
| 62 | |
| 63 | x.unique(); |
| 64 | |
| 65 | if (x.size() == 1) { |
| 66 | GECODE_ME_CHECK(y.eq(home,1)); |
| 67 | return ES_OK; |
| 68 | } |
| 69 | |
| 70 | GECODE_ME_CHECK(y.gq(home,1)); |
| 71 | GECODE_ME_CHECK(y.lq(home,2)); |
| 72 | |
| 73 | if (y.max() == 1) { |
| 74 | assert(y.assigned()); |
| 75 | ViewArray<BoolView> xc(home,x); |
| 76 | return Bool::NaryEq<BoolView>::post(home,xc); |
| 77 | } |
| 78 | |
| 79 | if (y.min() == 2) { |
| 80 | assert(y.assigned()); |
| 81 | ViewArray<BoolView> xc(home,x); |
| 82 | return Rel::NaryNq<BoolView>::post(home,xc); |
| 83 | } |
| 84 | |
| 85 | int n = x.size(); |
| 86 | int status = 0; |
| 87 | for (int i=n; i--; ) |
| 88 | if (x[i].zero()) { |
| 89 | if (status & VS_ONE) { |
| 90 | GECODE_ME_CHECK(y.eq(home,2)); |
| 91 | return ES_OK; |
| 92 | } |
| 93 | x[i] = x[--n]; |
| 94 | status |= VS_ZERO; |
| 95 | } else if (x[i].one()) { |
| 96 | if (status & VS_ZERO) { |
| 97 | GECODE_ME_CHECK(y.eq(home,2)); |
| 98 | return ES_OK; |
| 99 | } |
| 100 | x[i] = x[--n]; |
| 101 | status |= VS_ONE; |
| 102 | } |
| 103 | |
| 104 | assert(status != (VS_ZERO | VS_ONE)); |
| 105 | if (n == 0) { |
| 106 | assert(status != 0); |
| 107 | GECODE_ME_CHECK(y.eq(home,1)); |
| 108 | return ES_OK; |
| 109 | } |
| 110 | x.size(n); |
| 111 | |
| 112 | (void) new (home) EqBool<VY>(home,status,x,y); |
| 113 | return ES_OK; |