| 195 | |
| 196 | template<class VX> |
| 197 | ExecStatus |
| 198 | GqBoolInt<VX>::post(Home home, ViewArray<VX>& x, int c) { |
| 199 | // Eliminate assigned views |
| 200 | int n_x = x.size(); |
| 201 | for (int i=n_x; i--; ) |
| 202 | if (x[i].zero()) { |
| 203 | x[i] = x[--n_x]; |
| 204 | } else if (x[i].one()) { |
| 205 | x[i] = x[--n_x]; c--; |
| 206 | } |
| 207 | x.size(n_x); |
| 208 | // RHS too large |
| 209 | if (n_x < c) |
| 210 | return ES_FAILED; |
| 211 | // Whatever the x[i] take for values, the inequality is subsumed |
| 212 | if (c <= 0) |
| 213 | return ES_OK; |
| 214 | // Use Boolean disjunction for this special case |
| 215 | if (c == 1) |
| 216 | return Bool::NaryOrTrue<VX>::post(home,x); |
| 217 | // All views must be one to satisfy inequality |
| 218 | if (c == n_x) { |
| 219 | for (int i=0; i<n_x; i++) |
| 220 | GECODE_ME_CHECK(x[i].one_none(home)); |
| 221 | return ES_OK; |
| 222 | } |
| 223 | // This is the needed invariant as c+1 subscriptions must be created |
| 224 | assert(n_x > c); |
| 225 | (void) new (home) GqBoolInt<VX>(home,x,c); |
| 226 | return ES_OK; |
| 227 | } |
| 228 | |
| 229 | |
| 230 | |