| 150 | |
| 151 | template <class View> |
| 152 | ExecStatus |
| 153 | PushToEnd<View>::propagate(Space& home, const ModEventDelta&) { |
| 154 | // Find number of required positions |
| 155 | int min = 0; |
| 156 | for (int i = x.size(); i-- && x[i].min() >= val-1; ) { |
| 157 | ++min; |
| 158 | } |
| 159 | // Find number of possible positions |
| 160 | int max = 0; |
| 161 | { |
| 162 | int i = x.size(); |
| 163 | while (i--) { |
| 164 | if (x[i].max() != val) break; |
| 165 | ++max; |
| 166 | if (max >= y.max()) break; |
| 167 | } |
| 168 | // No variables later than max can have value val |
| 169 | while (i--) { |
| 170 | GECODE_ME_CHECK(x[i].le(home, val)); |
| 171 | } |
| 172 | } |
| 173 | |
| 174 | // Constrain y to be in {min..max} |
| 175 | GECODE_ME_CHECK(y.gq(home, min)); |
| 176 | GECODE_ME_CHECK(y.lq(home, max)); |
| 177 | |
| 178 | // At least the y.min() last values have value val |
| 179 | for (int i = 0, pos = x.size()-1; i < y.min(); ++i, --pos) { |
| 180 | GECODE_ME_CHECK(x[pos].eq(home, val)); |
| 181 | } |
| 182 | |
| 183 | return y.assigned() ? home.ES_SUBSUMED(*this) : ES_FIX; |
| 184 | } |
| 185 | |
| 186 | /** \brief Post PushToEnd propagator. |
| 187 | */ |