/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ /* * Main authors: * Guido Tack * * Contributing authors: * Mikael Lagerkvist * * Copyright: * Guido Tack, 2007 * Mikael Lagerkvist, 2009 * * Last modified: * $Date: 2012-03-21 16:25:08 +1100 (Wed, 21 Mar 2012) $ by $Author: tack $ * $Revision: 12605 $ * * 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 #include #include #include #ifdef GECODE_HAS_SET_VARS #include #endif #include namespace Gecode { namespace FlatZinc { Registry& registry(void) { static Registry r; return r; } void Registry::post(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { std::map::iterator i = r.find(ce.id); if (i == r.end()) { throw FlatZinc::Error("Registry", std::string("Constraint ")+ce.id+" not found"); } i->second(s, ce, ann); } void Registry::add(const std::string& id, poster p) { r[id] = p; } namespace { IntConLevel ann2icl(AST::Node* ann) { if (ann) { if (ann->hasAtom("val")) return ICL_VAL; if (ann->hasAtom("domain")) return ICL_DOM; if (ann->hasAtom("bounds") || ann->hasAtom("boundsR") || ann->hasAtom("boundsD") || ann->hasAtom("boundsZ")) return ICL_BND; } return ICL_DEF; } inline IntRelType swap(IntRelType irt) { switch (irt) { case IRT_LQ: return IRT_GQ; case IRT_LE: return IRT_GR; case IRT_GQ: return IRT_LQ; case IRT_GR: return IRT_LE; default: return irt; } } inline IntRelType neg(IntRelType irt) { switch (irt) { case IRT_EQ: return IRT_NQ; case IRT_NQ: return IRT_EQ; case IRT_LQ: return IRT_GR; case IRT_LE: return IRT_GQ; case IRT_GQ: return IRT_LE; case IRT_GR: default: assert(irt == IRT_GR); } return IRT_LQ; } inline IntArgs arg2intargs(AST::Node* arg, int offset = 0) { AST::Array* a = arg->getArray(); IntArgs ia(a->a.size()+offset); for (int i=offset; i--;) ia[i] = 0; for (int i=a->a.size(); i--;) ia[i+offset] = a->a[i]->getInt(); return ia; } inline IntArgs arg2boolargs(AST::Node* arg, int offset = 0) { AST::Array* a = arg->getArray(); IntArgs ia(a->a.size()+offset); for (int i=offset; i--;) ia[i] = 0; for (int i=a->a.size(); i--;) ia[i+offset] = a->a[i]->getBool(); return ia; } inline IntSet arg2intset(FlatZincSpace& s, AST::Node* n) { AST::SetLit* sl = n->getSet(); IntSet d; if (sl->interval) { d = IntSet(sl->min, sl->max); } else { Region re(s); int* is = re.alloc(static_cast(sl->s.size())); for (int i=sl->s.size(); i--; ) is[i] = sl->s[i]; d = IntSet(is, sl->s.size()); } return d; } inline IntSetArgs arg2intsetargs(FlatZincSpace& s, AST::Node* arg, int offset = 0) { AST::Array* a = arg->getArray(); if (a->a.size() == 0) { IntSetArgs emptyIa(0); return emptyIa; } IntSetArgs ia(a->a.size()+offset); for (int i=offset; i--;) ia[i] = IntSet::empty; for (int i=a->a.size(); i--;) { ia[i+offset] = arg2intset(s, a->a[i]); } return ia; } inline IntVarArgs arg2intvarargs(FlatZincSpace& s, AST::Node* arg, int offset = 0) { AST::Array* a = arg->getArray(); if (a->a.size() == 0) { IntVarArgs emptyIa(0); return emptyIa; } IntVarArgs ia(a->a.size()+offset); for (int i=offset; i--;) ia[i] = IntVar(s, 0, 0); for (int i=a->a.size(); i--;) { if (a->a[i]->isIntVar()) { ia[i+offset] = s.iv[a->a[i]->getIntVar()]; } else { int value = a->a[i]->getInt(); IntVar iv(s, value, value); ia[i+offset] = iv; } } return ia; } inline BoolVarArgs arg2boolvarargs(FlatZincSpace& s, AST::Node* arg, int offset = 0, int siv=-1) { AST::Array* a = arg->getArray(); if (a->a.size() == 0) { BoolVarArgs emptyIa(0); return emptyIa; } BoolVarArgs ia(a->a.size()+offset-(siv==-1?0:1)); for (int i=offset; i--;) ia[i] = BoolVar(s, 0, 0); for (int i=0; i(a->a.size()); i++) { if (i==siv) continue; if (a->a[i]->isBool()) { bool value = a->a[i]->getBool(); BoolVar iv(s, value, value); ia[offset++] = iv; } else if (a->a[i]->isIntVar() && s.aliasBool2Int(a->a[i]->getIntVar()) != -1) { ia[offset++] = s.bv[s.aliasBool2Int(a->a[i]->getIntVar())]; } else { ia[offset++] = s.bv[a->a[i]->getBoolVar()]; } } return ia; } #ifdef GECODE_HAS_SET_VARS SetVar getSetVar(FlatZincSpace& s, AST::Node* n) { SetVar x0; if (!n->isSetVar()) { IntSet d = arg2intset(s,n); x0 = SetVar(s, d, d); } else { x0 = s.sv[n->getSetVar()]; } return x0; } inline SetVarArgs arg2setvarargs(FlatZincSpace& s, AST::Node* arg, int offset = 0, int doffset = 0, const IntSet& od=IntSet::empty) { AST::Array* a = arg->getArray(); SetVarArgs ia(a->a.size()+offset); for (int i=offset; i--;) { IntSet d = ia.size(); i--;) { ia[i+offset] = getSetVar(s, a->a[i]); } return ia; } #endif BoolVar getBoolVar(FlatZincSpace& s, AST::Node* n) { BoolVar x0; if (n->isBool()) { x0 = BoolVar(s, n->getBool(), n->getBool()); } else { x0 = s.bv[n->getBoolVar()]; } return x0; } IntVar getIntVar(FlatZincSpace& s, AST::Node* n) { IntVar x0; if (n->isIntVar()) { x0 = s.iv[n->getIntVar()]; } else { x0 = IntVar(s, n->getInt(), n->getInt()); } return x0; } bool isBoolArray(FlatZincSpace& s, AST::Node* b, int& singleInt) { AST::Array* a = b->getArray(); singleInt = -1; if (a->a.size() == 0) return true; for (int i=a->a.size(); i--;) { if (a->a[i]->isBoolVar() || a->a[i]->isBool()) { } else if (a->a[i]->isIntVar()) { if (s.aliasBool2Int(a->a[i]->getIntVar()) == -1) { if (singleInt != -1) { return false; } singleInt = i; } } else { return false; } } return singleInt==-1 || a->a.size() > 1; } void p_distinct(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs va = arg2intvarargs(s, ce[0]); IntConLevel icl = ann2icl(ann); distinct(s, va, icl == ICL_DEF ? ICL_BND : icl); } void p_distinctOffset(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs va = arg2intvarargs(s, ce[1]); AST::Array* offs = ce.args->a[0]->getArray(); IntArgs oa(offs->a.size()); for (int i=offs->a.size(); i--; ) { oa[i] = offs->a[i]->getInt(); } IntConLevel icl = ann2icl(ann); distinct(s, oa, va, icl == ICL_DEF ? ICL_BND : icl); } void p_all_equal(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs va = arg2intvarargs(s, ce[0]); rel(s, va, IRT_EQ, ann2icl(ann)); } void p_int_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, AST::Node* ann) { if (ce[0]->isIntVar()) { if (ce[1]->isIntVar()) { rel(s, getIntVar(s, ce[0]), irt, getIntVar(s, ce[1]), ann2icl(ann)); } else { rel(s, getIntVar(s, ce[0]), irt, ce[1]->getInt(), ann2icl(ann)); } } else { rel(s, getIntVar(s, ce[1]), swap(irt), ce[0]->getInt(), ann2icl(ann)); } } void p_int_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_CMP(s, IRT_EQ, ce, ann); } void p_int_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_CMP(s, IRT_NQ, ce, ann); } void p_int_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_CMP(s, IRT_GQ, ce, ann); } void p_int_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_CMP(s, IRT_GR, ce, ann); } void p_int_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_CMP(s, IRT_LQ, ce, ann); } void p_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_CMP(s, IRT_LE, ce, ann); } void p_int_CMP_reif(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, AST::Node* ann) { if (ce[2]->isBool()) { if (ce[2]->getBool()) { p_int_CMP(s, irt, ce, ann); } else { p_int_CMP(s, neg(irt), ce, ann); } return; } if (ce[0]->isIntVar()) { if (ce[1]->isIntVar()) { rel(s, getIntVar(s, ce[0]), irt, getIntVar(s, ce[1]), getBoolVar(s, ce[2]), ann2icl(ann)); } else { rel(s, getIntVar(s, ce[0]), irt, ce[1]->getInt(), getBoolVar(s, ce[2]), ann2icl(ann)); } } else { rel(s, getIntVar(s, ce[1]), swap(irt), ce[0]->getInt(), getBoolVar(s, ce[2]), ann2icl(ann)); } } /* Comparisons */ void p_int_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_CMP_reif(s, IRT_EQ, ce, ann); } void p_int_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_CMP_reif(s, IRT_NQ, ce, ann); } void p_int_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_CMP_reif(s, IRT_GQ, ce, ann); } void p_int_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_CMP_reif(s, IRT_GR, ce, ann); } void p_int_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_CMP_reif(s, IRT_LQ, ce, ann); } void p_int_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_CMP_reif(s, IRT_LE, ce, ann); } /* linear (in-)equations */ void p_int_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, AST::Node* ann) { IntArgs ia = arg2intargs(ce[0]); int singleIntVar; if (isBoolArray(s,ce[1],singleIntVar)) { if (singleIntVar != -1) { if (std::abs(ia[singleIntVar]) == 1 && ce[2]->getInt() == 0) { IntVar siv = getIntVar(s, ce[1]->getArray()->a[singleIntVar]); BoolVarArgs iv = arg2boolvarargs(s, ce[1], 0, singleIntVar); IntArgs ia_tmp(ia.size()-1); int count = 0; for (int i=0; igetInt(), ann2icl(ann)); } } else { BoolVarArgs iv = arg2boolvarargs(s, ce[1]); linear(s, ia, iv, irt, ce[2]->getInt(), ann2icl(ann)); } } else { IntVarArgs iv = arg2intvarargs(s, ce[1]); linear(s, ia, iv, irt, ce[2]->getInt(), ann2icl(ann)); } } void p_int_lin_CMP_reif(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, AST::Node* ann) { if (ce[2]->isBool()) { if (ce[2]->getBool()) { p_int_lin_CMP(s, irt, ce, ann); } else { p_int_lin_CMP(s, neg(irt), ce, ann); } return; } IntArgs ia = arg2intargs(ce[0]); int singleIntVar; if (isBoolArray(s,ce[1],singleIntVar)) { if (singleIntVar != -1) { if (std::abs(ia[singleIntVar]) == 1 && ce[2]->getInt() == 0) { IntVar siv = getIntVar(s, ce[1]->getArray()->a[singleIntVar]); BoolVarArgs iv = arg2boolvarargs(s, ce[1], 0, singleIntVar); IntArgs ia_tmp(ia.size()-1); int count = 0; for (int i=0; igetInt(), getBoolVar(s, ce[3]), ann2icl(ann)); } } else { BoolVarArgs iv = arg2boolvarargs(s, ce[1]); linear(s, ia, iv, irt, ce[2]->getInt(), getBoolVar(s, ce[3]), ann2icl(ann)); } } else { IntVarArgs iv = arg2intvarargs(s, ce[1]); linear(s, ia, iv, irt, ce[2]->getInt(), getBoolVar(s, ce[3]), ann2icl(ann)); } } void p_int_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_lin_CMP(s, IRT_EQ, ce, ann); } void p_int_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_lin_CMP_reif(s, IRT_EQ, ce, ann); } void p_int_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_lin_CMP(s, IRT_NQ, ce, ann); } void p_int_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_lin_CMP_reif(s, IRT_NQ, ce, ann); } void p_int_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_lin_CMP(s, IRT_LQ, ce, ann); } void p_int_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_lin_CMP_reif(s, IRT_LQ, ce, ann); } void p_int_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_lin_CMP(s, IRT_LE, ce, ann); } void p_int_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_lin_CMP_reif(s, IRT_LE, ce, ann); } void p_int_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_lin_CMP(s, IRT_GQ, ce, ann); } void p_int_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_lin_CMP_reif(s, IRT_GQ, ce, ann); } void p_int_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_lin_CMP(s, IRT_GR, ce, ann); } void p_int_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_int_lin_CMP_reif(s, IRT_GR, ce, ann); } void p_bool_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, AST::Node* ann) { IntArgs ia = arg2intargs(ce[0]); BoolVarArgs iv = arg2boolvarargs(s, ce[1]); if (ce[2]->isIntVar()) linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()], ann2icl(ann)); else linear(s, ia, iv, irt, ce[2]->getInt(), ann2icl(ann)); } void p_bool_lin_CMP_reif(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, AST::Node* ann) { if (ce[2]->isBool()) { if (ce[2]->getBool()) { p_bool_lin_CMP(s, irt, ce, ann); } else { p_bool_lin_CMP(s, neg(irt), ce, ann); } return; } IntArgs ia = arg2intargs(ce[0]); BoolVarArgs iv = arg2boolvarargs(s, ce[1]); if (ce[2]->isIntVar()) linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()], getBoolVar(s, ce[3]), ann2icl(ann)); else linear(s, ia, iv, irt, ce[2]->getInt(), getBoolVar(s, ce[3]), ann2icl(ann)); } void p_bool_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_lin_CMP(s, IRT_EQ, ce, ann); } void p_bool_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_lin_CMP_reif(s, IRT_EQ, ce, ann); } void p_bool_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_lin_CMP(s, IRT_NQ, ce, ann); } void p_bool_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_lin_CMP_reif(s, IRT_NQ, ce, ann); } void p_bool_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_lin_CMP(s, IRT_LQ, ce, ann); } void p_bool_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_lin_CMP_reif(s, IRT_LQ, ce, ann); } void p_bool_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_lin_CMP(s, IRT_LE, ce, ann); } void p_bool_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_lin_CMP_reif(s, IRT_LE, ce, ann); } void p_bool_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_lin_CMP(s, IRT_GQ, ce, ann); } void p_bool_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_lin_CMP_reif(s, IRT_GQ, ce, ann); } void p_bool_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_lin_CMP(s, IRT_GR, ce, ann); } void p_bool_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_lin_CMP_reif(s, IRT_GR, ce, ann); } /* arithmetic constraints */ void p_int_plus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { if (!ce[0]->isIntVar()) { rel(s, ce[0]->getInt() + getIntVar(s, ce[1]) == getIntVar(s,ce[2]), ann2icl(ann)); } else if (!ce[1]->isIntVar()) { rel(s, getIntVar(s,ce[0]) + ce[1]->getInt() == getIntVar(s,ce[2]), ann2icl(ann)); } else if (!ce[2]->isIntVar()) { rel(s, getIntVar(s,ce[0]) + getIntVar(s,ce[1]) == ce[2]->getInt(), ann2icl(ann)); } else { rel(s, getIntVar(s,ce[0]) + getIntVar(s,ce[1]) == getIntVar(s,ce[2]), ann2icl(ann)); } } void p_int_minus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { if (!ce[0]->isIntVar()) { rel(s, ce[0]->getInt() - getIntVar(s, ce[1]) == getIntVar(s,ce[2]), ann2icl(ann)); } else if (!ce[1]->isIntVar()) { rel(s, getIntVar(s,ce[0]) - ce[1]->getInt() == getIntVar(s,ce[2]), ann2icl(ann)); } else if (!ce[2]->isIntVar()) { rel(s, getIntVar(s,ce[0]) - getIntVar(s,ce[1]) == ce[2]->getInt(), ann2icl(ann)); } else { rel(s, getIntVar(s,ce[0]) - getIntVar(s,ce[1]) == getIntVar(s,ce[2]), ann2icl(ann)); } } void p_int_times(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVar x0 = getIntVar(s, ce[0]); IntVar x1 = getIntVar(s, ce[1]); IntVar x2 = getIntVar(s, ce[2]); mult(s, x0, x1, x2, ann2icl(ann)); } void p_int_div(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVar x0 = getIntVar(s, ce[0]); IntVar x1 = getIntVar(s, ce[1]); IntVar x2 = getIntVar(s, ce[2]); div(s,x0,x1,x2, ann2icl(ann)); } void p_int_mod(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVar x0 = getIntVar(s, ce[0]); IntVar x1 = getIntVar(s, ce[1]); IntVar x2 = getIntVar(s, ce[2]); mod(s,x0,x1,x2, ann2icl(ann)); } void p_int_min(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVar x0 = getIntVar(s, ce[0]); IntVar x1 = getIntVar(s, ce[1]); IntVar x2 = getIntVar(s, ce[2]); min(s, x0, x1, x2, ann2icl(ann)); } void p_int_max(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVar x0 = getIntVar(s, ce[0]); IntVar x1 = getIntVar(s, ce[1]); IntVar x2 = getIntVar(s, ce[2]); max(s, x0, x1, x2, ann2icl(ann)); } void p_int_negate(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVar x0 = getIntVar(s, ce[0]); IntVar x1 = getIntVar(s, ce[1]); rel(s, x0 == -x1, ann2icl(ann)); } /* Boolean constraints */ void p_bool_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, AST::Node* ann) { rel(s, getBoolVar(s, ce[0]), irt, getBoolVar(s, ce[1]), ann2icl(ann)); } void p_bool_CMP_reif(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, AST::Node* ann) { rel(s, getBoolVar(s, ce[0]), irt, getBoolVar(s, ce[1]), getBoolVar(s, ce[2]), ann2icl(ann)); } void p_bool_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_CMP(s, IRT_EQ, ce, ann); } void p_bool_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_CMP_reif(s, IRT_EQ, ce, ann); } void p_bool_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_CMP(s, IRT_NQ, ce, ann); } void p_bool_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_CMP_reif(s, IRT_NQ, ce, ann); } void p_bool_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_CMP(s, IRT_GQ, ce, ann); } void p_bool_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_CMP_reif(s, IRT_GQ, ce, ann); } void p_bool_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_CMP(s, IRT_LQ, ce, ann); } void p_bool_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_CMP_reif(s, IRT_LQ, ce, ann); } void p_bool_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_CMP(s, IRT_GR, ce, ann); } void p_bool_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_CMP_reif(s, IRT_GR, ce, ann); } void p_bool_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_CMP(s, IRT_LE, ce, ann); } void p_bool_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_bool_CMP_reif(s, IRT_LE, ce, ann); } #define BOOL_OP(op) \ BoolVar b0 = getBoolVar(s, ce[0]); \ BoolVar b1 = getBoolVar(s, ce[1]); \ if (ce[2]->isBool()) { \ rel(s, b0, op, b1, ce[2]->getBool(), ann2icl(ann)); \ } else { \ rel(s, b0, op, b1, s.bv[ce[2]->getBoolVar()], ann2icl(ann)); \ } #define BOOL_ARRAY_OP(op) \ BoolVarArgs bv = arg2boolvarargs(s, ce[0]); \ if (ce.size()==1) { \ rel(s, op, bv, 1, ann2icl(ann)); \ } else if (ce[1]->isBool()) { \ rel(s, op, bv, ce[1]->getBool(), ann2icl(ann)); \ } else { \ rel(s, op, bv, s.bv[ce[1]->getBoolVar()], ann2icl(ann)); \ } void p_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BOOL_OP(BOT_OR); } void p_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BOOL_OP(BOT_AND); } void p_array_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BOOL_ARRAY_OP(BOT_AND); } void p_array_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BOOL_ARRAY_OP(BOT_OR); } void p_array_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BOOL_ARRAY_OP(BOT_XOR); } void p_array_bool_clause(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BoolVarArgs bvp = arg2boolvarargs(s, ce[0]); BoolVarArgs bvn = arg2boolvarargs(s, ce[1]); clause(s, BOT_OR, bvp, bvn, 1, ann2icl(ann)); } void p_array_bool_clause_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BoolVarArgs bvp = arg2boolvarargs(s, ce[0]); BoolVarArgs bvn = arg2boolvarargs(s, ce[1]); BoolVar b0 = getBoolVar(s, ce[2]); clause(s, BOT_OR, bvp, bvn, b0, ann2icl(ann)); } void p_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BOOL_OP(BOT_XOR); } void p_bool_l_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BoolVar b0 = getBoolVar(s, ce[0]); BoolVar b1 = getBoolVar(s, ce[1]); if (ce[2]->isBool()) { rel(s, b1, BOT_IMP, b0, ce[2]->getBool(), ann2icl(ann)); } else { rel(s, b1, BOT_IMP, b0, s.bv[ce[2]->getBoolVar()], ann2icl(ann)); } } void p_bool_r_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BOOL_OP(BOT_IMP); } void p_bool_not(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BoolVar x0 = getBoolVar(s, ce[0]); BoolVar x1 = getBoolVar(s, ce[1]); rel(s, x0, BOT_XOR, x1, 1, ann2icl(ann)); } /* element constraints */ void p_array_int_element(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { bool isConstant = true; AST::Array* a = ce[1]->getArray(); for (int i=a->a.size(); i--;) { if (!a->a[i]->isInt()) { isConstant = false; break; } } IntVar selector = getIntVar(s, ce[0]); rel(s, selector > 0); if (isConstant) { IntArgs ia = arg2intargs(ce[1], 1); element(s, ia, selector, getIntVar(s, ce[2]), ann2icl(ann)); } else { IntVarArgs iv = arg2intvarargs(s, ce[1], 1); element(s, iv, selector, getIntVar(s, ce[2]), ann2icl(ann)); } } void p_array_bool_element(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { bool isConstant = true; AST::Array* a = ce[1]->getArray(); for (int i=a->a.size(); i--;) { if (!a->a[i]->isBool()) { isConstant = false; break; } } IntVar selector = getIntVar(s, ce[0]); rel(s, selector > 0); if (isConstant) { IntArgs ia = arg2boolargs(ce[1], 1); element(s, ia, selector, getBoolVar(s, ce[2]), ann2icl(ann)); } else { BoolVarArgs iv = arg2boolvarargs(s, ce[1], 1); element(s, iv, selector, getBoolVar(s, ce[2]), ann2icl(ann)); } } /* coercion constraints */ void p_bool2int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BoolVar x0 = getBoolVar(s, ce[0]); IntVar x1 = getIntVar(s, ce[1]); if (ce[0]->isBoolVar() && ce[1]->isIntVar()) { s.aliasBool2Int(ce[1]->getIntVar(), ce[0]->getBoolVar()); } channel(s, x0, x1, ann2icl(ann)); } void p_int_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { IntSet d = arg2intset(s,ce[1]); if (ce[0]->isBoolVar()) { IntSetRanges dr(d); Iter::Ranges::Singleton sr(0,1); Iter::Ranges::Inter i(dr,sr); IntSet d01(i); if (d01.size() == 0) { s.fail(); } else { rel(s, getBoolVar(s, ce[0]), IRT_GQ, d01.min()); rel(s, getBoolVar(s, ce[0]), IRT_LQ, d01.max()); } } else { dom(s, getIntVar(s, ce[0]), d); } } void p_int_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { IntSet d = arg2intset(s,ce[1]); if (ce[0]->isBoolVar()) { IntSetRanges dr(d); Iter::Ranges::Singleton sr(0,1); Iter::Ranges::Inter i(dr,sr); IntSet d01(i); if (d01.size() == 0) { rel(s, getBoolVar(s, ce[2]) == 0); } else if (d01.max() == 0) { rel(s, getBoolVar(s, ce[2]) == !getBoolVar(s, ce[0])); } else if (d01.min() == 1) { rel(s, getBoolVar(s, ce[2]) == getBoolVar(s, ce[0])); } else { rel(s, getBoolVar(s, ce[2]) == 1); } } else { std::cerr << "in_in_reif("<isIntVar()) { if (!ce[2]->isIntVar()) { count(s, iv, ce[1]->getInt(), IRT_EQ, ce[2]->getInt(), ann2icl(ann)); } else { count(s, iv, ce[1]->getInt(), IRT_EQ, getIntVar(s, ce[2]), ann2icl(ann)); } } else if (!ce[2]->isIntVar()) { count(s, iv, getIntVar(s, ce[1]), IRT_EQ, ce[2]->getInt(), ann2icl(ann)); } else { count(s, iv, getIntVar(s, ce[1]), IRT_EQ, getIntVar(s, ce[2]), ann2icl(ann)); } } void count_rel(IntRelType irt, FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs iv = arg2intvarargs(s, ce[1]); count(s, iv, ce[2]->getInt(), irt, ce[0]->getInt(), ann2icl(ann)); } void p_at_most(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { count_rel(IRT_LQ, s, ce, ann); } void p_at_least(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { count_rel(IRT_GQ, s, ce, ann); } void p_bin_packing_load(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { int minIdx = ce[3]->getInt(); IntVarArgs load = arg2intvarargs(s, ce[0]); IntVarArgs l; IntVarArgs bin = arg2intvarargs(s, ce[1]); for (int i=bin.size(); i--;) rel(s, bin[i] >= minIdx); if (minIdx > 0) { for (int i=minIdx; i--;) l << IntVar(s,0,0); } else if (minIdx < 0) { IntVarArgs bin2(bin.size()); for (int i=bin.size(); i--;) bin2[i] = expr(s, bin[i]-minIdx, ann2icl(ann)); bin = bin2; } l << load; IntArgs sizes = arg2intargs(ce[2]); binpacking(s, l, bin, sizes, ann2icl(ann)); } void p_global_cardinality(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs iv0 = arg2intvarargs(s, ce[0]); IntArgs cover = arg2intargs(ce[1]); IntVarArgs iv1 = arg2intvarargs(s, ce[2]); Region re(s); IntSet cover_s(cover); IntSetRanges cover_r(cover_s); IntVarRanges* iv0_ri = re.alloc(iv0.size()); for (int i=iv0.size(); i--;) iv0_ri[i] = IntVarRanges(iv0[i]); Iter::Ranges::NaryUnion iv0_r(re,iv0_ri,iv0.size()); Iter::Ranges::Diff extra_r(iv0_r,cover_r); Iter::Ranges::ToValues > extra(extra_r); for (; extra(); ++extra) { cover << extra.val(); iv1 << IntVar(s,0,iv0.size()); } count(s, iv0, iv1, cover, ann2icl(ann)); } void p_global_cardinality_closed(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs iv0 = arg2intvarargs(s, ce[0]); IntArgs cover = arg2intargs(ce[1]); IntVarArgs iv1 = arg2intvarargs(s, ce[2]); count(s, iv0, iv1, cover, ann2icl(ann)); } void p_global_cardinality_low_up(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs x = arg2intvarargs(s, ce[0]); IntArgs cover = arg2intargs(ce[1]); IntArgs lbound = arg2intargs(ce[2]); IntArgs ubound = arg2intargs(ce[3]); IntSetArgs y(cover.size()); for (int i=cover.size(); i--;) y[i] = IntSet(lbound[i],ubound[i]); IntSet cover_s(cover); Region re(s); IntVarRanges* xrs = re.alloc(x.size()); for (int i=x.size(); i--;) xrs[i].init(x[i]); Iter::Ranges::NaryUnion u(re, xrs, x.size()); Iter::Ranges::ToValues uv(u); for (; uv(); ++uv) { if (!cover_s.in(uv.val())) { cover << uv.val(); y << IntSet(0,x.size()); } } count(s, x, y, cover, ann2icl(ann)); } void p_global_cardinality_low_up_closed(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs x = arg2intvarargs(s, ce[0]); IntArgs cover = arg2intargs(ce[1]); IntArgs lbound = arg2intargs(ce[2]); IntArgs ubound = arg2intargs(ce[3]); IntSetArgs y(cover.size()); for (int i=cover.size(); i--;) y[i] = IntSet(lbound[i],ubound[i]); count(s, x, y, cover, ann2icl(ann)); } void p_minimum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs iv = arg2intvarargs(s, ce[1]); min(s, iv, getIntVar(s, ce[0]), ann2icl(ann)); } void p_maximum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs iv = arg2intvarargs(s, ce[1]); max(s, iv, getIntVar(s, ce[0]), ann2icl(ann)); } void p_regular(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs iv = arg2intvarargs(s, ce[0]); int q = ce[1]->getInt(); int symbols = ce[2]->getInt(); IntArgs d = arg2intargs(ce[3]); int q0 = ce[4]->getInt(); int noOfTrans = 0; for (int i=1; i<=q; i++) { for (int j=1; j<=symbols; j++) { if (d[(i-1)*symbols+(j-1)] > 0) noOfTrans++; } } Region re(s); DFA::Transition* t = re.alloc(noOfTrans+1); noOfTrans = 0; for (int i=1; i<=q; i++) { for (int j=1; j<=symbols; j++) { if (d[(i-1)*symbols+(j-1)] > 0) { t[noOfTrans].i_state = i; t[noOfTrans].symbol = j; t[noOfTrans].o_state = d[(i-1)*symbols+(j-1)]; noOfTrans++; } } } t[noOfTrans].i_state = -1; // Final states AST::SetLit* sl = ce[5]->getSet(); int* f; if (sl->interval) { f = static_cast(malloc(sizeof(int)*(sl->max-sl->min+2))); for (int i=sl->min; i<=sl->max; i++) f[i-sl->min] = i; f[sl->max-sl->min+1] = -1; } else { f = static_cast(malloc(sizeof(int)*(sl->s.size()+1))); for (int j=sl->s.size(); j--; ) f[j] = sl->s[j]; f[sl->s.size()] = -1; } DFA dfa(q0,t,f); free(f); extensional(s, iv, dfa, ann2icl(ann)); } void p_sort(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs x = arg2intvarargs(s, ce[0]); IntVarArgs y = arg2intvarargs(s, ce[1]); IntVarArgs xy(x.size()+y.size()); for (int i=x.size(); i--;) xy[i] = x[i]; for (int i=y.size(); i--;) xy[i+x.size()] = y[i]; unshare(s, xy); for (int i=x.size(); i--;) x[i] = xy[i]; for (int i=y.size(); i--;) y[i] = xy[i+x.size()]; sorted(s, x, y, ann2icl(ann)); } void p_inverse_offsets(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs x = arg2intvarargs(s, ce[0]); int xoff = ce[1]->getInt(); IntVarArgs y = arg2intvarargs(s, ce[2]); int yoff = ce[3]->getInt(); channel(s, x, xoff, y, yoff, ann2icl(ann)); } void p_increasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs x = arg2intvarargs(s, ce[0]); rel(s,x,IRT_LQ,ann2icl(ann)); } void p_increasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BoolVarArgs x = arg2boolvarargs(s, ce[0]); rel(s,x,IRT_LQ,ann2icl(ann)); } void p_decreasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs x = arg2intvarargs(s, ce[0]); rel(s,x,IRT_GQ,ann2icl(ann)); } void p_decreasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BoolVarArgs x = arg2boolvarargs(s, ce[0]); rel(s,x,IRT_GQ,ann2icl(ann)); } void p_table_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs x = arg2intvarargs(s, ce[0]); IntArgs tuples = arg2intargs(ce[1]); int noOfVars = x.size(); int noOfTuples = tuples.size()/noOfVars; TupleSet ts; for (int i=0; i bound.max()/2) || (minHeight2 > bound.max()/2 && minHeight+minHeight2>bound.max()); if (disjunctive) { rel(s, bound >= max(height)); // Unary if (duration.assigned()) { IntArgs durationI(n); for (int i=n; i--;) durationI[i] = duration[i].val(); unary(s,start,durationI); } else { IntVarArgs end(n); for (int i=n; i--;) end[i] = expr(s,start[i]+duration[i]); unary(s,start,duration,end); } } else if (height.assigned()) { IntArgs heightI(n); for (int i=n; i--;) heightI[i] = height[i].val(); if (duration.assigned()) { IntArgs durationI(n); for (int i=n; i--;) durationI[i] = duration[i].val(); cumulative(s, bound, start, durationI, heightI); } else { IntVarArgs end(n); for (int i = n; i--; ) end[i] = expr(s,start[i]+duration[i]); cumulative(s, bound, start, duration, end, heightI); } } else if (bound.assigned()) { IntArgs machine = IntArgs::create(n,0,0); IntArgs limit(1, bound.val()); IntVarArgs end(n); for (int i=n; i--;) end[i] = expr(s,start[i]+duration[i]); cumulatives(s, machine, start, duration, end, height, limit, true, ann2icl(ann)); } else { int min = Gecode::Int::Limits::max; int max = Gecode::Int::Limits::min; IntVarArgs end(start.size()); for (int i = start.size(); i--; ) { min = std::min(min, start[i].min()); max = std::max(max, start[i].max() + duration[i].max()); end[i] = expr(s, start[i] + duration[i]); } for (int time = min; time < max; ++time) { IntVarArgs x(start.size()); for (int i = start.size(); i--; ) { IntVar overlaps = channel(s, expr(s, (start[i] <= time) && (time < end[i]))); x[i] = expr(s, overlaps * height[i]); } linear(s, x, IRT_LQ, bound); } } } void p_among_seq_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs x = arg2intvarargs(s, ce[0]); IntSet S = arg2intset(s, ce[1]); int q = ce[2]->getInt(); int l = ce[3]->getInt(); int u = ce[4]->getInt(); sequence(s, x, S, q, l, u, ann2icl(ann)); } void p_among_seq_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BoolVarArgs x = arg2boolvarargs(s, ce[0]); bool val = ce[1]->getBool(); int q = ce[2]->getInt(); int l = ce[3]->getInt(); int u = ce[4]->getInt(); IntSet S(val, val); sequence(s, x, S, q, l, u, ann2icl(ann)); } void p_schedule_unary(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { IntVarArgs x = arg2intvarargs(s, ce[0]); IntArgs p = arg2intargs(ce[1]); unary(s, x, p); } void p_schedule_unary_optional(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { IntVarArgs x = arg2intvarargs(s, ce[0]); IntArgs p = arg2intargs(ce[1]); BoolVarArgs m = arg2boolvarargs(s, ce[2]); unary(s, x, p, m); } void p_circuit(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { IntVarArgs xv = arg2intvarargs(s, ce[0]); circuit(s,xv,ann2icl(ann)); } void p_circuit_cost_array(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { IntArgs c = arg2intargs(ce[0]); IntVarArgs xv = arg2intvarargs(s, ce[1]); IntVarArgs yv = arg2intvarargs(s, ce[2]); IntVar z = getIntVar(s, ce[3]); circuit(s,c,xv,yv,z,ann2icl(ann)); } void p_circuit_cost(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { IntArgs c = arg2intargs(ce[0]); IntVarArgs xv = arg2intvarargs(s, ce[1]); IntVar z = getIntVar(s, ce[2]); circuit(s,c,xv,z,ann2icl(ann)); } void p_nooverlap(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { IntVarArgs x0 = arg2intvarargs(s, ce[0]); IntVarArgs w = arg2intvarargs(s, ce[1]); IntVarArgs y0 = arg2intvarargs(s, ce[2]); IntVarArgs h = arg2intvarargs(s, ce[3]); IntVarArgs x1(x0.size()), y1(y0.size()); for (int i=x0.size(); i--; ) x1[i] = expr(s, x0[i] + w[i]); for (int i=y0.size(); i--; ) y1[i] = expr(s, y0[i] + h[i]); nooverlap(s,x0,w,x1,y0,h,y1,ann2icl(ann)); } void p_precede(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs x = arg2intvarargs(s, ce[0]); IntArgs c = arg2intargs(ce[1]); precede(s,x,c,ann2icl(ann)); } void p_nvalue(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs x = arg2intvarargs(s, ce[1]); if (ce[0]->isIntVar()) { IntVar y = getIntVar(s,ce[0]); nvalues(s,x,IRT_EQ,y,ann2icl(ann)); } else { nvalues(s,x,IRT_EQ,ce[0]->getInt(),ann2icl(ann)); } } void p_among(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs x = arg2intvarargs(s, ce[1]); IntSet v = arg2intset(s, ce[2]); if (ce[0]->isIntVar()) { IntVar n = getIntVar(s,ce[0]); std::cerr << "count " << n << std::endl; count(s,x,v,IRT_EQ,n,ann2icl(ann)); } else { std::cerr << "count i " << x << " " << v << " " << ce[0]->getInt() << std::endl; count(s,x,v,IRT_EQ,ce[0]->getInt(),ann2icl(ann)); } } void p_member_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs x = arg2intvarargs(s, ce[0]); IntVar y = getIntVar(s, ce[1]); member(s,x,y,ann2icl(ann)); } void p_member_int_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntVarArgs x = arg2intvarargs(s, ce[0]); IntVar y = getIntVar(s, ce[1]); BoolVar b = getBoolVar(s, ce[2]); member(s,x,y,b,ann2icl(ann)); } void p_member_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BoolVarArgs x = arg2boolvarargs(s, ce[0]); BoolVar y = getBoolVar(s, ce[1]); member(s,x,y,ann2icl(ann)); } void p_member_bool_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { BoolVarArgs x = arg2boolvarargs(s, ce[0]); BoolVar y = getBoolVar(s, ce[1]); member(s,x,y,getBoolVar(s, ce[2]),ann2icl(ann)); } class IntPoster { public: IntPoster(void) { registry().add("all_different_int", &p_distinct); registry().add("all_different_offset", &p_distinctOffset); registry().add("all_equal_int", &p_all_equal); registry().add("int_eq", &p_int_eq); registry().add("int_ne", &p_int_ne); registry().add("int_ge", &p_int_ge); registry().add("int_gt", &p_int_gt); registry().add("int_le", &p_int_le); registry().add("int_lt", &p_int_lt); registry().add("int_eq_reif", &p_int_eq_reif); registry().add("int_ne_reif", &p_int_ne_reif); registry().add("int_ge_reif", &p_int_ge_reif); registry().add("int_gt_reif", &p_int_gt_reif); registry().add("int_le_reif", &p_int_le_reif); registry().add("int_lt_reif", &p_int_lt_reif); registry().add("int_lin_eq", &p_int_lin_eq); registry().add("int_lin_eq_reif", &p_int_lin_eq_reif); registry().add("int_lin_ne", &p_int_lin_ne); registry().add("int_lin_ne_reif", &p_int_lin_ne_reif); registry().add("int_lin_le", &p_int_lin_le); registry().add("int_lin_le_reif", &p_int_lin_le_reif); registry().add("int_lin_lt", &p_int_lin_lt); registry().add("int_lin_lt_reif", &p_int_lin_lt_reif); registry().add("int_lin_ge", &p_int_lin_ge); registry().add("int_lin_ge_reif", &p_int_lin_ge_reif); registry().add("int_lin_gt", &p_int_lin_gt); registry().add("int_lin_gt_reif", &p_int_lin_gt_reif); registry().add("int_plus", &p_int_plus); registry().add("int_minus", &p_int_minus); registry().add("int_times", &p_int_times); registry().add("int_div", &p_int_div); registry().add("int_mod", &p_int_mod); registry().add("int_min", &p_int_min); registry().add("int_max", &p_int_max); registry().add("int_abs", &p_abs); registry().add("int_negate", &p_int_negate); registry().add("bool_eq", &p_bool_eq); registry().add("bool_eq_reif", &p_bool_eq_reif); registry().add("bool_ne", &p_bool_ne); registry().add("bool_ne_reif", &p_bool_ne_reif); registry().add("bool_ge", &p_bool_ge); registry().add("bool_ge_reif", &p_bool_ge_reif); registry().add("bool_le", &p_bool_le); registry().add("bool_le_reif", &p_bool_le_reif); registry().add("bool_gt", &p_bool_gt); registry().add("bool_gt_reif", &p_bool_gt_reif); registry().add("bool_lt", &p_bool_lt); registry().add("bool_lt_reif", &p_bool_lt_reif); registry().add("bool_or", &p_bool_or); registry().add("bool_and", &p_bool_and); registry().add("bool_xor", &p_bool_xor); registry().add("array_bool_and", &p_array_bool_and); registry().add("array_bool_or", &p_array_bool_or); registry().add("array_bool_xor", &p_array_bool_xor); registry().add("bool_clause", &p_array_bool_clause); registry().add("bool_clause_reif", &p_array_bool_clause_reif); registry().add("bool_left_imp", &p_bool_l_imp); registry().add("bool_right_imp", &p_bool_r_imp); registry().add("bool_not", &p_bool_not); registry().add("array_int_element", &p_array_int_element); registry().add("array_var_int_element", &p_array_int_element); registry().add("array_bool_element", &p_array_bool_element); registry().add("array_var_bool_element", &p_array_bool_element); registry().add("bool2int", &p_bool2int); registry().add("int_in", &p_int_in); registry().add("int_in_reif", &p_int_in_reif); #ifndef GECODE_HAS_SET_VARS registry().add("set_in", &p_int_in); registry().add("set_in_reif", &p_int_in_reif); #endif registry().add("array_int_lt", &p_array_int_lt); registry().add("array_int_lq", &p_array_int_lq); registry().add("count", &p_count); registry().add("at_least_int", &p_at_least); registry().add("at_most_int", &p_at_most); registry().add("gecode_bin_packing_load", &p_bin_packing_load); registry().add("global_cardinality", &p_global_cardinality); registry().add("global_cardinality_closed", &p_global_cardinality_closed); registry().add("global_cardinality_low_up", &p_global_cardinality_low_up); registry().add("global_cardinality_low_up_closed", &p_global_cardinality_low_up_closed); registry().add("minimum_int", &p_minimum); registry().add("maximum_int", &p_maximum); registry().add("regular", &p_regular); registry().add("sort", &p_sort); registry().add("inverse_offsets", &p_inverse_offsets); registry().add("increasing_int", &p_increasing_int); registry().add("increasing_bool", &p_increasing_bool); registry().add("decreasing_int", &p_decreasing_int); registry().add("decreasing_bool", &p_decreasing_bool); registry().add("table_int", &p_table_int); registry().add("table_bool", &p_table_bool); registry().add("cumulatives", &p_cumulatives); registry().add("gecode_among_seq_int", &p_among_seq_int); registry().add("gecode_among_seq_bool", &p_among_seq_bool); registry().add("bool_lin_eq", &p_bool_lin_eq); registry().add("bool_lin_ne", &p_bool_lin_ne); registry().add("bool_lin_le", &p_bool_lin_le); registry().add("bool_lin_lt", &p_bool_lin_lt); registry().add("bool_lin_ge", &p_bool_lin_ge); registry().add("bool_lin_gt", &p_bool_lin_gt); registry().add("bool_lin_eq_reif", &p_bool_lin_eq_reif); registry().add("bool_lin_ne_reif", &p_bool_lin_ne_reif); registry().add("bool_lin_le_reif", &p_bool_lin_le_reif); registry().add("bool_lin_lt_reif", &p_bool_lin_lt_reif); registry().add("bool_lin_ge_reif", &p_bool_lin_ge_reif); registry().add("bool_lin_gt_reif", &p_bool_lin_gt_reif); registry().add("gecode_schedule_unary", &p_schedule_unary); registry().add("gecode_schedule_unary_optional", &p_schedule_unary_optional); registry().add("gecode_circuit", &p_circuit); registry().add("gecode_circuit_cost_array", &p_circuit_cost_array); registry().add("gecode_circuit_cost", &p_circuit_cost); registry().add("gecode_nooverlap", &p_nooverlap); registry().add("gecode_precede", &p_precede); registry().add("nvalue",&p_nvalue); registry().add("among",&p_among); registry().add("member_int",&p_member_int); registry().add("gecode_member_int_reif",&p_member_int_reif); registry().add("member_bool",&p_member_bool); registry().add("gecode_member_bool_reif",&p_member_bool_reif); } }; IntPoster __int_poster; #ifdef GECODE_HAS_SET_VARS void p_set_OP(FlatZincSpace& s, SetOpType op, const ConExpr& ce, AST::Node *) { rel(s, getSetVar(s, ce[0]), op, getSetVar(s, ce[1]), SRT_EQ, getSetVar(s, ce[2])); } void p_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { p_set_OP(s, SOT_UNION, ce, ann); } void p_set_intersect(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { p_set_OP(s, SOT_INTER, ce, ann); } void p_set_diff(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { p_set_OP(s, SOT_MINUS, ce, ann); } void p_set_symdiff(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { SetVar x = getSetVar(s, ce[0]); SetVar y = getSetVar(s, ce[1]); SetVarLubRanges xub(x); IntSet xubs(xub); SetVar x_y(s,IntSet::empty,xubs); rel(s, x, SOT_MINUS, y, SRT_EQ, x_y); SetVarLubRanges yub(y); IntSet yubs(yub); SetVar y_x(s,IntSet::empty,yubs); rel(s, y, SOT_MINUS, x, SRT_EQ, y_x); rel(s, x_y, SOT_UNION, y_x, SRT_EQ, getSetVar(s, ce[2])); } void p_array_set_OP(FlatZincSpace& s, SetOpType op, const ConExpr& ce, AST::Node *) { SetVarArgs xs = arg2setvarargs(s, ce[0]); rel(s, op, xs, getSetVar(s, ce[1])); } void p_array_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { p_array_set_OP(s, SOT_UNION, ce, ann); } void p_array_set_partition(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { p_array_set_OP(s, SOT_DUNION, ce, ann); } void p_set_rel(FlatZincSpace& s, SetRelType srt, const ConExpr& ce) { rel(s, getSetVar(s, ce[0]), srt, getSetVar(s, ce[1])); } void p_set_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { p_set_rel(s, SRT_EQ, ce); } void p_set_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { p_set_rel(s, SRT_NQ, ce); } void p_set_subset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { p_set_rel(s, SRT_SUB, ce); } void p_set_superset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { p_set_rel(s, SRT_SUP, ce); } void p_set_le(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { p_set_rel(s, SRT_LQ, ce); } void p_set_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { p_set_rel(s, SRT_LE, ce); } void p_set_card(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { if (!ce[1]->isIntVar()) { cardinality(s, getSetVar(s, ce[0]), ce[1]->getInt(), ce[1]->getInt()); } else { cardinality(s, getSetVar(s, ce[0]), getIntVar(s, ce[1])); } } void p_set_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { if (!ce[1]->isSetVar()) { IntSet d = arg2intset(s,ce[1]); if (ce[0]->isBoolVar()) { IntSetRanges dr(d); Iter::Ranges::Singleton sr(0,1); Iter::Ranges::Inter i(dr,sr); IntSet d01(i); if (d01.size() == 0) { s.fail(); } else { rel(s, getBoolVar(s, ce[0]), IRT_GQ, d01.min()); rel(s, getBoolVar(s, ce[0]), IRT_LQ, d01.max()); } } else { dom(s, getIntVar(s, ce[0]), d); } } else { if (!ce[0]->isIntVar()) { dom(s, getSetVar(s, ce[1]), SRT_SUP, ce[0]->getInt()); } else { rel(s, getSetVar(s, ce[1]), SRT_SUP, getIntVar(s, ce[0])); } } } void p_set_rel_reif(FlatZincSpace& s, SetRelType srt, const ConExpr& ce) { rel(s, getSetVar(s, ce[0]), srt, getSetVar(s, ce[1]), getBoolVar(s, ce[2])); } void p_set_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { p_set_rel_reif(s,SRT_EQ,ce); } void p_set_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { p_set_rel_reif(s,SRT_LQ,ce); } void p_set_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { p_set_rel_reif(s,SRT_LE,ce); } void p_set_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { p_set_rel_reif(s,SRT_NQ,ce); } void p_set_subset_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { p_set_rel_reif(s,SRT_SUB,ce); } void p_set_superset_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { p_set_rel_reif(s,SRT_SUP,ce); } void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { if (!ce[1]->isSetVar()) { IntSet d = arg2intset(s,ce[1]); if (ce[0]->isBoolVar()) { IntSetRanges dr(d); Iter::Ranges::Singleton sr(0,1); Iter::Ranges::Inter i(dr,sr); IntSet d01(i); if (d01.size() == 0) { rel(s, getBoolVar(s, ce[2]) == 0); } else if (d01.max() == 0) { rel(s, getBoolVar(s, ce[2]) == !getBoolVar(s, ce[0])); } else if (d01.min() == 1) { rel(s, getBoolVar(s, ce[2]) == getBoolVar(s, ce[0])); } else { rel(s, getBoolVar(s, ce[2]) == 1); } } else { dom(s, getIntVar(s, ce[0]), d, getBoolVar(s, ce[2])); } } else { if (!ce[0]->isIntVar()) { dom(s, getSetVar(s, ce[1]), SRT_SUP, ce[0]->getInt(), getBoolVar(s, ce[2])); } else { rel(s, getSetVar(s, ce[1]), SRT_SUP, getIntVar(s, ce[0]), getBoolVar(s, ce[2])); } } } void p_set_disjoint(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { rel(s, getSetVar(s, ce[0]), SRT_DISJ, getSetVar(s, ce[1])); } void p_link_set_to_booleans(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { SetVar x = getSetVar(s, ce[0]); int idx = ce[2]->getInt(); assert(idx >= 0); rel(s, x || IntSet(Set::Limits::min,idx-1)); BoolVarArgs y = arg2boolvarargs(s,ce[1],idx); channel(s, y, x); } void p_array_set_element(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { bool isConstant = true; AST::Array* a = ce[1]->getArray(); for (int i=a->a.size(); i--;) { if (a->a[i]->isSetVar()) { isConstant = false; break; } } IntVar selector = getIntVar(s, ce[0]); rel(s, selector > 0); if (isConstant) { IntSetArgs sv = arg2intsetargs(s,ce[1],1); element(s, sv, selector, getSetVar(s, ce[2])); } else { SetVarArgs sv = arg2setvarargs(s, ce[1], 1); element(s, sv, selector, getSetVar(s, ce[2])); } } void p_array_set_element_op(FlatZincSpace& s, const ConExpr& ce, AST::Node*, SetOpType op, const IntSet& universe = IntSet(Set::Limits::min,Set::Limits::max)) { bool isConstant = true; AST::Array* a = ce[1]->getArray(); for (int i=a->a.size(); i--;) { if (a->a[i]->isSetVar()) { isConstant = false; break; } } SetVar selector = getSetVar(s, ce[0]); dom(s, selector, SRT_DISJ, 0); if (isConstant) { IntSetArgs sv = arg2intsetargs(s,ce[1], 1); element(s, op, sv, selector, getSetVar(s, ce[2]), universe); } else { SetVarArgs sv = arg2setvarargs(s, ce[1], 1); element(s, op, sv, selector, getSetVar(s, ce[2]), universe); } } void p_array_set_element_union(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_array_set_element_op(s, ce, ann, SOT_UNION); } void p_array_set_element_intersect(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_array_set_element_op(s, ce, ann, SOT_INTER); } void p_array_set_element_intersect_in(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { IntSet d = arg2intset(s, ce[3]); p_array_set_element_op(s, ce, ann, SOT_INTER, d); } void p_array_set_element_partition(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { p_array_set_element_op(s, ce, ann, SOT_DUNION); } void p_set_convex(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { convex(s, getSetVar(s, ce[0])); } void p_array_set_seq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { SetVarArgs sv = arg2setvarargs(s, ce[0]); sequence(s, sv); } void p_array_set_seq_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { SetVarArgs sv = arg2setvarargs(s, ce[0]); sequence(s, sv, getSetVar(s, ce[1])); } void p_int_set_channel(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { int xoff=ce[1]->getInt(); assert(xoff >= 0); int yoff=ce[3]->getInt(); assert(yoff >= 0); IntVarArgs xv = arg2intvarargs(s, ce[0], xoff); SetVarArgs yv = arg2setvarargs(s, ce[2], yoff, 1, IntSet(0, xoff-1)); IntSet xd(yoff,yv.size()-1); for (int i=xoff; igetInt(); assert(xoff >= 0); IntVarArgs xv = arg2intvarargs(s,ce[0],xoff); element(s, SOT_UNION, xv, getSetVar(s,ce[2]), getSetVar(s,ce[3])); } void p_weights(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { IntArgs e = arg2intargs(ce[0]); IntArgs w = arg2intargs(ce[1]); SetVar x = getSetVar(s,ce[2]); IntVar y = getIntVar(s,ce[3]); weights(s,e,w,x,y); } class SetPoster { public: SetPoster(void) { registry().add("set_eq", &p_set_eq); registry().add("set_le", &p_set_le); registry().add("set_lt", &p_set_lt); registry().add("equal", &p_set_eq); registry().add("set_ne", &p_set_ne); registry().add("set_union", &p_set_union); registry().add("array_set_element", &p_array_set_element); registry().add("array_var_set_element", &p_array_set_element); registry().add("set_intersect", &p_set_intersect); registry().add("set_diff", &p_set_diff); registry().add("set_symdiff", &p_set_symdiff); registry().add("set_subset", &p_set_subset); registry().add("set_superset", &p_set_superset); registry().add("set_card", &p_set_card); registry().add("set_in", &p_set_in); registry().add("set_eq_reif", &p_set_eq_reif); registry().add("set_le_reif", &p_set_le_reif); registry().add("set_lt_reif", &p_set_lt_reif); registry().add("equal_reif", &p_set_eq_reif); registry().add("set_ne_reif", &p_set_ne_reif); registry().add("set_subset_reif", &p_set_subset_reif); registry().add("set_superset_reif", &p_set_superset_reif); registry().add("set_in_reif", &p_set_in_reif); registry().add("disjoint", &p_set_disjoint); registry().add("gecode_link_set_to_booleans", &p_link_set_to_booleans); registry().add("array_set_union", &p_array_set_union); registry().add("array_set_partition", &p_array_set_partition); registry().add("set_convex", &p_set_convex); registry().add("array_set_seq", &p_array_set_seq); registry().add("array_set_seq_union", &p_array_set_seq_union); registry().add("gecode_array_set_element_union", &p_array_set_element_union); registry().add("gecode_array_set_element_intersect", &p_array_set_element_intersect); registry().add("gecode_array_set_element_intersect_in", &p_array_set_element_intersect_in); registry().add("gecode_array_set_element_partition", &p_array_set_element_partition); registry().add("gecode_int_set_channel", &p_int_set_channel); registry().add("gecode_range", &p_range); registry().add("gecode_set_weights", &p_weights); } }; SetPoster __set_poster; #endif } }} // STATISTICS: flatzinc-any