| 287 | } |
| 288 | |
| 289 | BoolVar |
| 290 | NNF::expr(Home home, const IntPropLevels& ipls) const { |
| 291 | if ((t == BoolExpr::NT_VAR) && !u.a.neg) |
| 292 | return u.a.x->x; |
| 293 | BoolVar b(home,0,1); |
| 294 | switch (t) { |
| 295 | case BoolExpr::NT_VAR: |
| 296 | assert(u.a.neg); |
| 297 | Gecode::rel(home, u.a.x->x, IRT_NQ, b); |
| 298 | break; |
| 299 | case BoolExpr::NT_RLIN: |
| 300 | u.a.x->rl.post(home, b, !u.a.neg, ipls); |
| 301 | break; |
| 302 | #ifdef GECODE_HAS_FLOAT_VARS |
| 303 | case BoolExpr::NT_RLINFLOAT: |
| 304 | u.a.x->rfl.post(home, b, !u.a.neg); |
| 305 | break; |
| 306 | #endif |
| 307 | #ifdef GECODE_HAS_SET_VARS |
| 308 | case BoolExpr::NT_RSET: |
| 309 | u.a.x->rs.post(home, b, !u.a.neg); |
| 310 | break; |
| 311 | #endif |
| 312 | case BoolExpr::NT_MISC: |
| 313 | u.a.x->m->post(home, b, u.a.neg, ipls); |
| 314 | break; |
| 315 | case BoolExpr::NT_AND: |
| 316 | { |
| 317 | BoolVarArgs bp(p), bn(n); |
| 318 | int ip=0, in=0; |
| 319 | post(home, BoolExpr::NT_AND, bp, bn, ip, in, ipls); |
| 320 | clause(home, BOT_AND, bp, bn, b); |
| 321 | } |
| 322 | break; |
| 323 | case BoolExpr::NT_OR: |
| 324 | { |
| 325 | BoolVarArgs bp(p), bn(n); |
| 326 | int ip=0, in=0; |
| 327 | post(home, BoolExpr::NT_OR, bp, bn, ip, in, ipls); |
| 328 | clause(home, BOT_OR, bp, bn, b); |
| 329 | } |
| 330 | break; |
| 331 | case BoolExpr::NT_EQV: |
| 332 | { |
| 333 | bool n = false; |
| 334 | BoolVar l; |
| 335 | if (u.b.l->t == BoolExpr::NT_VAR) { |
| 336 | l = u.b.l->u.a.x->x; |
| 337 | if (u.b.l->u.a.neg) n = !n; |
| 338 | } else { |
| 339 | l = u.b.l->expr(home,ipls); |
| 340 | } |
| 341 | BoolVar r; |
| 342 | if (u.b.r->t == BoolExpr::NT_VAR) { |
| 343 | r = u.b.r->u.a.x->x; |
| 344 | if (u.b.r->u.a.neg) n = !n; |
| 345 | } else { |
| 346 | r = u.b.r->expr(home,ipls); |