Something went wrong. Try again.
This repository has no description
Something went wrong. Try again.
24 kB · 849 lines
C++
at develop
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- *//* * Main authors: * Guido Tack <tack@gecode.org> * Christian Schulte <schulte@gecode.org> * * Copyright: * Guido Tack, 2010 * Christian Schulte, 2004 * * This file is part of Gecode, the generic constraint * development environment: * http://www.gecode.org * * Permission is hereby granted, free of charge, to any person obtaining * a copy of this software and associated documentation files (the * "Software"), to deal in the Software without restriction, including * without limitation the rights to use, copy, modify, merge, publish, * distribute, sublicense, and/or sell copies of the Software, and to * permit persons to whom the Software is furnished to do so, subject to * the following conditions: * * The above copyright notice and this permission notice shall be * included in all copies or substantial portions of the Software. * * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. * */
#include <gecode/minimodel.hh>
#ifdef GECODE_HAS_SET_VARS
namespace Gecode {
namespace { /// Check if types agree static bool same(SetExpr::NodeType t0, SetExpr::NodeType t1) { return (t0==t1) || (t1==SetExpr::NT_VAR) || (t1==SetExpr::NT_CONST) || (t1==SetExpr::NT_LEXP); } }
/// %Node for set expression class SetExpr::Node { public: /// Nodes are reference counted unsigned int use; /// Number of variables in subtree with same type (for INTER and UNION) int same; /// Type of expression NodeType t; /// Subexpressions Node *l, *r; /// Possibly a variable SetVar x; /// Possibly a constant IntSet s; /// Possibly a linear expression LinIntExpr e;
/// Default constructor Node(void); /// Decrement reference count and possibly free memory GECODE_MINIMODEL_EXPORT bool decrement(void); /// Memory management static void* operator new(size_t size); /// Memory management static void operator delete(void* p, size_t size); };
/* * Operations for nodes * */ SetExpr::Node::Node(void) : use(1) {}
void* SetExpr::Node::operator new(size_t size) { return heap.ralloc(size); } void SetExpr::Node::operator delete(void* p, size_t) { heap.rfree(p); }
bool SetExpr::Node::decrement(void) { if (--use == 0) { if ((l != nullptr) && l->decrement()) delete l; if ((r != nullptr) && r->decrement()) delete r; return true; } return false; }
namespace { /// %Node for negation normalform (%NNF) class NNF { public: typedef SetExpr::NodeType NodeType; typedef SetExpr::Node Node; /// Type of node NodeType t; /// Number of positive literals for node type int p; /// Number of negative literals for node type int n; /// Union depending on nodetype \a t union { /// For binary nodes (and, or, eqv) struct { /// Left subtree NNF* l; /// Right subtree NNF* r; } b; /// For atomic nodes struct { /// Pointer to corresponding Boolean expression node Node* x; } a; } u; /// Is formula negative bool neg; /// Create negation normalform static NNF* nnf(Region& r, Node* n, bool neg); /// Post propagators for nested conjunctive and disjunctive expression void post(Home home, NodeType t, SetVarArgs& b, int& i) const; /// Post propagators for expression void post(Home home, SetRelType srt, SetVar s) const; /// Post propagators for reified expression void post(Home home, SetRelType srt, SetVar s, BoolVar b) const; /// Post propagators for relation void post(Home home, SetRelType srt, const NNF* n) const; /// Post reified propagators for relation (or negated relation if \a t is false) void post(Home home, BoolVar b, bool t, SetRelType srt, const NNF* n) const; /// Allocate memory from region static void* operator new(size_t s, Region& r); /// No-op (for exceptions) static void operator delete(void*); /// No-op static void operator delete(void*, Region&); };
/* * Operations for negation normalform * */ forceinline void NNF::operator delete(void*) {}
forceinline void NNF::operator delete(void*, Region&) {}
forceinline void* NNF::operator new(size_t s, Region& r) { return r.ralloc(s); }
void NNF::post(Home home, SetRelType srt, SetVar s) const { switch (t) { case SetExpr::NT_VAR: if (neg) { switch (srt) { case SRT_EQ: rel(home, u.a.x->x, SRT_CMPL, s); break; case SRT_CMPL: rel(home, u.a.x->x, SRT_EQ, s); break; default: SetVar bc(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, s, SRT_CMPL, bc); rel(home, u.a.x->x, srt, bc); break; } } else rel(home, u.a.x->x, srt, s); break; case SetExpr::NT_CONST: { IntSet ss; if (neg) { IntSetRanges sr(u.a.x->s); Set::RangesCompl<IntSetRanges> src(sr); ss = IntSet(src); } else { ss = u.a.x->s; } switch (srt) { case SRT_SUB: srt = SRT_SUP; break; case SRT_SUP: srt = SRT_SUB; break; default: break; } dom(home, s, srt, ss); } break; case SetExpr::NT_LEXP: { IntVar iv = u.a.x->e.post(home,IntPropLevels::def); if (neg) { SetVar ic(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, iv, SRT_CMPL, ic); rel(home,ic,srt,s); } else { rel(home,iv,srt,s); } } break; case SetExpr::NT_INTER: { SetVarArgs bs(p+n); int i=0; post(home, SetExpr::NT_INTER, bs, i); if (i == 2) { rel(home, bs[0], SOT_INTER, bs[1], srt, s); } else { if (srt == SRT_EQ) rel(home, SOT_INTER, bs, s); else { SetVar bc(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, SOT_INTER, bs, bc); rel(home, bc, srt, s); } } } break; case SetExpr::NT_UNION: { SetVarArgs bs(p+n); int i=0; post(home, SetExpr::NT_UNION, bs, i); if (i == 2) { rel(home, bs[0], SOT_UNION, bs[1], srt, s); } else { if (srt == SRT_EQ) rel(home, SOT_UNION, bs, s); else { SetVar bc(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, SOT_UNION, bs, bc); rel(home, bc, srt, s); } } } break; case SetExpr::NT_DUNION: { SetVarArgs bs(p+n); int i=0; post(home, SetExpr::NT_DUNION, bs, i);
if (i == 2) { if (neg) { if (srt == SRT_CMPL) { rel(home, bs[0], SOT_DUNION, bs[1], srt, s); } else { SetVar bc(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home,s,SRT_CMPL,bc); rel(home, bs[0], SOT_DUNION, bs[1], srt, bc); } } else { rel(home, bs[0], SOT_DUNION, bs[1], srt, s); } } else { if (neg) { if (srt == SRT_CMPL) { rel(home, SOT_DUNION, bs, s); } else { SetVar br(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, SOT_DUNION, bs, br); if (srt == SRT_EQ) rel(home, br, SRT_CMPL, s); else { SetVar bc(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, br, srt, bc); rel(home, bc, SRT_CMPL, s); } } } else { if (srt == SRT_EQ) rel(home, SOT_DUNION, bs, s); else { SetVar br(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, SOT_DUNION, bs, br); rel(home, br, srt, s); } } } } break; default: GECODE_NEVER; } }
void NNF::post(Home home, SetRelType srt, SetVar s, BoolVar b) const { switch (t) { case SetExpr::NT_VAR: if (neg) { switch (srt) { case SRT_EQ: rel(home, u.a.x->x, SRT_CMPL, s, b); break; case SRT_CMPL: rel(home, u.a.x->x, SRT_EQ, s, b); break; default: SetVar bc(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, s, SRT_CMPL, bc); rel(home, u.a.x->x, srt, bc, b); break; } } else rel(home, u.a.x->x, srt, s, b); break; case SetExpr::NT_CONST: { IntSet ss; if (neg) { IntSetRanges sr(u.a.x->s); Set::RangesCompl<IntSetRanges> src(sr); ss = IntSet(src); } else { ss = u.a.x->s; } SetRelType invsrt; switch (srt) { case SRT_SUB: invsrt = SRT_SUP; break; case SRT_SUP: invsrt = SRT_SUB; break; case SRT_LQ: invsrt = SRT_GQ; break; case SRT_LE: invsrt = SRT_GR; break; case SRT_GQ: invsrt = SRT_LQ; break; case SRT_GR: invsrt = SRT_LE; break; case SRT_EQ: case SRT_NQ: case SRT_DISJ: case SRT_CMPL: invsrt = srt; break; default: invsrt = srt; GECODE_NEVER; } dom(home, s, invsrt, ss, b); } break; case SetExpr::NT_LEXP: { IntVar iv = u.a.x->e.post(home,IntPropLevels::def); if (neg) { SetVar ic(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, iv, SRT_CMPL, ic); rel(home,ic,srt,s,b); } else { rel(home,iv,srt,s,b); } } break; case SetExpr::NT_INTER: { SetVarArgs bs(p+n); int i=0; post(home, SetExpr::NT_INTER, bs, i); SetVar br(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, SOT_INTER, bs, br); rel(home, br, srt, s, b); } break; case SetExpr::NT_UNION: { SetVarArgs bs(p+n); int i=0; post(home, SetExpr::NT_UNION, bs, i); SetVar br(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, SOT_UNION, bs, br); rel(home, br, srt, s, b); } break; case SetExpr::NT_DUNION: { SetVarArgs bs(p+n); int i=0; post(home, SetExpr::NT_DUNION, bs, i);
if (neg) { SetVar br(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, SOT_DUNION, bs, br); if (srt == SRT_CMPL) rel(home, br, SRT_EQ, s, b); else if (srt == SRT_EQ) rel(home, br, SRT_CMPL, s, b); else { SetVar bc(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, br, srt, bc); rel(home, bc, SRT_CMPL, s, b); } } else { SetVar br(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, SOT_DUNION, bs, br); rel(home, br, srt, s, b); } } break; default: GECODE_NEVER; } }
void NNF::post(Home home, NodeType t, SetVarArgs& b, int& i) const { if (this->t != t) { switch (this->t) { case SetExpr::NT_VAR: if (neg) { SetVar xc(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); rel(home, xc, SRT_CMPL, u.a.x->x); b[i++]=xc; } else { b[i++]=u.a.x->x; } break; default: { SetVar s(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); post(home,SRT_EQ,s); b[i++] = s; } break; } } else { u.b.l->post(home, t, b, i); u.b.r->post(home, t, b, i); } }
void NNF::post(Home home, SetRelType srt, const NNF* n) const { if (n->t == SetExpr::NT_VAR && !n->neg) { post(home,srt,n->u.a.x->x); } else if (t == SetExpr::NT_VAR && !neg) { SetRelType n_srt; switch (srt) { case SRT_SUB: n_srt = SRT_SUP; break; case SRT_SUP: n_srt = SRT_SUB; break; default: n_srt = srt; } n->post(home,n_srt,this); } else { SetVar nx(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); n->post(home,SRT_EQ,nx); post(home,srt,nx); } }
void NNF::post(Home home, BoolVar b, bool pt, SetRelType srt, const NNF* n) const { if (pt) { if (n->t == SetExpr::NT_VAR && !n->neg) { post(home,srt,n->u.a.x->x,b); } else if (t == SetExpr::NT_VAR && !neg) { SetRelType n_srt; switch (srt) { case SRT_SUB: n_srt = SRT_SUP; break; case SRT_SUP: n_srt = SRT_SUB; break; default: n_srt = srt; } n->post(home,b,true,n_srt,this); } else { SetVar nx(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); n->post(home,SRT_EQ,nx); post(home,srt,nx,b); } } else if (srt == SRT_EQ) { post(home,b,true,SRT_NQ,n); } else if (srt == SRT_NQ) { post(home,b,true,SRT_EQ,n); } else { BoolVar nb(home,0,1); rel(home,b,IRT_NQ,nb); post(home,nb,true,srt,n); } }
NNF* NNF::nnf(Region& r, Node* n, bool neg) { switch (n->t) { case SetExpr::NT_VAR: case SetExpr::NT_CONST: case SetExpr::NT_LEXP: { NNF* x = new (r) NNF; x->t = n->t; x->neg = neg; x->u.a.x = n; if (neg) { x->p = 0; x->n = 1; } else { x->p = 1; x->n = 0; } return x; } case SetExpr::NT_CMPL: return nnf(r,n->l,!neg); case SetExpr::NT_INTER: case SetExpr::NT_UNION: case SetExpr::NT_DUNION: { NodeType t; bool xneg; if (n->t == SetExpr::NT_DUNION) { t = n->t; xneg = neg; neg = false; } else { t = ((n->t == SetExpr::NT_INTER) == neg) ? SetExpr::NT_UNION : SetExpr::NT_INTER; xneg = false; } NNF* x = new (r) NNF; x->neg = xneg; x->t = t; x->u.b.l = nnf(r,n->l,neg); x->u.b.r = nnf(r,n->r,neg); int p_l, n_l; if ((x->u.b.l->t == t) || (x->u.b.l->t == SetExpr::NT_VAR)) { p_l=x->u.b.l->p; n_l=x->u.b.l->n; } else { p_l=1; n_l=0; } int p_r, n_r; if ((x->u.b.r->t == t) || (x->u.b.r->t == SetExpr::NT_VAR)) { p_r=x->u.b.r->p; n_r=x->u.b.r->n; } else { p_r=1; n_r=0; } x->p = p_l+p_r; x->n = n_l+n_r; return x; } default: GECODE_NEVER; } GECODE_NEVER; return nullptr; } }
SetExpr::SetExpr(const SetVar& x) : n(new Node) { n->same = 1; n->t = NT_VAR; n->l = nullptr; n->r = nullptr; n->x = x; }
SetExpr::SetExpr(const IntSet& s) : n(new Node) { n->same = 1; n->t = NT_CONST; n->l = nullptr; n->r = nullptr; n->s = s; }
SetExpr::SetExpr(const LinIntExpr& e) : n(new Node) { n->same = 1; n->t = NT_LEXP; n->l = nullptr; n->r = nullptr; n->e = e; }
SetExpr::SetExpr(const SetExpr& l, NodeType t, const SetExpr& r) : n(new Node) { int ls = same(t,l.n->t) ? l.n->same : 1; int rs = same(t,r.n->t) ? r.n->same : 1; n->same = ls+rs; n->t = t; n->l = l.n; n->l->use++; n->r = r.n; n->r->use++; }
SetExpr::SetExpr(const SetExpr& l, NodeType t) { (void) t; assert(t == NT_CMPL); if (l.n->t == NT_CMPL) { n = l.n->l; n->use++; } else { n = new Node; n->same = 1; n->t = NT_CMPL; n->l = l.n; n->l->use++; n->r = nullptr; } }
const SetExpr& SetExpr::operator =(const SetExpr& e) { if (this != &e) { if (n != nullptr && n->decrement()) delete n; n = e.n; n->use++; } return *this; }
SetExpr::~SetExpr(void) { if (n != nullptr && n->decrement()) delete n; }
SetExpr::SetExpr(const SetExpr& e) : n(e.n) { n->use++; }
SetVar SetExpr::post(Home home) const { Region r; SetVar s(home,IntSet::empty, IntSet(Set::Limits::min,Set::Limits::max)); NNF::nnf(r,n,false)->post(home,SRT_EQ,s); return s; }
void SetExpr::post(Home home, SetRelType srt, const SetExpr& e) const { Region r; return NNF::nnf(r,n,false)->post(home,srt,NNF::nnf(r,e.n,false)); } void SetExpr::post(Home home, BoolVar b, bool t, SetRelType srt, const SetExpr& e) const { Region r; return NNF::nnf(r,n,false)->post(home,b,t,srt, NNF::nnf(r,e.n,false)); }
SetExpr operator &(const SetExpr& l, const SetExpr& r) { return SetExpr(l,SetExpr::NT_INTER,r); } SetExpr operator |(const SetExpr& l, const SetExpr& r) { return SetExpr(l,SetExpr::NT_UNION,r); } SetExpr operator +(const SetExpr& l, const SetExpr& r) { return SetExpr(l,SetExpr::NT_DUNION,r); } SetExpr operator -(const SetExpr& e) { return SetExpr(e,SetExpr::NT_CMPL); } SetExpr operator -(const SetExpr& l, const SetExpr& r) { return SetExpr(l,SetExpr::NT_INTER,-r); } SetExpr singleton(const LinIntExpr& e) { return SetExpr(e); }
SetExpr inter(const SetVarArgs& x) { if (x.size() == 0) return SetExpr(IntSet(Set::Limits::min,Set::Limits::max)); SetExpr r(x[0]); for (int i=1; i<x.size(); i++) r = (r & x[i]); return r; } SetExpr setunion(const SetVarArgs& x) { if (x.size() == 0) return SetExpr(IntSet::empty); SetExpr r(x[0]); for (int i=1; i<x.size(); i++) r = (r | x[i]); return r; } SetExpr setdunion(const SetVarArgs& x) { if (x.size() == 0) return SetExpr(IntSet::empty); SetExpr r(x[0]); for (int i=1; i<x.size(); i++) r = (r + x[i]); return r; }
namespace MiniModel { /// Integer valued set expressions class GECODE_MINIMODEL_EXPORT SetNonLinIntExpr : public NonLinIntExpr { public: /// The expression type enum SetNonLinIntExprType { SNLE_CARD, ///< Cardinality expression SNLE_MIN, ///< Minimum element expression SNLE_MAX ///< Maximum element expression } t; /// The expression SetExpr e; /// Constructor SetNonLinIntExpr(const SetExpr& e0, SetNonLinIntExprType t0) : t(t0), e(e0) {} /// Post expression virtual IntVar post(Home home, IntVar* ret, const IntPropLevels&) const { IntVar m = result(home,ret); switch (t) { case SNLE_CARD: cardinality(home, e.post(home), m); break; case SNLE_MIN: min(home, e.post(home), m); break; case SNLE_MAX: max(home, e.post(home), m); break; default: GECODE_NEVER; break; } return m; } virtual void post(Home home, IntRelType irt, int c, const IntPropLevels& ipls) const { if (t==SNLE_CARD && irt!=IRT_NQ) { switch (irt) { case IRT_LQ: cardinality(home, e.post(home), 0U, static_cast<unsigned int>(c)); break; case IRT_LE: cardinality(home, e.post(home), 0U, static_cast<unsigned int>(c-1)); break; case IRT_GQ: cardinality(home, e.post(home), static_cast<unsigned int>(c), Set::Limits::card); break; case IRT_GR: cardinality(home, e.post(home), static_cast<unsigned int>(c+1), Set::Limits::card); break; case IRT_EQ: cardinality(home, e.post(home), static_cast<unsigned int>(c), static_cast<unsigned int>(c)); break; default: GECODE_NEVER; } } else if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) { c = (irt==IRT_GQ ? c : c+1); dom(home, e.post(home), SRT_SUB, c, Set::Limits::max); } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) { c = (irt==IRT_LQ ? c : c-1); dom(home, e.post(home), SRT_SUB, Set::Limits::min, c); } else { rel(home, post(home,nullptr,ipls), irt, c); } } virtual void post(Home home, IntRelType irt, int c, BoolVar b, const IntPropLevels& ipls) const { if (t==SNLE_MIN && (irt==IRT_GR || irt==IRT_GQ)) { c = (irt==IRT_GQ ? c : c+1); dom(home, e.post(home), SRT_SUB, c, Set::Limits::max, b); } else if (t==SNLE_MAX && (irt==IRT_LE || irt==IRT_LQ)) { c = (irt==IRT_LQ ? c : c-1); dom(home, e.post(home), SRT_SUB, Set::Limits::min, c, b); } else { rel(home, post(home,nullptr,ipls), irt, c, b); } } }; }
LinIntExpr cardinality(const SetExpr& e) { return LinIntExpr(new MiniModel::SetNonLinIntExpr(e, MiniModel::SetNonLinIntExpr::SNLE_CARD)); } LinIntExpr min(const SetExpr& e) { return LinIntExpr(new MiniModel::SetNonLinIntExpr(e, MiniModel::SetNonLinIntExpr::SNLE_MIN)); } LinIntExpr max(const SetExpr& e) { return LinIntExpr(new MiniModel::SetNonLinIntExpr(e, MiniModel::SetNonLinIntExpr::SNLE_MAX)); }
/* * Posting set expressions * */ SetVar expr(Home home, const SetExpr& e) { PostInfo pi(home); if (!home.failed()) return e.post(home); SetVar x(home,IntSet::empty,IntSet::empty); return x; }
}
#endif
// STATISTICS: minimodel-any