61 #ifdef GECODE_HAS_FLOAT_VARS
65 #ifdef GECODE_HAS_SET_VARS
80 static void*
operator new(
size_t size);
82 static void operator delete(
void*
p,
size_t size);
91 : use(1),
l(NULL),
r(NULL), m(NULL) {}
98 BoolExpr::Node::operator
new(
size_t size) {
102 BoolExpr::Node::operator
delete(
void*
p, size_t) {
109 if ((
l != NULL) &&
l->decrement())
111 if ((
r != NULL) &&
r->decrement())
134 int ls = ((l.n->
t ==
t) || (l.n->
t ==
NT_VAR)) ? l.n->
same : 1;
135 int rs = ((r.n->
t == t) || (r.n->
t ==
NT_VAR)) ? r.n->
same : 1;
169 #ifdef GECODE_HAS_FLOAT_VARS
180 #ifdef GECODE_HAS_SET_VARS
258 static NNF* nnf(Region&
r, Node* n,
bool neg);
262 BoolVarArgs& bp, BoolVarArgs& bn,
272 static void*
operator new(
size_t s, Region&
r);
274 static void operator delete(
void*);
276 static void operator delete(
void*, Region&);
284 NNF::operator
delete(
void*) {}
287 NNF::operator
delete(
void*, Region&) {}
290 NNF::operator
new(
size_t s, Region&
r) {
305 u.a.x->rl.post(home,
b, !
u.a.neg, icl);
307 #ifdef GECODE_HAS_FLOAT_VARS
309 u.a.x->rfl.post(home,
b, !
u.a.neg);
312 #ifdef GECODE_HAS_SET_VARS
314 u.a.x->rs.post(home,
b, !
u.a.neg);
318 u.a.x->m->post(home,
b, !
u.a.neg, icl);
322 BoolVarArgs bp(
p), bn(n);
330 BoolVarArgs bp(
p), bn(n);
342 if (
u.b.l->u.a.neg) n = !n;
344 l =
u.b.l->expr(home,icl);
349 if (
u.b.r->u.a.neg) n = !n;
351 r =
u.b.r->expr(home,icl);
364 BoolVarArgs& bp, BoolVarArgs& bn,
379 u.a.x->rl.post(home,
b, !
u.a.neg, icl);
383 #ifdef GECODE_HAS_FLOAT_VARS
387 u.a.x->rfl.post(home,
b, !
u.a.neg);
392 #ifdef GECODE_HAS_SET_VARS
396 u.a.x->rs.post(home,
b, !
u.a.neg);
404 u.a.x->m->post(home,
b, !
u.a.neg, icl);
409 bp[ip++] =
expr(home, icl);
413 u.b.l->post(home, t, bp, bn, ip, in, icl);
414 u.b.r->post(home, t, bp, bn, ip, in, icl);
425 u.a.x->rl.post(home, !
u.a.neg, icl);
427 #ifdef GECODE_HAS_FLOAT_VARS
429 u.a.x->rfl.post(home, !
u.a.neg);
432 #ifdef GECODE_HAS_SET_VARS
434 u.a.x->rs.post(home, !
u.a.neg);
439 BoolVar
b(home,!
u.a.neg,!
u.a.neg);
440 u.a.x->m->post(home,
b,
false, icl);
444 u.b.l->rel(home, icl);
445 u.b.r->rel(home, icl);
449 BoolVarArgs bp(
p), bn(n);
458 u.b.r->u.a.x->rl.post(home,
u.b.l->u.a.x->x,
459 u.b.l->u.a.neg==
u.b.r->u.a.neg, icl);
462 u.b.l->u.a.x->rl.post(home,
u.b.r->u.a.x->x,
463 u.b.l->u.a.neg==
u.b.r->u.a.neg, icl);
465 u.b.l->u.a.x->rl.post(home,
u.b.r->expr(home,icl),
466 !
u.b.l->u.a.neg,icl);
468 u.b.r->u.a.x->rl.post(home,
u.b.l->expr(home,icl),
469 !
u.b.r->u.a.neg,icl);
470 #ifdef GECODE_HAS_FLOAT_VARS
473 u.b.r->u.a.x->rfl.post(home,
u.b.l->u.a.x->x,
474 u.b.l->u.a.neg==
u.b.r->u.a.neg);
477 u.b.l->u.a.x->rfl.post(home,
u.b.r->u.a.x->x,
478 u.b.l->u.a.neg==
u.b.r->u.a.neg);
480 u.b.l->u.a.x->rfl.post(home,
u.b.r->expr(home,icl),
483 u.b.r->u.a.x->rfl.post(home,
u.b.l->expr(home,icl),
486 #ifdef GECODE_HAS_SET_VARS
489 u.b.r->u.a.x->rs.post(home,
u.b.l->u.a.x->x,
490 u.b.l->u.a.neg==
u.b.r->u.a.neg);
493 u.b.l->u.a.x->rs.post(home,
u.b.r->u.a.x->x,
494 u.b.l->u.a.neg==
u.b.r->u.a.neg);
496 u.b.l->u.a.x->rs.post(home,
u.b.r->expr(home,icl),
499 u.b.r->u.a.x->rs.post(home,
u.b.l->expr(home,icl),
512 NNF::nnf(Region& r, Node* n,
bool neg) {
517 #ifdef GECODE_HAS_FLOAT_VARS
520 #ifdef GECODE_HAS_SET_VARS
524 NNF*
x =
new (
r) NNF;
525 x->t = n->t; x->u.a.neg =
neg; x->u.a.x = n;
534 return nnf(r,n->l,!neg);
539 NNF* x =
new (
r) NNF;
541 x->u.b.l = nnf(r,n->l,neg);
542 x->u.b.r = nnf(r,n->r,neg);
544 if ((x->u.b.l->t == t) ||
546 p_l=x->u.b.l->p; n_l=x->u.b.l->n;
551 if ((x->u.b.r->t == t) ||
553 p_r=x->u.b.r->p; n_r=x->u.b.r->n;
563 NNF* x =
new (
r) NNF;
565 x->u.b.l = nnf(r,n->l,neg);
566 x->u.b.r = nnf(r,n->r,
false);
581 return NNF::nnf(r,n,
false)->expr(home,icl);
587 return NNF::nnf(r,n,
false)->rel(home,icl);
634 return e.
expr(home,icl);
641 if (home.
failed())
return;
692 for (
int i=b.
size();
i--;)