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;
534 return nnf(
r,
n->l,!
neg);
539 NNF*
x =
new (
r) NNF;
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;
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--;)
const BoolExpr & operator=(const BoolExpr &e)
Assignment operator.
BoolExpr operator &&(const BoolExpr &l, const BoolExpr &r)
Conjunction of Boolean expressions.
Miscealloneous Boolean expressions.
IntConLevel
Consistency levels for integer propagators.
void post(Home home, Term *t, int n, FloatRelType frt, FloatVal c)
Post propagator for linear constraint over floats.
void rfree(void *p)
Free memory block starting at p.
LinIntExpr idx
The linear expression for the index.
int same
Number of variables in subtree with same type (for AND and OR)
bool assigned(void) const
Test whether view is assigned.
Node for Boolean expression
Linear relations over integer variables.
BoolExpr operator ^(const BoolExpr &l, const BoolExpr &r)
Exclusive-or of Boolean expressions.
bool pos(const View &x)
Test whether x is postive.
struct Gecode::@511::NNF::@54::@55 b
For binary nodes (and, or, eqv)
void * ralloc(size_t s)
Allocate s bytes from heap.
BoolExpr * a
The Boolean expressions.
~BoolExpr(void)
Destructor.
virtual ~MiscExpr(void)
Destructor.
Comparison relation (for two-sided comparisons)
void rel(Home home, IntConLevel icl) const
Post propagators for relation.
Heap heap
The single global heap.
int p
Number of positive literals for node type.
Gecode::IntArgs i(4, 1, 2, 3, 4)
int n
Number of negative literals for node type.
BoolVar x
Possibly a variable.
void clause(Home home, BoolOpType o, const BoolVarArgs &x, const BoolVarArgs &y, int n, IntConLevel)
Post domain consistent propagator for Boolean clause with positive variables x and negative variables...
int val(void) const
Return assigned value.
bool failed(void) const
Check whether corresponding space is failed.
unsigned int size(I &i)
Size of all ranges of range iterator i.
BElementExpr(int size)
Constructor.
MiscExpr * m
Possibly a misc Boolean expression.
SetRel rs
Possibly a reified set relation.
void element(Home home, IntSharedArray c, IntVar x0, IntVar x1, IntConLevel)
Post domain consistent propagator for .
NodeType t
Type of expression.
Passing Boolean variables.
struct Gecode::@511::NNF::@54::@56 a
For atomic nodes.
Other Boolean expression.
Boolean integer variables.
BoolVar expr(Home home, const BoolExpr &e, IntConLevel icl)
Post Boolean expression and return its value.
NodeType
Type of Boolean expression.
int n
The number of Boolean expressions.
void free(T *b, long unsigned int n)
Delete n objects starting at b.
Node * x
Pointer to corresponding Boolean expression node.
union Gecode::@511::NNF::@54 u
Union depending on nodetype t.
Linear expressions over integer variables.
Boolean element expressions.
LinFloatRel rfl
Possibly a reified float linear relation.
BoolExpr operator !(const BoolExpr &e)
Negated Boolean expression.
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVal n)
Propagates .
Node(void)
Default constructor.
Archive & operator<<(Archive &e, FloatNumBranch nl)
#define GECODE_MINIMODEL_EXPORT
virtual ~BElementExpr(void)
Destructor.
bool operator==(const FloatVal &x, const FloatVal &y)
Gecode toplevel namespace
bool operator !=(const FloatVal &x, const FloatVal &y)
LinIntRel rl
Possibly a reified linear relation.
Home class for posting propagators
bool decrement(void)
Decrement reference count and possibly free memory.
#define GECODE_NEVER
Assert that this command is never executed.
void post(Home home, IntRelType irt, IntConLevel icl) const
Post propagator.
BoolVar expr(Home home, IntConLevel icl) const
Post propagators for expression.
BoolExpr operator||(const BoolExpr &l, const BoolExpr &r)
Disjunction of Boolean expressions.
virtual void post(Space &home, BoolVar b, bool neg, IntConLevel icl)
Constrain b to be equivalent to the expression (negated if neg)
bool neg
Is atomic formula negative.
void rel(Home home, const BoolExpr &e, IntConLevel icl)
Post Boolean relation.
BoolExpr(void)
Default constructor.
unsigned int use
Nodes are reference counted.
Archive & operator >>(Archive &e, FloatNumBranch &nl)