57#ifdef GECODE_HAS_FLOAT_VARS
61#ifdef GECODE_HAS_SET_VARS
76 static void*
operator new(
size_t size);
78 static void operator delete(
void*
p,
size_t size);
87 : use(1),
l(nullptr),
r(nullptr), m(nullptr) {}
94 BoolExpr::Node::operator
new(
size_t size) {
98 BoolExpr::Node::operator
delete(
void*
p, size_t) {
105 if ((
l !=
nullptr) &&
l->decrement())
107 if ((
r !=
nullptr) &&
r->decrement())
130 int ls = ((
l.n->t ==
t) || (
l.n->t ==
NT_VAR)) ?
l.n->same : 1;
131 int rs = ((
r.n->t ==
t) || (
r.n->t ==
NT_VAR)) ?
r.n->same : 1;
165#ifdef GECODE_HAS_FLOAT_VARS
176#ifdef GECODE_HAS_SET_VARS
253 static NNF* nnf(Region&
r, Node*
n,
bool neg);
256 void post(Home home, NodeType
t,
257 BoolVarArgs& bp, BoolVarArgs& bn,
259 const IntPropLevels& ipls)
const;
262 BoolVar
expr(Home home,
const IntPropLevels& ipls)
const;
265 void rel(Home home,
const IntPropLevels& ipls)
const;
267 static void*
operator new(
size_t s, Region&
r);
269 static void operator delete(
void*);
271 static void operator delete(
void*, Region&);
279 NNF::operator
delete(
void*) {}
282 NNF::operator
delete(
void*, Region&) {}
285 NNF::operator
new(
size_t s, Region&
r) {
290 NNF::expr(Home home,
const IntPropLevels& ipls)
const {
300 u.a.x->rl.post(home,
b, !
u.a.neg, ipls);
302#ifdef GECODE_HAS_FLOAT_VARS
304 u.a.x->rfl.post(home,
b, !
u.a.neg);
307#ifdef GECODE_HAS_SET_VARS
309 u.a.x->rs.post(home,
b, !
u.a.neg);
313 u.a.x->m->post(home,
b,
u.a.neg, ipls);
317 BoolVarArgs bp(
p), bn(n);
325 BoolVarArgs bp(
p), bn(n);
337 if (
u.b.l->u.a.neg)
n = !
n;
339 l =
u.b.l->expr(home,ipls);
344 if (
u.b.r->u.a.neg)
n = !
n;
346 r =
u.b.r->expr(home,ipls);
359 BoolVarArgs& bp, BoolVarArgs& bn,
361 const IntPropLevels& ipls)
const {
374 u.a.x->rl.post(home,
b, !
u.a.neg, ipls);
378#ifdef GECODE_HAS_FLOAT_VARS
382 u.a.x->rfl.post(home,
b, !
u.a.neg);
387#ifdef GECODE_HAS_SET_VARS
391 u.a.x->rs.post(home,
b, !
u.a.neg);
399 u.a.x->m->post(home,
b,
u.a.neg, ipls);
404 bp[ip++] =
expr(home, ipls);
408 u.b.l->post(home,
t, bp, bn, ip, in, ipls);
409 u.b.r->post(home,
t, bp, bn, ip, in, ipls);
414 NNF::rel(Home home,
const IntPropLevels& ipls)
const {
420 u.a.x->rl.post(home, !
u.a.neg, ipls);
422#ifdef GECODE_HAS_FLOAT_VARS
424 u.a.x->rfl.post(home, !
u.a.neg);
427#ifdef GECODE_HAS_SET_VARS
429 u.a.x->rs.post(home, !
u.a.neg);
434 BoolVar
b(home,!
u.a.neg,!
u.a.neg);
435 u.a.x->m->post(home,
b,
false, ipls);
439 u.b.l->rel(home, ipls);
440 u.b.r->rel(home, ipls);
444 BoolVarArgs bp(
p), bn(n);
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);
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);
460 u.b.l->u.a.x->rl.post(home,
u.b.r->expr(home,ipls),
461 !
u.b.l->u.a.neg,ipls);
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
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);
472 u.b.l->u.a.x->rfl.post(home,
u.b.r->u.a.x->x,
473 u.b.l->u.a.neg==
u.b.r->u.a.neg);
475 u.b.l->u.a.x->rfl.post(home,
u.b.r->expr(home,ipls),
478 u.b.r->u.a.x->rfl.post(home,
u.b.l->expr(home,ipls),
481#ifdef GECODE_HAS_SET_VARS
484 u.b.r->u.a.x->rs.post(home,
u.b.l->u.a.x->x,
485 u.b.l->u.a.neg==
u.b.r->u.a.neg);
488 u.b.l->u.a.x->rs.post(home,
u.b.r->u.a.x->x,
489 u.b.l->u.a.neg==
u.b.r->u.a.neg);
491 u.b.l->u.a.x->rs.post(home,
u.b.r->expr(home,ipls),
494 u.b.r->u.a.x->rs.post(home,
u.b.l->expr(home,ipls),
507 NNF::nnf(Region&
r, Node* n,
bool neg) {
512 #ifdef GECODE_HAS_FLOAT_VARS
515 #ifdef GECODE_HAS_SET_VARS
519 NNF*
x =
new (
r) NNF;
520 x->t =
n->t;
x->u.a.neg =
neg;
x->u.a.
x =
n;
529 return nnf(
r,
n->l,!
neg);
534 NNF*
x =
new (
r) NNF;
536 x->u.b.l = nnf(
r,
n->l,
neg);
537 x->u.b.r = nnf(
r,
n->r,
neg);
539 if ((
x->u.b.l->t ==
t) ||
541 p_l=
x->u.b.l->p; n_l=
x->u.b.l->n;
546 if ((
x->u.b.r->t ==
t) ||
548 p_r=
x->u.b.r->p; n_r=
x->u.b.r->n;
558 NNF*
x =
new (
r) NNF;
560 x->u.b.l = nnf(
r,
n->l,
neg);
561 x->u.b.r = nnf(
r,
n->r,
false);
576 return NNF::nnf(
r,
n,
false)->expr(home,ipls);
582 return NNF::nnf(
r,
n,
false)->rel(home,ipls);
632 return e.
expr(home,ipls);
669 for (
int i=
b.
size(); i--;)
687 x[i] =
a[i].
expr(home,ipls);
struct Gecode::@603::NNF::@65::@66 b
For binary nodes (and, or, eqv)
union Gecode::@603::NNF::@65 u
Union depending on nodetype t.
int p
Number of positive literals for node type.
int n
Number of negative literals for node type.
struct Gecode::@603::NNF::@65::@67 a
For atomic nodes.
Node * x
Pointer to corresponding Boolean expression node.
bool neg
Is atomic formula negative.
int size(void) const
Return size of array (number of elements)
Boolean element expressions.
LinIntExpr idx
The linear expression for the index.
int n
The number of Boolean expressions.
virtual void post(Home home, BoolVar b, bool neg, const IntPropLevels &ipls)
Constrain b to be equivalent to the expression (negated if neg)
virtual ~BElementExpr(void)
Destructor.
BElementExpr(const BoolVarArgs &b, const LinIntExpr &idx)
Constructor.
BoolExpr * a
The Boolean expressions.
Miscealloneous Boolean expressions.
virtual ~Misc(void)
Destructor.
Node for Boolean expression
BoolVar x
Possibly a variable.
NodeType t
Type of expression.
Node(void)
Default constructor.
LinFloatRel rfl
Possibly a reified float linear relation.
LinIntRel rl
Possibly a reified linear relation.
SetRel rs
Possibly a reified set relation.
bool decrement(void)
Decrement reference count and possibly free memory.
Misc * m
Possibly a misc Boolean expression.
unsigned int use
Nodes are reference counted.
int same
Number of variables in subtree with same type (for AND and OR)
BoolExpr(void)
Default constructor.
NodeType
Type of Boolean expression.
@ NT_RLINFLOAT
Reified linear relation.
@ NT_RLIN
Reified linear relation.
@ NT_MISC
Other Boolean expression.
@ NT_RSET
Reified set relation.
const BoolExpr & operator=(const BoolExpr &e)
Assignment operator.
BoolVar expr(Home home, const IntPropLevels &ipls) const
Post propagators for expression.
~BoolExpr(void)
Destructor.
void rel(Home home, const IntPropLevels &ipls) const
Post propagators for relation.
Passing Boolean variables.
Boolean integer variables.
void free(T *b, long unsigned int n)
Delete n objects starting at b.
void rfree(void *p)
Free memory block starting at p.
void * ralloc(size_t s)
Allocate s bytes from heap.
Home class for posting propagators
bool failed(void) const
Check whether corresponding space is failed.
Class for specifying integer propagation levels used by minimodel.
IntPropLevel element(void) const
Return integer propagation level for element constraints.
Linear expressions over integer variables.
void post(Home home, IntRelType irt, const IntPropLevels &ipls) const
Post propagator.
Linear relations over integer variables.
Class to set group information when a post function is executed.
Comparison relation (for two-sided comparisons)
bool assigned(void) const
Test whether view is assigned.
VarImp * x
Pointer to variable implementation.
void post(Home home, Term *t, int n, FloatRelType frt, FloatVal c)
Post propagator for linear constraint over floats.
Heap heap
The single global heap.
#define GECODE_POST
Check for failure in a constraint post function.
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVar x1)
Post propagator for .
void clause(Home home, BoolOpType o, const BoolVarArgs &x, const BoolVarArgs &y, BoolVar z, IntPropLevel ipl=IPL_DEF)
Post domain consistent propagator for Boolean clause with positive variables x and negative variables...
#define GECODE_MINIMODEL_EXPORT
Gecode toplevel namespace
Post propagator for SetVar SetOpType SetVar SetRelType r
SetRel operator||(const SetExpr &, const SetExpr &)
Disjointness of set expressions.
IntVar expr(Home home, const LinIntExpr &e, const IntPropLevels &ipls=IntPropLevels::def)
Post linear expression and return its value.
Archive & operator<<(Archive &e, FloatNumBranch nl)
void element(Home home, IntSharedArray n, IntVar x0, IntVar x1, IntPropLevel ipl=IPL_DEF)
Post domain consistent propagator for .
BoolExpr operator!(const BoolExpr &)
Negated Boolean expression.
Post propagator for SetVar SetOpType SetVar SetRelType SetVar z
BoolExpr operator^(const BoolExpr &, const BoolExpr &)
Exclusive-or of Boolean expressions.
BoolExpr operator&&(const BoolExpr &, const BoolExpr &)
Conjunction of Boolean expressions.
TFE post(PropagatorGroup g)
Only post functions (but not propagators) from g are considered.
Archive & operator>>(Archive &e, FloatNumBranch &nl)
Post propagator for SetVar x
bool operator==(const FloatVal &x, const FloatVal &y)
bool operator!=(const FloatVal &x, const FloatVal &y)
#define GECODE_NEVER
Assert that this command is never executed.