38#ifdef GECODE_HAS_SET_VARS
74 static void*
operator new(
size_t size);
76 static void operator delete(
void*
p,
size_t size);
86 SetExpr::Node::operator
new(
size_t size) {
90 SetExpr::Node::operator
delete(
void*
p, size_t) {
97 if ((
l !=
nullptr) &&
l->decrement())
99 if ((
r !=
nullptr) &&
r->decrement())
136 static NNF* nnf(Region&
r, Node*
n,
bool neg);
138 void post(Home home, NodeType
t, SetVarArgs&
b,
int& i)
const;
140 void post(Home home, SetRelType srt, SetVar s)
const;
142 void post(Home home, SetRelType srt, SetVar s, BoolVar
b)
const;
144 void post(Home home, SetRelType srt,
const NNF*
n)
const;
146 void post(Home home, BoolVar
b,
bool t, SetRelType srt,
149 static void*
operator new(
size_t s, Region&
r);
151 static void operator delete(
void*);
153 static void operator delete(
void*, Region&);
161 NNF::operator
delete(
void*) {}
164 NNF::operator
delete(
void*, Region&) {}
167 NNF::operator
new(
size_t s, Region&
r) {
172 NNF::post(Home home,
SetRelType srt, SetVar s)
const {
187 rel(home,
u.a.x->x, srt, bc);
191 rel(home,
u.a.x->x, srt, s);
197 IntSetRanges sr(
u.a.x->s);
198 Set::RangesCompl<IntSetRanges> src(sr);
208 dom(home, s, srt, ss);
238 rel(home, bc, srt, s);
257 rel(home, bc, srt, s);
294 rel(home, br, srt, bc);
305 rel(home, br, srt, s);
317 NNF::post(Home home,
SetRelType srt, SetVar s, BoolVar
b)
const {
332 rel(home,
u.a.x->x, srt, bc,
b);
336 rel(home,
u.a.x->x, srt, s,
b);
342 IntSetRanges sr(
u.a.x->s);
343 Set::RangesCompl<IntSetRanges> src(sr);
366 dom(home, s, invsrt, ss,
b);
376 rel(home,ic,srt,s,
b);
378 rel(home,iv,srt,s,
b);
390 rel(home, br, srt, s,
b);
401 rel(home, br, srt, s,
b);
421 rel(home, br, srt, bc);
428 rel(home, br, srt, s,
b);
438 NNF::post(Home home,
NodeType t, SetVarArgs&
b,
int& i)
const {
461 u.b.l->post(home,
t,
b, i);
462 u.b.r->post(home,
t,
b, i);
467 NNF::post(Home home,
SetRelType srt,
const NNF* n)
const {
469 post(home,srt,
n->u.a.x->x);
475 default: n_srt = srt;
477 n->post(home,n_srt,
this);
487 NNF::post(Home home, BoolVar
b,
bool pt,
491 post(home,srt,
n->u.a.x->x,
b);
497 default: n_srt = srt;
499 n->post(home,
b,
true,n_srt,
this);
506 }
else if (srt ==
SRT_EQ) {
508 }
else if (srt ==
SRT_NQ) {
511 BoolVar nb(home,0,1);
513 post(home,nb,
true,srt,n);
518 NNF::nnf(Region&
r, Node* n,
bool neg) {
524 NNF*
x =
new (
r) NNF;
534 return nnf(
r,
n->l,!
neg);
547 NNF*
x =
new (
r) NNF;
550 x->u.b.l = nnf(
r,
n->l,
neg);
551 x->u.b.r = nnf(
r,
n->r,
neg);
554 p_l=
x->u.b.l->p; n_l=
x->u.b.l->n;
560 p_r=
x->u.b.r->p; n_r=
x->u.b.r->n;
602 int ls =
same(
t,
l.n->t) ?
l.n->same : 1;
603 int rs =
same(
t,
r.n->t) ?
r.n->same : 1;
631 if (
n !=
nullptr &&
n->decrement())
640 if (
n !=
nullptr &&
n->decrement())
653 NNF::nnf(
r,
n,
false)->post(home,
SRT_EQ,s);
660 return NNF::nnf(
r,
n,
false)->post(home,srt,NNF::nnf(
r,e.n,
false));
666 return NNF::nnf(
r,
n,
false)->post(home,
b,
t,srt,
667 NNF::nnf(
r,e.n,
false));
700 for (
int i=1; i<
x.size(); i++)
709 for (
int i=1; i<
x.size(); i++)
718 for (
int i=1; i<
x.size(); i++)
723 namespace MiniModel {
741 IntVar m = result(home,ret);
747 min(home, e.
post(home), m);
750 max(home, e.
post(home), m);
760 if (
t==SNLE_CARD && irt!=
IRT_NQ) {
765 static_cast<unsigned int>(c));
770 static_cast<unsigned int>(c-1));
774 static_cast<unsigned int>(c),
779 static_cast<unsigned int>(c+1),
784 static_cast<unsigned int>(c),
785 static_cast<unsigned int>(c));
791 c = (irt==
IRT_GQ ? c : c+1);
794 c = (irt==
IRT_LQ ? c : c-1);
797 rel(home, post(home,
nullptr,ipls), irt, c);
804 c = (irt==
IRT_GQ ? c : c+1);
807 c = (irt==
IRT_LQ ? c : c-1);
810 rel(home, post(home,
nullptr,ipls), irt, c,
b);
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.
Boolean integer variables.
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.
static const IntPropLevels def
Default propagation levels for all constraints.
static const IntSet empty
Empty set.
Linear expressions over integer variables.
Integer valued set expressions.
virtual void post(Home home, IntRelType irt, int c, const IntPropLevels &ipls) const
Post expression to be in relation irt with c.
virtual void post(Home home, IntRelType irt, int c, BoolVar b, const IntPropLevels &ipls) const
Post reified expression to be in relation irt with c.
SetNonLinIntExpr(const SetExpr &e0, SetNonLinIntExprType t0)
Constructor.
SetNonLinIntExprType
The expression type.
@ SNLE_MAX
Maximum element expression.
@ SNLE_MIN
Minimum element expression.
@ SNLE_CARD
Cardinality expression.
virtual IntVar post(Home home, IntVar *ret, const IntPropLevels &) const
Post expression.
Base class for non-linear expressions over integer variables.
Class to set group information when a post function is executed.
int same
Number of variables in subtree with same type (for INTER and UNION)
NodeType t
Type of expression.
bool decrement(void)
Decrement reference count and possibly free memory.
SetVar x
Possibly a variable.
Node(void)
Default constructor.
LinIntExpr e
Possibly a linear expression.
unsigned int use
Nodes are reference counted.
IntSet s
Possibly a constant.
SetExpr(void)
Default constructor.
SetVar post(Home home) const
Post propagators for expression.
~SetExpr(void)
Destructor.
NodeType
Type of set expression.
@ NT_DUNION
Disjoint union.
@ NT_LEXP
Linear expression.
const SetExpr & operator=(const SetExpr &e)
Assignment operator.
VarImp * x
Pointer to variable implementation.
Heap heap
The single global heap.
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVar x1)
Post propagator for .
IntRelType
Relation types for integers.
@ IRT_GQ
Greater or equal ( )
@ IRT_LQ
Less or equal ( )
SetRelType
Common relation types for sets.
@ SOT_DUNION
Disjoint union.
@ SRT_GQ
Greater or equal ( )
@ SRT_LQ
Less or equal ( )
#define GECODE_MINIMODEL_EXPORT
const int min
Smallest allowed integer in integer set.
const int max
Largest allowed integer in integer set.
Gecode toplevel namespace
FloatVal operator-(const FloatVal &x)
FloatVal operator+(const FloatVal &x)
Post propagator for SetVar SetOpType SetVar SetRelType r
IntVar expr(Home home, const LinIntExpr &e, const IntPropLevels &ipls=IntPropLevels::def)
Post linear expression and return its value.
SetExpr operator&(const SetExpr &, const SetExpr &)
Intersection of set expressions.
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
void dom(Home home, FloatVar x, FloatVal n)
Propagates .
SetExpr inter(const SetVarArgs &)
Intersection of set variables.
bool same(VarArgArray< Var > x, VarArgArray< Var > y)
SetExpr setdunion(const SetVarArgs &)
Disjoint union of set variables.
SetExpr setunion(const SetVarArgs &)
Union of set variables.
SetExpr singleton(const LinIntExpr &)
Singleton expression.
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
SetExpr operator|(const SetExpr &, const SetExpr &)
Union of set expressions.
LinIntExpr cardinality(const SetExpr &)
Cardinality of set expression.
Post propagator for SetVar x
Gecode::IntArgs i({1, 2, 3, 4})
#define GECODE_NEVER
Assert that this command is never executed.