00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034 namespace Gecode { namespace Int { namespace Bool {
00035
00036
00037
00038
00039
00040
00041 template<class VX, class VY>
00042 forceinline
00043 ClauseTrue<VX,VY>::ClauseTrue(Home home,
00044 ViewArray<VX>& x0, ViewArray<VY>& y0)
00045 : MixBinaryPropagator<VX,PC_BOOL_VAL,VY,PC_BOOL_VAL>
00046 (home,x0[x0.size()-1],y0[y0.size()-1]), x(x0), y(y0) {
00047 assert((x.size() > 0) && (y.size() > 0));
00048 x.size(x.size()-1); y.size(y.size()-1);
00049 }
00050
00051 template<class VX, class VY>
00052 PropCost
00053 ClauseTrue<VX,VY>::cost(const Space&, const ModEventDelta&) const {
00054 return PropCost::binary(PropCost::LO);
00055 }
00056
00057 template<class VX, class VY>
00058 forceinline
00059 ClauseTrue<VX,VY>::ClauseTrue(Space& home, ClauseTrue<VX,VY>& p)
00060 : MixBinaryPropagator<VX,PC_BOOL_VAL,VY,PC_BOOL_VAL>(home,p) {
00061 x.update(home,p.x);
00062 y.update(home,p.y);
00063 }
00064
00065 template<class VX, class VY>
00066 Actor*
00067 ClauseTrue<VX,VY>::copy(Space& home) {
00068 {
00069 int n = x.size();
00070 if (n > 0) {
00071
00072 for (int i=n; i--; )
00073 if (x[i].one()) {
00074
00075 x[0]=x[i]; n=1; break;
00076 } else if (x[i].zero()) {
00077
00078 x[i]=x[--n];
00079 }
00080 x.size(n);
00081 }
00082 }
00083 {
00084 int n = y.size();
00085 if (n > 0) {
00086
00087 for (int i=n; i--; )
00088 if (y[i].one()) {
00089
00090 y[0]=y[i]; n=1; break;
00091 } else if (y[i].zero()) {
00092
00093 y[i]=y[--n];
00094 }
00095 y.size(n);
00096 }
00097 }
00098 if ((x.size() == 0) && (y.size() == 0))
00099 return new (home) BinOrTrue<VX,VY>(home,*this,x0,x1);
00100 else
00101 return new (home) ClauseTrue<VX,VY>(home,*this);
00102 }
00103
00104 template<class VX, class VY>
00105 inline ExecStatus
00106 ClauseTrue<VX,VY>::post(Home home, ViewArray<VX>& x, ViewArray<VY>& y) {
00107 for (int i=x.size(); i--; )
00108 if (x[i].one())
00109 return ES_OK;
00110 else if (x[i].zero())
00111 x.move_lst(i);
00112 if (x.size() == 0)
00113 return NaryOrTrue<VY>::post(home,y);
00114 for (int i=y.size(); i--; )
00115 if (y[i].one())
00116 return ES_OK;
00117 else if (y[i].zero())
00118 y.move_lst(i);
00119 if (y.size() == 0)
00120 return NaryOrTrue<VX>::post(home,x);
00121 if ((x.size() == 1) && (y.size() == 1)) {
00122 return BinOrTrue<VX,VY>::post(home,x[0],y[0]);
00123 } else if (!shared(x,y)) {
00124 (void) new (home) ClauseTrue(home,x,y);
00125 }
00126 return ES_OK;
00127 }
00128
00129 template<class VX, class VY>
00130 forceinline size_t
00131 ClauseTrue<VX,VY>::dispose(Space& home) {
00132 (void) MixBinaryPropagator<VX,PC_BOOL_VAL,VY,PC_BOOL_VAL>::dispose(home);
00133 return sizeof(*this);
00134 }
00135
00136 template<class VX, class VY>
00137 forceinline ExecStatus
00138 resubscribe(Space& home, Propagator& p,
00139 VX& x0, ViewArray<VX>& x,
00140 VY& x1, ViewArray<VY>& y) {
00141 if (x0.zero()) {
00142 int n = x.size();
00143 for (int i=n; i--; )
00144 if (x[i].one()) {
00145 x.size(n);
00146 return home.ES_SUBSUMED(p);
00147 } else if (x[i].zero()) {
00148 x[i] = x[--n];
00149 } else {
00150
00151 if ((i == 0) && (y.size() == 0)) {
00152 VX z = x[0]; x.size(0);
00153 GECODE_REWRITE(p,(BinOrTrue<VX,VY>::post(home(p),z,x1)));
00154 }
00155
00156 x0=x[i]; x[i]=x[--n];
00157 x.size(n);
00158 x0.subscribe(home,p,PC_BOOL_VAL,false);
00159 return ES_FIX;
00160 }
00161
00162 ViewArray<VY> z(home,y.size()+1);
00163 for (int i=0; i<y.size(); i++)
00164 z[i]=y[i];
00165 z[y.size()] = x1;
00166 GECODE_REWRITE(p,(NaryOrTrue<VY>::post(home(p),z)));
00167 }
00168 return ES_FIX;
00169 }
00170
00171 template<class VX, class VY>
00172 ExecStatus
00173 ClauseTrue<VX,VY>::propagate(Space& home, const ModEventDelta&) {
00174 if (x0.one() || x1.one())
00175 return home.ES_SUBSUMED(*this);
00176 GECODE_ES_CHECK(resubscribe(home,*this,x0,x,x1,y));
00177 GECODE_ES_CHECK(resubscribe(home,*this,x1,y,x0,x));
00178 return ES_FIX;
00179 }
00180
00181
00182
00183
00184
00185
00186
00187
00188
00189
00190
00191 template<class VX, class VY>
00192 forceinline
00193 Clause<VX,VY>::Tagged::Tagged(Space& home, Propagator& p,
00194 Council<Tagged>& c, bool x0)
00195 : Advisor(home,p,c), x(x0) {}
00196
00197 template<class VX, class VY>
00198 forceinline
00199 Clause<VX,VY>::Tagged::Tagged(Space& home, Tagged& a)
00200 : Advisor(home,a), x(a.x) {}
00201
00202 template<class VX, class VY>
00203 forceinline
00204 Clause<VX,VY>::Clause(Home home, ViewArray<VX>& x0, ViewArray<VY>& y0,
00205 VX z0)
00206 : Propagator(home), x(x0), y(y0), z(z0), n_zero(0), c(home) {
00207 x.subscribe(home,*new (home) Tagged(home,*this,c,true));
00208 y.subscribe(home,*new (home) Tagged(home,*this,c,false));
00209 z.subscribe(home,*this,PC_BOOL_VAL);
00210 }
00211
00212 template<class VX, class VY>
00213 forceinline
00214 Clause<VX,VY>::Clause(Space& home, Clause<VX,VY>& p)
00215 : Propagator(home,p), n_zero(p.n_zero) {
00216 x.update(home,p.x);
00217 y.update(home,p.y);
00218 z.update(home,p.z);
00219 c.update(home,p.c);
00220 }
00221
00222 template<class VX>
00223 forceinline void
00224 eliminate_zero(ViewArray<VX>& x, int& n_zero) {
00225 if (n_zero > 0) {
00226 int n=x.size();
00227
00228 for (int i=n; i--; )
00229 if (x[i].zero()) {
00230 x[i]=x[--n]; n_zero--;
00231 }
00232 x.size(n);
00233 }
00234 }
00235
00236 template<class VX, class VY>
00237 Actor*
00238 Clause<VX,VY>::copy(Space& home) {
00239 eliminate_zero(x,n_zero);
00240 eliminate_zero(y,n_zero);
00241 return new (home) Clause<VX,VY>(home,*this);
00242 }
00243
00244 template<class VX, class VY>
00245 inline ExecStatus
00246 Clause<VX,VY>::post(Home home, ViewArray<VX>& x, ViewArray<VY>& y, VX z) {
00247 assert(!shared(x) && !shared(y));
00248 if (z.one())
00249 return ClauseTrue<VX,VY>::post(home,x,y);
00250 if (z.zero()) {
00251 for (int i=0; i<x.size(); i++)
00252 GECODE_ME_CHECK(x[i].zero(home));
00253 for (int i=0; i<y.size(); i++)
00254 GECODE_ME_CHECK(y[i].zero(home));
00255 return ES_OK;
00256 }
00257 for (int i=x.size(); i--; )
00258 if (x[i].one()) {
00259 GECODE_ME_CHECK(z.one_none(home));
00260 return ES_OK;
00261 } else if (x[i].zero()) {
00262 x.move_lst(i);
00263 }
00264 if (x.size() == 0)
00265 return NaryOr<VY,VX>::post(home,y,z);
00266 for (int i=y.size(); i--; )
00267 if (y[i].one()) {
00268 GECODE_ME_CHECK(z.one_none(home));
00269 return ES_OK;
00270 } else if (y[i].zero()) {
00271 y.move_lst(i);
00272 }
00273 if (y.size() == 0)
00274 return NaryOr<VX,VX>::post(home,x,z);
00275 if ((x.size() == 1) && (y.size() == 1)) {
00276 return Or<VX,VY,VX>::post(home,x[0],y[0],z);
00277 } else if (shared(x,y)) {
00278 GECODE_ME_CHECK(z.one_none(home));
00279 } else {
00280 (void) new (home) Clause<VX,VY>(home,x,y,z);
00281 }
00282 return ES_OK;
00283 }
00284
00285 template<class VX, class VY>
00286 PropCost
00287 Clause<VX,VY>::cost(const Space&, const ModEventDelta&) const {
00288 return PropCost::unary(PropCost::LO);
00289 }
00290
00291 template<class VX, class VY>
00292 forceinline void
00293 Clause<VX,VY>::cancel(Space& home) {
00294 for (Advisors<Tagged> as(c); as(); ++as) {
00295 if (as.advisor().x)
00296 x.cancel(home,as.advisor());
00297 else
00298 y.cancel(home,as.advisor());
00299 as.advisor().dispose(home,c);
00300 }
00301 c.dispose(home);
00302 z.cancel(home,*this,PC_BOOL_VAL);
00303 }
00304
00305 template<class VX, class VY>
00306 forceinline size_t
00307 Clause<VX,VY>::dispose(Space& home) {
00308 cancel(home);
00309 (void) Propagator::dispose(home);
00310 return sizeof(*this);
00311 }
00312
00313
00314 template<class VX, class VY>
00315 ExecStatus
00316 Clause<VX,VY>::advise(Space&, Advisor& _a, const Delta& d) {
00317 Tagged& a = static_cast<Tagged&>(_a);
00318
00319 if ((a.x && VX::zero(d)) || (!a.x && VY::zero(d)))
00320 if (++n_zero < x.size() + y.size())
00321 return ES_FIX;
00322 return ES_NOFIX;
00323 }
00324
00325 template<class VX, class VY>
00326 void
00327 Clause<VX,VY>::reschedule(Space& home) {
00328 z.reschedule(home,*this,PC_BOOL_VAL);
00329 if (n_zero == x.size() + y.size())
00330 VX::schedule(home,*this,ME_BOOL_VAL);
00331 for (int i=0; i<x.size(); i++)
00332 if (x[i].one()) {
00333 VX::schedule(home,*this,ME_BOOL_VAL);
00334 return;
00335 }
00336 for (int i=0; i<y.size(); i++)
00337 if (y[i].one()) {
00338 VX::schedule(home,*this,ME_BOOL_VAL);
00339 return;
00340 }
00341 }
00342
00343 template<class VX, class VY>
00344 ExecStatus
00345 Clause<VX,VY>::propagate(Space& home, const ModEventDelta&) {
00346 if (z.one())
00347 GECODE_REWRITE(*this,(ClauseTrue<VX,VY>::post(home(*this),x,y)));
00348 if (z.zero()) {
00349 for (int i=0; i<x.size(); i++)
00350 GECODE_ME_CHECK(x[i].zero(home));
00351 for (int i=0; i<y.size(); i++)
00352 GECODE_ME_CHECK(y[i].zero(home));
00353 c.dispose(home);
00354 } else if (n_zero == x.size() + y.size()) {
00355 GECODE_ME_CHECK(z.zero_none(home));
00356 c.dispose(home);
00357 } else {
00358
00359 GECODE_ME_CHECK(z.one_none(home));
00360 }
00361 return home.ES_SUBSUMED(*this);
00362 }
00363
00364 }}}
00365
00366
00367