this repo has no description
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, 2004 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 34namespace Gecode { namespace Int { namespace Linear { 35 36 /* 37 * Base-class 38 * 39 */ 40 template<class XV, class YV> 41 forceinline 42 LinBoolView<XV,YV>::LinBoolView(Home home, 43 ViewArray<XV>& x0, YV y0, int c0) 44 : Propagator(home), x(x0), y(y0), c(c0) { 45 x.subscribe(home,*this,PC_INT_VAL); 46 y.subscribe(home,*this,PC_INT_BND); 47 } 48 49 template<class XV, class YV> 50 forceinline size_t 51 LinBoolView<XV,YV>::dispose(Space& home) { 52 x.cancel(home,*this,PC_INT_VAL); 53 y.cancel(home,*this,PC_INT_BND); 54 (void) Propagator::dispose(home); 55 return sizeof(*this); 56 } 57 58 template<class XV, class YV> 59 forceinline 60 LinBoolView<XV,YV>::LinBoolView(Space& home, LinBoolView& p) 61 : Propagator(home,p), c(p.c) { 62 x.update(home,p.x); 63 y.update(home,p.y); 64 } 65 66 template<class XV, class YV> 67 PropCost 68 LinBoolView<XV,YV>::cost(const Space&, const ModEventDelta&) const { 69 return PropCost::linear(PropCost::LO, x.size()); 70 } 71 72 template<class XV, class YV> 73 void 74 LinBoolView<XV,YV>::reschedule(Space& home) { 75 x.reschedule(home,*this,PC_INT_VAL); 76 y.reschedule(home,*this,PC_INT_BND); 77 } 78 79 80 /* 81 * Equality propagator 82 * 83 */ 84 template<class XV, class YV> 85 forceinline 86 EqBoolView<XV,YV>::EqBoolView(Home home, ViewArray<XV>& x, YV y, int c) 87 : LinBoolView<XV,YV>(home,x,y,c) {} 88 89 template<class XV, class YV> 90 ExecStatus 91 EqBoolView<XV,YV>::post(Home home, ViewArray<XV>& x, YV y, int c) { 92 if (y.assigned()) 93 return EqBoolInt<XV>::post(home,x,y.val()+c); 94 int n = x.size(); 95 for (int i=n; i--; ) 96 if (x[i].one()) { 97 x[i]=x[--n]; c--; 98 } else if (x[i].zero()) { 99 x[i]=x[--n]; 100 } 101 x.size(n); 102 GECODE_ME_CHECK(y.lq(home,n-c)); 103 GECODE_ME_CHECK(y.gq(home,-c)); 104 if (n == 0) 105 return ES_OK; 106 if (y.min()+c == n) { 107 assert(y.assigned()); 108 for (int i=0; i<n; i++) 109 GECODE_ME_CHECK(x[i].one_none(home)); 110 return ES_OK; 111 } 112 if (y.max()+c == 0) { 113 assert(y.assigned()); 114 for (int i=0; i<n; i++) 115 GECODE_ME_CHECK(x[i].zero_none(home)); 116 return ES_OK; 117 } 118 (void) new (home) EqBoolView<XV,YV>(home,x,y,c); 119 return ES_OK; 120 } 121 122 template<class XV, class YV> 123 forceinline 124 EqBoolView<XV,YV>::EqBoolView(Space& home, EqBoolView<XV,YV>& p) 125 : LinBoolView<XV,YV>(home,p) {} 126 127 template<class XV, class YV> 128 Actor* 129 EqBoolView<XV,YV>::copy(Space& home) { 130 return new (home) EqBoolView<XV,YV>(home,*this); 131 } 132 133 template<class XV, class YV> 134 ExecStatus 135 EqBoolView<XV,YV>::propagate(Space& home, const ModEventDelta&) { 136 int n = x.size(); 137 for (int i=n; i--; ) 138 if (x[i].one()) { 139 x[i]=x[--n]; c--; 140 } else if (x[i].zero()) { 141 x[i]=x[--n]; 142 } 143 x.size(n); 144 GECODE_ME_CHECK(y.lq(home,n-c)); 145 GECODE_ME_CHECK(y.gq(home,-c)); 146 if (n == 0) 147 return home.ES_SUBSUMED(*this); 148 if (y.min()+c == n) { 149 assert(y.assigned()); 150 for (int i=0; i<n; i++) 151 GECODE_ME_CHECK(x[i].one_none(home)); 152 return home.ES_SUBSUMED(*this); 153 } 154 if (y.max()+c == 0) { 155 assert(y.assigned()); 156 for (int i=0; i<n; i++) 157 GECODE_ME_CHECK(x[i].zero_none(home)); 158 return home.ES_SUBSUMED(*this); 159 } 160 if (y.assigned()) 161 GECODE_REWRITE(*this,EqBoolInt<XV>::post(home(*this),x,y.val()+c)); 162 return ES_FIX; 163 } 164 165 166 /* 167 * Disequality propagator 168 * 169 */ 170 template<class XV, class YV> 171 forceinline 172 NqBoolView<XV,YV>::NqBoolView(Home home, ViewArray<XV>& x, YV y, int c) 173 : LinBoolView<XV,YV>(home,x,y,c) {} 174 175 template<class XV, class YV> 176 ExecStatus 177 NqBoolView<XV,YV>::post(Home home, ViewArray<XV>& x, YV y, int c) { 178 if (y.assigned()) 179 return NqBoolInt<XV>::post(home,x,y.val()+c); 180 int n = x.size(); 181 for (int i = n; i--; ) 182 if (x[i].one()) { 183 x[i]=x[--n]; c--; 184 } else if (x[i].zero()) { 185 x[i]=x[--n]; 186 } 187 x.size(n); 188 if ((n-c < y.min() ) || (-c > y.max())) 189 return ES_OK; 190 if (n == 0) { 191 GECODE_ME_CHECK(y.nq(home,-c)); 192 return ES_OK; 193 } 194 if ((n == 1) && y.assigned()) { 195 if (y.val()+c == 1) { 196 GECODE_ME_CHECK(x[0].zero_none(home)); 197 } else { 198 assert(y.val()+c == 0); 199 GECODE_ME_CHECK(x[0].one_none(home)); 200 } 201 return ES_OK; 202 } 203 (void) new (home) NqBoolView<XV,YV>(home,x,y,c); 204 return ES_OK; 205 } 206 207 208 template<class XV, class YV> 209 forceinline 210 NqBoolView<XV,YV>::NqBoolView(Space& home, NqBoolView<XV,YV>& p) 211 : LinBoolView<XV,YV>(home,p) {} 212 213 template<class XV, class YV> 214 Actor* 215 NqBoolView<XV,YV>::copy(Space& home) { 216 return new (home) NqBoolView<XV,YV>(home,*this); 217 } 218 219 template<class XV, class YV> 220 ExecStatus 221 NqBoolView<XV,YV>::propagate(Space& home, const ModEventDelta&) { 222 int n = x.size(); 223 for (int i = n; i--; ) 224 if (x[i].one()) { 225 x[i]=x[--n]; c--; 226 } else if (x[i].zero()) { 227 x[i]=x[--n]; 228 } 229 x.size(n); 230 if ((n-c < y.min() ) || (-c > y.max())) 231 return home.ES_SUBSUMED(*this); 232 if (n == 0) { 233 GECODE_ME_CHECK(y.nq(home,-c)); 234 return home.ES_SUBSUMED(*this); 235 } 236 if ((n == 1) && y.assigned()) { 237 if (y.val()+c == 1) { 238 GECODE_ME_CHECK(x[0].zero_none(home)); 239 } else { 240 assert(y.val()+c == 0); 241 GECODE_ME_CHECK(x[0].one_none(home)); 242 } 243 return home.ES_SUBSUMED(*this); 244 } 245 return ES_FIX; 246 } 247 248 249 /* 250 * Greater or equal propagator 251 * 252 */ 253 template<class XV, class YV> 254 forceinline 255 GqBoolView<XV,YV>::GqBoolView(Home home, ViewArray<XV>& x, YV y, int c) 256 : LinBoolView<XV,YV>(home,x,y,c) {} 257 258 template<class XV, class YV> 259 ExecStatus 260 GqBoolView<XV,YV>::post(Home home, ViewArray<XV>& x, YV y, int c) { 261 if (y.assigned()) 262 return GqBoolInt<XV>::post(home,x,y.val()+c); 263 // Eliminate assigned views 264 int n = x.size(); 265 for (int i = n; i--; ) 266 if (x[i].one()) { 267 x[i]=x[--n]; c--; 268 } else if (x[i].zero()) { 269 x[i]=x[--n]; 270 } 271 x.size(n); 272 GECODE_ME_CHECK(y.lq(home,n-c)); 273 if (-c >= y.max()) 274 return ES_OK; 275 if (y.min()+c == n) { 276 for (int i = n; i--; ) 277 GECODE_ME_CHECK(x[i].one_none(home)); 278 return ES_OK; 279 } 280 (void) new (home) GqBoolView<XV,YV>(home,x,y,c); 281 return ES_OK; 282 } 283 284 285 template<class XV, class YV> 286 forceinline 287 GqBoolView<XV,YV>::GqBoolView(Space& home, GqBoolView<XV,YV>& p) 288 : LinBoolView<XV,YV>(home,p) {} 289 290 template<class XV, class YV> 291 Actor* 292 GqBoolView<XV,YV>::copy(Space& home) { 293 return new (home) GqBoolView<XV,YV>(home,*this); 294 } 295 296 template<class XV, class YV> 297 ExecStatus 298 GqBoolView<XV,YV>::propagate(Space& home, const ModEventDelta&) { 299 int n = x.size(); 300 for (int i = n; i--; ) 301 if (x[i].one()) { 302 x[i]=x[--n]; c--; 303 } else if (x[i].zero()) { 304 x[i]=x[--n]; 305 } 306 x.size(n); 307 GECODE_ME_CHECK(y.lq(home,n-c)); 308 if (-c >= y.max()) 309 return home.ES_SUBSUMED(*this); 310 if (y.min()+c == n) { 311 for (int i = n; i--; ) 312 GECODE_ME_CHECK(x[i].one_none(home)); 313 return home.ES_SUBSUMED(*this); 314 } 315 if (y.assigned()) 316 GECODE_REWRITE(*this,GqBoolInt<XV>::post(home(*this),x,y.val()+c)); 317 return ES_FIX; 318 } 319 320}}} 321 322// STATISTICS: int-prop 323