1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ 2 /* 3 * Main authors: 4 * Guido Tack <tack@gecode.org> 5 * 6 * Contributing authors: 7 * Mikael Lagerkvist <lagerkvist@gmail.com> 8 * 9 * Copyright: 10 * Guido Tack, 2007 11 * Mikael Lagerkvist, 2009 12 * 13 * This file is part of Gecode, the generic constraint 14 * development environment: 15 * http://www.gecode.org 16 * 17 * Permission is hereby granted, free of charge, to any person obtaining 18 * a copy of this software and associated documentation files (the 19 * "Software"), to deal in the Software without restriction, including 20 * without limitation the rights to use, copy, modify, merge, publish, 21 * distribute, sublicense, and/or sell copies of the Software, and to 22 * permit persons to whom the Software is furnished to do so, subject to 23 * the following conditions: 24 * 25 * The above copyright notice and this permission notice shall be 26 * included in all copies or substantial portions of the Software. 27 * 28 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 29 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 30 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 31 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE 32 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION 33 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION 34 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 35 * 36 */ 37 38 #include <gecode/flatzinc/registry.hh> 39 #include <gecode/kernel.hh> 40 #include <gecode/int.hh> 41 #include <gecode/minimodel.hh> 42 43 #ifdef GECODE_HAS_SET_VARS 44 #include <gecode/set.hh> 45 #endif 46 #ifdef GECODE_HAS_FLOAT_VARS 47 #include <gecode/float.hh> 48 #endif 49 #include <gecode/flatzinc.hh> 50 51 namespace Gecode { namespace FlatZinc { 52 registry(void)53 Registry& registry(void) { 54 static Registry r; 55 return r; 56 } 57 58 void post(FlatZincSpace & s,const ConExpr & ce)59 Registry::post(FlatZincSpace& s, const ConExpr& ce) { 60 std::map<std::string,poster>::iterator i = r.find(ce.id); 61 if (i == r.end()) { 62 throw FlatZinc::Error("Registry", 63 std::string("Constraint ")+ce.id+" not found", ce.ann); 64 } 65 i->second(s, ce, ce.ann); 66 } 67 68 void add(const std::string & id,poster p)69 Registry::add(const std::string& id, poster p) { 70 r[id] = p; 71 r["gecode_" + id] = p; 72 r["fzn_" + id] = p; 73 } 74 75 namespace { 76 p_distinct(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)77 void p_distinct(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 78 IntVarArgs va = s.arg2intvarargs(ce[0]); 79 IntPropLevel ipl = s.ann2ipl(ann); 80 unshare(s, va); 81 distinct(s, va, ipl == IPL_DEF ? IPL_BND : ipl); 82 } 83 p_distinctOffset(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)84 void p_distinctOffset(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 85 IntVarArgs va = s.arg2intvarargs(ce[1]); 86 unshare(s, va); 87 AST::Array* offs = ce.args->a[0]->getArray(); 88 IntArgs oa(offs->a.size()); 89 for (int i=offs->a.size(); i--; ) { 90 oa[i] = offs->a[i]->getInt(); 91 } 92 IntPropLevel ipl = s.ann2ipl(ann); 93 distinct(s, oa, va, ipl == IPL_DEF ? IPL_BND : ipl); 94 } 95 p_all_equal(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)96 void p_all_equal(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 97 IntVarArgs va = s.arg2intvarargs(ce[0]); 98 rel(s, va, IRT_EQ, s.ann2ipl(ann)); 99 } 100 p_int_CMP(FlatZincSpace & s,IntRelType irt,const ConExpr & ce,AST::Node * ann)101 void p_int_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, 102 AST::Node* ann) { 103 if (ce[0]->isIntVar()) { 104 if (ce[1]->isIntVar()) { 105 rel(s, s.arg2IntVar(ce[0]), irt, s.arg2IntVar(ce[1]), 106 s.ann2ipl(ann)); 107 } else { 108 rel(s, s.arg2IntVar(ce[0]), irt, ce[1]->getInt(), s.ann2ipl(ann)); 109 } 110 } else { 111 rel(s, s.arg2IntVar(ce[1]), swap(irt), ce[0]->getInt(), 112 s.ann2ipl(ann)); 113 } 114 } p_int_eq(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)115 void p_int_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 116 p_int_CMP(s, IRT_EQ, ce, ann); 117 } p_int_ne(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)118 void p_int_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 119 p_int_CMP(s, IRT_NQ, ce, ann); 120 } p_int_ge(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)121 void p_int_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 122 p_int_CMP(s, IRT_GQ, ce, ann); 123 } p_int_gt(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)124 void p_int_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 125 p_int_CMP(s, IRT_GR, ce, ann); 126 } p_int_le(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)127 void p_int_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 128 p_int_CMP(s, IRT_LQ, ce, ann); 129 } p_int_lt(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)130 void p_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 131 p_int_CMP(s, IRT_LE, ce, ann); 132 } p_int_CMP_reif(FlatZincSpace & s,IntRelType irt,ReifyMode rm,const ConExpr & ce,AST::Node * ann)133 void p_int_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm, 134 const ConExpr& ce, AST::Node* ann) { 135 if (rm == RM_EQV && ce[2]->isBool()) { 136 if (ce[2]->getBool()) { 137 p_int_CMP(s, irt, ce, ann); 138 } else { 139 p_int_CMP(s, neg(irt), ce, ann); 140 } 141 return; 142 } 143 if (ce[0]->isIntVar()) { 144 if (ce[1]->isIntVar()) { 145 rel(s, s.arg2IntVar(ce[0]), irt, s.arg2IntVar(ce[1]), 146 Reify(s.arg2BoolVar(ce[2]), rm), s.ann2ipl(ann)); 147 } else { 148 rel(s, s.arg2IntVar(ce[0]), irt, ce[1]->getInt(), 149 Reify(s.arg2BoolVar(ce[2]), rm), s.ann2ipl(ann)); 150 } 151 } else { 152 rel(s, s.arg2IntVar(ce[1]), swap(irt), ce[0]->getInt(), 153 Reify(s.arg2BoolVar(ce[2]), rm), s.ann2ipl(ann)); 154 } 155 } 156 157 /* Comparisons */ p_int_eq_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)158 void p_int_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 159 p_int_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann); 160 } p_int_ne_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)161 void p_int_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 162 p_int_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann); 163 } p_int_ge_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)164 void p_int_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 165 p_int_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann); 166 } p_int_gt_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)167 void p_int_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 168 p_int_CMP_reif(s, IRT_GR, RM_EQV, ce, ann); 169 } p_int_le_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)170 void p_int_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 171 p_int_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann); 172 } p_int_lt_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)173 void p_int_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 174 p_int_CMP_reif(s, IRT_LE, RM_EQV, ce, ann); 175 } 176 p_int_eq_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)177 void p_int_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 178 p_int_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann); 179 } p_int_ne_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)180 void p_int_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 181 p_int_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann); 182 } p_int_ge_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)183 void p_int_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 184 p_int_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann); 185 } p_int_gt_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)186 void p_int_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 187 p_int_CMP_reif(s, IRT_GR, RM_IMP, ce, ann); 188 } p_int_le_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)189 void p_int_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 190 p_int_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann); 191 } p_int_lt_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)192 void p_int_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 193 p_int_CMP_reif(s, IRT_LE, RM_IMP, ce, ann); 194 } 195 196 /* linear (in-)equations */ p_int_lin_CMP(FlatZincSpace & s,IntRelType irt,const ConExpr & ce,AST::Node * ann)197 void p_int_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, 198 AST::Node* ann) { 199 IntArgs ia = s.arg2intargs(ce[0]); 200 int singleIntVar; 201 if (s.isBoolArray(ce[1],singleIntVar)) { 202 if (singleIntVar != -1) { 203 if (std::abs(ia[singleIntVar]) == 1 && ce[2]->getInt() == 0) { 204 IntVar siv = s.arg2IntVar(ce[1]->getArray()->a[singleIntVar]); 205 BoolVarArgs iv = s.arg2boolvarargs(ce[1], 0, singleIntVar); 206 IntArgs ia_tmp(ia.size()-1); 207 int count = 0; 208 for (int i=0; i<ia.size(); i++) { 209 if (i != singleIntVar) 210 ia_tmp[count++] = ia[singleIntVar] == -1 ? ia[i] : -ia[i]; 211 } 212 IntRelType t = (ia[singleIntVar] == -1 ? irt : swap(irt)); 213 linear(s, ia_tmp, iv, t, siv, s.ann2ipl(ann)); 214 } else { 215 IntVarArgs iv = s.arg2intvarargs(ce[1]); 216 linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2ipl(ann)); 217 } 218 } else { 219 BoolVarArgs iv = s.arg2boolvarargs(ce[1]); 220 linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2ipl(ann)); 221 } 222 } else { 223 IntVarArgs iv = s.arg2intvarargs(ce[1]); 224 linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2ipl(ann)); 225 } 226 } p_int_lin_CMP_reif(FlatZincSpace & s,IntRelType irt,ReifyMode rm,const ConExpr & ce,AST::Node * ann)227 void p_int_lin_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm, 228 const ConExpr& ce, AST::Node* ann) { 229 if (rm == RM_EQV && ce[2]->isBool()) { 230 if (ce[2]->getBool()) { 231 p_int_lin_CMP(s, irt, ce, ann); 232 } else { 233 p_int_lin_CMP(s, neg(irt), ce, ann); 234 } 235 return; 236 } 237 IntArgs ia = s.arg2intargs(ce[0]); 238 int singleIntVar; 239 if (s.isBoolArray(ce[1],singleIntVar)) { 240 if (singleIntVar != -1) { 241 if (std::abs(ia[singleIntVar]) == 1 && ce[2]->getInt() == 0) { 242 IntVar siv = s.arg2IntVar(ce[1]->getArray()->a[singleIntVar]); 243 BoolVarArgs iv = s.arg2boolvarargs(ce[1], 0, singleIntVar); 244 IntArgs ia_tmp(ia.size()-1); 245 int count = 0; 246 for (int i=0; i<ia.size(); i++) { 247 if (i != singleIntVar) 248 ia_tmp[count++] = ia[singleIntVar] == -1 ? ia[i] : -ia[i]; 249 } 250 IntRelType t = (ia[singleIntVar] == -1 ? irt : swap(irt)); 251 linear(s, ia_tmp, iv, t, siv, Reify(s.arg2BoolVar(ce[3]), rm), 252 s.ann2ipl(ann)); 253 } else { 254 IntVarArgs iv = s.arg2intvarargs(ce[1]); 255 linear(s, ia, iv, irt, ce[2]->getInt(), 256 Reify(s.arg2BoolVar(ce[3]), rm), s.ann2ipl(ann)); 257 } 258 } else { 259 BoolVarArgs iv = s.arg2boolvarargs(ce[1]); 260 linear(s, ia, iv, irt, ce[2]->getInt(), 261 Reify(s.arg2BoolVar(ce[3]), rm), s.ann2ipl(ann)); 262 } 263 } else { 264 IntVarArgs iv = s.arg2intvarargs(ce[1]); 265 linear(s, ia, iv, irt, ce[2]->getInt(), 266 Reify(s.arg2BoolVar(ce[3]), rm), 267 s.ann2ipl(ann)); 268 } 269 } p_int_lin_eq(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)270 void p_int_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 271 p_int_lin_CMP(s, IRT_EQ, ce, ann); 272 } p_int_lin_eq_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)273 void p_int_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 274 p_int_lin_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann); 275 } p_int_lin_eq_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)276 void p_int_lin_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 277 p_int_lin_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann); 278 } p_int_lin_ne(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)279 void p_int_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 280 p_int_lin_CMP(s, IRT_NQ, ce, ann); 281 } p_int_lin_ne_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)282 void p_int_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 283 p_int_lin_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann); 284 } p_int_lin_ne_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)285 void p_int_lin_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 286 p_int_lin_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann); 287 } p_int_lin_le(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)288 void p_int_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 289 p_int_lin_CMP(s, IRT_LQ, ce, ann); 290 } p_int_lin_le_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)291 void p_int_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 292 p_int_lin_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann); 293 } p_int_lin_le_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)294 void p_int_lin_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 295 p_int_lin_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann); 296 } p_int_lin_lt(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)297 void p_int_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 298 p_int_lin_CMP(s, IRT_LE, ce, ann); 299 } p_int_lin_lt_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)300 void p_int_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 301 p_int_lin_CMP_reif(s, IRT_LE, RM_EQV, ce, ann); 302 } p_int_lin_lt_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)303 void p_int_lin_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 304 p_int_lin_CMP_reif(s, IRT_LE, RM_IMP, ce, ann); 305 } p_int_lin_ge(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)306 void p_int_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 307 p_int_lin_CMP(s, IRT_GQ, ce, ann); 308 } p_int_lin_ge_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)309 void p_int_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 310 p_int_lin_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann); 311 } p_int_lin_ge_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)312 void p_int_lin_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 313 p_int_lin_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann); 314 } p_int_lin_gt(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)315 void p_int_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 316 p_int_lin_CMP(s, IRT_GR, ce, ann); 317 } p_int_lin_gt_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)318 void p_int_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 319 p_int_lin_CMP_reif(s, IRT_GR, RM_EQV, ce, ann); 320 } p_int_lin_gt_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)321 void p_int_lin_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 322 p_int_lin_CMP_reif(s, IRT_GR, RM_IMP, ce, ann); 323 } 324 p_bool_lin_CMP(FlatZincSpace & s,IntRelType irt,const ConExpr & ce,AST::Node * ann)325 void p_bool_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, 326 AST::Node* ann) { 327 IntArgs ia = s.arg2intargs(ce[0]); 328 BoolVarArgs iv = s.arg2boolvarargs(ce[1]); 329 if (ce[2]->isIntVar()) 330 linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()], s.ann2ipl(ann)); 331 else 332 linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2ipl(ann)); 333 } p_bool_lin_CMP_reif(FlatZincSpace & s,IntRelType irt,ReifyMode rm,const ConExpr & ce,AST::Node * ann)334 void p_bool_lin_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm, 335 const ConExpr& ce, AST::Node* ann) { 336 if (rm == RM_EQV && ce[2]->isBool()) { 337 if (ce[2]->getBool()) { 338 p_bool_lin_CMP(s, irt, ce, ann); 339 } else { 340 p_bool_lin_CMP(s, neg(irt), ce, ann); 341 } 342 return; 343 } 344 IntArgs ia = s.arg2intargs(ce[0]); 345 BoolVarArgs iv = s.arg2boolvarargs(ce[1]); 346 if (ce[2]->isIntVar()) 347 linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()], 348 Reify(s.arg2BoolVar(ce[3]), rm), 349 s.ann2ipl(ann)); 350 else 351 linear(s, ia, iv, irt, ce[2]->getInt(), 352 Reify(s.arg2BoolVar(ce[3]), rm), 353 s.ann2ipl(ann)); 354 } p_bool_lin_eq(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)355 void p_bool_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 356 p_bool_lin_CMP(s, IRT_EQ, ce, ann); 357 } p_bool_lin_eq_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)358 void p_bool_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 359 { 360 p_bool_lin_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann); 361 } p_bool_lin_eq_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)362 void p_bool_lin_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 363 { 364 p_bool_lin_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann); 365 } p_bool_lin_ne(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)366 void p_bool_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 367 p_bool_lin_CMP(s, IRT_NQ, ce, ann); 368 } p_bool_lin_ne_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)369 void p_bool_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 370 { 371 p_bool_lin_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann); 372 } p_bool_lin_ne_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)373 void p_bool_lin_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 374 { 375 p_bool_lin_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann); 376 } p_bool_lin_le(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)377 void p_bool_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 378 p_bool_lin_CMP(s, IRT_LQ, ce, ann); 379 } p_bool_lin_le_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)380 void p_bool_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 381 { 382 p_bool_lin_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann); 383 } p_bool_lin_le_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)384 void p_bool_lin_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 385 { 386 p_bool_lin_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann); 387 } p_bool_lin_lt(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)388 void p_bool_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 389 { 390 p_bool_lin_CMP(s, IRT_LE, ce, ann); 391 } p_bool_lin_lt_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)392 void p_bool_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 393 { 394 p_bool_lin_CMP_reif(s, IRT_LE, RM_EQV, ce, ann); 395 } p_bool_lin_lt_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)396 void p_bool_lin_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 397 { 398 p_bool_lin_CMP_reif(s, IRT_LE, RM_IMP, ce, ann); 399 } p_bool_lin_ge(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)400 void p_bool_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 401 p_bool_lin_CMP(s, IRT_GQ, ce, ann); 402 } p_bool_lin_ge_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)403 void p_bool_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 404 { 405 p_bool_lin_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann); 406 } p_bool_lin_ge_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)407 void p_bool_lin_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 408 { 409 p_bool_lin_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann); 410 } p_bool_lin_gt(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)411 void p_bool_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 412 p_bool_lin_CMP(s, IRT_GR, ce, ann); 413 } p_bool_lin_gt_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)414 void p_bool_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 415 { 416 p_bool_lin_CMP_reif(s, IRT_GR, RM_EQV, ce, ann); 417 } p_bool_lin_gt_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)418 void p_bool_lin_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 419 { 420 p_bool_lin_CMP_reif(s, IRT_GR, RM_IMP, ce, ann); 421 } 422 423 /* arithmetic constraints */ 424 p_int_plus(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)425 void p_int_plus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 426 if (!ce[0]->isIntVar()) { 427 rel(s, ce[0]->getInt() + s.arg2IntVar(ce[1]) 428 == s.arg2IntVar(ce[2]), s.ann2ipl(ann)); 429 } else if (!ce[1]->isIntVar()) { 430 rel(s, s.arg2IntVar(ce[0]) + ce[1]->getInt() 431 == s.arg2IntVar(ce[2]), s.ann2ipl(ann)); 432 } else if (!ce[2]->isIntVar()) { 433 rel(s, s.arg2IntVar(ce[0]) + s.arg2IntVar(ce[1]) 434 == ce[2]->getInt(), s.ann2ipl(ann)); 435 } else { 436 rel(s, s.arg2IntVar(ce[0]) + s.arg2IntVar(ce[1]) 437 == s.arg2IntVar(ce[2]), s.ann2ipl(ann)); 438 } 439 } 440 p_int_minus(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)441 void p_int_minus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 442 if (!ce[0]->isIntVar()) { 443 rel(s, ce[0]->getInt() - s.arg2IntVar(ce[1]) 444 == s.arg2IntVar(ce[2]), s.ann2ipl(ann)); 445 } else if (!ce[1]->isIntVar()) { 446 rel(s, s.arg2IntVar(ce[0]) - ce[1]->getInt() 447 == s.arg2IntVar(ce[2]), s.ann2ipl(ann)); 448 } else if (!ce[2]->isIntVar()) { 449 rel(s, s.arg2IntVar(ce[0]) - s.arg2IntVar(ce[1]) 450 == ce[2]->getInt(), s.ann2ipl(ann)); 451 } else { 452 rel(s, s.arg2IntVar(ce[0]) - s.arg2IntVar(ce[1]) 453 == s.arg2IntVar(ce[2]), s.ann2ipl(ann)); 454 } 455 } 456 p_int_times(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)457 void p_int_times(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 458 IntVar x0 = s.arg2IntVar(ce[0]); 459 IntVar x1 = s.arg2IntVar(ce[1]); 460 IntVar x2 = s.arg2IntVar(ce[2]); 461 mult(s, x0, x1, x2, s.ann2ipl(ann)); 462 } p_int_pow(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)463 void p_int_pow(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 464 IntVar x0 = s.arg2IntVar(ce[0]); 465 IntVar x2 = s.arg2IntVar(ce[2]); 466 pow(s, x0, ce[1]->getInt(), x2, s.ann2ipl(ann)); 467 } p_int_div(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)468 void p_int_div(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 469 IntVar x0 = s.arg2IntVar(ce[0]); 470 IntVar x1 = s.arg2IntVar(ce[1]); 471 IntVar x2 = s.arg2IntVar(ce[2]); 472 div(s,x0,x1,x2, s.ann2ipl(ann)); 473 } p_int_mod(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)474 void p_int_mod(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 475 IntVar x0 = s.arg2IntVar(ce[0]); 476 IntVar x1 = s.arg2IntVar(ce[1]); 477 IntVar x2 = s.arg2IntVar(ce[2]); 478 mod(s,x0,x1,x2, s.ann2ipl(ann)); 479 } 480 p_int_min(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)481 void p_int_min(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 482 IntVar x0 = s.arg2IntVar(ce[0]); 483 IntVar x1 = s.arg2IntVar(ce[1]); 484 IntVar x2 = s.arg2IntVar(ce[2]); 485 min(s, x0, x1, x2, s.ann2ipl(ann)); 486 } p_int_max(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)487 void p_int_max(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 488 IntVar x0 = s.arg2IntVar(ce[0]); 489 IntVar x1 = s.arg2IntVar(ce[1]); 490 IntVar x2 = s.arg2IntVar(ce[2]); 491 max(s, x0, x1, x2, s.ann2ipl(ann)); 492 } p_int_negate(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)493 void p_int_negate(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 494 IntVar x0 = s.arg2IntVar(ce[0]); 495 IntVar x1 = s.arg2IntVar(ce[1]); 496 rel(s, x0 == -x1, s.ann2ipl(ann)); 497 } 498 499 /* Boolean constraints */ p_bool_CMP(FlatZincSpace & s,IntRelType irt,const ConExpr & ce,AST::Node * ann)500 void p_bool_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, 501 AST::Node* ann) { 502 rel(s, s.arg2BoolVar(ce[0]), irt, s.arg2BoolVar(ce[1]), 503 s.ann2ipl(ann)); 504 } p_bool_CMP_reif(FlatZincSpace & s,IntRelType irt,ReifyMode rm,const ConExpr & ce,AST::Node * ann)505 void p_bool_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm, 506 const ConExpr& ce, AST::Node* ann) { 507 rel(s, s.arg2BoolVar(ce[0]), irt, s.arg2BoolVar(ce[1]), 508 Reify(s.arg2BoolVar(ce[2]), rm), s.ann2ipl(ann)); 509 } p_bool_eq(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)510 void p_bool_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 511 p_bool_CMP(s, IRT_EQ, ce, ann); 512 } p_bool_eq_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)513 void p_bool_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 514 p_bool_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann); 515 } p_bool_eq_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)516 void p_bool_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 517 p_bool_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann); 518 } p_bool_ne(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)519 void p_bool_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 520 p_bool_CMP(s, IRT_NQ, ce, ann); 521 } p_bool_ne_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)522 void p_bool_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 523 p_bool_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann); 524 } p_bool_ne_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)525 void p_bool_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 526 p_bool_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann); 527 } p_bool_ge(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)528 void p_bool_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 529 p_bool_CMP(s, IRT_GQ, ce, ann); 530 } p_bool_ge_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)531 void p_bool_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 532 p_bool_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann); 533 } p_bool_ge_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)534 void p_bool_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 535 p_bool_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann); 536 } p_bool_le(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)537 void p_bool_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 538 p_bool_CMP(s, IRT_LQ, ce, ann); 539 } p_bool_le_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)540 void p_bool_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 541 p_bool_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann); 542 } p_bool_le_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)543 void p_bool_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 544 p_bool_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann); 545 } p_bool_gt(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)546 void p_bool_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 547 p_bool_CMP(s, IRT_GR, ce, ann); 548 } p_bool_gt_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)549 void p_bool_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 550 p_bool_CMP_reif(s, IRT_GR, RM_EQV, ce, ann); 551 } p_bool_gt_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)552 void p_bool_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 553 p_bool_CMP_reif(s, IRT_GR, RM_IMP, ce, ann); 554 } p_bool_lt(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)555 void p_bool_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 556 p_bool_CMP(s, IRT_LE, ce, ann); 557 } p_bool_lt_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)558 void p_bool_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 559 p_bool_CMP_reif(s, IRT_LE, RM_EQV, ce, ann); 560 } p_bool_lt_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)561 void p_bool_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 562 p_bool_CMP_reif(s, IRT_LE, RM_IMP, ce, ann); 563 } 564 565 #define BOOL_OP(op) \ 566 BoolVar b0 = s.arg2BoolVar(ce[0]); \ 567 BoolVar b1 = s.arg2BoolVar(ce[1]); \ 568 if (ce[2]->isBool()) { \ 569 rel(s, b0, op, b1, ce[2]->getBool(), s.ann2ipl(ann)); \ 570 } else { \ 571 rel(s, b0, op, b1, s.bv[ce[2]->getBoolVar()], s.ann2ipl(ann)); \ 572 } 573 574 #define BOOL_ARRAY_OP(op) \ 575 BoolVarArgs bv = s.arg2boolvarargs(ce[0]); \ 576 if (ce.size()==1) { \ 577 rel(s, op, bv, 1, s.ann2ipl(ann)); \ 578 } else if (ce[1]->isBool()) { \ 579 rel(s, op, bv, ce[1]->getBool(), s.ann2ipl(ann)); \ 580 } else { \ 581 rel(s, op, bv, s.bv[ce[1]->getBoolVar()], s.ann2ipl(ann)); \ 582 } 583 p_bool_or(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)584 void p_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 585 BOOL_OP(BOT_OR); 586 } p_bool_or_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)587 void p_bool_or_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 588 BoolVar b0 = s.arg2BoolVar(ce[0]); 589 BoolVar b1 = s.arg2BoolVar(ce[1]); 590 BoolVar b2 = s.arg2BoolVar(ce[2]); 591 clause(s, BOT_OR, BoolVarArgs()<<b0<<b1, BoolVarArgs()<<b2, 1, 592 s.ann2ipl(ann)); 593 } p_bool_and(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)594 void p_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 595 BOOL_OP(BOT_AND); 596 } p_bool_and_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)597 void p_bool_and_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 598 BoolVar b0 = s.arg2BoolVar(ce[0]); 599 BoolVar b1 = s.arg2BoolVar(ce[1]); 600 BoolVar b2 = s.arg2BoolVar(ce[2]); 601 rel(s, b2, BOT_IMP, b0, 1, s.ann2ipl(ann)); 602 rel(s, b2, BOT_IMP, b1, 1, s.ann2ipl(ann)); 603 } p_array_bool_and(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)604 void p_array_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 605 { 606 BOOL_ARRAY_OP(BOT_AND); 607 } p_array_bool_and_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)608 void p_array_bool_and_imp(FlatZincSpace& s, const ConExpr& ce, 609 AST::Node* ann) 610 { 611 BoolVarArgs bv = s.arg2boolvarargs(ce[0]); 612 BoolVar b1 = s.arg2BoolVar(ce[1]); 613 for (unsigned int i=bv.size(); i--;) 614 rel(s, b1, BOT_IMP, bv[i], 1, s.ann2ipl(ann)); 615 } p_array_bool_or(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)616 void p_array_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 617 { 618 BOOL_ARRAY_OP(BOT_OR); 619 } p_array_bool_or_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)620 void p_array_bool_or_imp(FlatZincSpace& s, const ConExpr& ce, 621 AST::Node* ann) 622 { 623 BoolVarArgs bv = s.arg2boolvarargs(ce[0]); 624 BoolVar b1 = s.arg2BoolVar(ce[1]); 625 clause(s, BOT_OR, bv, BoolVarArgs()<<b1, 1, s.ann2ipl(ann)); 626 } p_array_bool_xor(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)627 void p_array_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 628 { 629 BOOL_ARRAY_OP(BOT_XOR); 630 } p_array_bool_xor_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)631 void p_array_bool_xor_imp(FlatZincSpace& s, const ConExpr& ce, 632 AST::Node* ann) 633 { 634 BoolVarArgs bv = s.arg2boolvarargs(ce[0]); 635 BoolVar tmp(s,0,1); 636 rel(s, BOT_XOR, bv, tmp, s.ann2ipl(ann)); 637 rel(s, s.arg2BoolVar(ce[1]), BOT_IMP, tmp, 1); 638 } p_array_bool_clause(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)639 void p_array_bool_clause(FlatZincSpace& s, const ConExpr& ce, 640 AST::Node* ann) { 641 BoolVarArgs bvp = s.arg2boolvarargs(ce[0]); 642 BoolVarArgs bvn = s.arg2boolvarargs(ce[1]); 643 clause(s, BOT_OR, bvp, bvn, 1, s.ann2ipl(ann)); 644 } p_array_bool_clause_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)645 void p_array_bool_clause_reif(FlatZincSpace& s, const ConExpr& ce, 646 AST::Node* ann) { 647 BoolVarArgs bvp = s.arg2boolvarargs(ce[0]); 648 BoolVarArgs bvn = s.arg2boolvarargs(ce[1]); 649 BoolVar b0 = s.arg2BoolVar(ce[2]); 650 clause(s, BOT_OR, bvp, bvn, b0, s.ann2ipl(ann)); 651 } p_array_bool_clause_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)652 void p_array_bool_clause_imp(FlatZincSpace& s, const ConExpr& ce, 653 AST::Node* ann) { 654 BoolVarArgs bvp = s.arg2boolvarargs(ce[0]); 655 BoolVarArgs bvn = s.arg2boolvarargs(ce[1]); 656 BoolVar b0 = s.arg2BoolVar(ce[2]); 657 clause(s, BOT_OR, bvp, bvn, b0, s.ann2ipl(ann)); 658 } p_bool_xor(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)659 void p_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 660 BOOL_OP(BOT_XOR); 661 } p_bool_xor_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)662 void p_bool_xor_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 663 BoolVar b0 = s.arg2BoolVar(ce[0]); 664 BoolVar b1 = s.arg2BoolVar(ce[1]); 665 BoolVar b2 = s.arg2BoolVar(ce[2]); 666 clause(s, BOT_OR, BoolVarArgs()<<b0<<b1, BoolVarArgs()<<b2, 1, 667 s.ann2ipl(ann)); 668 clause(s, BOT_OR, BoolVarArgs(), BoolVarArgs()<<b0<<b1<<b2, 1, 669 s.ann2ipl(ann)); 670 } p_bool_l_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)671 void p_bool_l_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 672 BoolVar b0 = s.arg2BoolVar(ce[0]); 673 BoolVar b1 = s.arg2BoolVar(ce[1]); 674 if (ce[2]->isBool()) { 675 rel(s, b1, BOT_IMP, b0, ce[2]->getBool(), s.ann2ipl(ann)); 676 } else { 677 rel(s, b1, BOT_IMP, b0, s.bv[ce[2]->getBoolVar()], s.ann2ipl(ann)); 678 } 679 } p_bool_r_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)680 void p_bool_r_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 681 BOOL_OP(BOT_IMP); 682 } p_bool_not(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)683 void p_bool_not(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 684 BoolVar x0 = s.arg2BoolVar(ce[0]); 685 BoolVar x1 = s.arg2BoolVar(ce[1]); 686 rel(s, x0, BOT_XOR, x1, 1, s.ann2ipl(ann)); 687 } 688 689 /* element constraints */ p_array_int_element(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)690 void p_array_int_element(FlatZincSpace& s, const ConExpr& ce, 691 AST::Node* ann) { 692 bool isConstant = true; 693 AST::Array* a = ce[1]->getArray(); 694 for (int i=a->a.size(); i--;) { 695 if (!a->a[i]->isInt()) { 696 isConstant = false; 697 break; 698 } 699 } 700 IntVar selector = s.arg2IntVar(ce[0]); 701 rel(s, selector > 0); 702 if (isConstant) { 703 IntSharedArray sia = s.arg2intsharedarray(ce[1]); 704 element(s, sia, selector, -1, s.arg2IntVar(ce[2]), s.ann2ipl(ann)); 705 } else { 706 IntVarArgs iv = s.arg2intvarargs(ce[1]); 707 element(s, iv, selector, -1, s.arg2IntVar(ce[2]), s.ann2ipl(ann)); 708 } 709 } p_array_int_element_offset(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)710 void p_array_int_element_offset(FlatZincSpace& s, const ConExpr& ce, 711 AST::Node* ann) { 712 bool isConstant = true; 713 AST::Array* a = ce[2]->getArray(); 714 for (int i=a->a.size(); i--;) { 715 if (!a->a[i]->isInt()) { 716 isConstant = false; 717 break; 718 } 719 } 720 IntVar selector = s.arg2IntVar(ce[0]); 721 int offset = ce[1]->getInt(); 722 rel(s, selector >= offset); 723 if (isConstant) { 724 IntSharedArray sia = s.arg2intsharedarray(ce[2]); 725 element(s, sia, selector, -offset, s.arg2IntVar(ce[3]), s.ann2ipl(ann)); 726 } else { 727 IntVarArgs iv = s.arg2intvarargs(ce[2]); 728 element(s, iv, selector, -offset, s.arg2IntVar(ce[3]), s.ann2ipl(ann)); 729 } 730 } p_array_int_element2d(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)731 void p_array_int_element2d(FlatZincSpace& s, const ConExpr& ce, 732 AST::Node* ann) { 733 bool isConstant = true; 734 AST::Array* a = ce[2]->getArray(); 735 for (int i=a->a.size(); i--;) { 736 if (!a->a[i]->isInt()) { 737 isConstant = false; 738 break; 739 } 740 } 741 IntVar selector0 = s.arg2IntVar(ce[0]); 742 IntVar selector1 = s.arg2IntVar(ce[1]); 743 IntSet idxset0 = s.arg2intset(ce[3]); 744 IntSet idxset1 = s.arg2intset(ce[4]); 745 746 int w = idxset1.size(); 747 int s1off = idxset1.min(); 748 int h = idxset0.size(); 749 int s0off = idxset0.min(); 750 751 if (isConstant) { 752 IntSharedArray sia = s.arg2intsharedarray(ce[2], 0); 753 element(s, sia, selector1, -s1off, w, selector0, -s0off, h, s.arg2IntVar(ce[5]), s.ann2ipl(ann)); 754 } else { 755 IntVarArgs iv = s.arg2intvarargs(ce[2], 0); 756 element(s, iv, selector1, -s1off, w, selector0, -s0off, h, s.arg2IntVar(ce[5]), s.ann2ipl(ann)); 757 } 758 } p_array_bool_element(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)759 void p_array_bool_element(FlatZincSpace& s, const ConExpr& ce, 760 AST::Node* ann) { 761 bool isConstant = true; 762 AST::Array* a = ce[1]->getArray(); 763 for (int i=a->a.size(); i--;) { 764 if (!a->a[i]->isBool()) { 765 isConstant = false; 766 break; 767 } 768 } 769 IntVar selector = s.arg2IntVar(ce[0]); 770 rel(s, selector > 0); 771 if (isConstant) { 772 IntSharedArray sia = s.arg2boolsharedarray(ce[1], 1); 773 element(s, sia, selector, s.arg2BoolVar(ce[2]), s.ann2ipl(ann)); 774 } else { 775 BoolVarArgs iv = s.arg2boolvarargs(ce[1], 1); 776 element(s, iv, selector, s.arg2BoolVar(ce[2]), s.ann2ipl(ann)); 777 } 778 } p_array_bool_element_offset(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)779 void p_array_bool_element_offset(FlatZincSpace& s, const ConExpr& ce, 780 AST::Node* ann) { 781 bool isConstant = true; 782 AST::Array* a = ce[2]->getArray(); 783 for (int i=a->a.size(); i--;) { 784 if (!a->a[i]->isBool()) { 785 isConstant = false; 786 break; 787 } 788 } 789 IntVar selector = s.arg2IntVar(ce[0]); 790 int offset = ce[1]->getInt(); 791 rel(s, selector >= offset); 792 if (isConstant) { 793 IntSharedArray sia = s.arg2boolsharedarray(ce[2]); 794 element(s, sia, selector, -offset, s.arg2BoolVar(ce[3]), s.ann2ipl(ann)); 795 } else { 796 BoolVarArgs iv = s.arg2boolvarargs(ce[2]); 797 element(s, iv, selector, -offset, s.arg2BoolVar(ce[3]), s.ann2ipl(ann)); 798 } 799 } p_array_bool_element2d(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)800 void p_array_bool_element2d(FlatZincSpace& s, const ConExpr& ce, 801 AST::Node* ann) { 802 bool isConstant = true; 803 AST::Array* a = ce[2]->getArray(); 804 for (int i=a->a.size(); i--;) { 805 if (!a->a[i]->isBool()) { 806 isConstant = false; 807 break; 808 } 809 } 810 IntVar selector0 = s.arg2IntVar(ce[0]); 811 IntVar selector1 = s.arg2IntVar(ce[1]); 812 IntSet idxset0 = s.arg2intset(ce[3]); 813 IntSet idxset1 = s.arg2intset(ce[4]); 814 815 int w = idxset1.size(); 816 int s1off = idxset1.min(); 817 int h = idxset0.size(); 818 int s0off = idxset0.min(); 819 820 if (isConstant) { 821 IntSharedArray sia = s.arg2boolsharedarray(ce[2], 0); 822 element(s, sia, selector1, -s1off, w, selector0, -s0off, h, s.arg2BoolVar(ce[5]), s.ann2ipl(ann)); 823 } else { 824 BoolVarArgs iv = s.arg2boolvarargs(ce[2], 0); 825 element(s, iv, selector1, -s1off, w, selector0, -s0off, h, s.arg2BoolVar(ce[5]), s.ann2ipl(ann)); 826 } 827 } 828 829 /* coercion constraints */ p_bool2int(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)830 void p_bool2int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 831 BoolVar x0 = s.arg2BoolVar(ce[0]); 832 IntVar x1 = s.arg2IntVar(ce[1]); 833 if (ce[0]->isBoolVar() && ce[1]->isIntVar()) { 834 s.aliasBool2Int(ce[1]->getIntVar(), ce[0]->getBoolVar()); 835 } 836 channel(s, x0, x1, s.ann2ipl(ann)); 837 } 838 p_int_in(FlatZincSpace & s,const ConExpr & ce,AST::Node *)839 void p_int_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 840 IntSet d = s.arg2intset(ce[1]); 841 if (ce[0]->isBoolVar()) { 842 IntSetRanges dr(d); 843 Iter::Ranges::Singleton sr(0,1); 844 Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr); 845 IntSet d01(i); 846 if (d01.size() == 0) { 847 s.fail(); 848 } else { 849 rel(s, s.arg2BoolVar(ce[0]), IRT_GQ, d01.min()); 850 rel(s, s.arg2BoolVar(ce[0]), IRT_LQ, d01.max()); 851 } 852 } else { 853 dom(s, s.arg2IntVar(ce[0]), d); 854 } 855 } p_int_in_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node *)856 void p_int_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 857 IntSet d = s.arg2intset(ce[1]); 858 if (ce[0]->isBoolVar()) { 859 IntSetRanges dr(d); 860 Iter::Ranges::Singleton sr(0,1); 861 Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr); 862 IntSet d01(i); 863 if (d01.size() == 0) { 864 rel(s, s.arg2BoolVar(ce[2]) == 0); 865 } else if (d01.max() == 0) { 866 rel(s, s.arg2BoolVar(ce[2]) == !s.arg2BoolVar(ce[0])); 867 } else if (d01.min() == 1) { 868 rel(s, s.arg2BoolVar(ce[2]) == s.arg2BoolVar(ce[0])); 869 } else { 870 rel(s, s.arg2BoolVar(ce[2]) == 1); 871 } 872 } else { 873 dom(s, s.arg2IntVar(ce[0]), d, s.arg2BoolVar(ce[2])); 874 } 875 } p_int_in_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node *)876 void p_int_in_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 877 IntSet d = s.arg2intset(ce[1]); 878 if (ce[0]->isBoolVar()) { 879 IntSetRanges dr(d); 880 Iter::Ranges::Singleton sr(0,1); 881 Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr); 882 IntSet d01(i); 883 if (d01.size() == 0) { 884 rel(s, s.arg2BoolVar(ce[2]) == 0); 885 } else if (d01.max() == 0) { 886 rel(s, s.arg2BoolVar(ce[2]) >> !s.arg2BoolVar(ce[0])); 887 } else if (d01.min() == 1) { 888 rel(s, s.arg2BoolVar(ce[2]) >> s.arg2BoolVar(ce[0])); 889 } 890 } else { 891 dom(s, s.arg2IntVar(ce[0]), d, Reify(s.arg2BoolVar(ce[2]),RM_IMP)); 892 } 893 } 894 895 /* constraints from the standard library */ 896 p_abs(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)897 void p_abs(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 898 IntVar x0 = s.arg2IntVar(ce[0]); 899 IntVar x1 = s.arg2IntVar(ce[1]); 900 abs(s, x0, x1, s.ann2ipl(ann)); 901 } 902 p_array_int_lt(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)903 void p_array_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 904 IntVarArgs iv0 = s.arg2intvarargs(ce[0]); 905 IntVarArgs iv1 = s.arg2intvarargs(ce[1]); 906 rel(s, iv0, IRT_LE, iv1, s.ann2ipl(ann)); 907 } 908 p_array_int_lq(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)909 void p_array_int_lq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 910 IntVarArgs iv0 = s.arg2intvarargs(ce[0]); 911 IntVarArgs iv1 = s.arg2intvarargs(ce[1]); 912 rel(s, iv0, IRT_LQ, iv1, s.ann2ipl(ann)); 913 } 914 p_array_bool_lt(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)915 void p_array_bool_lt(FlatZincSpace& s, const ConExpr& ce, 916 AST::Node* ann) { 917 BoolVarArgs bv0 = s.arg2boolvarargs(ce[0]); 918 BoolVarArgs bv1 = s.arg2boolvarargs(ce[1]); 919 rel(s, bv0, IRT_LE, bv1, s.ann2ipl(ann)); 920 } 921 p_array_bool_lq(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)922 void p_array_bool_lq(FlatZincSpace& s, const ConExpr& ce, 923 AST::Node* ann) { 924 BoolVarArgs bv0 = s.arg2boolvarargs(ce[0]); 925 BoolVarArgs bv1 = s.arg2boolvarargs(ce[1]); 926 rel(s, bv0, IRT_LQ, bv1, s.ann2ipl(ann)); 927 } 928 p_count(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)929 void p_count(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 930 IntVarArgs iv = s.arg2intvarargs(ce[0]); 931 if (!ce[1]->isIntVar()) { 932 if (!ce[2]->isIntVar()) { 933 count(s, iv, ce[1]->getInt(), IRT_EQ, ce[2]->getInt(), 934 s.ann2ipl(ann)); 935 } else { 936 count(s, iv, ce[1]->getInt(), IRT_EQ, s.arg2IntVar(ce[2]), 937 s.ann2ipl(ann)); 938 } 939 } else if (!ce[2]->isIntVar()) { 940 count(s, iv, s.arg2IntVar(ce[1]), IRT_EQ, ce[2]->getInt(), 941 s.ann2ipl(ann)); 942 } else { 943 count(s, iv, s.arg2IntVar(ce[1]), IRT_EQ, s.arg2IntVar(ce[2]), 944 s.ann2ipl(ann)); 945 } 946 } 947 p_count_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)948 void p_count_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 949 IntVarArgs iv = s.arg2intvarargs(ce[0]); 950 IntVar x = s.arg2IntVar(ce[1]); 951 IntVar y = s.arg2IntVar(ce[2]); 952 BoolVar b = s.arg2BoolVar(ce[3]); 953 IntVar c(s,0,Int::Limits::max); 954 count(s,iv,x,IRT_EQ,c,s.ann2ipl(ann)); 955 rel(s, b == (c==y)); 956 } p_count_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)957 void p_count_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 958 IntVarArgs iv = s.arg2intvarargs(ce[0]); 959 IntVar x = s.arg2IntVar(ce[1]); 960 IntVar y = s.arg2IntVar(ce[2]); 961 BoolVar b = s.arg2BoolVar(ce[3]); 962 IntVar c(s,0,Int::Limits::max); 963 count(s,iv,x,IRT_EQ,c,s.ann2ipl(ann)); 964 rel(s, b >> (c==y)); 965 } 966 count_rel(IntRelType irt,FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)967 void count_rel(IntRelType irt, 968 FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 969 IntVarArgs iv = s.arg2intvarargs(ce[1]); 970 count(s, iv, ce[2]->getInt(), irt, ce[0]->getInt(), s.ann2ipl(ann)); 971 } 972 p_at_most(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)973 void p_at_most(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 974 count_rel(IRT_LQ, s, ce, ann); 975 } 976 p_at_least(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)977 void p_at_least(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 978 count_rel(IRT_GQ, s, ce, ann); 979 } 980 p_bin_packing_load(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)981 void p_bin_packing_load(FlatZincSpace& s, const ConExpr& ce, 982 AST::Node* ann) { 983 int minIdx = ce[3]->getInt(); 984 IntVarArgs load = s.arg2intvarargs(ce[0]); 985 IntVarArgs l; 986 IntVarArgs bin = s.arg2intvarargs(ce[1]); 987 for (int i=bin.size(); i--;) 988 rel(s, bin[i] >= minIdx); 989 if (minIdx > 0) { 990 for (int i=minIdx; i--;) 991 l << IntVar(s,0,0); 992 } else if (minIdx < 0) { 993 IntVarArgs bin2(bin.size()); 994 for (int i=bin.size(); i--;) 995 bin2[i] = expr(s, bin[i]-minIdx, s.ann2ipl(ann)); 996 bin = bin2; 997 } 998 l << load; 999 IntArgs sizes = s.arg2intargs(ce[2]); 1000 1001 IntVarArgs allvars = l + bin; 1002 unshare(s, allvars); 1003 binpacking(s, allvars.slice(0,1,l.size()), allvars.slice(l.size(),1,bin.size()), 1004 sizes, s.ann2ipl(ann)); 1005 } 1006 p_global_cardinality(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1007 void p_global_cardinality(FlatZincSpace& s, const ConExpr& ce, 1008 AST::Node* ann) { 1009 IntVarArgs iv0 = s.arg2intvarargs(ce[0]); 1010 IntArgs cover = s.arg2intargs(ce[1]); 1011 IntVarArgs iv1 = s.arg2intvarargs(ce[2]); 1012 1013 Region re; 1014 IntSet cover_s(cover); 1015 IntSetRanges cover_r(cover_s); 1016 IntVarRanges* iv0_ri = re.alloc<IntVarRanges>(iv0.size()); 1017 for (int i=iv0.size(); i--;) 1018 iv0_ri[i] = IntVarRanges(iv0[i]); 1019 Iter::Ranges::NaryUnion iv0_r(re,iv0_ri,iv0.size()); 1020 Iter::Ranges::Diff<Iter::Ranges::NaryUnion,IntSetRanges> 1021 extra_r(iv0_r,cover_r); 1022 Iter::Ranges::ToValues<Iter::Ranges::Diff< 1023 Iter::Ranges::NaryUnion,IntSetRanges> > extra(extra_r); 1024 for (; extra(); ++extra) { 1025 cover << extra.val(); 1026 iv1 << IntVar(s,0,iv0.size()); 1027 } 1028 IntPropLevel ipl = s.ann2ipl(ann); 1029 if (ipl==IPL_DEF) 1030 ipl=IPL_BND; 1031 if (ipl==IPL_DOM) { 1032 IntVarArgs allvars = iv0+iv1; 1033 unshare(s, allvars); 1034 count(s, allvars.slice(0,1,iv0.size()), 1035 allvars.slice(iv0.size(),1,iv1.size()), 1036 cover, ipl); 1037 } else { 1038 unshare(s, iv0); 1039 count(s, iv0, iv1, cover, ipl); 1040 } 1041 } 1042 p_global_cardinality_closed(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1043 void p_global_cardinality_closed(FlatZincSpace& s, const ConExpr& ce, 1044 AST::Node* ann) { 1045 IntVarArgs iv0 = s.arg2intvarargs(ce[0]); 1046 IntArgs cover = s.arg2intargs(ce[1]); 1047 IntVarArgs iv1 = s.arg2intvarargs(ce[2]); 1048 IntPropLevel ipl = s.ann2ipl(ann); 1049 if (ipl==IPL_DEF) 1050 ipl=IPL_BND; 1051 if (ipl==IPL_DOM) { 1052 IntVarArgs allvars = iv0+iv1; 1053 unshare(s, allvars); 1054 count(s, allvars.slice(0,1,iv0.size()), 1055 allvars.slice(iv0.size(),1,iv1.size()), 1056 cover, ipl); 1057 } else { 1058 unshare(s, iv0); 1059 count(s, iv0, iv1, cover, ipl); 1060 } 1061 } 1062 p_global_cardinality_low_up(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1063 void p_global_cardinality_low_up(FlatZincSpace& s, const ConExpr& ce, 1064 AST::Node* ann) { 1065 IntVarArgs x = s.arg2intvarargs(ce[0]); 1066 IntArgs cover = s.arg2intargs(ce[1]); 1067 1068 IntArgs lbound = s.arg2intargs(ce[2]); 1069 IntArgs ubound = s.arg2intargs(ce[3]); 1070 IntSetArgs y(cover.size()); 1071 for (int i=cover.size(); i--;) 1072 y[i] = IntSet(lbound[i],ubound[i]); 1073 1074 IntSet cover_s(cover); 1075 Region re; 1076 IntVarRanges* xrs = re.alloc<IntVarRanges>(x.size()); 1077 for (int i=x.size(); i--;) 1078 xrs[i].init(x[i]); 1079 Iter::Ranges::NaryUnion u(re, xrs, x.size()); 1080 Iter::Ranges::ToValues<Iter::Ranges::NaryUnion> uv(u); 1081 for (; uv(); ++uv) { 1082 if (!cover_s.in(uv.val())) { 1083 cover << uv.val(); 1084 y << IntSet(0,x.size()); 1085 } 1086 } 1087 unshare(s, x); 1088 IntPropLevel ipl = s.ann2ipl(ann); 1089 if (ipl==IPL_DEF) 1090 ipl=IPL_BND; 1091 count(s, x, y, cover, ipl); 1092 } 1093 p_global_cardinality_low_up_closed(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1094 void p_global_cardinality_low_up_closed(FlatZincSpace& s, 1095 const ConExpr& ce, 1096 AST::Node* ann) { 1097 IntVarArgs x = s.arg2intvarargs(ce[0]); 1098 IntArgs cover = s.arg2intargs(ce[1]); 1099 1100 IntArgs lbound = s.arg2intargs(ce[2]); 1101 IntArgs ubound = s.arg2intargs(ce[3]); 1102 IntSetArgs y(cover.size()); 1103 for (int i=cover.size(); i--;) 1104 y[i] = IntSet(lbound[i],ubound[i]); 1105 unshare(s, x); 1106 IntPropLevel ipl = s.ann2ipl(ann); 1107 if (ipl==IPL_DEF) 1108 ipl=IPL_BND; 1109 count(s, x, y, cover, ipl); 1110 } 1111 p_minimum(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1112 void p_minimum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1113 IntVarArgs iv = s.arg2intvarargs(ce[1]); 1114 min(s, iv, s.arg2IntVar(ce[0]), s.ann2ipl(ann)); 1115 } 1116 p_maximum(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1117 void p_maximum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1118 IntVarArgs iv = s.arg2intvarargs(ce[1]); 1119 max(s, iv, s.arg2IntVar(ce[0]), s.ann2ipl(ann)); 1120 } 1121 p_minimum_arg(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1122 void p_minimum_arg(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1123 IntVarArgs iv = s.arg2intvarargs(ce[0]); 1124 int offset = ce[1]->getInt(); 1125 argmin(s, iv, offset, s.arg2IntVar(ce[2]), true, s.ann2ipl(ann)); 1126 } 1127 p_maximum_arg(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1128 void p_maximum_arg(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1129 IntVarArgs iv = s.arg2intvarargs(ce[0]); 1130 int offset = ce[1]->getInt(); 1131 argmax(s, iv, offset, s.arg2IntVar(ce[2]), true, s.ann2ipl(ann)); 1132 } 1133 p_minimum_arg_bool(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1134 void p_minimum_arg_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1135 BoolVarArgs bv = s.arg2boolvarargs(ce[0]); 1136 int offset = ce[1]->getInt(); 1137 argmin(s, bv, offset, s.arg2IntVar(ce[2]), true, s.ann2ipl(ann)); 1138 } 1139 p_maximum_arg_bool(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1140 void p_maximum_arg_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1141 BoolVarArgs bv = s.arg2boolvarargs(ce[0]); 1142 int offset = ce[1]->getInt(); 1143 argmax(s, bv, offset, s.arg2IntVar(ce[2]), true, s.ann2ipl(ann)); 1144 } 1145 p_regular(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1146 void p_regular(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1147 IntVarArgs iv = s.arg2intvarargs(ce[0]); 1148 int q = ce[1]->getInt(); 1149 int symbols = ce[2]->getInt(); 1150 IntArgs d = s.arg2intargs(ce[3]); 1151 int q0 = ce[4]->getInt(); 1152 1153 int noOfTrans = 0; 1154 for (int i=1; i<=q; i++) { 1155 for (int j=1; j<=symbols; j++) { 1156 if (d[(i-1)*symbols+(j-1)] > 0) 1157 noOfTrans++; 1158 } 1159 } 1160 1161 Region re; 1162 DFA::Transition* t = re.alloc<DFA::Transition>(noOfTrans+1); 1163 noOfTrans = 0; 1164 for (int i=1; i<=q; i++) { 1165 for (int j=1; j<=symbols; j++) { 1166 if (d[(i-1)*symbols+(j-1)] > 0) { 1167 t[noOfTrans].i_state = i; 1168 t[noOfTrans].symbol = j; 1169 t[noOfTrans].o_state = d[(i-1)*symbols+(j-1)]; 1170 noOfTrans++; 1171 } 1172 } 1173 } 1174 t[noOfTrans].i_state = -1; 1175 1176 // Final states 1177 AST::SetLit* sl = ce[5]->getSet(); 1178 int* f; 1179 if (sl->interval) { 1180 f = static_cast<int*>(heap.ralloc(sizeof(int)*(sl->max-sl->min+2))); 1181 for (int i=sl->min; i<=sl->max; i++) 1182 f[i-sl->min] = i; 1183 f[sl->max-sl->min+1] = -1; 1184 } else { 1185 f = static_cast<int*>(heap.ralloc(sizeof(int)*(sl->s.size()+1))); 1186 for (int j=sl->s.size(); j--; ) 1187 f[j] = sl->s[j]; 1188 f[sl->s.size()] = -1; 1189 } 1190 1191 DFA dfa(q0,t,f); 1192 free(f); 1193 unshare(s, iv); 1194 extensional(s, iv, s.getSharedDFA(dfa), s.ann2ipl(ann)); 1195 } 1196 1197 void p_sort(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1198 p_sort(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1199 IntVarArgs x = s.arg2intvarargs(ce[0]); 1200 IntVarArgs y = s.arg2intvarargs(ce[1]); 1201 IntVarArgs xy(x.size()+y.size()); 1202 for (int i=x.size(); i--;) 1203 xy[i] = x[i]; 1204 for (int i=y.size(); i--;) 1205 xy[i+x.size()] = y[i]; 1206 unshare(s, xy); 1207 for (int i=x.size(); i--;) 1208 x[i] = xy[i]; 1209 for (int i=y.size(); i--;) 1210 y[i] = xy[i+x.size()]; 1211 sorted(s, x, y, s.ann2ipl(ann)); 1212 } 1213 1214 void p_inverse_offsets(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1215 p_inverse_offsets(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1216 IntVarArgs x = s.arg2intvarargs(ce[0]); 1217 unshare(s, x); 1218 int xoff = ce[1]->getInt(); 1219 IntVarArgs y = s.arg2intvarargs(ce[2]); 1220 unshare(s, y); 1221 int yoff = ce[3]->getInt(); 1222 channel(s, x, xoff, y, yoff, s.ann2ipl(ann)); 1223 } 1224 1225 void p_increasing_int(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1226 p_increasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1227 IntVarArgs x = s.arg2intvarargs(ce[0]); 1228 rel(s,x,IRT_LQ,s.ann2ipl(ann)); 1229 } 1230 1231 void p_increasing_bool(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1232 p_increasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1233 BoolVarArgs x = s.arg2boolvarargs(ce[0]); 1234 rel(s,x,IRT_LQ,s.ann2ipl(ann)); 1235 } 1236 1237 void p_decreasing_int(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1238 p_decreasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1239 IntVarArgs x = s.arg2intvarargs(ce[0]); 1240 rel(s,x,IRT_GQ,s.ann2ipl(ann)); 1241 } 1242 1243 void p_decreasing_bool(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1244 p_decreasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1245 BoolVarArgs x = s.arg2boolvarargs(ce[0]); 1246 rel(s,x,IRT_GQ,s.ann2ipl(ann)); 1247 } 1248 1249 void p_table_int(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1250 p_table_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1251 IntVarArgs x = s.arg2intvarargs(ce[0]); 1252 IntArgs tuples = s.arg2intargs(ce[1]); 1253 TupleSet ts = s.arg2tupleset(tuples,x.size()); 1254 extensional(s,x,ts,s.ann2ipl(ann)); 1255 } 1256 1257 void p_table_int_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1258 p_table_int_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1259 IntVarArgs x = s.arg2intvarargs(ce[0]); 1260 IntArgs tuples = s.arg2intargs(ce[1]); 1261 TupleSet ts = s.arg2tupleset(tuples,x.size()); 1262 extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_EQV),s.ann2ipl(ann)); 1263 } 1264 1265 void p_table_int_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1266 p_table_int_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1267 IntVarArgs x = s.arg2intvarargs(ce[0]); 1268 IntArgs tuples = s.arg2intargs(ce[1]); 1269 TupleSet ts = s.arg2tupleset(tuples,x.size()); 1270 extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_IMP),s.ann2ipl(ann)); 1271 } 1272 1273 void p_table_bool(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1274 p_table_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1275 BoolVarArgs x = s.arg2boolvarargs(ce[0]); 1276 IntArgs tuples = s.arg2boolargs(ce[1]); 1277 TupleSet ts = s.arg2tupleset(tuples,x.size()); 1278 extensional(s,x,ts,s.ann2ipl(ann)); 1279 } 1280 1281 void p_table_bool_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1282 p_table_bool_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1283 BoolVarArgs x = s.arg2boolvarargs(ce[0]); 1284 IntArgs tuples = s.arg2boolargs(ce[1]); 1285 TupleSet ts = s.arg2tupleset(tuples,x.size()); 1286 extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_EQV),s.ann2ipl(ann)); 1287 } 1288 1289 void p_table_bool_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1290 p_table_bool_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1291 BoolVarArgs x = s.arg2boolvarargs(ce[0]); 1292 IntArgs tuples = s.arg2boolargs(ce[1]); 1293 TupleSet ts = s.arg2tupleset(tuples,x.size()); 1294 extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_IMP),s.ann2ipl(ann)); 1295 } 1296 p_cumulative_opt(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1297 void p_cumulative_opt(FlatZincSpace& s, const ConExpr& ce, 1298 AST::Node* ann) { 1299 IntVarArgs start = s.arg2intvarargs(ce[0]); 1300 IntArgs duration = s.arg2intargs(ce[1]); 1301 IntArgs height = s.arg2intargs(ce[2]); 1302 BoolVarArgs opt = s.arg2boolvarargs(ce[3]); 1303 int bound = ce[4]->getInt(); 1304 unshare(s,start); 1305 cumulative(s,bound,start,duration,height,opt,s.ann2ipl(ann)); 1306 } 1307 p_cumulatives(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1308 void p_cumulatives(FlatZincSpace& s, const ConExpr& ce, 1309 AST::Node* ann) { 1310 IntVarArgs start = s.arg2intvarargs(ce[0]); 1311 IntVarArgs duration = s.arg2intvarargs(ce[1]); 1312 IntVarArgs height = s.arg2intvarargs(ce[2]); 1313 int n = start.size(); 1314 IntVar bound = s.arg2IntVar(ce[3]); 1315 1316 if (n==0) 1317 return; 1318 1319 if (n == 1) { 1320 rel(s, height[0] <= bound); 1321 return; 1322 } 1323 1324 bool nonzeroDuration = true; 1325 for (int i=0; i<n; i++) { 1326 if (duration[i].min() <= 0) { 1327 nonzeroDuration = false; 1328 break; 1329 } 1330 } 1331 1332 int minHeight = std::min(height[0].min(),height[1].min()); 1333 int minHeight2 = std::max(height[0].min(),height[1].min()); 1334 for (int i=2; i<n; i++) { 1335 if (height[i].min() < minHeight) { 1336 minHeight2 = minHeight; 1337 minHeight = height[i].min(); 1338 } else if (height[i].min() < minHeight2) { 1339 minHeight2 = height[i].min(); 1340 } 1341 } 1342 bool disjunctive = nonzeroDuration && ( 1343 (minHeight > bound.max()/2) || 1344 (minHeight2 > bound.max()/2 && minHeight+minHeight2>bound.max())); 1345 if (disjunctive) { 1346 rel(s, bound >= max(height)); 1347 // Unary 1348 if (duration.assigned()) { 1349 IntArgs durationI(n); 1350 for (int i=n; i--;) 1351 durationI[i] = duration[i].val(); 1352 unshare(s,start); 1353 unary(s,start,durationI); 1354 } else { 1355 IntVarArgs end(n); 1356 for (int i=n; i--;) 1357 end[i] = expr(s,start[i]+duration[i]); 1358 unshare(s,start); 1359 unary(s,start,duration,end); 1360 } 1361 } else if (nonzeroDuration && height.assigned()) { 1362 IntArgs heightI(n); 1363 for (int i=n; i--;) 1364 heightI[i] = height[i].val(); 1365 if (duration.assigned()) { 1366 IntArgs durationI(n); 1367 for (int i=n; i--;) 1368 durationI[i] = duration[i].val(); 1369 cumulative(s, bound, start, durationI, heightI); 1370 } else { 1371 IntVarArgs end(n); 1372 for (int i = n; i--; ) 1373 end[i] = expr(s,start[i]+duration[i]); 1374 cumulative(s, bound, start, duration, end, heightI); 1375 } 1376 } else if (nonzeroDuration && bound.assigned()) { 1377 IntArgs machine = IntArgs::create(n,0,0); 1378 IntArgs limit({bound.val()}); 1379 IntVarArgs end(n); 1380 for (int i=n; i--;) 1381 end[i] = expr(s,start[i]+duration[i]); 1382 cumulatives(s, machine, start, duration, end, height, limit, true, 1383 s.ann2ipl(ann)); 1384 } else { 1385 int min = Gecode::Int::Limits::max; 1386 int max = Gecode::Int::Limits::min; 1387 IntVarArgs end(start.size()); 1388 for (int i = start.size(); i--; ) { 1389 min = std::min(min, start[i].min()); 1390 max = std::max(max, start[i].max() + duration[i].max()); 1391 end[i] = expr(s, start[i] + duration[i]); 1392 } 1393 for (int time = min; time < max; ++time) { 1394 IntVarArgs x(start.size()); 1395 for (int i = start.size(); i--; ) { 1396 IntVar overlaps = channel(s, expr(s, (start[i] <= time) && 1397 (time < end[i]))); 1398 x[i] = expr(s, overlaps * height[i]); 1399 } 1400 linear(s, x, IRT_LQ, bound); 1401 } 1402 } 1403 } 1404 p_among_seq_int(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1405 void p_among_seq_int(FlatZincSpace& s, const ConExpr& ce, 1406 AST::Node* ann) { 1407 IntVarArgs x = s.arg2intvarargs(ce[0]); 1408 IntSet S = s.arg2intset(ce[1]); 1409 int q = ce[2]->getInt(); 1410 int l = ce[3]->getInt(); 1411 int u = ce[4]->getInt(); 1412 unshare(s, x); 1413 sequence(s, x, S, q, l, u, s.ann2ipl(ann)); 1414 } 1415 p_among_seq_bool(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1416 void p_among_seq_bool(FlatZincSpace& s, const ConExpr& ce, 1417 AST::Node* ann) { 1418 BoolVarArgs x = s.arg2boolvarargs(ce[0]); 1419 bool val = ce[1]->getBool(); 1420 int q = ce[2]->getInt(); 1421 int l = ce[3]->getInt(); 1422 int u = ce[4]->getInt(); 1423 IntSet S(val, val); 1424 unshare(s, x); 1425 sequence(s, x, S, q, l, u, s.ann2ipl(ann)); 1426 } 1427 p_schedule_unary(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1428 void p_schedule_unary(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 1429 IntVarArgs x = s.arg2intvarargs(ce[0]); 1430 IntArgs p = s.arg2intargs(ce[1]); 1431 unshare(s,x); 1432 unary(s, x, p); 1433 } 1434 p_schedule_unary_optional(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1435 void p_schedule_unary_optional(FlatZincSpace& s, const ConExpr& ce, 1436 AST::Node*) { 1437 IntVarArgs x = s.arg2intvarargs(ce[0]); 1438 IntArgs p = s.arg2intargs(ce[1]); 1439 BoolVarArgs m = s.arg2boolvarargs(ce[2]); 1440 unshare(s,x); 1441 unary(s, x, p, m); 1442 } 1443 p_circuit(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1444 void p_circuit(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 1445 int off = ce[0]->getInt(); 1446 IntVarArgs xv = s.arg2intvarargs(ce[1]); 1447 unshare(s,xv); 1448 circuit(s,off,xv,s.ann2ipl(ann)); 1449 } p_circuit_cost_array(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1450 void p_circuit_cost_array(FlatZincSpace& s, const ConExpr& ce, 1451 AST::Node *ann) { 1452 IntArgs c = s.arg2intargs(ce[0]); 1453 IntVarArgs xv = s.arg2intvarargs(ce[1]); 1454 IntVarArgs yv = s.arg2intvarargs(ce[2]); 1455 IntVar z = s.arg2IntVar(ce[3]); 1456 unshare(s,xv); 1457 circuit(s,c,xv,yv,z,s.ann2ipl(ann)); 1458 } p_circuit_cost(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1459 void p_circuit_cost(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 1460 IntArgs c = s.arg2intargs(ce[0]); 1461 IntVarArgs xv = s.arg2intvarargs(ce[1]); 1462 IntVar z = s.arg2IntVar(ce[2]); 1463 unshare(s,xv); 1464 circuit(s,c,xv,z,s.ann2ipl(ann)); 1465 } 1466 p_nooverlap(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1467 void p_nooverlap(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 1468 IntVarArgs x0 = s.arg2intvarargs(ce[0]); 1469 IntVarArgs w = s.arg2intvarargs(ce[1]); 1470 IntVarArgs y0 = s.arg2intvarargs(ce[2]); 1471 IntVarArgs h = s.arg2intvarargs(ce[3]); 1472 if (w.assigned() && h.assigned()) { 1473 IntArgs iw(w.size()); 1474 for (int i=w.size(); i--;) 1475 iw[i] = w[i].val(); 1476 IntArgs ih(h.size()); 1477 for (int i=h.size(); i--;) 1478 ih[i] = h[i].val(); 1479 nooverlap(s,x0,iw,y0,ih,s.ann2ipl(ann)); 1480 1481 int miny = y0[0].min(); 1482 int maxy = y0[0].max(); 1483 int maxdy = ih[0]; 1484 for (int i=1; i<y0.size(); i++) { 1485 miny = std::min(miny,y0[i].min()); 1486 maxy = std::max(maxy,y0[i].max()); 1487 maxdy = std::max(maxdy,ih[i]); 1488 } 1489 int minx = x0[0].min(); 1490 int maxx = x0[0].max(); 1491 int maxdx = iw[0]; 1492 for (int i=1; i<x0.size(); i++) { 1493 minx = std::min(minx,x0[i].min()); 1494 maxx = std::max(maxx,x0[i].max()); 1495 maxdx = std::max(maxdx,iw[i]); 1496 } 1497 if (miny > Int::Limits::min && maxy < Int::Limits::max) { 1498 cumulative(s,maxdy+maxy-miny,x0,iw,ih); 1499 cumulative(s,maxdx+maxx-minx,y0,ih,iw); 1500 } 1501 } else { 1502 IntVarArgs x1(x0.size()), y1(y0.size()); 1503 for (int i=x0.size(); i--; ) 1504 x1[i] = expr(s, x0[i] + w[i]); 1505 for (int i=y0.size(); i--; ) 1506 y1[i] = expr(s, y0[i] + h[i]); 1507 nooverlap(s,x0,w,x1,y0,h,y1,s.ann2ipl(ann)); 1508 } 1509 } 1510 p_precede(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1511 void p_precede(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1512 IntVarArgs x = s.arg2intvarargs(ce[0]); 1513 int p_s = ce[1]->getInt(); 1514 int p_t = ce[2]->getInt(); 1515 precede(s,x,p_s,p_t,s.ann2ipl(ann)); 1516 } 1517 p_nvalue(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1518 void p_nvalue(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1519 IntVarArgs x = s.arg2intvarargs(ce[1]); 1520 if (ce[0]->isIntVar()) { 1521 IntVar y = s.arg2IntVar(ce[0]); 1522 nvalues(s,x,IRT_EQ,y,s.ann2ipl(ann)); 1523 } else { 1524 nvalues(s,x,IRT_EQ,ce[0]->getInt(),s.ann2ipl(ann)); 1525 } 1526 } 1527 p_among(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1528 void p_among(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1529 IntVarArgs x = s.arg2intvarargs(ce[1]); 1530 IntSet v = s.arg2intset(ce[2]); 1531 if (ce[0]->isIntVar()) { 1532 IntVar n = s.arg2IntVar(ce[0]); 1533 unshare(s, x); 1534 count(s,x,v,IRT_EQ,n,s.ann2ipl(ann)); 1535 } else { 1536 unshare(s, x); 1537 count(s,x,v,IRT_EQ,ce[0]->getInt(),s.ann2ipl(ann)); 1538 } 1539 } 1540 p_member_int(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1541 void p_member_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1542 IntVarArgs x = s.arg2intvarargs(ce[0]); 1543 IntVar y = s.arg2IntVar(ce[1]); 1544 member(s,x,y,s.ann2ipl(ann)); 1545 } p_member_int_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1546 void p_member_int_reif(FlatZincSpace& s, const ConExpr& ce, 1547 AST::Node* ann) { 1548 IntVarArgs x = s.arg2intvarargs(ce[0]); 1549 IntVar y = s.arg2IntVar(ce[1]); 1550 BoolVar b = s.arg2BoolVar(ce[2]); 1551 member(s,x,y,b,s.ann2ipl(ann)); 1552 } p_member_bool(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1553 void p_member_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1554 BoolVarArgs x = s.arg2boolvarargs(ce[0]); 1555 BoolVar y = s.arg2BoolVar(ce[1]); 1556 member(s,x,y,s.ann2ipl(ann)); 1557 } p_member_bool_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1558 void p_member_bool_reif(FlatZincSpace& s, const ConExpr& ce, 1559 AST::Node* ann) { 1560 BoolVarArgs x = s.arg2boolvarargs(ce[0]); 1561 BoolVar y = s.arg2BoolVar(ce[1]); 1562 member(s,x,y,s.arg2BoolVar(ce[2]),s.ann2ipl(ann)); 1563 } 1564 1565 class IntPoster { 1566 public: IntPoster(void)1567 IntPoster(void) { 1568 registry().add("all_different_int", &p_distinct); 1569 registry().add("all_different_offset", &p_distinctOffset); 1570 registry().add("all_equal_int", &p_all_equal); 1571 registry().add("int_eq", &p_int_eq); 1572 registry().add("int_ne", &p_int_ne); 1573 registry().add("int_ge", &p_int_ge); 1574 registry().add("int_gt", &p_int_gt); 1575 registry().add("int_le", &p_int_le); 1576 registry().add("int_lt", &p_int_lt); 1577 registry().add("int_eq_reif", &p_int_eq_reif); 1578 registry().add("int_ne_reif", &p_int_ne_reif); 1579 registry().add("int_ge_reif", &p_int_ge_reif); 1580 registry().add("int_gt_reif", &p_int_gt_reif); 1581 registry().add("int_le_reif", &p_int_le_reif); 1582 registry().add("int_lt_reif", &p_int_lt_reif); 1583 registry().add("int_eq_imp", &p_int_eq_imp); 1584 registry().add("int_ne_imp", &p_int_ne_imp); 1585 registry().add("int_ge_imp", &p_int_ge_imp); 1586 registry().add("int_gt_imp", &p_int_gt_imp); 1587 registry().add("int_le_imp", &p_int_le_imp); 1588 registry().add("int_lt_imp", &p_int_lt_imp); 1589 registry().add("int_lin_eq", &p_int_lin_eq); 1590 registry().add("int_lin_eq_reif", &p_int_lin_eq_reif); 1591 registry().add("int_lin_eq_imp", &p_int_lin_eq_imp); 1592 registry().add("int_lin_ne", &p_int_lin_ne); 1593 registry().add("int_lin_ne_reif", &p_int_lin_ne_reif); 1594 registry().add("int_lin_ne_imp", &p_int_lin_ne_imp); 1595 registry().add("int_lin_le", &p_int_lin_le); 1596 registry().add("int_lin_le_reif", &p_int_lin_le_reif); 1597 registry().add("int_lin_le_imp", &p_int_lin_le_imp); 1598 registry().add("int_lin_lt", &p_int_lin_lt); 1599 registry().add("int_lin_lt_reif", &p_int_lin_lt_reif); 1600 registry().add("int_lin_lt_imp", &p_int_lin_lt_imp); 1601 registry().add("int_lin_ge", &p_int_lin_ge); 1602 registry().add("int_lin_ge_reif", &p_int_lin_ge_reif); 1603 registry().add("int_lin_ge_imp", &p_int_lin_ge_imp); 1604 registry().add("int_lin_gt", &p_int_lin_gt); 1605 registry().add("int_lin_gt_reif", &p_int_lin_gt_reif); 1606 registry().add("int_lin_gt_imp", &p_int_lin_gt_imp); 1607 registry().add("int_plus", &p_int_plus); 1608 registry().add("int_minus", &p_int_minus); 1609 registry().add("int_times", &p_int_times); 1610 registry().add("gecode_int_pow", &p_int_pow); 1611 registry().add("int_div", &p_int_div); 1612 registry().add("int_mod", &p_int_mod); 1613 registry().add("int_min", &p_int_min); 1614 registry().add("int_max", &p_int_max); 1615 registry().add("int_abs", &p_abs); 1616 registry().add("int_negate", &p_int_negate); 1617 registry().add("bool_eq", &p_bool_eq); 1618 registry().add("bool_eq_reif", &p_bool_eq_reif); 1619 registry().add("bool_eq_imp", &p_bool_eq_imp); 1620 registry().add("bool_ne", &p_bool_ne); 1621 registry().add("bool_ne_reif", &p_bool_ne_reif); 1622 registry().add("bool_ne_imp", &p_bool_ne_imp); 1623 registry().add("bool_ge", &p_bool_ge); 1624 registry().add("bool_ge_reif", &p_bool_ge_reif); 1625 registry().add("bool_ge_imp", &p_bool_ge_imp); 1626 registry().add("bool_le", &p_bool_le); 1627 registry().add("bool_le_reif", &p_bool_le_reif); 1628 registry().add("bool_le_imp", &p_bool_le_imp); 1629 registry().add("bool_gt", &p_bool_gt); 1630 registry().add("bool_gt_reif", &p_bool_gt_reif); 1631 registry().add("bool_gt_imp", &p_bool_gt_imp); 1632 registry().add("bool_lt", &p_bool_lt); 1633 registry().add("bool_lt_reif", &p_bool_lt_reif); 1634 registry().add("bool_lt_imp", &p_bool_lt_imp); 1635 registry().add("bool_or", &p_bool_or); 1636 registry().add("bool_or_imp", &p_bool_or_imp); 1637 registry().add("bool_and", &p_bool_and); 1638 registry().add("bool_and_imp", &p_bool_and_imp); 1639 registry().add("bool_xor", &p_bool_xor); 1640 registry().add("bool_xor_imp", &p_bool_xor_imp); 1641 registry().add("array_bool_and", &p_array_bool_and); 1642 registry().add("array_bool_and_imp", &p_array_bool_and_imp); 1643 registry().add("array_bool_or", &p_array_bool_or); 1644 registry().add("array_bool_or_imp", &p_array_bool_or_imp); 1645 registry().add("array_bool_xor", &p_array_bool_xor); 1646 registry().add("array_bool_xor_imp", &p_array_bool_xor_imp); 1647 registry().add("bool_clause", &p_array_bool_clause); 1648 registry().add("bool_clause_reif", &p_array_bool_clause_reif); 1649 registry().add("bool_clause_imp", &p_array_bool_clause_imp); 1650 registry().add("bool_left_imp", &p_bool_l_imp); 1651 registry().add("bool_right_imp", &p_bool_r_imp); 1652 registry().add("bool_not", &p_bool_not); 1653 registry().add("array_int_element", &p_array_int_element); 1654 registry().add("array_var_int_element", &p_array_int_element); 1655 registry().add("gecode_int_element", &p_array_int_element_offset); 1656 registry().add("gecode_var_int_element", &p_array_int_element_offset); 1657 registry().add("gecode_int_element2d", &p_array_int_element2d); 1658 registry().add("array_bool_element", &p_array_bool_element); 1659 registry().add("array_var_bool_element", &p_array_bool_element); 1660 registry().add("gecode_bool_element", &p_array_bool_element_offset); 1661 registry().add("gecode_var_bool_element", &p_array_bool_element_offset); 1662 registry().add("gecode_bool_element2d", &p_array_bool_element2d); 1663 registry().add("bool2int", &p_bool2int); 1664 registry().add("int_in", &p_int_in); 1665 registry().add("int_in_reif", &p_int_in_reif); 1666 registry().add("int_in_imp", &p_int_in_imp); 1667 #ifndef GECODE_HAS_SET_VARS 1668 registry().add("set_in", &p_int_in); 1669 registry().add("set_in_reif", &p_int_in_reif); 1670 registry().add("set_in_imp", &p_int_in_imp); 1671 #endif 1672 1673 registry().add("array_int_lt", &p_array_int_lt); 1674 registry().add("array_int_lq", &p_array_int_lq); 1675 registry().add("array_bool_lt", &p_array_bool_lt); 1676 registry().add("array_bool_lq", &p_array_bool_lq); 1677 registry().add("count", &p_count); 1678 registry().add("count_reif", &p_count_reif); 1679 registry().add("count_imp", &p_count_imp); 1680 registry().add("count_eq", &p_count); 1681 registry().add("count_eq_reif", &p_count_reif); 1682 registry().add("count_eq_imp", &p_count_imp); 1683 registry().add("at_least_int", &p_at_least); 1684 registry().add("at_most_int", &p_at_most); 1685 registry().add("gecode_bin_packing_load", &p_bin_packing_load); 1686 registry().add("gecode_global_cardinality", &p_global_cardinality); 1687 registry().add("gecode_global_cardinality_closed", 1688 &p_global_cardinality_closed); 1689 registry().add("global_cardinality_low_up", 1690 &p_global_cardinality_low_up); 1691 registry().add("global_cardinality_low_up_closed", 1692 &p_global_cardinality_low_up_closed); 1693 registry().add("array_int_minimum", &p_minimum); 1694 registry().add("array_int_maximum", &p_maximum); 1695 registry().add("gecode_minimum_arg_int_offset", &p_minimum_arg); 1696 registry().add("gecode_maximum_arg_int_offset", &p_maximum_arg); 1697 registry().add("gecode_minimum_arg_bool_offset", &p_minimum_arg_bool); 1698 registry().add("gecode_maximum_arg_bool_offset", &p_maximum_arg_bool); 1699 registry().add("array_int_maximum", &p_maximum); 1700 registry().add("gecode_regular", &p_regular); 1701 registry().add("sort", &p_sort); 1702 registry().add("inverse_offsets", &p_inverse_offsets); 1703 registry().add("increasing_int", &p_increasing_int); 1704 registry().add("increasing_bool", &p_increasing_bool); 1705 registry().add("decreasing_int", &p_decreasing_int); 1706 registry().add("decreasing_bool", &p_decreasing_bool); 1707 registry().add("gecode_table_int", &p_table_int); 1708 registry().add("gecode_table_int_reif", &p_table_int_reif); 1709 registry().add("gecode_table_int_imp", &p_table_int_imp); 1710 registry().add("gecode_table_bool", &p_table_bool); 1711 registry().add("gecode_table_bool_reif", &p_table_bool_reif); 1712 registry().add("gecode_table_bool_imp", &p_table_bool_imp); 1713 registry().add("cumulatives", &p_cumulatives); 1714 registry().add("gecode_among_seq_int", &p_among_seq_int); 1715 registry().add("gecode_among_seq_bool", &p_among_seq_bool); 1716 1717 registry().add("bool_lin_eq", &p_bool_lin_eq); 1718 registry().add("bool_lin_ne", &p_bool_lin_ne); 1719 registry().add("bool_lin_le", &p_bool_lin_le); 1720 registry().add("bool_lin_lt", &p_bool_lin_lt); 1721 registry().add("bool_lin_ge", &p_bool_lin_ge); 1722 registry().add("bool_lin_gt", &p_bool_lin_gt); 1723 1724 registry().add("bool_lin_eq_reif", &p_bool_lin_eq_reif); 1725 registry().add("bool_lin_eq_imp", &p_bool_lin_eq_imp); 1726 registry().add("bool_lin_ne_reif", &p_bool_lin_ne_reif); 1727 registry().add("bool_lin_ne_imp", &p_bool_lin_ne_imp); 1728 registry().add("bool_lin_le_reif", &p_bool_lin_le_reif); 1729 registry().add("bool_lin_le_imp", &p_bool_lin_le_imp); 1730 registry().add("bool_lin_lt_reif", &p_bool_lin_lt_reif); 1731 registry().add("bool_lin_lt_imp", &p_bool_lin_lt_imp); 1732 registry().add("bool_lin_ge_reif", &p_bool_lin_ge_reif); 1733 registry().add("bool_lin_ge_imp", &p_bool_lin_ge_imp); 1734 registry().add("bool_lin_gt_reif", &p_bool_lin_gt_reif); 1735 registry().add("bool_lin_gt_imp", &p_bool_lin_gt_imp); 1736 1737 registry().add("gecode_schedule_unary", &p_schedule_unary); 1738 registry().add("gecode_schedule_unary_optional", &p_schedule_unary_optional); 1739 registry().add("gecode_schedule_cumulative_optional", &p_cumulative_opt); 1740 1741 registry().add("gecode_circuit", &p_circuit); 1742 registry().add("gecode_circuit_cost_array", &p_circuit_cost_array); 1743 registry().add("gecode_circuit_cost", &p_circuit_cost); 1744 registry().add("gecode_nooverlap", &p_nooverlap); 1745 registry().add("gecode_precede", &p_precede); 1746 registry().add("nvalue",&p_nvalue); 1747 registry().add("among",&p_among); 1748 registry().add("member_int",&p_member_int); 1749 registry().add("gecode_member_int_reif",&p_member_int_reif); 1750 registry().add("member_bool",&p_member_bool); 1751 registry().add("gecode_member_bool_reif",&p_member_bool_reif); 1752 } 1753 }; 1754 IntPoster __int_poster; 1755 1756 #ifdef GECODE_HAS_SET_VARS p_set_OP(FlatZincSpace & s,SetOpType op,const ConExpr & ce,AST::Node *)1757 void p_set_OP(FlatZincSpace& s, SetOpType op, 1758 const ConExpr& ce, AST::Node *) { 1759 rel(s, s.arg2SetVar(ce[0]), op, s.arg2SetVar(ce[1]), 1760 SRT_EQ, s.arg2SetVar(ce[2])); 1761 } p_set_union(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1762 void p_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 1763 p_set_OP(s, SOT_UNION, ce, ann); 1764 } p_set_intersect(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1765 void p_set_intersect(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 1766 p_set_OP(s, SOT_INTER, ce, ann); 1767 } p_set_diff(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1768 void p_set_diff(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 1769 p_set_OP(s, SOT_MINUS, ce, ann); 1770 } 1771 p_set_symdiff(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1772 void p_set_symdiff(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 1773 SetVar x = s.arg2SetVar(ce[0]); 1774 SetVar y = s.arg2SetVar(ce[1]); 1775 1776 SetVarLubRanges xub(x); 1777 IntSet xubs(xub); 1778 SetVar x_y(s,IntSet::empty,xubs); 1779 rel(s, x, SOT_MINUS, y, SRT_EQ, x_y); 1780 1781 SetVarLubRanges yub(y); 1782 IntSet yubs(yub); 1783 SetVar y_x(s,IntSet::empty,yubs); 1784 rel(s, y, SOT_MINUS, x, SRT_EQ, y_x); 1785 1786 rel(s, x_y, SOT_UNION, y_x, SRT_EQ, s.arg2SetVar(ce[2])); 1787 } 1788 p_array_set_OP(FlatZincSpace & s,SetOpType op,const ConExpr & ce,AST::Node *)1789 void p_array_set_OP(FlatZincSpace& s, SetOpType op, 1790 const ConExpr& ce, AST::Node *) { 1791 SetVarArgs xs = s.arg2setvarargs(ce[0]); 1792 rel(s, op, xs, s.arg2SetVar(ce[1])); 1793 } p_array_set_union(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1794 void p_array_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 1795 p_array_set_OP(s, SOT_UNION, ce, ann); 1796 } p_array_set_partition(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1797 void p_array_set_partition(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 1798 p_array_set_OP(s, SOT_DUNION, ce, ann); 1799 } 1800 1801 p_set_rel(FlatZincSpace & s,SetRelType srt,const ConExpr & ce)1802 void p_set_rel(FlatZincSpace& s, SetRelType srt, const ConExpr& ce) { 1803 rel(s, s.arg2SetVar(ce[0]), srt, s.arg2SetVar(ce[1])); 1804 } 1805 p_set_eq(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1806 void p_set_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1807 p_set_rel(s, SRT_EQ, ce); 1808 } p_set_ne(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1809 void p_set_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1810 p_set_rel(s, SRT_NQ, ce); 1811 } p_set_subset(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1812 void p_set_subset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1813 p_set_rel(s, SRT_SUB, ce); 1814 } p_set_superset(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1815 void p_set_superset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1816 p_set_rel(s, SRT_SUP, ce); 1817 } p_set_le(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1818 void p_set_le(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1819 p_set_rel(s, SRT_LQ, ce); 1820 } p_set_lt(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1821 void p_set_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1822 p_set_rel(s, SRT_LE, ce); 1823 } p_set_card(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1824 void p_set_card(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1825 if (!ce[1]->isIntVar()) { 1826 cardinality(s, s.arg2SetVar(ce[0]), ce[1]->getInt(), 1827 ce[1]->getInt()); 1828 } else { 1829 cardinality(s, s.arg2SetVar(ce[0]), s.arg2IntVar(ce[1])); 1830 } 1831 } p_set_in(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1832 void p_set_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1833 if (!ce[1]->isSetVar()) { 1834 IntSet d = s.arg2intset(ce[1]); 1835 if (ce[0]->isBoolVar()) { 1836 IntSetRanges dr(d); 1837 Iter::Ranges::Singleton sr(0,1); 1838 Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr); 1839 IntSet d01(i); 1840 if (d01.size() == 0) { 1841 s.fail(); 1842 } else { 1843 rel(s, s.arg2BoolVar(ce[0]), IRT_GQ, d01.min()); 1844 rel(s, s.arg2BoolVar(ce[0]), IRT_LQ, d01.max()); 1845 } 1846 } else { 1847 dom(s, s.arg2IntVar(ce[0]), d); 1848 } 1849 } else { 1850 if (!ce[0]->isIntVar()) { 1851 dom(s, s.arg2SetVar(ce[1]), SRT_SUP, ce[0]->getInt()); 1852 } else { 1853 rel(s, s.arg2SetVar(ce[1]), SRT_SUP, s.arg2IntVar(ce[0])); 1854 } 1855 } 1856 } p_set_rel_reif(FlatZincSpace & s,SetRelType srt,const ConExpr & ce)1857 void p_set_rel_reif(FlatZincSpace& s, SetRelType srt, const ConExpr& ce) { 1858 rel(s, s.arg2SetVar(ce[0]), srt, s.arg2SetVar(ce[1]), 1859 s.arg2BoolVar(ce[2])); 1860 } 1861 p_set_eq_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1862 void p_set_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1863 p_set_rel_reif(s,SRT_EQ,ce); 1864 } p_set_le_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1865 void p_set_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1866 p_set_rel_reif(s,SRT_LQ,ce); 1867 } p_set_lt_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1868 void p_set_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1869 p_set_rel_reif(s,SRT_LE,ce); 1870 } p_set_ne_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1871 void p_set_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1872 p_set_rel_reif(s,SRT_NQ,ce); 1873 } p_set_subset_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1874 void p_set_subset_reif(FlatZincSpace& s, const ConExpr& ce, 1875 AST::Node *) { 1876 p_set_rel_reif(s,SRT_SUB,ce); 1877 } p_set_superset_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1878 void p_set_superset_reif(FlatZincSpace& s, const ConExpr& ce, 1879 AST::Node *) { 1880 p_set_rel_reif(s,SRT_SUP,ce); 1881 } p_set_in_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann,ReifyMode rm)1882 void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann, ReifyMode rm) { 1883 if (!ce[1]->isSetVar()) { 1884 if (rm==RM_EQV) { 1885 p_int_in_reif(s,ce,ann); 1886 } else { 1887 assert(rm==RM_IMP); 1888 p_int_in_imp(s,ce,ann); 1889 } 1890 } else { 1891 if (!ce[0]->isIntVar()) { 1892 dom(s, s.arg2SetVar(ce[1]), SRT_SUP, ce[0]->getInt(), 1893 Reify(s.arg2BoolVar(ce[2]),rm)); 1894 } else { 1895 rel(s, s.arg2SetVar(ce[1]), SRT_SUP, s.arg2IntVar(ce[0]), 1896 Reify(s.arg2BoolVar(ce[2]),rm)); 1897 } 1898 } 1899 } p_set_in_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1900 void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1901 p_set_in_reif(s,ce,ann,RM_EQV); 1902 } p_set_in_imp(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1903 void p_set_in_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 1904 p_set_in_reif(s,ce,ann,RM_IMP); 1905 } p_set_disjoint(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1906 void p_set_disjoint(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1907 rel(s, s.arg2SetVar(ce[0]), SRT_DISJ, s.arg2SetVar(ce[1])); 1908 } 1909 p_link_set_to_booleans(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1910 void p_link_set_to_booleans(FlatZincSpace& s, const ConExpr& ce, 1911 AST::Node *) { 1912 SetVar x = s.arg2SetVar(ce[0]); 1913 int idx = ce[2]->getInt(); 1914 assert(idx >= 0); 1915 rel(s, x || IntSet(Set::Limits::min,idx-1)); 1916 BoolVarArgs y = s.arg2boolvarargs(ce[1],idx); 1917 unshare(s, y); 1918 channel(s, y, x); 1919 } 1920 p_array_set_element(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1921 void p_array_set_element(FlatZincSpace& s, const ConExpr& ce, 1922 AST::Node*) { 1923 bool isConstant = true; 1924 AST::Array* a = ce[1]->getArray(); 1925 for (int i=a->a.size(); i--;) { 1926 if (a->a[i]->isSetVar()) { 1927 isConstant = false; 1928 break; 1929 } 1930 } 1931 IntVar selector = s.arg2IntVar(ce[0]); 1932 rel(s, selector > 0); 1933 if (isConstant) { 1934 IntSetArgs sv = s.arg2intsetargs(ce[1],1); 1935 element(s, sv, selector, s.arg2SetVar(ce[2])); 1936 } else { 1937 SetVarArgs sv = s.arg2setvarargs(ce[1], 1); 1938 element(s, sv, selector, s.arg2SetVar(ce[2])); 1939 } 1940 } 1941 p_array_set_element_op(FlatZincSpace & s,const ConExpr & ce,AST::Node *,SetOpType op,const IntSet & universe=IntSet (Set::Limits::min,Set::Limits::max))1942 void p_array_set_element_op(FlatZincSpace& s, const ConExpr& ce, 1943 AST::Node*, SetOpType op, 1944 const IntSet& universe = 1945 IntSet(Set::Limits::min,Set::Limits::max)) { 1946 bool isConstant = true; 1947 AST::Array* a = ce[1]->getArray(); 1948 for (int i=a->a.size(); i--;) { 1949 if (a->a[i]->isSetVar()) { 1950 isConstant = false; 1951 break; 1952 } 1953 } 1954 SetVar selector = s.arg2SetVar(ce[0]); 1955 dom(s, selector, SRT_DISJ, 0); 1956 if (isConstant) { 1957 IntSetArgs sv = s.arg2intsetargs(ce[1], 1); 1958 element(s, op, sv, selector, s.arg2SetVar(ce[2]), universe); 1959 } else { 1960 SetVarArgs sv = s.arg2setvarargs(ce[1], 1); 1961 element(s, op, sv, selector, s.arg2SetVar(ce[2]), universe); 1962 } 1963 } 1964 p_array_set_element_union(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1965 void p_array_set_element_union(FlatZincSpace& s, const ConExpr& ce, 1966 AST::Node* ann) { 1967 p_array_set_element_op(s, ce, ann, SOT_UNION); 1968 } 1969 p_array_set_element_intersect(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1970 void p_array_set_element_intersect(FlatZincSpace& s, const ConExpr& ce, 1971 AST::Node* ann) { 1972 p_array_set_element_op(s, ce, ann, SOT_INTER); 1973 } 1974 p_array_set_element_intersect_in(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1975 void p_array_set_element_intersect_in(FlatZincSpace& s, 1976 const ConExpr& ce, 1977 AST::Node* ann) { 1978 IntSet d = s.arg2intset(ce[3]); 1979 p_array_set_element_op(s, ce, ann, SOT_INTER, d); 1980 } 1981 p_array_set_element_partition(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)1982 void p_array_set_element_partition(FlatZincSpace& s, const ConExpr& ce, 1983 AST::Node* ann) { 1984 p_array_set_element_op(s, ce, ann, SOT_DUNION); 1985 } 1986 p_set_convex(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1987 void p_set_convex(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1988 convex(s, s.arg2SetVar(ce[0])); 1989 } 1990 p_array_set_seq(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1991 void p_array_set_seq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 1992 SetVarArgs sv = s.arg2setvarargs(ce[0]); 1993 sequence(s, sv); 1994 } 1995 p_array_set_seq_union(FlatZincSpace & s,const ConExpr & ce,AST::Node *)1996 void p_array_set_seq_union(FlatZincSpace& s, const ConExpr& ce, 1997 AST::Node *) { 1998 SetVarArgs sv = s.arg2setvarargs(ce[0]); 1999 sequence(s, sv, s.arg2SetVar(ce[1])); 2000 } 2001 p_int_set_channel(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2002 void p_int_set_channel(FlatZincSpace& s, const ConExpr& ce, 2003 AST::Node *) { 2004 int xoff=ce[1]->getInt(); 2005 assert(xoff >= 0); 2006 int yoff=ce[3]->getInt(); 2007 assert(yoff >= 0); 2008 IntVarArgs xv = s.arg2intvarargs(ce[0], xoff); 2009 SetVarArgs yv = s.arg2setvarargs(ce[2], yoff, 1, IntSet(0, xoff-1)); 2010 IntSet xd(yoff,yv.size()-1); 2011 for (int i=xoff; i<xv.size(); i++) { 2012 dom(s, xv[i], xd); 2013 } 2014 IntSet yd(xoff,xv.size()-1); 2015 for (int i=yoff; i<yv.size(); i++) { 2016 dom(s, yv[i], SRT_SUB, yd); 2017 } 2018 channel(s,xv,yv); 2019 } 2020 p_range(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2021 void p_range(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2022 int xoff=ce[1]->getInt(); 2023 assert(xoff >= 0); 2024 IntVarArgs xv = s.arg2intvarargs(ce[0],xoff); 2025 element(s, SOT_UNION, xv, s.arg2SetVar(ce[2]), s.arg2SetVar(ce[3])); 2026 } 2027 p_weights(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2028 void p_weights(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2029 IntArgs e = s.arg2intargs(ce[0]); 2030 IntArgs w = s.arg2intargs(ce[1]); 2031 SetVar x = s.arg2SetVar(ce[2]); 2032 IntVar y = s.arg2IntVar(ce[3]); 2033 weights(s,e,w,x,y); 2034 } 2035 p_inverse_set(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2036 void p_inverse_set(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2037 int xoff = ce[2]->getInt(); 2038 int yoff = ce[3]->getInt(); 2039 SetVarArgs x = s.arg2setvarargs(ce[0],xoff); 2040 SetVarArgs y = s.arg2setvarargs(ce[1],yoff); 2041 channel(s, x, y); 2042 } 2043 p_precede_set(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2044 void p_precede_set(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2045 SetVarArgs x = s.arg2setvarargs(ce[0]); 2046 int p_s = ce[1]->getInt(); 2047 int p_t = ce[2]->getInt(); 2048 precede(s,x,p_s,p_t); 2049 } 2050 2051 class SetPoster { 2052 public: SetPoster(void)2053 SetPoster(void) { 2054 registry().add("set_eq", &p_set_eq); 2055 registry().add("set_le", &p_set_le); 2056 registry().add("set_lt", &p_set_lt); 2057 registry().add("equal", &p_set_eq); 2058 registry().add("set_ne", &p_set_ne); 2059 registry().add("set_union", &p_set_union); 2060 registry().add("array_set_element", &p_array_set_element); 2061 registry().add("array_var_set_element", &p_array_set_element); 2062 registry().add("set_intersect", &p_set_intersect); 2063 registry().add("set_diff", &p_set_diff); 2064 registry().add("set_symdiff", &p_set_symdiff); 2065 registry().add("set_subset", &p_set_subset); 2066 registry().add("set_superset", &p_set_superset); 2067 registry().add("set_card", &p_set_card); 2068 registry().add("set_in", &p_set_in); 2069 registry().add("set_eq_reif", &p_set_eq_reif); 2070 registry().add("set_le_reif", &p_set_le_reif); 2071 registry().add("set_lt_reif", &p_set_lt_reif); 2072 registry().add("equal_reif", &p_set_eq_reif); 2073 registry().add("set_ne_reif", &p_set_ne_reif); 2074 registry().add("set_subset_reif", &p_set_subset_reif); 2075 registry().add("set_superset_reif", &p_set_superset_reif); 2076 registry().add("set_in_reif", &p_set_in_reif); 2077 registry().add("set_in_imp", &p_set_in_imp); 2078 registry().add("disjoint", &p_set_disjoint); 2079 registry().add("gecode_link_set_to_booleans", 2080 &p_link_set_to_booleans); 2081 2082 registry().add("array_set_union", &p_array_set_union); 2083 registry().add("array_set_partition", &p_array_set_partition); 2084 registry().add("set_convex", &p_set_convex); 2085 registry().add("array_set_seq", &p_array_set_seq); 2086 registry().add("array_set_seq_union", &p_array_set_seq_union); 2087 registry().add("gecode_array_set_element_union", 2088 &p_array_set_element_union); 2089 registry().add("gecode_array_set_element_intersect", 2090 &p_array_set_element_intersect); 2091 registry().add("gecode_array_set_element_intersect_in", 2092 &p_array_set_element_intersect_in); 2093 registry().add("gecode_array_set_element_partition", 2094 &p_array_set_element_partition); 2095 registry().add("gecode_int_set_channel", 2096 &p_int_set_channel); 2097 registry().add("gecode_range", 2098 &p_range); 2099 registry().add("gecode_set_weights", 2100 &p_weights); 2101 registry().add("gecode_inverse_set", &p_inverse_set); 2102 registry().add("gecode_precede_set", &p_precede_set); 2103 } 2104 }; 2105 SetPoster __set_poster; 2106 #endif 2107 2108 #ifdef GECODE_HAS_FLOAT_VARS 2109 p_int2float(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2110 void p_int2float(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2111 IntVar x0 = s.arg2IntVar(ce[0]); 2112 FloatVar x1 = s.arg2FloatVar(ce[1]); 2113 channel(s, x0, x1); 2114 } 2115 p_float_lin_cmp(FlatZincSpace & s,FloatRelType frt,const ConExpr & ce,AST::Node *)2116 void p_float_lin_cmp(FlatZincSpace& s, FloatRelType frt, 2117 const ConExpr& ce, AST::Node*) { 2118 FloatValArgs fa = s.arg2floatargs(ce[0]); 2119 FloatVarArgs fv = s.arg2floatvarargs(ce[1]); 2120 linear(s, fa, fv, frt, ce[2]->getFloat()); 2121 } p_float_lin_cmp_reif(FlatZincSpace & s,FloatRelType frt,const ConExpr & ce,AST::Node *)2122 void p_float_lin_cmp_reif(FlatZincSpace& s, FloatRelType frt, 2123 const ConExpr& ce, AST::Node*) { 2124 FloatValArgs fa = s.arg2floatargs(ce[0]); 2125 FloatVarArgs fv = s.arg2floatvarargs(ce[1]); 2126 linear(s, fa, fv, frt, ce[2]->getFloat(), s.arg2BoolVar(ce[3])); 2127 } p_float_lin_eq(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)2128 void p_float_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 2129 p_float_lin_cmp(s,FRT_EQ,ce,ann); 2130 } p_float_lin_eq_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)2131 void p_float_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, 2132 AST::Node* ann) { 2133 p_float_lin_cmp_reif(s,FRT_EQ,ce,ann); 2134 } p_float_lin_le(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)2135 void p_float_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 2136 p_float_lin_cmp(s,FRT_LQ,ce,ann); 2137 } p_float_lin_lt(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)2138 void p_float_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 2139 p_float_lin_cmp(s,FRT_LE,ce,ann); 2140 } p_float_lin_le_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)2141 void p_float_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, 2142 AST::Node* ann) { 2143 p_float_lin_cmp_reif(s,FRT_LQ,ce,ann); 2144 } p_float_lin_lt_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node * ann)2145 void p_float_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, 2146 AST::Node* ann) { 2147 p_float_lin_cmp_reif(s,FRT_LE,ce,ann); 2148 } 2149 p_float_times(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2150 void p_float_times(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2151 FloatVar x = s.arg2FloatVar(ce[0]); 2152 FloatVar y = s.arg2FloatVar(ce[1]); 2153 FloatVar z = s.arg2FloatVar(ce[2]); 2154 mult(s,x,y,z); 2155 } 2156 p_float_div(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2157 void p_float_div(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2158 FloatVar x = s.arg2FloatVar(ce[0]); 2159 FloatVar y = s.arg2FloatVar(ce[1]); 2160 FloatVar z = s.arg2FloatVar(ce[2]); 2161 div(s,x,y,z); 2162 } 2163 p_float_plus(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2164 void p_float_plus(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2165 FloatVar x = s.arg2FloatVar(ce[0]); 2166 FloatVar y = s.arg2FloatVar(ce[1]); 2167 FloatVar z = s.arg2FloatVar(ce[2]); 2168 rel(s,x+y==z); 2169 } 2170 p_float_sqrt(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2171 void p_float_sqrt(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2172 FloatVar x = s.arg2FloatVar(ce[0]); 2173 FloatVar y = s.arg2FloatVar(ce[1]); 2174 sqrt(s,x,y); 2175 } 2176 p_float_abs(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2177 void p_float_abs(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2178 FloatVar x = s.arg2FloatVar(ce[0]); 2179 FloatVar y = s.arg2FloatVar(ce[1]); 2180 abs(s,x,y); 2181 } 2182 p_float_eq(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2183 void p_float_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2184 FloatVar x = s.arg2FloatVar(ce[0]); 2185 FloatVar y = s.arg2FloatVar(ce[1]); 2186 rel(s,x,FRT_EQ,y); 2187 } p_float_eq_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2188 void p_float_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2189 FloatVar x = s.arg2FloatVar(ce[0]); 2190 FloatVar y = s.arg2FloatVar(ce[1]); 2191 BoolVar b = s.arg2BoolVar(ce[2]); 2192 rel(s,x,FRT_EQ,y,b); 2193 } p_float_le(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2194 void p_float_le(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2195 FloatVar x = s.arg2FloatVar(ce[0]); 2196 FloatVar y = s.arg2FloatVar(ce[1]); 2197 rel(s,x,FRT_LQ,y); 2198 } p_float_le_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2199 void p_float_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2200 FloatVar x = s.arg2FloatVar(ce[0]); 2201 FloatVar y = s.arg2FloatVar(ce[1]); 2202 BoolVar b = s.arg2BoolVar(ce[2]); 2203 rel(s,x,FRT_LQ,y,b); 2204 } p_float_max(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2205 void p_float_max(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2206 FloatVar x = s.arg2FloatVar(ce[0]); 2207 FloatVar y = s.arg2FloatVar(ce[1]); 2208 FloatVar z = s.arg2FloatVar(ce[2]); 2209 max(s,x,y,z); 2210 } p_float_min(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2211 void p_float_min(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2212 FloatVar x = s.arg2FloatVar(ce[0]); 2213 FloatVar y = s.arg2FloatVar(ce[1]); 2214 FloatVar z = s.arg2FloatVar(ce[2]); 2215 min(s,x,y,z); 2216 } p_float_lt(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2217 void p_float_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2218 FloatVar x = s.arg2FloatVar(ce[0]); 2219 FloatVar y = s.arg2FloatVar(ce[1]); 2220 rel(s, x, FRT_LQ, y); 2221 rel(s, x, FRT_EQ, y, BoolVar(s,0,0)); 2222 } 2223 p_float_lt_reif(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2224 void p_float_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2225 FloatVar x = s.arg2FloatVar(ce[0]); 2226 FloatVar y = s.arg2FloatVar(ce[1]); 2227 BoolVar b = s.arg2BoolVar(ce[2]); 2228 BoolVar b0(s,0,1); 2229 BoolVar b1(s,0,1); 2230 rel(s, b == (b0 && !b1)); 2231 rel(s, x, FRT_LQ, y, b0); 2232 rel(s, x, FRT_EQ, y, b1); 2233 } 2234 p_float_ne(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2235 void p_float_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2236 FloatVar x = s.arg2FloatVar(ce[0]); 2237 FloatVar y = s.arg2FloatVar(ce[1]); 2238 rel(s, x, FRT_EQ, y, BoolVar(s,0,0)); 2239 } 2240 2241 #ifdef GECODE_HAS_MPFR 2242 #define P_FLOAT_OP(Op) \ 2243 void p_float_ ## Op (FlatZincSpace& s, const ConExpr& ce, AST::Node*) {\ 2244 FloatVar x = s.arg2FloatVar(ce[0]);\ 2245 FloatVar y = s.arg2FloatVar(ce[1]);\ 2246 Op(s,x,y);\ 2247 } 2248 P_FLOAT_OP(acos) P_FLOAT_OP(asin)2249 P_FLOAT_OP(asin) 2250 P_FLOAT_OP(atan) 2251 P_FLOAT_OP(cos) 2252 P_FLOAT_OP(exp) 2253 P_FLOAT_OP(sin) 2254 P_FLOAT_OP(tan) 2255 // P_FLOAT_OP(sinh) 2256 // P_FLOAT_OP(tanh) 2257 // P_FLOAT_OP(cosh) 2258 #undef P_FLOAT_OP 2259 2260 void p_float_ln(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2261 FloatVar x = s.arg2FloatVar(ce[0]); 2262 FloatVar y = s.arg2FloatVar(ce[1]); 2263 log(s,x,y); 2264 } p_float_log10(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2265 void p_float_log10(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2266 FloatVar x = s.arg2FloatVar(ce[0]); 2267 FloatVar y = s.arg2FloatVar(ce[1]); 2268 log(s,10.0,x,y); 2269 } p_float_log2(FlatZincSpace & s,const ConExpr & ce,AST::Node *)2270 void p_float_log2(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 2271 FloatVar x = s.arg2FloatVar(ce[0]); 2272 FloatVar y = s.arg2FloatVar(ce[1]); 2273 log(s,2.0,x,y); 2274 } 2275 2276 #endif 2277 2278 class FloatPoster { 2279 public: FloatPoster(void)2280 FloatPoster(void) { 2281 registry().add("int2float",&p_int2float); 2282 registry().add("float_abs",&p_float_abs); 2283 registry().add("float_sqrt",&p_float_sqrt); 2284 registry().add("float_eq",&p_float_eq); 2285 registry().add("float_eq_reif",&p_float_eq_reif); 2286 registry().add("float_le",&p_float_le); 2287 registry().add("float_le_reif",&p_float_le_reif); 2288 registry().add("float_lt",&p_float_lt); 2289 registry().add("float_lt_reif",&p_float_lt_reif); 2290 registry().add("float_ne",&p_float_ne); 2291 registry().add("float_times",&p_float_times); 2292 registry().add("float_div",&p_float_div); 2293 registry().add("float_plus",&p_float_plus); 2294 registry().add("float_max",&p_float_max); 2295 registry().add("float_min",&p_float_min); 2296 2297 registry().add("float_lin_eq",&p_float_lin_eq); 2298 registry().add("float_lin_eq_reif",&p_float_lin_eq_reif); 2299 registry().add("float_lin_le",&p_float_lin_le); 2300 registry().add("float_lin_lt",&p_float_lin_lt); 2301 registry().add("float_lin_le_reif",&p_float_lin_le_reif); 2302 registry().add("float_lin_lt_reif",&p_float_lin_lt_reif); 2303 2304 #ifdef GECODE_HAS_MPFR 2305 registry().add("float_acos",&p_float_acos); 2306 registry().add("float_asin",&p_float_asin); 2307 registry().add("float_atan",&p_float_atan); 2308 registry().add("float_cos",&p_float_cos); 2309 // registry().add("float_cosh",&p_float_cosh); 2310 registry().add("float_exp",&p_float_exp); 2311 registry().add("float_ln",&p_float_ln); 2312 registry().add("float_log10",&p_float_log10); 2313 registry().add("float_log2",&p_float_log2); 2314 registry().add("float_sin",&p_float_sin); 2315 // registry().add("float_sinh",&p_float_sinh); 2316 registry().add("float_tan",&p_float_tan); 2317 // registry().add("float_tanh",&p_float_tanh); 2318 #endif 2319 } 2320 } __float_poster; 2321 #endif 2322 2323 } 2324 }} 2325 2326 // STATISTICS: flatzinc-any 2327