| 71 | |
| 72 | template<class Card> |
| 73 | ExecStatus |
| 74 | prop_card(Space& home, |
| 75 | ViewArray<IntView>& x, ViewArray<Card>& k) { |
| 76 | int n = x.size(); |
| 77 | int m = k.size(); |
| 78 | Region r; |
| 79 | UnReachable* rv = r.alloc<UnReachable>(m); |
| 80 | for(int i = m; i--; ) |
| 81 | rv[i].minb=rv[i].maxb=rv[i].le=rv[i].gr=rv[i].eq=0; |
| 82 | |
| 83 | for (int i = n; i--; ) { |
| 84 | int min_idx; |
| 85 | if (!lookupValue(k,x[i].min(),min_idx)) |
| 86 | return ES_FAILED; |
| 87 | if (x[i].assigned()) { |
| 88 | rv[min_idx].minb++; |
| 89 | rv[min_idx].maxb++; |
| 90 | rv[min_idx].eq++; |
| 91 | } else { |
| 92 | // count the number of variables |
| 93 | // with lower bound k[min_idx].card() |
| 94 | rv[min_idx].minb++; |
| 95 | int max_idx; |
| 96 | if (!lookupValue(k,x[i].max(),max_idx)) |
| 97 | return ES_FAILED; |
| 98 | // count the number of variables |
| 99 | // with upper bound k[max_idx].card() |
| 100 | rv[max_idx].maxb++; |
| 101 | } |
| 102 | } |
| 103 | |
| 104 | rv[0].le = 0; |
| 105 | int c_min = 0; |
| 106 | for (int i = 1; i < m; i++) { |
| 107 | rv[i].le = c_min + rv[i - 1].maxb; |
| 108 | c_min += rv[i - 1].maxb; |
| 109 | } |
| 110 | |
| 111 | rv[m-1].gr = 0; |
| 112 | int c_max = 0; |
| 113 | for (int i = m-1; i--; ) { |
| 114 | rv[i].gr = c_max + rv[i + 1].minb; |
| 115 | c_max += rv[i + 1].minb; |
| 116 | } |
| 117 | |
| 118 | for (int i = m; i--; ) { |
| 119 | int reachable = x.size() - rv[i].le - rv[i].gr; |
| 120 | if (!k[i].assigned()) { |
| 121 | GECODE_ME_CHECK(k[i].lq(home, reachable)); |
| 122 | GECODE_ME_CHECK(k[i].gq(home, rv[i].eq)); |
| 123 | } else { |
| 124 | // check validity of the cardinality value |
| 125 | if ((rv[i].eq > k[i].max()) || (k[i].max() > reachable)) |
| 126 | return ES_FAILED; |
| 127 | } |
| 128 | } |
| 129 | |
| 130 | return ES_OK; |