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);
261 void post(Home home, NodeType t,
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--;)
bool failed(void) const
Check whether corresponding space is failed.
const BoolExpr & operator=(const BoolExpr &e)
Assignment operator.
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.
int size(void) const
Return size of array (number of elements)
LinIntExpr idx
The linear expression for the index.
int same
Number of variables in subtree with same type (for AND and OR)
Node for Boolean expression
Linear relations over integer variables.
bool pos(const View &x)
Test whether x is postive.
BoolExpr operator&&(const BoolExpr &l, const BoolExpr &r)
Conjunction of Boolean expressions.
void rel(Home home, IntConLevel icl) const
Post propagators for relation.
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)
BoolExpr operator^(const BoolExpr &l, const BoolExpr &r)
Exclusive-or of Boolean expressions.
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.
bool operator!=(const FloatVal &x, const FloatVal &y)
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...
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 .
BoolVar expr(Home home, IntConLevel icl) const
Post propagators for expression.
NodeType t
Type of expression.
Passing Boolean variables.
Other Boolean expression.
Boolean integer variables.
union Gecode::@518::NNF::@57 u
Union depending on nodetype t.
Archive & operator>>(Archive &e, FloatNumBranch &nl)
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.
Linear expressions over integer variables.
Boolean element expressions.
LinFloatRel rfl
Possibly a reified float linear relation.
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVal n)
Propagates .
int val(void) const
Return assigned value.
BoolExpr operator!(const BoolExpr &e)
Negated Boolean expression.
Node(void)
Default constructor.
Archive & operator<<(Archive &e, FloatNumBranch nl)
#define GECODE_MINIMODEL_EXPORT
bool assigned(void) const
Test whether view is assigned.
virtual ~BElementExpr(void)
Destructor.
bool operator==(const FloatVal &x, const FloatVal &y)
struct Gecode::@518::NNF::@57::@58 b
For binary nodes (and, or, eqv)
Gecode toplevel namespace
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.
struct Gecode::@518::NNF::@57::@59 a
For atomic nodes.
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 post(Home home, IntRelType irt, IntConLevel icl) const
Post propagator.
void rel(Home home, const BoolExpr &e, IntConLevel icl)
Post Boolean relation.
BoolExpr(void)
Default constructor.
unsigned int use
Nodes are reference counted.