| 411 | } |
| 412 | |
| 413 | void |
| 414 | NNF::rel(Home home, const IntPropLevels& ipls) const { |
| 415 | switch (t) { |
| 416 | case BoolExpr::NT_VAR: |
| 417 | Gecode::rel(home, u.a.x->x, IRT_EQ, u.a.neg ? 0 : 1); |
| 418 | break; |
| 419 | case BoolExpr::NT_RLIN: |
| 420 | u.a.x->rl.post(home, !u.a.neg, ipls); |
| 421 | break; |
| 422 | #ifdef GECODE_HAS_FLOAT_VARS |
| 423 | case BoolExpr::NT_RLINFLOAT: |
| 424 | u.a.x->rfl.post(home, !u.a.neg); |
| 425 | break; |
| 426 | #endif |
| 427 | #ifdef GECODE_HAS_SET_VARS |
| 428 | case BoolExpr::NT_RSET: |
| 429 | u.a.x->rs.post(home, !u.a.neg); |
| 430 | break; |
| 431 | #endif |
| 432 | case BoolExpr::NT_MISC: |
| 433 | { |
| 434 | BoolVar b(home,!u.a.neg,!u.a.neg); |
| 435 | u.a.x->m->post(home, b, false, ipls); |
| 436 | } |
| 437 | break; |
| 438 | case BoolExpr::NT_AND: |
| 439 | u.b.l->rel(home, ipls); |
| 440 | u.b.r->rel(home, ipls); |
| 441 | break; |
| 442 | case BoolExpr::NT_OR: |
| 443 | { |
| 444 | BoolVarArgs bp(p), bn(n); |
| 445 | int ip=0, in=0; |
| 446 | post(home, BoolExpr::NT_OR, bp, bn, ip, in, ipls); |
| 447 | clause(home, BOT_OR, bp, bn, 1); |
| 448 | } |
| 449 | break; |
| 450 | case BoolExpr::NT_EQV: |
| 451 | if (u.b.l->t==BoolExpr::NT_VAR && |
| 452 | u.b.r->t==BoolExpr::NT_RLIN) { |
| 453 | u.b.r->u.a.x->rl.post(home, u.b.l->u.a.x->x, |
| 454 | u.b.l->u.a.neg==u.b.r->u.a.neg, ipls); |
| 455 | } else if (u.b.r->t==BoolExpr::NT_VAR && |
| 456 | u.b.l->t==BoolExpr::NT_RLIN) { |
| 457 | u.b.l->u.a.x->rl.post(home, u.b.r->u.a.x->x, |
| 458 | u.b.l->u.a.neg==u.b.r->u.a.neg, ipls); |
| 459 | } else if (u.b.l->t==BoolExpr::NT_RLIN) { |
| 460 | u.b.l->u.a.x->rl.post(home, u.b.r->expr(home,ipls), |
| 461 | !u.b.l->u.a.neg,ipls); |
| 462 | } else if (u.b.r->t==BoolExpr::NT_RLIN) { |
| 463 | u.b.r->u.a.x->rl.post(home, u.b.l->expr(home,ipls), |
| 464 | !u.b.r->u.a.neg,ipls); |
| 465 | #ifdef GECODE_HAS_FLOAT_VARS |
| 466 | } else if (u.b.l->t==BoolExpr::NT_VAR && |
| 467 | u.b.r->t==BoolExpr::NT_RLINFLOAT) { |
| 468 | u.b.r->u.a.x->rfl.post(home, u.b.l->u.a.x->x, |
| 469 | u.b.l->u.a.neg==u.b.r->u.a.neg); |
| 470 | } else if (u.b.r->t==BoolExpr::NT_VAR && |