registry.cpp
Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */ 00002 /* 00003 * Main authors: 00004 * Guido Tack <tack@gecode.org> 00005 * 00006 * Contributing authors: 00007 * Mikael Lagerkvist <lagerkvist@gmail.com> 00008 * 00009 * Copyright: 00010 * Guido Tack, 2007 00011 * Mikael Lagerkvist, 2009 00012 * 00013 * Last modified: 00014 * $Date: 2011-01-17 12:20:14 +0100 (Mon, 17 Jan 2011) $ by $Author: tack $ 00015 * $Revision: 11537 $ 00016 * 00017 * This file is part of Gecode, the generic constraint 00018 * development environment: 00019 * http://www.gecode.org 00020 * 00021 * Permission is hereby granted, free of charge, to any person obtaining 00022 * a copy of this software and associated documentation files (the 00023 * "Software"), to deal in the Software without restriction, including 00024 * without limitation the rights to use, copy, modify, merge, publish, 00025 * distribute, sublicense, and/or sell copies of the Software, and to 00026 * permit persons to whom the Software is furnished to do so, subject to 00027 * the following conditions: 00028 * 00029 * The above copyright notice and this permission notice shall be 00030 * included in all copies or substantial portions of the Software. 00031 * 00032 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 00033 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 00034 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND 00035 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE 00036 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION 00037 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION 00038 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 00039 * 00040 */ 00041 00042 #include <gecode/flatzinc/registry.hh> 00043 #include <gecode/kernel.hh> 00044 #include <gecode/int.hh> 00045 #include <gecode/scheduling.hh> 00046 #include <gecode/graph.hh> 00047 #include <gecode/minimodel.hh> 00048 #ifdef GECODE_HAS_SET_VARS 00049 #include <gecode/set.hh> 00050 #endif 00051 #include <gecode/flatzinc.hh> 00052 00053 namespace Gecode { namespace FlatZinc { 00054 00055 Registry& registry(void) { 00056 static Registry r; 00057 return r; 00058 } 00059 00060 void 00061 Registry::post(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00062 std::map<std::string,poster>::iterator i = r.find(ce.id); 00063 if (i == r.end()) { 00064 throw FlatZinc::Error("Registry", 00065 std::string("Constraint ")+ce.id+" not found"); 00066 } 00067 i->second(s, ce, ann); 00068 } 00069 00070 void 00071 Registry::add(const std::string& id, poster p) { 00072 r[id] = p; 00073 } 00074 00075 namespace { 00076 00077 IntConLevel ann2icl(AST::Node* ann) { 00078 if (ann) { 00079 if (ann->hasAtom("val")) 00080 return ICL_VAL; 00081 if (ann->hasAtom("domain")) 00082 return ICL_DOM; 00083 if (ann->hasAtom("bounds") || 00084 ann->hasAtom("boundsR") || 00085 ann->hasAtom("boundsD") || 00086 ann->hasAtom("boundsZ")) 00087 return ICL_BND; 00088 } 00089 return ICL_DEF; 00090 } 00091 00092 inline IntRelType 00093 swap(IntRelType irt) { 00094 switch (irt) { 00095 case IRT_LQ: return IRT_GQ; 00096 case IRT_LE: return IRT_GR; 00097 case IRT_GQ: return IRT_LQ; 00098 case IRT_GR: return IRT_LE; 00099 default: return irt; 00100 } 00101 } 00102 00103 inline IntRelType 00104 neg(IntRelType irt) { 00105 switch (irt) { 00106 case IRT_EQ: return IRT_NQ; 00107 case IRT_NQ: return IRT_EQ; 00108 case IRT_LQ: return IRT_GR; 00109 case IRT_LE: return IRT_GQ; 00110 case IRT_GQ: return IRT_LE; 00111 case IRT_GR: 00112 default: 00113 assert(irt == IRT_GR); 00114 } 00115 return IRT_LQ; 00116 } 00117 00118 inline IntArgs arg2intargs(AST::Node* arg, int offset = 0) { 00119 AST::Array* a = arg->getArray(); 00120 IntArgs ia(a->a.size()+offset); 00121 for (int i=offset; i--;) 00122 ia[i] = 0; 00123 for (int i=a->a.size(); i--;) 00124 ia[i+offset] = a->a[i]->getInt(); 00125 return ia; 00126 } 00127 00128 inline IntArgs arg2boolargs(AST::Node* arg, int offset = 0) { 00129 AST::Array* a = arg->getArray(); 00130 IntArgs ia(a->a.size()+offset); 00131 for (int i=offset; i--;) 00132 ia[i] = 0; 00133 for (int i=a->a.size(); i--;) 00134 ia[i+offset] = a->a[i]->getBool(); 00135 return ia; 00136 } 00137 00138 inline IntSet arg2intset(FlatZincSpace& s, AST::Node* n) { 00139 AST::SetLit* sl = n->getSet(); 00140 IntSet d; 00141 if (sl->interval) { 00142 d = IntSet(sl->min, sl->max); 00143 } else { 00144 Region re(s); 00145 int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size())); 00146 for (int i=sl->s.size(); i--; ) 00147 is[i] = sl->s[i]; 00148 d = IntSet(is, sl->s.size()); 00149 } 00150 return d; 00151 } 00152 00153 inline IntSetArgs arg2intsetargs(FlatZincSpace& s, 00154 AST::Node* arg, int offset = 0) { 00155 AST::Array* a = arg->getArray(); 00156 if (a->a.size() == 0) { 00157 IntSetArgs emptyIa(0); 00158 return emptyIa; 00159 } 00160 IntSetArgs ia(a->a.size()+offset); 00161 for (int i=offset; i--;) 00162 ia[i] = IntSet::empty; 00163 for (int i=a->a.size(); i--;) { 00164 ia[i+offset] = arg2intset(s, a->a[i]); 00165 } 00166 return ia; 00167 } 00168 00169 inline IntVarArgs arg2intvarargs(FlatZincSpace& s, AST::Node* arg, 00170 int offset = 0) { 00171 AST::Array* a = arg->getArray(); 00172 if (a->a.size() == 0) { 00173 IntVarArgs emptyIa(0); 00174 return emptyIa; 00175 } 00176 IntVarArgs ia(a->a.size()+offset); 00177 for (int i=offset; i--;) 00178 ia[i] = IntVar(s, 0, 0); 00179 for (int i=a->a.size(); i--;) { 00180 if (a->a[i]->isIntVar()) { 00181 ia[i+offset] = s.iv[a->a[i]->getIntVar()]; 00182 } else { 00183 int value = a->a[i]->getInt(); 00184 IntVar iv(s, value, value); 00185 ia[i+offset] = iv; 00186 } 00187 } 00188 return ia; 00189 } 00190 00191 inline BoolVarArgs arg2boolvarargs(FlatZincSpace& s, AST::Node* arg, 00192 int offset = 0, int siv=-1) { 00193 AST::Array* a = arg->getArray(); 00194 if (a->a.size() == 0) { 00195 BoolVarArgs emptyIa(0); 00196 return emptyIa; 00197 } 00198 BoolVarArgs ia(a->a.size()+offset-(siv==-1?0:1)); 00199 for (int i=offset; i--;) 00200 ia[i] = BoolVar(s, 0, 0); 00201 for (int i=0; i<static_cast<int>(a->a.size()); i++) { 00202 if (i==siv) 00203 continue; 00204 if (a->a[i]->isBool()) { 00205 bool value = a->a[i]->getBool(); 00206 BoolVar iv(s, value, value); 00207 ia[offset++] = iv; 00208 } else if (a->a[i]->isIntVar() && 00209 s.aliasBool2Int(a->a[i]->getIntVar()) != -1) { 00210 ia[offset++] = s.bv[s.aliasBool2Int(a->a[i]->getIntVar())]; 00211 } else { 00212 ia[offset++] = s.bv[a->a[i]->getBoolVar()]; 00213 } 00214 } 00215 return ia; 00216 } 00217 00218 #ifdef GECODE_HAS_SET_VARS 00219 SetVar getSetVar(FlatZincSpace& s, AST::Node* n) { 00220 SetVar x0; 00221 if (!n->isSetVar()) { 00222 IntSet d = arg2intset(s,n); 00223 x0 = SetVar(s, d, d); 00224 } else { 00225 x0 = s.sv[n->getSetVar()]; 00226 } 00227 return x0; 00228 } 00229 00230 inline SetVarArgs arg2setvarargs(FlatZincSpace& s, AST::Node* arg, 00231 int offset = 0) { 00232 AST::Array* a = arg->getArray(); 00233 if (a->a.size() == 0) { 00234 SetVarArgs emptyIa(0); 00235 return emptyIa; 00236 } 00237 SetVarArgs ia(a->a.size()+offset); 00238 for (int i=offset; i--;) 00239 ia[i] = SetVar(s, IntSet::empty, IntSet::empty); 00240 for (int i=a->a.size(); i--;) { 00241 ia[i+offset] = getSetVar(s, a->a[i]); 00242 } 00243 return ia; 00244 } 00245 #endif 00246 00247 BoolVar getBoolVar(FlatZincSpace& s, AST::Node* n) { 00248 BoolVar x0; 00249 if (n->isBool()) { 00250 x0 = BoolVar(s, n->getBool(), n->getBool()); 00251 } 00252 else { 00253 x0 = s.bv[n->getBoolVar()]; 00254 } 00255 return x0; 00256 } 00257 00258 IntVar getIntVar(FlatZincSpace& s, AST::Node* n) { 00259 IntVar x0; 00260 if (n->isIntVar()) { 00261 x0 = s.iv[n->getIntVar()]; 00262 } else { 00263 x0 = IntVar(s, n->getInt(), n->getInt()); 00264 } 00265 return x0; 00266 } 00267 00268 bool isBoolArray(FlatZincSpace& s, AST::Node* b, int& singleInt) { 00269 AST::Array* a = b->getArray(); 00270 singleInt = -1; 00271 if (a->a.size() == 0) 00272 return true; 00273 for (int i=a->a.size(); i--;) { 00274 if (a->a[i]->isBoolVar() || a->a[i]->isBool()) { 00275 } else if (a->a[i]->isIntVar()) { 00276 if (s.aliasBool2Int(a->a[i]->getIntVar()) == -1) { 00277 if (singleInt != -1) { 00278 return false; 00279 } 00280 singleInt = i; 00281 } 00282 } else { 00283 return false; 00284 } 00285 } 00286 return singleInt==-1 || a->a.size() > 1; 00287 } 00288 00289 void p_distinct(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00290 IntVarArgs va = arg2intvarargs(s, ce[0]); 00291 distinct(s, va, ann2icl(ann)); 00292 } 00293 void p_distinctOffset(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00294 IntVarArgs va = arg2intvarargs(s, ce[1]); 00295 AST::Array* offs = ce.args->a[0]->getArray(); 00296 IntArgs oa(offs->a.size()); 00297 for (int i=offs->a.size(); i--; ) { 00298 oa[i] = offs->a[i]->getInt(); 00299 } 00300 distinct(s, oa, va, ann2icl(ann)); 00301 } 00302 00303 void p_all_equal(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00304 IntVarArgs va = arg2intvarargs(s, ce[0]); 00305 rel(s, va, IRT_EQ, ann2icl(ann)); 00306 } 00307 00308 void p_int_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, 00309 AST::Node* ann) { 00310 if (ce[0]->isIntVar()) { 00311 if (ce[1]->isIntVar()) { 00312 rel(s, getIntVar(s, ce[0]), irt, getIntVar(s, ce[1]), 00313 ann2icl(ann)); 00314 } else { 00315 rel(s, getIntVar(s, ce[0]), irt, ce[1]->getInt(), ann2icl(ann)); 00316 } 00317 } else { 00318 rel(s, getIntVar(s, ce[1]), swap(irt), ce[0]->getInt(), 00319 ann2icl(ann)); 00320 } 00321 } 00322 void p_int_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00323 p_int_CMP(s, IRT_EQ, ce, ann); 00324 } 00325 void p_int_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00326 p_int_CMP(s, IRT_NQ, ce, ann); 00327 } 00328 void p_int_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00329 p_int_CMP(s, IRT_GQ, ce, ann); 00330 } 00331 void p_int_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00332 p_int_CMP(s, IRT_GR, ce, ann); 00333 } 00334 void p_int_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00335 p_int_CMP(s, IRT_LQ, ce, ann); 00336 } 00337 void p_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00338 p_int_CMP(s, IRT_LE, ce, ann); 00339 } 00340 void p_int_CMP_reif(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, 00341 AST::Node* ann) { 00342 if (ce[2]->isBool()) { 00343 if (ce[2]->getBool()) { 00344 p_int_CMP(s, irt, ce, ann); 00345 } else { 00346 p_int_CMP(s, neg(irt), ce, ann); 00347 } 00348 return; 00349 } 00350 if (ce[0]->isIntVar()) { 00351 if (ce[1]->isIntVar()) { 00352 rel(s, getIntVar(s, ce[0]), irt, getIntVar(s, ce[1]), 00353 getBoolVar(s, ce[2]), ann2icl(ann)); 00354 } else { 00355 rel(s, getIntVar(s, ce[0]), irt, ce[1]->getInt(), 00356 getBoolVar(s, ce[2]), ann2icl(ann)); 00357 } 00358 } else { 00359 rel(s, getIntVar(s, ce[1]), swap(irt), ce[0]->getInt(), 00360 getBoolVar(s, ce[2]), ann2icl(ann)); 00361 } 00362 } 00363 00364 /* Comparisons */ 00365 void p_int_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00366 p_int_CMP_reif(s, IRT_EQ, ce, ann); 00367 } 00368 void p_int_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00369 p_int_CMP_reif(s, IRT_NQ, ce, ann); 00370 } 00371 void p_int_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00372 p_int_CMP_reif(s, IRT_GQ, ce, ann); 00373 } 00374 void p_int_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00375 p_int_CMP_reif(s, IRT_GR, ce, ann); 00376 } 00377 void p_int_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00378 p_int_CMP_reif(s, IRT_LQ, ce, ann); 00379 } 00380 void p_int_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00381 p_int_CMP_reif(s, IRT_LE, ce, ann); 00382 } 00383 00384 /* linear (in-)equations */ 00385 void p_int_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, 00386 AST::Node* ann) { 00387 IntArgs ia = arg2intargs(ce[0]); 00388 int singleIntVar; 00389 if (isBoolArray(s,ce[1],singleIntVar)) { 00390 if (singleIntVar != -1) { 00391 if (std::abs(ia[singleIntVar]) == 1 && ce[2]->getInt() == 0) { 00392 IntVar siv = getIntVar(s, ce[1]->getArray()->a[singleIntVar]); 00393 BoolVarArgs iv = arg2boolvarargs(s, ce[1], 0, singleIntVar); 00394 IntArgs ia_tmp(ia.size()-1); 00395 int count = 0; 00396 for (int i=0; i<ia.size(); i++) { 00397 if (i != singleIntVar) 00398 ia_tmp[count++] = ia[singleIntVar] == -1 ? ia[i] : -ia[i]; 00399 } 00400 linear(s, ia_tmp, iv, irt, siv, ann2icl(ann)); 00401 } else { 00402 IntVarArgs iv = arg2intvarargs(s, ce[1]); 00403 linear(s, ia, iv, irt, ce[2]->getInt(), ann2icl(ann)); 00404 } 00405 } else { 00406 BoolVarArgs iv = arg2boolvarargs(s, ce[1]); 00407 linear(s, ia, iv, irt, ce[2]->getInt(), ann2icl(ann)); 00408 } 00409 } else { 00410 IntVarArgs iv = arg2intvarargs(s, ce[1]); 00411 linear(s, ia, iv, irt, ce[2]->getInt(), ann2icl(ann)); 00412 } 00413 } 00414 void p_int_lin_CMP_reif(FlatZincSpace& s, IntRelType irt, 00415 const ConExpr& ce, AST::Node* ann) { 00416 if (ce[2]->isBool()) { 00417 if (ce[2]->getBool()) { 00418 p_int_lin_CMP(s, irt, ce, ann); 00419 } else { 00420 p_int_lin_CMP(s, neg(irt), ce, ann); 00421 } 00422 return; 00423 } 00424 IntArgs ia = arg2intargs(ce[0]); 00425 int singleIntVar; 00426 if (isBoolArray(s,ce[1],singleIntVar)) { 00427 if (singleIntVar != -1) { 00428 if (std::abs(ia[singleIntVar]) == 1 && ce[2]->getInt() == 0) { 00429 IntVar siv = getIntVar(s, ce[1]->getArray()->a[singleIntVar]); 00430 BoolVarArgs iv = arg2boolvarargs(s, ce[1], 0, singleIntVar); 00431 IntArgs ia_tmp(ia.size()-1); 00432 int count = 0; 00433 for (int i=0; i<ia.size(); i++) { 00434 if (i != singleIntVar) 00435 ia_tmp[count++] = ia[singleIntVar] == -1 ? ia[i] : -ia[i]; 00436 } 00437 linear(s, ia_tmp, iv, irt, siv, getBoolVar(s, ce[3]), 00438 ann2icl(ann)); 00439 } else { 00440 IntVarArgs iv = arg2intvarargs(s, ce[1]); 00441 linear(s, ia, iv, irt, ce[2]->getInt(), 00442 getBoolVar(s, ce[3]), ann2icl(ann)); 00443 } 00444 } else { 00445 BoolVarArgs iv = arg2boolvarargs(s, ce[1]); 00446 linear(s, ia, iv, irt, ce[2]->getInt(), 00447 getBoolVar(s, ce[3]), ann2icl(ann)); 00448 } 00449 } else { 00450 IntVarArgs iv = arg2intvarargs(s, ce[1]); 00451 linear(s, ia, iv, irt, ce[2]->getInt(), getBoolVar(s, ce[3]), 00452 ann2icl(ann)); 00453 } 00454 } 00455 void p_int_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00456 p_int_lin_CMP(s, IRT_EQ, ce, ann); 00457 } 00458 void p_int_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00459 p_int_lin_CMP_reif(s, IRT_EQ, ce, ann); 00460 } 00461 void p_int_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00462 p_int_lin_CMP(s, IRT_NQ, ce, ann); 00463 } 00464 void p_int_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00465 p_int_lin_CMP_reif(s, IRT_NQ, ce, ann); 00466 } 00467 void p_int_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00468 p_int_lin_CMP(s, IRT_LQ, ce, ann); 00469 } 00470 void p_int_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00471 p_int_lin_CMP_reif(s, IRT_LQ, ce, ann); 00472 } 00473 void p_int_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00474 p_int_lin_CMP(s, IRT_LE, ce, ann); 00475 } 00476 void p_int_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00477 p_int_lin_CMP_reif(s, IRT_LE, ce, ann); 00478 } 00479 void p_int_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00480 p_int_lin_CMP(s, IRT_GQ, ce, ann); 00481 } 00482 void p_int_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00483 p_int_lin_CMP_reif(s, IRT_GQ, ce, ann); 00484 } 00485 void p_int_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00486 p_int_lin_CMP(s, IRT_GR, ce, ann); 00487 } 00488 void p_int_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00489 p_int_lin_CMP_reif(s, IRT_GR, ce, ann); 00490 } 00491 00492 void p_bool_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, 00493 AST::Node* ann) { 00494 IntArgs ia = arg2intargs(ce[0]); 00495 BoolVarArgs iv = arg2boolvarargs(s, ce[1]); 00496 if (ce[2]->isIntVar()) 00497 linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()], ann2icl(ann)); 00498 else 00499 linear(s, ia, iv, irt, ce[2]->getInt(), ann2icl(ann)); 00500 } 00501 void p_bool_lin_CMP_reif(FlatZincSpace& s, IntRelType irt, 00502 const ConExpr& ce, AST::Node* ann) { 00503 if (ce[2]->isBool()) { 00504 if (ce[2]->getBool()) { 00505 p_bool_lin_CMP(s, irt, ce, ann); 00506 } else { 00507 p_bool_lin_CMP(s, neg(irt), ce, ann); 00508 } 00509 return; 00510 } 00511 IntArgs ia = arg2intargs(ce[0]); 00512 BoolVarArgs iv = arg2boolvarargs(s, ce[1]); 00513 if (ce[2]->isIntVar()) 00514 linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()], getBoolVar(s, ce[3]), 00515 ann2icl(ann)); 00516 else 00517 linear(s, ia, iv, irt, ce[2]->getInt(), getBoolVar(s, ce[3]), 00518 ann2icl(ann)); 00519 } 00520 void p_bool_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00521 p_bool_lin_CMP(s, IRT_EQ, ce, ann); 00522 } 00523 void p_bool_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 00524 { 00525 p_bool_lin_CMP_reif(s, IRT_EQ, ce, ann); 00526 } 00527 void p_bool_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00528 p_bool_lin_CMP(s, IRT_NQ, ce, ann); 00529 } 00530 void p_bool_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 00531 { 00532 p_bool_lin_CMP_reif(s, IRT_NQ, ce, ann); 00533 } 00534 void p_bool_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00535 p_bool_lin_CMP(s, IRT_LQ, ce, ann); 00536 } 00537 void p_bool_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 00538 { 00539 p_bool_lin_CMP_reif(s, IRT_LQ, ce, ann); 00540 } 00541 void p_bool_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 00542 { 00543 p_bool_lin_CMP(s, IRT_LE, ce, ann); 00544 } 00545 void p_bool_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 00546 { 00547 p_bool_lin_CMP_reif(s, IRT_LE, ce, ann); 00548 } 00549 void p_bool_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00550 p_bool_lin_CMP(s, IRT_GQ, ce, ann); 00551 } 00552 void p_bool_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 00553 { 00554 p_bool_lin_CMP_reif(s, IRT_GQ, ce, ann); 00555 } 00556 void p_bool_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00557 p_bool_lin_CMP(s, IRT_GR, ce, ann); 00558 } 00559 void p_bool_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 00560 { 00561 p_bool_lin_CMP_reif(s, IRT_GR, ce, ann); 00562 } 00563 00564 /* arithmetic constraints */ 00565 00566 void p_int_plus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00567 if (!ce[0]->isIntVar()) { 00568 rel(s, ce[0]->getInt() + getIntVar(s, ce[1]) 00569 == getIntVar(s,ce[2]), ann2icl(ann)); 00570 } else if (!ce[1]->isIntVar()) { 00571 rel(s, getIntVar(s,ce[0]) + ce[1]->getInt() 00572 == getIntVar(s,ce[2]), ann2icl(ann)); 00573 } else if (!ce[2]->isIntVar()) { 00574 rel(s, getIntVar(s,ce[0]) + getIntVar(s,ce[1]) 00575 == ce[2]->getInt(), ann2icl(ann)); 00576 } else { 00577 rel(s, getIntVar(s,ce[0]) + getIntVar(s,ce[1]) 00578 == getIntVar(s,ce[2]), ann2icl(ann)); 00579 } 00580 } 00581 00582 void p_int_minus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00583 if (!ce[0]->isIntVar()) { 00584 rel(s, ce[0]->getInt() - getIntVar(s, ce[1]) 00585 == getIntVar(s,ce[2]), ann2icl(ann)); 00586 } else if (!ce[1]->isIntVar()) { 00587 rel(s, getIntVar(s,ce[0]) - ce[1]->getInt() 00588 == getIntVar(s,ce[2]), ann2icl(ann)); 00589 } else if (!ce[2]->isIntVar()) { 00590 rel(s, getIntVar(s,ce[0]) - getIntVar(s,ce[1]) 00591 == ce[2]->getInt(), ann2icl(ann)); 00592 } else { 00593 rel(s, getIntVar(s,ce[0]) - getIntVar(s,ce[1]) 00594 == getIntVar(s,ce[2]), ann2icl(ann)); 00595 } 00596 } 00597 00598 void p_int_times(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00599 IntVar x0 = getIntVar(s, ce[0]); 00600 IntVar x1 = getIntVar(s, ce[1]); 00601 IntVar x2 = getIntVar(s, ce[2]); 00602 mult(s, x0, x1, x2, ann2icl(ann)); 00603 } 00604 void p_int_div(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00605 IntVar x0 = getIntVar(s, ce[0]); 00606 IntVar x1 = getIntVar(s, ce[1]); 00607 IntVar x2 = getIntVar(s, ce[2]); 00608 div(s,x0,x1,x2, ann2icl(ann)); 00609 } 00610 void p_int_mod(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00611 IntVar x0 = getIntVar(s, ce[0]); 00612 IntVar x1 = getIntVar(s, ce[1]); 00613 IntVar x2 = getIntVar(s, ce[2]); 00614 mod(s,x0,x1,x2, ann2icl(ann)); 00615 } 00616 00617 void p_int_min(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00618 IntVar x0 = getIntVar(s, ce[0]); 00619 IntVar x1 = getIntVar(s, ce[1]); 00620 IntVar x2 = getIntVar(s, ce[2]); 00621 min(s, x0, x1, x2, ann2icl(ann)); 00622 } 00623 void p_int_max(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00624 IntVar x0 = getIntVar(s, ce[0]); 00625 IntVar x1 = getIntVar(s, ce[1]); 00626 IntVar x2 = getIntVar(s, ce[2]); 00627 max(s, x0, x1, x2, ann2icl(ann)); 00628 } 00629 void p_int_negate(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00630 IntVar x0 = getIntVar(s, ce[0]); 00631 IntVar x1 = getIntVar(s, ce[1]); 00632 rel(s, x0 == -x1, ann2icl(ann)); 00633 } 00634 00635 /* Boolean constraints */ 00636 void p_bool_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, 00637 AST::Node* ann) { 00638 rel(s, getBoolVar(s, ce[0]), irt, getBoolVar(s, ce[1]), 00639 ann2icl(ann)); 00640 } 00641 void p_bool_CMP_reif(FlatZincSpace& s, IntRelType irt, const ConExpr& ce, 00642 AST::Node* ann) { 00643 rel(s, getBoolVar(s, ce[0]), irt, getBoolVar(s, ce[1]), 00644 getBoolVar(s, ce[2]), ann2icl(ann)); 00645 } 00646 void p_bool_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00647 p_bool_CMP(s, IRT_EQ, ce, ann); 00648 } 00649 void p_bool_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00650 p_bool_CMP_reif(s, IRT_EQ, ce, ann); 00651 } 00652 void p_bool_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00653 p_bool_CMP(s, IRT_NQ, ce, ann); 00654 } 00655 void p_bool_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00656 p_bool_CMP_reif(s, IRT_NQ, ce, ann); 00657 } 00658 void p_bool_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00659 p_bool_CMP(s, IRT_GQ, ce, ann); 00660 } 00661 void p_bool_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00662 p_bool_CMP_reif(s, IRT_GQ, ce, ann); 00663 } 00664 void p_bool_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00665 p_bool_CMP(s, IRT_LQ, ce, ann); 00666 } 00667 void p_bool_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00668 p_bool_CMP_reif(s, IRT_LQ, ce, ann); 00669 } 00670 void p_bool_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00671 p_bool_CMP(s, IRT_GR, ce, ann); 00672 } 00673 void p_bool_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00674 p_bool_CMP_reif(s, IRT_GR, ce, ann); 00675 } 00676 void p_bool_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00677 p_bool_CMP(s, IRT_LE, ce, ann); 00678 } 00679 void p_bool_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00680 p_bool_CMP_reif(s, IRT_LE, ce, ann); 00681 } 00682 00683 #define BOOL_OP(op) \ 00684 BoolVar b0 = getBoolVar(s, ce[0]); \ 00685 BoolVar b1 = getBoolVar(s, ce[1]); \ 00686 if (ce[2]->isBool()) { \ 00687 rel(s, b0, op, b1, ce[2]->getBool(), ann2icl(ann)); \ 00688 } else { \ 00689 rel(s, b0, op, b1, s.bv[ce[2]->getBoolVar()], ann2icl(ann)); \ 00690 } 00691 00692 #define BOOL_ARRAY_OP(op) \ 00693 BoolVarArgs bv = arg2boolvarargs(s, ce[0]); \ 00694 if (ce[1]->isBool()) { \ 00695 rel(s, op, bv, ce[1]->getBool(), ann2icl(ann)); \ 00696 } else { \ 00697 rel(s, op, bv, s.bv[ce[1]->getBoolVar()], ann2icl(ann)); \ 00698 } 00699 00700 void p_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00701 BOOL_OP(BOT_OR); 00702 } 00703 void p_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00704 BOOL_OP(BOT_AND); 00705 } 00706 void p_array_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 00707 { 00708 BOOL_ARRAY_OP(BOT_AND); 00709 } 00710 void p_array_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) 00711 { 00712 BOOL_ARRAY_OP(BOT_OR); 00713 } 00714 void p_array_bool_clause(FlatZincSpace& s, const ConExpr& ce, 00715 AST::Node* ann) { 00716 BoolVarArgs bvp = arg2boolvarargs(s, ce[0]); 00717 BoolVarArgs bvn = arg2boolvarargs(s, ce[1]); 00718 clause(s, BOT_OR, bvp, bvn, 1, ann2icl(ann)); 00719 } 00720 void p_array_bool_clause_reif(FlatZincSpace& s, const ConExpr& ce, 00721 AST::Node* ann) { 00722 BoolVarArgs bvp = arg2boolvarargs(s, ce[0]); 00723 BoolVarArgs bvn = arg2boolvarargs(s, ce[1]); 00724 BoolVar b0 = getBoolVar(s, ce[2]); 00725 clause(s, BOT_OR, bvp, bvn, b0, ann2icl(ann)); 00726 } 00727 void p_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00728 BOOL_OP(BOT_XOR); 00729 } 00730 void p_bool_l_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00731 BoolVar b0 = getBoolVar(s, ce[0]); 00732 BoolVar b1 = getBoolVar(s, ce[1]); 00733 if (ce[2]->isBool()) { 00734 rel(s, b1, BOT_IMP, b0, ce[2]->getBool(), ann2icl(ann)); 00735 } else { 00736 rel(s, b1, BOT_IMP, b0, s.bv[ce[2]->getBoolVar()], ann2icl(ann)); 00737 } 00738 } 00739 void p_bool_r_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00740 BOOL_OP(BOT_IMP); 00741 } 00742 void p_bool_not(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00743 BoolVar x0 = getBoolVar(s, ce[0]); 00744 BoolVar x1 = getBoolVar(s, ce[1]); 00745 rel(s, x0, BOT_XOR, x1, 1, ann2icl(ann)); 00746 } 00747 00748 /* element constraints */ 00749 void p_array_int_element(FlatZincSpace& s, const ConExpr& ce, 00750 AST::Node* ann) { 00751 bool isConstant = true; 00752 AST::Array* a = ce[1]->getArray(); 00753 for (int i=a->a.size(); i--;) { 00754 if (!a->a[i]->isInt()) { 00755 isConstant = false; 00756 break; 00757 } 00758 } 00759 IntVar selector = getIntVar(s, ce[0]); 00760 rel(s, selector > 0); 00761 if (isConstant) { 00762 IntArgs ia = arg2intargs(ce[1], 1); 00763 element(s, ia, selector, getIntVar(s, ce[2]), ann2icl(ann)); 00764 } else { 00765 IntVarArgs iv = arg2intvarargs(s, ce[1], 1); 00766 element(s, iv, selector, getIntVar(s, ce[2]), ann2icl(ann)); 00767 } 00768 } 00769 void p_array_bool_element(FlatZincSpace& s, const ConExpr& ce, 00770 AST::Node* ann) { 00771 bool isConstant = true; 00772 AST::Array* a = ce[1]->getArray(); 00773 for (int i=a->a.size(); i--;) { 00774 if (!a->a[i]->isBool()) { 00775 isConstant = false; 00776 break; 00777 } 00778 } 00779 IntVar selector = getIntVar(s, ce[0]); 00780 rel(s, selector > 0); 00781 if (isConstant) { 00782 IntArgs ia = arg2boolargs(ce[1], 1); 00783 element(s, ia, selector, getBoolVar(s, ce[2]), ann2icl(ann)); 00784 } else { 00785 BoolVarArgs iv = arg2boolvarargs(s, ce[1], 1); 00786 element(s, iv, selector, getBoolVar(s, ce[2]), ann2icl(ann)); 00787 } 00788 } 00789 00790 /* coercion constraints */ 00791 void p_bool2int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00792 BoolVar x0 = getBoolVar(s, ce[0]); 00793 IntVar x1 = getIntVar(s, ce[1]); 00794 if (ce[0]->isBoolVar() && ce[1]->isIntVar()) { 00795 s.aliasBool2Int(ce[1]->getIntVar(), ce[0]->getBoolVar()); 00796 } 00797 channel(s, x0, x1, ann2icl(ann)); 00798 } 00799 00800 void p_int_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 00801 IntSet d = arg2intset(s,ce[1]); 00802 if (ce[0]->isBoolVar()) { 00803 IntSetRanges dr(d); 00804 Iter::Ranges::Singleton sr(0,1); 00805 Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr); 00806 IntSet d01(i); 00807 if (d01.size() == 0) { 00808 s.fail(); 00809 } else { 00810 rel(s, getBoolVar(s, ce[0]), IRT_GQ, d01.min()); 00811 rel(s, getBoolVar(s, ce[0]), IRT_LQ, d01.max()); 00812 } 00813 } else { 00814 dom(s, getIntVar(s, ce[0]), d); 00815 } 00816 } 00817 00818 /* constraints from the standard library */ 00819 00820 void p_abs(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00821 IntVar x0 = getIntVar(s, ce[0]); 00822 IntVar x1 = getIntVar(s, ce[1]); 00823 abs(s, x0, x1, ann2icl(ann)); 00824 } 00825 00826 void p_array_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00827 IntVarArgs iv0 = arg2intvarargs(s, ce[0]); 00828 IntVarArgs iv1 = arg2intvarargs(s, ce[1]); 00829 rel(s, iv0, IRT_LE, iv1, ann2icl(ann)); 00830 } 00831 00832 void p_array_int_lq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00833 IntVarArgs iv0 = arg2intvarargs(s, ce[0]); 00834 IntVarArgs iv1 = arg2intvarargs(s, ce[1]); 00835 rel(s, iv0, IRT_LQ, iv1, ann2icl(ann)); 00836 } 00837 00838 void p_count(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00839 IntVarArgs iv = arg2intvarargs(s, ce[0]); 00840 if (!ce[1]->isIntVar()) { 00841 if (!ce[2]->isIntVar()) { 00842 count(s, iv, ce[1]->getInt(), IRT_EQ, ce[2]->getInt(), 00843 ann2icl(ann)); 00844 } else { 00845 count(s, iv, ce[1]->getInt(), IRT_EQ, getIntVar(s, ce[2]), 00846 ann2icl(ann)); 00847 } 00848 } else if (!ce[2]->isIntVar()) { 00849 count(s, iv, getIntVar(s, ce[1]), IRT_EQ, ce[2]->getInt(), 00850 ann2icl(ann)); 00851 } else { 00852 count(s, iv, getIntVar(s, ce[1]), IRT_EQ, getIntVar(s, ce[2]), 00853 ann2icl(ann)); 00854 } 00855 } 00856 00857 void count_rel(IntRelType irt, 00858 FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00859 IntVarArgs iv = arg2intvarargs(s, ce[1]); 00860 count(s, iv, ce[2]->getInt(), irt, ce[0]->getInt(), ann2icl(ann)); 00861 } 00862 00863 void p_at_most(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00864 count_rel(IRT_LQ, s, ce, ann); 00865 } 00866 00867 void p_at_least(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00868 count_rel(IRT_GQ, s, ce, ann); 00869 } 00870 00871 void p_bin_packing_load(FlatZincSpace& s, const ConExpr& ce, 00872 AST::Node* ann) { 00873 int minIdx = ce[3]->getInt(); 00874 IntVarArgs load = arg2intvarargs(s, ce[0]); 00875 IntVarArgs l; 00876 IntVarArgs bin = arg2intvarargs(s, ce[1]); 00877 for (int i=bin.size(); i--;) 00878 rel(s, bin[i] >= minIdx); 00879 if (minIdx > 0) { 00880 for (int i=minIdx; i--;) 00881 l << IntVar(s,0,0); 00882 } else if (minIdx < 0) { 00883 IntVarArgs bin2(bin.size()); 00884 for (int i=bin.size(); i--;) 00885 bin2[i] = expr(s, bin[i]-minIdx, ann2icl(ann)); 00886 bin = bin2; 00887 } 00888 l << load; 00889 IntArgs sizes = arg2intargs(ce[2]); 00890 binpacking(s, l, bin, sizes, ann2icl(ann)); 00891 } 00892 00893 void p_global_cardinality(FlatZincSpace& s, const ConExpr& ce, 00894 AST::Node* ann) { 00895 IntVarArgs iv0 = arg2intvarargs(s, ce[0]); 00896 IntArgs cover = arg2intargs(ce[1]); 00897 IntVarArgs iv1 = arg2intvarargs(s, ce[2]); 00898 00899 Region re(s); 00900 IntSet cover_s(cover); 00901 IntSetRanges cover_r(cover_s); 00902 IntVarRanges* iv0_ri = re.alloc<IntVarRanges>(iv0.size()); 00903 for (int i=iv0.size(); i--;) 00904 iv0_ri[i] = IntVarRanges(iv0[i]); 00905 Iter::Ranges::NaryUnion<IntVarRanges> iv0_r(re,iv0_ri,iv0.size()); 00906 Iter::Ranges::Diff<Iter::Ranges::NaryUnion<IntVarRanges>,IntSetRanges> 00907 extra_r(iv0_r,cover_r); 00908 Iter::Ranges::ToValues<Iter::Ranges::Diff< 00909 Iter::Ranges::NaryUnion<IntVarRanges>,IntSetRanges> > extra(extra_r); 00910 for (; extra(); ++extra) { 00911 cover << extra.val(); 00912 iv1 << IntVar(s,0,iv0.size()); 00913 } 00914 count(s, iv0, iv1, cover, ann2icl(ann)); 00915 } 00916 00917 void p_global_cardinality_closed(FlatZincSpace& s, const ConExpr& ce, 00918 AST::Node* ann) { 00919 IntVarArgs iv0 = arg2intvarargs(s, ce[0]); 00920 IntArgs cover = arg2intargs(ce[1]); 00921 IntVarArgs iv1 = arg2intvarargs(s, ce[2]); 00922 count(s, iv0, iv1, cover, ann2icl(ann)); 00923 } 00924 00925 void p_global_cardinality_low_up(FlatZincSpace& s, const ConExpr& ce, 00926 AST::Node* ann) { 00927 IntVarArgs x = arg2intvarargs(s, ce[0]); 00928 IntArgs cover = arg2intargs(ce[1]); 00929 00930 IntArgs lbound = arg2intargs(ce[2]); 00931 IntArgs ubound = arg2intargs(ce[3]); 00932 IntSetArgs y(cover.size()); 00933 for (int i=cover.size(); i--;) 00934 y[i] = IntSet(lbound[i],ubound[i]); 00935 00936 IntSet cover_s(cover); 00937 Region re(s); 00938 IntVarRanges* xrs = re.alloc<IntVarRanges>(x.size()); 00939 for (int i=x.size(); i--;) 00940 xrs[i].init(x[i]); 00941 Iter::Ranges::NaryUnion<IntVarRanges> u(re, xrs, x.size()); 00942 Iter::Ranges::ToValues<Iter::Ranges::NaryUnion<IntVarRanges> > uv(u); 00943 for (; uv(); ++uv) { 00944 if (!cover_s.in(uv.val())) { 00945 cover << uv.val(); 00946 y << IntSet(0,x.size()); 00947 } 00948 } 00949 00950 count(s, x, y, cover, ann2icl(ann)); 00951 } 00952 00953 void p_global_cardinality_low_up_closed(FlatZincSpace& s, 00954 const ConExpr& ce, 00955 AST::Node* ann) { 00956 IntVarArgs x = arg2intvarargs(s, ce[0]); 00957 IntArgs cover = arg2intargs(ce[1]); 00958 00959 IntArgs lbound = arg2intargs(ce[2]); 00960 IntArgs ubound = arg2intargs(ce[3]); 00961 IntSetArgs y(cover.size()); 00962 for (int i=cover.size(); i--;) 00963 y[i] = IntSet(lbound[i],ubound[i]); 00964 00965 count(s, x, y, cover, ann2icl(ann)); 00966 } 00967 00968 void p_minimum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00969 IntVarArgs iv = arg2intvarargs(s, ce[1]); 00970 min(s, iv, getIntVar(s, ce[0]), ann2icl(ann)); 00971 } 00972 00973 void p_maximum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00974 IntVarArgs iv = arg2intvarargs(s, ce[1]); 00975 max(s, iv, getIntVar(s, ce[0]), ann2icl(ann)); 00976 } 00977 00978 void p_regular(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 00979 IntVarArgs iv = arg2intvarargs(s, ce[0]); 00980 int q = ce[1]->getInt(); 00981 int symbols = ce[2]->getInt(); 00982 IntArgs d = arg2intargs(ce[3]); 00983 int q0 = ce[4]->getInt(); 00984 00985 int noOfTrans = 0; 00986 for (int i=1; i<=q; i++) { 00987 for (int j=1; j<=symbols; j++) { 00988 if (d[(i-1)*symbols+(j-1)] > 0) 00989 noOfTrans++; 00990 } 00991 } 00992 00993 Region re(s); 00994 DFA::Transition* t = re.alloc<DFA::Transition>(noOfTrans+1); 00995 noOfTrans = 0; 00996 for (int i=1; i<=q; i++) { 00997 for (int j=1; j<=symbols; j++) { 00998 if (d[(i-1)*symbols+(j-1)] > 0) { 00999 t[noOfTrans].i_state = i; 01000 t[noOfTrans].symbol = j; 01001 t[noOfTrans].o_state = d[(i-1)*symbols+(j-1)]; 01002 noOfTrans++; 01003 } 01004 } 01005 } 01006 t[noOfTrans].i_state = -1; 01007 01008 // Final states 01009 AST::SetLit* sl = ce[5]->getSet(); 01010 int* f; 01011 if (sl->interval) { 01012 f = static_cast<int*>(malloc(sizeof(int)*(sl->max-sl->min+2))); 01013 for (int i=sl->min; i<=sl->max; i++) 01014 f[i-sl->min] = i; 01015 f[sl->max-sl->min+1] = -1; 01016 } else { 01017 f = static_cast<int*>(malloc(sizeof(int)*(sl->s.size()+1))); 01018 for (int j=sl->s.size(); j--; ) 01019 f[j] = sl->s[j]; 01020 f[sl->s.size()] = -1; 01021 } 01022 01023 DFA dfa(q0,t,f); 01024 free(f); 01025 extensional(s, iv, dfa, ann2icl(ann)); 01026 } 01027 01028 void 01029 p_sort(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 01030 IntVarArgs x = arg2intvarargs(s, ce[0]); 01031 IntVarArgs y = arg2intvarargs(s, ce[1]); 01032 IntVarArgs xy(x.size()+y.size()); 01033 for (int i=x.size(); i--;) 01034 xy[i] = x[i]; 01035 for (int i=y.size(); i--;) 01036 xy[i+x.size()] = y[i]; 01037 unshare(s, xy); 01038 for (int i=x.size(); i--;) 01039 x[i] = xy[i]; 01040 for (int i=y.size(); i--;) 01041 y[i] = xy[i+x.size()]; 01042 sorted(s, x, y, ann2icl(ann)); 01043 } 01044 01045 void 01046 p_inverse_offsets(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 01047 IntVarArgs x = arg2intvarargs(s, ce[0]); 01048 int xoff = ce[1]->getInt(); 01049 IntVarArgs y = arg2intvarargs(s, ce[2]); 01050 int yoff = ce[3]->getInt(); 01051 channel(s, x, xoff, y, yoff, ann2icl(ann)); 01052 } 01053 01054 void 01055 p_increasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 01056 IntVarArgs x = arg2intvarargs(s, ce[0]); 01057 rel(s,x,IRT_LQ,ann2icl(ann)); 01058 } 01059 01060 void 01061 p_increasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 01062 BoolVarArgs x = arg2boolvarargs(s, ce[0]); 01063 rel(s,x,IRT_LQ,ann2icl(ann)); 01064 } 01065 01066 void 01067 p_decreasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 01068 IntVarArgs x = arg2intvarargs(s, ce[0]); 01069 rel(s,x,IRT_GQ,ann2icl(ann)); 01070 } 01071 01072 void 01073 p_decreasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 01074 BoolVarArgs x = arg2boolvarargs(s, ce[0]); 01075 rel(s,x,IRT_GQ,ann2icl(ann)); 01076 } 01077 01078 void 01079 p_table_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 01080 IntVarArgs x = arg2intvarargs(s, ce[0]); 01081 IntArgs tuples = arg2intargs(ce[1]); 01082 int noOfVars = x.size(); 01083 int noOfTuples = tuples.size()/noOfVars; 01084 TupleSet ts; 01085 for (int i=0; i<noOfTuples; i++) { 01086 IntArgs t(noOfVars); 01087 for (int j=0; j<x.size(); j++) { 01088 t[j] = tuples[i*noOfVars+j]; 01089 } 01090 ts.add(t); 01091 } 01092 ts.finalize(); 01093 extensional(s,x,ts,EPK_DEF,ann2icl(ann)); 01094 } 01095 void 01096 p_table_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) { 01097 BoolVarArgs x = arg2boolvarargs(s, ce[0]); 01098 IntArgs tuples = arg2boolargs(ce[1]); 01099 int noOfVars = x.size(); 01100 int noOfTuples = tuples.size()/noOfVars; 01101 TupleSet ts; 01102 for (int i=0; i<noOfTuples; i++) { 01103 IntArgs t(noOfVars); 01104 for (int j=0; j<x.size(); j++) { 01105 t[j] = tuples[i*noOfVars+j]; 01106 } 01107 ts.add(t); 01108 } 01109 ts.finalize(); 01110 extensional(s,x,ts,EPK_DEF,ann2icl(ann)); 01111 } 01112 01113 void p_cumulatives(FlatZincSpace& s, const ConExpr& ce, 01114 AST::Node* ann) { 01115 IntVarArgs start = arg2intvarargs(s, ce[0]); 01116 IntVarArgs duration = arg2intvarargs(s, ce[1]); 01117 IntVarArgs height = arg2intvarargs(s, ce[2]); 01118 int n = start.size(); 01119 IntVar bound = getIntVar(s, ce[3]); 01120 01121 int minHeight = INT_MAX; int minHeight2 = INT_MAX; 01122 for (int i=n; i--;) 01123 if (height[i].min() < minHeight) 01124 minHeight = height[i].min(); 01125 else if (height[i].min() < minHeight2) 01126 minHeight2 = height[i].min(); 01127 bool disjunctive = 01128 (minHeight > bound.max()/2) || 01129 (minHeight2 > bound.max()/2 && minHeight+minHeight2>bound.max()); 01130 if (disjunctive) { 01131 rel(s, bound >= max(height)); 01132 // Unary 01133 if (duration.assigned()) { 01134 IntArgs durationI(n); 01135 bool allone = true; 01136 for (int i=n; i--;) { 01137 durationI[i] = duration[i].val(); 01138 if (durationI[i] != 1) 01139 allone = false; 01140 } 01141 if (allone) { 01142 distinct(s,start,ann2icl(ann)); 01143 } else { 01144 unary(s,start,durationI); 01145 } 01146 } else { 01147 IntVarArgs end(s,n,Int::Limits::min,Int::Limits::max); 01148 for (int i=n; i--;) 01149 rel(s,start[i]+duration[i]==end[i]); 01150 unary(s,start,duration,end); 01151 } 01152 } else if (bound.assigned()) { 01153 if (height.assigned()) { 01154 IntArgs heightI(n); 01155 for (int i=n; i--;) 01156 heightI[i] = height[i].val(); 01157 if (duration.assigned()) { 01158 IntArgs durationI(n); 01159 for (int i=n; i--;) 01160 durationI[i] = duration[i].val(); 01161 cumulative(s, bound.val(), start, durationI, heightI); 01162 } else { 01163 IntVarArgs end(n); 01164 for (int i = n; i--; ) 01165 end[i] = expr(s, start[i]+duration[i]); 01166 cumulative(s, bound.val(), start, duration, end, heightI); 01167 } 01168 } else { 01169 IntArgs machine = IntArgs::create(n,0,0); 01170 IntArgs limit(1, bound.val()); 01171 IntVarArgs end(n); 01172 for (int i = n; i--; ) end[i] = IntVar(s, 0, Int::Limits::max); 01173 cumulatives(s, machine, start, duration, end, height, limit, true, 01174 ann2icl(ann)); 01175 } 01176 } else { 01177 int min = Gecode::Int::Limits::max; 01178 int max = Gecode::Int::Limits::min; 01179 IntVarArgs end(start.size()); 01180 for (int i = start.size(); i--; ) { 01181 min = std::min(min, start[i].min()); 01182 max = std::max(max, start[i].max() + duration[i].max()); 01183 end[i] = expr(s, start[i] + duration[i]); 01184 } 01185 for (int time = min; time < max; ++time) { 01186 IntVarArgs x(start.size()); 01187 for (int i = start.size(); i--; ) { 01188 IntVar overlaps = channel(s, expr(s, (start[i] <= time) && 01189 (time < end[i]))); 01190 x[i] = expr(s, overlaps * height[i]); 01191 } 01192 linear(s, x, IRT_LQ, bound); 01193 } 01194 } 01195 } 01196 01197 void p_among_seq_int(FlatZincSpace& s, const ConExpr& ce, 01198 AST::Node* ann) { 01199 IntVarArgs x = arg2intvarargs(s, ce[0]); 01200 IntSet S = arg2intset(s, ce[1]); 01201 int q = ce[2]->getInt(); 01202 int l = ce[3]->getInt(); 01203 int u = ce[4]->getInt(); 01204 sequence(s, x, S, q, l, u, ann2icl(ann)); 01205 } 01206 01207 void p_among_seq_bool(FlatZincSpace& s, const ConExpr& ce, 01208 AST::Node* ann) { 01209 BoolVarArgs x = arg2boolvarargs(s, ce[0]); 01210 bool val = ce[1]->getBool(); 01211 int q = ce[2]->getInt(); 01212 int l = ce[3]->getInt(); 01213 int u = ce[4]->getInt(); 01214 IntSet S(val, val); 01215 sequence(s, x, S, q, l, u, ann2icl(ann)); 01216 } 01217 01218 void p_schedule_unary(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 01219 IntVarArgs x = arg2intvarargs(s, ce[0]); 01220 IntArgs p = arg2intargs(ce[1]); 01221 unary(s, x, p); 01222 } 01223 01224 void p_schedule_unary_optional(FlatZincSpace& s, const ConExpr& ce, 01225 AST::Node*) { 01226 IntVarArgs x = arg2intvarargs(s, ce[0]); 01227 IntArgs p = arg2intargs(ce[1]); 01228 BoolVarArgs m = arg2boolvarargs(s, ce[2]); 01229 unary(s, x, p, m); 01230 } 01231 01232 void p_circuit(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 01233 IntVarArgs xv = arg2intvarargs(s, ce[0]); 01234 circuit(s,xv,ann2icl(ann)); 01235 } 01236 void p_circuit_cost_array(FlatZincSpace& s, const ConExpr& ce, 01237 AST::Node *ann) { 01238 IntArgs c = arg2intargs(ce[0]); 01239 IntVarArgs xv = arg2intvarargs(s, ce[1]); 01240 IntVarArgs yv = arg2intvarargs(s, ce[2]); 01241 IntVar z = getIntVar(s, ce[3]); 01242 circuit(s,c,xv,yv,z,ann2icl(ann)); 01243 } 01244 void p_circuit_cost(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 01245 IntArgs c = arg2intargs(ce[0]); 01246 IntVarArgs xv = arg2intvarargs(s, ce[1]); 01247 IntVar z = getIntVar(s, ce[2]); 01248 circuit(s,c,xv,z,ann2icl(ann)); 01249 } 01250 01251 class IntPoster { 01252 public: 01253 IntPoster(void) { 01254 registry().add("all_different_int", &p_distinct); 01255 registry().add("all_different_offset", &p_distinctOffset); 01256 registry().add("all_equal_int", &p_all_equal); 01257 registry().add("int_eq", &p_int_eq); 01258 registry().add("int_ne", &p_int_ne); 01259 registry().add("int_ge", &p_int_ge); 01260 registry().add("int_gt", &p_int_gt); 01261 registry().add("int_le", &p_int_le); 01262 registry().add("int_lt", &p_int_lt); 01263 registry().add("int_eq_reif", &p_int_eq_reif); 01264 registry().add("int_ne_reif", &p_int_ne_reif); 01265 registry().add("int_ge_reif", &p_int_ge_reif); 01266 registry().add("int_gt_reif", &p_int_gt_reif); 01267 registry().add("int_le_reif", &p_int_le_reif); 01268 registry().add("int_lt_reif", &p_int_lt_reif); 01269 registry().add("int_lin_eq", &p_int_lin_eq); 01270 registry().add("int_lin_eq_reif", &p_int_lin_eq_reif); 01271 registry().add("int_lin_ne", &p_int_lin_ne); 01272 registry().add("int_lin_ne_reif", &p_int_lin_ne_reif); 01273 registry().add("int_lin_le", &p_int_lin_le); 01274 registry().add("int_lin_le_reif", &p_int_lin_le_reif); 01275 registry().add("int_lin_lt", &p_int_lin_lt); 01276 registry().add("int_lin_lt_reif", &p_int_lin_lt_reif); 01277 registry().add("int_lin_ge", &p_int_lin_ge); 01278 registry().add("int_lin_ge_reif", &p_int_lin_ge_reif); 01279 registry().add("int_lin_gt", &p_int_lin_gt); 01280 registry().add("int_lin_gt_reif", &p_int_lin_gt_reif); 01281 registry().add("int_plus", &p_int_plus); 01282 registry().add("int_minus", &p_int_minus); 01283 registry().add("int_times", &p_int_times); 01284 registry().add("int_div", &p_int_div); 01285 registry().add("int_mod", &p_int_mod); 01286 registry().add("int_min", &p_int_min); 01287 registry().add("int_max", &p_int_max); 01288 registry().add("int_abs", &p_abs); 01289 registry().add("int_negate", &p_int_negate); 01290 registry().add("bool_eq", &p_bool_eq); 01291 registry().add("bool_eq_reif", &p_bool_eq_reif); 01292 registry().add("bool_ne", &p_bool_ne); 01293 registry().add("bool_ne_reif", &p_bool_ne_reif); 01294 registry().add("bool_ge", &p_bool_ge); 01295 registry().add("bool_ge_reif", &p_bool_ge_reif); 01296 registry().add("bool_le", &p_bool_le); 01297 registry().add("bool_le_reif", &p_bool_le_reif); 01298 registry().add("bool_gt", &p_bool_gt); 01299 registry().add("bool_gt_reif", &p_bool_gt_reif); 01300 registry().add("bool_lt", &p_bool_lt); 01301 registry().add("bool_lt_reif", &p_bool_lt_reif); 01302 registry().add("bool_or", &p_bool_or); 01303 registry().add("bool_and", &p_bool_and); 01304 registry().add("bool_xor", &p_bool_xor); 01305 registry().add("array_bool_and", &p_array_bool_and); 01306 registry().add("array_bool_or", &p_array_bool_or); 01307 registry().add("bool_clause", &p_array_bool_clause); 01308 registry().add("bool_clause_reif", &p_array_bool_clause_reif); 01309 registry().add("bool_left_imp", &p_bool_l_imp); 01310 registry().add("bool_right_imp", &p_bool_r_imp); 01311 registry().add("bool_not", &p_bool_not); 01312 registry().add("array_int_element", &p_array_int_element); 01313 registry().add("array_var_int_element", &p_array_int_element); 01314 registry().add("array_bool_element", &p_array_bool_element); 01315 registry().add("array_var_bool_element", &p_array_bool_element); 01316 registry().add("bool2int", &p_bool2int); 01317 registry().add("int_in", &p_int_in); 01318 01319 registry().add("array_int_lt", &p_array_int_lt); 01320 registry().add("array_int_lq", &p_array_int_lq); 01321 registry().add("count", &p_count); 01322 registry().add("at_least_int", &p_at_least); 01323 registry().add("at_most_int", &p_at_most); 01324 registry().add("bin_packing_load_gecode", &p_bin_packing_load); 01325 registry().add("global_cardinality_gecode", &p_global_cardinality); 01326 registry().add("global_cardinality_closed_gecode", 01327 &p_global_cardinality_closed); 01328 registry().add("global_cardinality_low_up", 01329 &p_global_cardinality_low_up); 01330 registry().add("global_cardinality_low_up_closed", 01331 &p_global_cardinality_low_up_closed); 01332 registry().add("minimum_int", &p_minimum); 01333 registry().add("maximum_int", &p_maximum); 01334 registry().add("regular", &p_regular); 01335 registry().add("sort", &p_sort); 01336 registry().add("inverse_offsets", &p_inverse_offsets); 01337 registry().add("increasing_int", &p_increasing_int); 01338 registry().add("increasing_bool", &p_increasing_bool); 01339 registry().add("decreasing_int", &p_decreasing_int); 01340 registry().add("decreasing_bool", &p_decreasing_bool); 01341 registry().add("table_int", &p_table_int); 01342 registry().add("table_bool", &p_table_bool); 01343 registry().add("cumulatives", &p_cumulatives); 01344 registry().add("among_seq_int", &p_among_seq_int); 01345 registry().add("among_seq_bool", &p_among_seq_bool); 01346 01347 registry().add("bool_lin_eq", &p_bool_lin_eq); 01348 registry().add("bool_lin_ne", &p_bool_lin_ne); 01349 registry().add("bool_lin_le", &p_bool_lin_le); 01350 registry().add("bool_lin_lt", &p_bool_lin_lt); 01351 registry().add("bool_lin_ge", &p_bool_lin_ge); 01352 registry().add("bool_lin_gt", &p_bool_lin_gt); 01353 01354 registry().add("bool_lin_eq_reif", &p_bool_lin_eq_reif); 01355 registry().add("bool_lin_ne_reif", &p_bool_lin_ne_reif); 01356 registry().add("bool_lin_le_reif", &p_bool_lin_le_reif); 01357 registry().add("bool_lin_lt_reif", &p_bool_lin_lt_reif); 01358 registry().add("bool_lin_ge_reif", &p_bool_lin_ge_reif); 01359 registry().add("bool_lin_gt_reif", &p_bool_lin_gt_reif); 01360 01361 registry().add("schedule_unary", &p_schedule_unary); 01362 registry().add("schedule_unary_optional", &p_schedule_unary_optional); 01363 01364 registry().add("circuit", &p_circuit); 01365 registry().add("circuit_cost_array", &p_circuit_cost_array); 01366 registry().add("circuit_cost", &p_circuit_cost); 01367 } 01368 }; 01369 IntPoster __int_poster; 01370 01371 #ifdef GECODE_HAS_SET_VARS 01372 void p_set_OP(FlatZincSpace& s, SetOpType op, 01373 const ConExpr& ce, AST::Node *) { 01374 rel(s, getSetVar(s, ce[0]), op, getSetVar(s, ce[1]), 01375 SRT_EQ, getSetVar(s, ce[2])); 01376 } 01377 void p_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 01378 p_set_OP(s, SOT_UNION, ce, ann); 01379 } 01380 void p_set_intersect(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 01381 p_set_OP(s, SOT_INTER, ce, ann); 01382 } 01383 void p_set_diff(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 01384 p_set_OP(s, SOT_MINUS, ce, ann); 01385 } 01386 01387 void p_set_symdiff(FlatZincSpace& s, const ConExpr& ce, AST::Node*) { 01388 SetVar x = getSetVar(s, ce[0]); 01389 SetVar y = getSetVar(s, ce[1]); 01390 01391 SetVarLubRanges xub(x); 01392 IntSet xubs(xub); 01393 SetVar x_y(s,IntSet::empty,xubs); 01394 rel(s, x, SOT_MINUS, y, SRT_EQ, x_y); 01395 01396 SetVarLubRanges yub(y); 01397 IntSet yubs(yub); 01398 SetVar y_x(s,IntSet::empty,yubs); 01399 rel(s, y, SOT_MINUS, x, SRT_EQ, y_x); 01400 01401 rel(s, x_y, SOT_UNION, y_x, SRT_EQ, getSetVar(s, ce[2])); 01402 } 01403 01404 void p_array_set_OP(FlatZincSpace& s, SetOpType op, 01405 const ConExpr& ce, AST::Node *) { 01406 SetVarArgs xs = arg2setvarargs(s, ce[0]); 01407 rel(s, op, xs, getSetVar(s, ce[1])); 01408 } 01409 void p_array_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 01410 p_array_set_OP(s, SOT_UNION, ce, ann); 01411 } 01412 void p_array_set_partition(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) { 01413 p_array_set_OP(s, SOT_DUNION, ce, ann); 01414 } 01415 01416 01417 void p_set_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 01418 rel(s, getSetVar(s, ce[0]), SRT_EQ, getSetVar(s, ce[1])); 01419 } 01420 void p_set_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 01421 rel(s, getSetVar(s, ce[0]), SRT_NQ, getSetVar(s, ce[1])); 01422 } 01423 void p_set_subset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 01424 rel(s, getSetVar(s, ce[0]), SRT_SUB, getSetVar(s, ce[1])); 01425 } 01426 void p_set_superset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 01427 rel(s, getSetVar(s, ce[0]), SRT_SUP, getSetVar(s, ce[1])); 01428 } 01429 void p_set_card(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 01430 if (!ce[1]->isIntVar()) { 01431 cardinality(s, getSetVar(s, ce[0]), ce[1]->getInt(), 01432 ce[1]->getInt()); 01433 } else { 01434 cardinality(s, getSetVar(s, ce[0]), getIntVar(s, ce[1])); 01435 } 01436 } 01437 void p_set_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 01438 if (!ce[1]->isSetVar()) { 01439 IntSet d = arg2intset(s,ce[1]); 01440 if (ce[0]->isBoolVar()) { 01441 IntSetRanges dr(d); 01442 Iter::Ranges::Singleton sr(0,1); 01443 Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr); 01444 IntSet d01(i); 01445 if (d01.size() == 0) { 01446 s.fail(); 01447 } else { 01448 rel(s, getBoolVar(s, ce[0]), IRT_GQ, d01.min()); 01449 rel(s, getBoolVar(s, ce[0]), IRT_LQ, d01.max()); 01450 } 01451 } else { 01452 dom(s, getIntVar(s, ce[0]), d); 01453 } 01454 } else { 01455 if (!ce[0]->isIntVar()) { 01456 dom(s, getSetVar(s, ce[1]), SRT_SUP, ce[0]->getInt()); 01457 } else { 01458 rel(s, getSetVar(s, ce[1]), SRT_SUP, getIntVar(s, ce[0])); 01459 } 01460 } 01461 } 01462 void p_set_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 01463 rel(s, getSetVar(s, ce[0]), SRT_EQ, getSetVar(s, ce[1]), 01464 getBoolVar(s, ce[2])); 01465 } 01466 void p_set_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 01467 rel(s, getSetVar(s, ce[0]), SRT_NQ, getSetVar(s, ce[1]), 01468 getBoolVar(s, ce[2])); 01469 } 01470 void p_set_subset_reif(FlatZincSpace& s, const ConExpr& ce, 01471 AST::Node *) { 01472 rel(s, getSetVar(s, ce[0]), SRT_SUB, getSetVar(s, ce[1]), 01473 getBoolVar(s, ce[2])); 01474 } 01475 void p_set_superset_reif(FlatZincSpace& s, const ConExpr& ce, 01476 AST::Node *) { 01477 rel(s, getSetVar(s, ce[0]), SRT_SUP, getSetVar(s, ce[1]), 01478 getBoolVar(s, ce[2])); 01479 } 01480 void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 01481 if (!ce[1]->isSetVar()) { 01482 IntSet d = arg2intset(s,ce[1]); 01483 if (ce[0]->isBoolVar()) { 01484 IntSetRanges dr(d); 01485 Iter::Ranges::Singleton sr(0,1); 01486 Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr); 01487 IntSet d01(i); 01488 if (d01.size() == 0) { 01489 rel(s, getBoolVar(s, ce[2]) == 0); 01490 } else if (d01.max() == 0) { 01491 rel(s, getBoolVar(s, ce[2]) == !getBoolVar(s, ce[0])); 01492 } else if (d01.min() == 1) { 01493 rel(s, getBoolVar(s, ce[2]) == getBoolVar(s, ce[0])); 01494 } else { 01495 rel(s, getBoolVar(s, ce[2]) == 1); 01496 } 01497 } else { 01498 dom(s, getIntVar(s, ce[0]), d, getBoolVar(s, ce[2])); 01499 } 01500 } else { 01501 if (!ce[0]->isIntVar()) { 01502 dom(s, getSetVar(s, ce[1]), SRT_SUP, ce[0]->getInt(), 01503 getBoolVar(s, ce[2])); 01504 } else { 01505 rel(s, getSetVar(s, ce[1]), SRT_SUP, getIntVar(s, ce[0]), 01506 getBoolVar(s, ce[2])); 01507 } 01508 } 01509 } 01510 void p_set_disjoint(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 01511 rel(s, getSetVar(s, ce[0]), SRT_DISJ, getSetVar(s, ce[1])); 01512 } 01513 01514 void p_array_set_element(FlatZincSpace& s, const ConExpr& ce, 01515 AST::Node*) { 01516 bool isConstant = true; 01517 AST::Array* a = ce[1]->getArray(); 01518 for (int i=a->a.size(); i--;) { 01519 if (a->a[i]->isSetVar()) { 01520 isConstant = false; 01521 break; 01522 } 01523 } 01524 IntVar selector = getIntVar(s, ce[0]); 01525 rel(s, selector > 0); 01526 if (isConstant) { 01527 IntSetArgs sv = arg2intsetargs(s,ce[1],1); 01528 element(s, sv, selector, getSetVar(s, ce[2])); 01529 } else { 01530 SetVarArgs sv = arg2setvarargs(s, ce[1], 1); 01531 element(s, sv, selector, getSetVar(s, ce[2])); 01532 } 01533 } 01534 01535 void p_array_set_element_op(FlatZincSpace& s, const ConExpr& ce, 01536 AST::Node*, SetOpType op, 01537 const IntSet& universe = 01538 IntSet(Set::Limits::min,Set::Limits::max)) { 01539 bool isConstant = true; 01540 AST::Array* a = ce[1]->getArray(); 01541 for (int i=a->a.size(); i--;) { 01542 if (a->a[i]->isSetVar()) { 01543 isConstant = false; 01544 break; 01545 } 01546 } 01547 SetVar selector = getSetVar(s, ce[0]); 01548 dom(s, selector, SRT_DISJ, 0); 01549 if (isConstant) { 01550 IntSetArgs sv = arg2intsetargs(s,ce[1], 1); 01551 element(s, op, sv, selector, getSetVar(s, ce[2]), universe); 01552 } else { 01553 SetVarArgs sv = arg2setvarargs(s, ce[1], 1); 01554 element(s, op, sv, selector, getSetVar(s, ce[2]), universe); 01555 } 01556 } 01557 01558 void p_array_set_element_union(FlatZincSpace& s, const ConExpr& ce, 01559 AST::Node* ann) { 01560 p_array_set_element_op(s, ce, ann, SOT_UNION); 01561 } 01562 01563 void p_array_set_element_intersect(FlatZincSpace& s, const ConExpr& ce, 01564 AST::Node* ann) { 01565 p_array_set_element_op(s, ce, ann, SOT_INTER); 01566 } 01567 01568 void p_array_set_element_intersect_in(FlatZincSpace& s, 01569 const ConExpr& ce, 01570 AST::Node* ann) { 01571 IntSet d = arg2intset(s, ce[3]); 01572 p_array_set_element_op(s, ce, ann, SOT_INTER, d); 01573 } 01574 01575 void p_array_set_element_partition(FlatZincSpace& s, const ConExpr& ce, 01576 AST::Node* ann) { 01577 p_array_set_element_op(s, ce, ann, SOT_DUNION); 01578 } 01579 01580 void p_set_convex(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 01581 convex(s, getSetVar(s, ce[0])); 01582 } 01583 01584 void p_array_set_seq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) { 01585 SetVarArgs sv = arg2setvarargs(s, ce[0]); 01586 sequence(s, sv); 01587 } 01588 01589 void p_array_set_seq_union(FlatZincSpace& s, const ConExpr& ce, 01590 AST::Node *) { 01591 SetVarArgs sv = arg2setvarargs(s, ce[0]); 01592 sequence(s, sv, getSetVar(s, ce[1])); 01593 } 01594 01595 class SetPoster { 01596 public: 01597 SetPoster(void) { 01598 registry().add("set_eq", &p_set_eq); 01599 registry().add("equal", &p_set_eq); 01600 registry().add("set_ne", &p_set_ne); 01601 registry().add("set_union", &p_set_union); 01602 registry().add("array_set_element", &p_array_set_element); 01603 registry().add("array_var_set_element", &p_array_set_element); 01604 registry().add("set_intersect", &p_set_intersect); 01605 registry().add("set_diff", &p_set_diff); 01606 registry().add("set_symdiff", &p_set_symdiff); 01607 registry().add("set_subset", &p_set_subset); 01608 registry().add("set_superset", &p_set_superset); 01609 registry().add("set_card", &p_set_card); 01610 registry().add("set_in", &p_set_in); 01611 registry().add("set_eq_reif", &p_set_eq_reif); 01612 registry().add("equal_reif", &p_set_eq_reif); 01613 registry().add("set_ne_reif", &p_set_ne_reif); 01614 registry().add("set_subset_reif", &p_set_subset_reif); 01615 registry().add("set_superset_reif", &p_set_superset_reif); 01616 registry().add("set_in_reif", &p_set_in_reif); 01617 registry().add("disjoint", &p_set_disjoint); 01618 01619 registry().add("array_set_union", &p_array_set_union); 01620 registry().add("array_set_partition", &p_array_set_partition); 01621 registry().add("set_convex", &p_set_convex); 01622 registry().add("array_set_seq", &p_array_set_seq); 01623 registry().add("array_set_seq_union", &p_array_set_seq_union); 01624 registry().add("array_set_element_union", 01625 &p_array_set_element_union); 01626 registry().add("array_set_element_intersect", 01627 &p_array_set_element_intersect); 01628 registry().add("array_set_element_intersect_in", 01629 &p_array_set_element_intersect_in); 01630 registry().add("array_set_element_partition", 01631 &p_array_set_element_partition); 01632 } 01633 }; 01634 SetPoster __set_poster; 01635 #endif 01636 01637 } 01638 }} 01639 01640 // STATISTICS: flatzinc-any