00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038
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 true;
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
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
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
00565
00566 void p_int_plus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00567 if (!ce[0]->isIntVar()) {
00568 post(s, ce[0]->getInt() + getIntVar(s, ce[1])
00569 == getIntVar(s,ce[2]), ann2icl(ann));
00570 } else if (!ce[1]->isIntVar()) {
00571 post(s, getIntVar(s,ce[0]) + ce[1]->getInt()
00572 == getIntVar(s,ce[2]), ann2icl(ann));
00573 } else if (!ce[2]->isIntVar()) {
00574 post(s, getIntVar(s,ce[0]) + getIntVar(s,ce[1])
00575 == ce[2]->getInt(), ann2icl(ann));
00576 } else {
00577 post(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 post(s, ce[0]->getInt() - getIntVar(s, ce[1])
00585 == getIntVar(s,ce[2]), ann2icl(ann));
00586 } else if (!ce[1]->isIntVar()) {
00587 post(s, getIntVar(s,ce[0]) - ce[1]->getInt()
00588 == getIntVar(s,ce[2]), ann2icl(ann));
00589 } else if (!ce[2]->isIntVar()) {
00590 post(s, getIntVar(s,ce[0]) - getIntVar(s,ce[1])
00591 == ce[2]->getInt(), ann2icl(ann));
00592 } else {
00593 post(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 post(s, x0 == -x1, ann2icl(ann));
00633 }
00634
00635
00636 void p_bool_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
00637 AST::Node* ann) {
00638 if (ce[0]->isBoolVar()) {
00639 if (ce[1]->isBoolVar()) {
00640 rel(s, getBoolVar(s, ce[0]), irt, getBoolVar(s, ce[1]),
00641 ann2icl(ann));
00642 } else {
00643 rel(s, getBoolVar(s, ce[0]), irt, ce[1]->getBool(), ann2icl(ann));
00644 }
00645 } else {
00646 if (ce[1]->isBoolVar()) {
00647 rel(s, getBoolVar(s, ce[1]), swap(irt), ce[0]->getBool(),
00648 ann2icl(ann));
00649 } else {
00650 if (ce[0]->getBool() != ce[1]->getBool())
00651 s.fail();
00652 }
00653 }
00654 }
00655 void p_bool_CMP_reif(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
00656 AST::Node* ann) {
00657 rel(s, getBoolVar(s, ce[0]), irt, getBoolVar(s, ce[1]),
00658 getBoolVar(s, ce[2]), ann2icl(ann));
00659 }
00660 void p_bool_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00661 p_bool_CMP(s, IRT_EQ, ce, ann);
00662 }
00663 void p_bool_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00664 p_bool_CMP_reif(s, IRT_EQ, ce, ann);
00665 }
00666 void p_bool_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00667 p_bool_CMP(s, IRT_NQ, ce, ann);
00668 }
00669 void p_bool_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00670 p_bool_CMP_reif(s, IRT_NQ, ce, ann);
00671 }
00672 void p_bool_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00673 p_bool_CMP(s, IRT_GQ, ce, ann);
00674 }
00675 void p_bool_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00676 p_bool_CMP_reif(s, IRT_GQ, ce, ann);
00677 }
00678 void p_bool_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00679 p_bool_CMP(s, IRT_LQ, ce, ann);
00680 }
00681 void p_bool_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00682 p_bool_CMP_reif(s, IRT_LQ, ce, ann);
00683 }
00684 void p_bool_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00685 p_bool_CMP(s, IRT_GR, ce, ann);
00686 }
00687 void p_bool_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00688 p_bool_CMP_reif(s, IRT_GR, ce, ann);
00689 }
00690 void p_bool_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00691 p_bool_CMP(s, IRT_LE, ce, ann);
00692 }
00693 void p_bool_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00694 p_bool_CMP_reif(s, IRT_LE, ce, ann);
00695 }
00696
00697 #define BOOL_OP(op) \
00698 BoolVar b0 = getBoolVar(s, ce[0]); \
00699 BoolVar b1 = getBoolVar(s, ce[1]); \
00700 if (ce[2]->isBool()) { \
00701 rel(s, b0, op, b1, ce[2]->getBool(), ann2icl(ann)); \
00702 } else { \
00703 rel(s, b0, op, b1, s.bv[ce[2]->getBoolVar()], ann2icl(ann)); \
00704 }
00705
00706 #define BOOL_ARRAY_OP(op) \
00707 BoolVarArgs bv = arg2boolvarargs(s, ce[0]); \
00708 if (ce[1]->isBool()) { \
00709 rel(s, op, bv, ce[1]->getBool(), ann2icl(ann)); \
00710 } else { \
00711 rel(s, op, bv, s.bv[ce[1]->getBoolVar()], ann2icl(ann)); \
00712 }
00713
00714 void p_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00715 BOOL_OP(BOT_OR);
00716 }
00717 void p_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00718 BOOL_OP(BOT_AND);
00719 }
00720 void p_array_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00721 {
00722 BOOL_ARRAY_OP(BOT_AND);
00723 }
00724 void p_array_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00725 {
00726 BOOL_ARRAY_OP(BOT_OR);
00727 }
00728 void p_array_bool_clause(FlatZincSpace& s, const ConExpr& ce,
00729 AST::Node* ann) {
00730 BoolVarArgs bvp = arg2boolvarargs(s, ce[0]);
00731 BoolVarArgs bvn = arg2boolvarargs(s, ce[1]);
00732 clause(s, BOT_OR, bvp, bvn, 1, ann2icl(ann));
00733 }
00734 void p_array_bool_clause_reif(FlatZincSpace& s, const ConExpr& ce,
00735 AST::Node* ann) {
00736 BoolVarArgs bvp = arg2boolvarargs(s, ce[0]);
00737 BoolVarArgs bvn = arg2boolvarargs(s, ce[1]);
00738 BoolVar b0 = getBoolVar(s, ce[2]);
00739 clause(s, BOT_OR, bvp, bvn, b0, ann2icl(ann));
00740 }
00741 void p_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00742 BOOL_OP(BOT_XOR);
00743 }
00744 void p_bool_l_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00745 BoolVar b0 = getBoolVar(s, ce[0]);
00746 BoolVar b1 = getBoolVar(s, ce[1]);
00747 if (ce[2]->isBool()) {
00748 rel(s, b1, BOT_IMP, b0, ce[2]->getBool(), ann2icl(ann));
00749 } else {
00750 rel(s, b1, BOT_IMP, b0, s.bv[ce[2]->getBoolVar()], ann2icl(ann));
00751 }
00752 }
00753 void p_bool_r_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00754 BOOL_OP(BOT_IMP);
00755 }
00756 void p_bool_not(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00757 BoolVar x0 = getBoolVar(s, ce[0]);
00758 BoolVar x1 = getBoolVar(s, ce[1]);
00759 rel(s, x0, BOT_XOR, x1, 1, ann2icl(ann));
00760 }
00761
00762
00763 void p_array_int_element(FlatZincSpace& s, const ConExpr& ce,
00764 AST::Node* ann) {
00765 bool isConstant = true;
00766 AST::Array* a = ce[1]->getArray();
00767 for (int i=a->a.size(); i--;) {
00768 if (!a->a[i]->isInt()) {
00769 isConstant = false;
00770 break;
00771 }
00772 }
00773 IntVar selector = getIntVar(s, ce[0]);
00774 post(s, selector > 0);
00775 if (isConstant) {
00776 IntArgs ia = arg2intargs(ce[1], 1);
00777 element(s, ia, selector, getIntVar(s, ce[2]), ann2icl(ann));
00778 } else {
00779 IntVarArgs iv = arg2intvarargs(s, ce[1], 1);
00780 element(s, iv, selector, getIntVar(s, ce[2]), ann2icl(ann));
00781 }
00782 }
00783 void p_array_bool_element(FlatZincSpace& s, const ConExpr& ce,
00784 AST::Node* ann) {
00785 bool isConstant = true;
00786 AST::Array* a = ce[1]->getArray();
00787 for (int i=a->a.size(); i--;) {
00788 if (!a->a[i]->isBool()) {
00789 isConstant = false;
00790 break;
00791 }
00792 }
00793 IntVar selector = getIntVar(s, ce[0]);
00794 post(s, selector > 0);
00795 if (isConstant) {
00796 IntArgs ia = arg2boolargs(ce[1], 1);
00797 element(s, ia, selector, getBoolVar(s, ce[2]), ann2icl(ann));
00798 } else {
00799 BoolVarArgs iv = arg2boolvarargs(s, ce[1], 1);
00800 element(s, iv, selector, getBoolVar(s, ce[2]), ann2icl(ann));
00801 }
00802 }
00803
00804
00805 void p_bool2int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00806 BoolVar x0 = getBoolVar(s, ce[0]);
00807 IntVar x1 = getIntVar(s, ce[1]);
00808 if (ce[0]->isBoolVar() && ce[1]->isIntVar()) {
00809 s.aliasBool2Int(ce[1]->getIntVar(), ce[0]->getBoolVar());
00810 }
00811 channel(s, x0, x1, ann2icl(ann));
00812 }
00813
00814 void p_int_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
00815 IntSet d = arg2intset(s,ce[1]);
00816 if (ce[0]->isBoolVar()) {
00817 IntSetRanges dr(d);
00818 Iter::Ranges::Singleton sr(0,1);
00819 Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
00820 IntSet d01(i);
00821 if (d01.size() == 0) {
00822 s.fail();
00823 } else {
00824 rel(s, getBoolVar(s, ce[0]), IRT_GQ, d01.min());
00825 rel(s, getBoolVar(s, ce[0]), IRT_LQ, d01.max());
00826 }
00827 } else {
00828 dom(s, getIntVar(s, ce[0]), d);
00829 }
00830 }
00831
00832
00833
00834 void p_abs(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00835 IntVar x0 = getIntVar(s, ce[0]);
00836 IntVar x1 = getIntVar(s, ce[1]);
00837 abs(s, x0, x1, ann2icl(ann));
00838 }
00839
00840 void p_array_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00841 IntVarArgs iv0 = arg2intvarargs(s, ce[0]);
00842 IntVarArgs iv1 = arg2intvarargs(s, ce[1]);
00843 rel(s, iv0, IRT_LE, iv1, ann2icl(ann));
00844 }
00845
00846 void p_array_int_lq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00847 IntVarArgs iv0 = arg2intvarargs(s, ce[0]);
00848 IntVarArgs iv1 = arg2intvarargs(s, ce[1]);
00849 rel(s, iv0, IRT_LQ, iv1, ann2icl(ann));
00850 }
00851
00852 void p_count(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00853 IntVarArgs iv = arg2intvarargs(s, ce[0]);
00854 if (!ce[1]->isIntVar()) {
00855 if (!ce[2]->isIntVar()) {
00856 count(s, iv, ce[1]->getInt(), IRT_EQ, ce[2]->getInt(),
00857 ann2icl(ann));
00858 } else {
00859 count(s, iv, ce[1]->getInt(), IRT_EQ, getIntVar(s, ce[2]),
00860 ann2icl(ann));
00861 }
00862 } else if (!ce[2]->isIntVar()) {
00863 count(s, iv, getIntVar(s, ce[1]), IRT_EQ, ce[2]->getInt(),
00864 ann2icl(ann));
00865 } else {
00866 count(s, iv, getIntVar(s, ce[1]), IRT_EQ, getIntVar(s, ce[2]),
00867 ann2icl(ann));
00868 }
00869 }
00870
00871 void count_rel(IntRelType irt,
00872 FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00873 IntVarArgs iv = arg2intvarargs(s, ce[1]);
00874 count(s, iv, ce[2]->getInt(), irt, ce[0]->getInt(), ann2icl(ann));
00875 }
00876
00877 void p_at_most(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00878 count_rel(IRT_LQ, s, ce, ann);
00879 }
00880
00881 void p_at_least(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00882 count_rel(IRT_GQ, s, ce, ann);
00883 }
00884
00885 void p_global_cardinality(FlatZincSpace& s, const ConExpr& ce,
00886 AST::Node* ann) {
00887 IntVarArgs iv0 = arg2intvarargs(s, ce[0]);
00888 IntVarArgs iv1 = arg2intvarargs(s, ce[1]);
00889 int cmin = ce[2]->getInt();
00890
00891 int smallest = cmin;
00892 int largest = iv1.size()-1;
00893 for (int i=iv0.size(); i--;) {
00894 smallest = std::min(smallest, iv0[i].min());
00895 largest = std::max(largest, iv0[i].max());
00896 }
00897
00898
00899 if (cmin == 0 && smallest == 0 && largest == iv1.size()-1) {
00900 count(s, iv0, iv1, ann2icl(ann));
00901 } else {
00902 IntArgs values(largest - smallest + 1);
00903 for (int i=largest-smallest+1; i--;)
00904 values[i] = i+smallest;
00905 IntVarArgs iv1tmp(largest-smallest+1);
00906 int k = 0;
00907 for (int i=cmin-smallest; i--;) {
00908 iv1tmp[k++] = IntVar(s, 0, iv0.size());
00909 }
00910 for (int i=0; i<iv1.size(); i++)
00911 iv1tmp[k++] = iv1[i];
00912 for (int i=k; i<iv1tmp.size(); i++) {
00913 iv1tmp[i] = IntVar(s, 0, iv0.size());
00914 }
00915 count(s, iv0, iv1tmp, values, ann2icl(ann));
00916 }
00917 }
00918
00919 void p_minimum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00920 IntVarArgs iv = arg2intvarargs(s, ce[1]);
00921 min(s, iv, getIntVar(s, ce[0]), ann2icl(ann));
00922 }
00923
00924 void p_maximum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00925 IntVarArgs iv = arg2intvarargs(s, ce[1]);
00926 max(s, iv, getIntVar(s, ce[0]), ann2icl(ann));
00927 }
00928
00929 void p_regular(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00930 IntVarArgs iv = arg2intvarargs(s, ce[0]);
00931 int q = ce[1]->getInt();
00932 int symbols = ce[2]->getInt();
00933 IntArgs d = arg2intargs(ce[3]);
00934 int q0 = ce[4]->getInt();
00935
00936 int noOfTrans = 0;
00937 for (int i=1; i<=q; i++) {
00938 for (int j=1; j<=symbols; j++) {
00939 if (d[(i-1)*symbols+(j-1)] > 0)
00940 noOfTrans++;
00941 }
00942 }
00943
00944 Region re(s);
00945 DFA::Transition* t = re.alloc<DFA::Transition>(noOfTrans+1);
00946 noOfTrans = 0;
00947 for (int i=1; i<=q; i++) {
00948 for (int j=1; j<=symbols; j++) {
00949 if (d[(i-1)*symbols+(j-1)] > 0) {
00950 t[noOfTrans].i_state = i;
00951 t[noOfTrans].symbol = j;
00952 t[noOfTrans].o_state = d[(i-1)*symbols+(j-1)];
00953 noOfTrans++;
00954 }
00955 }
00956 }
00957 t[noOfTrans].i_state = -1;
00958
00959
00960 AST::SetLit* sl = ce[5]->getSet();
00961 int* f;
00962 if (sl->interval) {
00963 f = static_cast<int*>(malloc(sizeof(int)*(sl->max-sl->min+2)));
00964 for (int i=sl->min; i<=sl->max; i++)
00965 f[i-sl->min] = i;
00966 f[sl->max-sl->min+1] = -1;
00967 } else {
00968 f = static_cast<int*>(malloc(sizeof(int)*(sl->s.size()+1)));
00969 for (int j=sl->s.size(); j--; )
00970 f[j] = sl->s[j];
00971 f[sl->s.size()] = -1;
00972 }
00973
00974 DFA dfa(q0,t,f);
00975 free(f);
00976 extensional(s, iv, dfa, ann2icl(ann));
00977 }
00978
00979 void
00980 p_sort(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00981 IntVarArgs x = arg2intvarargs(s, ce[0]);
00982 IntVarArgs y = arg2intvarargs(s, ce[1]);
00983 IntVarArgs xy(x.size()+y.size());
00984 for (int i=x.size(); i--;)
00985 xy[i] = x[i];
00986 for (int i=y.size(); i--;)
00987 xy[i+x.size()] = y[i];
00988 unshare(s, xy);
00989 for (int i=x.size(); i--;)
00990 x[i] = xy[i];
00991 for (int i=y.size(); i--;)
00992 y[i] = xy[i+x.size()];
00993 sorted(s, x, y, ann2icl(ann));
00994 }
00995
00996 void
00997 p_inverse_offsets(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00998 IntVarArgs x = arg2intvarargs(s, ce[0]);
00999 int xoff = ce[1]->getInt();
01000 IntVarArgs y = arg2intvarargs(s, ce[2]);
01001 int yoff = ce[3]->getInt();
01002 channel(s, x, xoff, y, yoff, ann2icl(ann));
01003 }
01004
01005 void
01006 p_increasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01007 IntVarArgs x = arg2intvarargs(s, ce[0]);
01008 rel(s,x,IRT_LQ,ann2icl(ann));
01009 }
01010
01011 void
01012 p_increasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01013 BoolVarArgs x = arg2boolvarargs(s, ce[0]);
01014 rel(s,x,IRT_LQ,ann2icl(ann));
01015 }
01016
01017 void
01018 p_decreasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01019 IntVarArgs x = arg2intvarargs(s, ce[0]);
01020 rel(s,x,IRT_GQ,ann2icl(ann));
01021 }
01022
01023 void
01024 p_decreasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01025 BoolVarArgs x = arg2boolvarargs(s, ce[0]);
01026 rel(s,x,IRT_GQ,ann2icl(ann));
01027 }
01028
01029 void
01030 p_table_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01031 IntVarArgs x = arg2intvarargs(s, ce[0]);
01032 IntArgs tuples = arg2intargs(ce[1]);
01033 int noOfVars = x.size();
01034 int noOfTuples = tuples.size()/noOfVars;
01035 TupleSet ts;
01036 for (int i=0; i<noOfTuples; i++) {
01037 IntArgs t(noOfVars);
01038 for (int j=0; j<x.size(); j++) {
01039 t[j] = tuples[i*noOfVars+j];
01040 }
01041 ts.add(t);
01042 }
01043 ts.finalize();
01044 extensional(s,x,ts,EPK_DEF,ann2icl(ann));
01045 }
01046 void
01047 p_table_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01048 BoolVarArgs x = arg2boolvarargs(s, ce[0]);
01049 IntArgs tuples = arg2boolargs(ce[1]);
01050 int noOfVars = x.size();
01051 int noOfTuples = tuples.size()/noOfVars;
01052 TupleSet ts;
01053 for (int i=0; i<noOfTuples; i++) {
01054 IntArgs t(noOfVars);
01055 for (int j=0; j<x.size(); j++) {
01056 t[j] = tuples[i*noOfVars+j];
01057 }
01058 ts.add(t);
01059 }
01060 ts.finalize();
01061 extensional(s,x,ts,EPK_DEF,ann2icl(ann));
01062 }
01063
01064 void p_cumulatives(FlatZincSpace& s, const ConExpr& ce,
01065 AST::Node* ann) {
01066 IntVarArgs start = arg2intvarargs(s, ce[0]);
01067 IntVarArgs duration = arg2intvarargs(s, ce[1]);
01068 IntVarArgs height = arg2intvarargs(s, ce[2]);
01069 int n = start.size();
01070 IntVar bound = getIntVar(s, ce[3]);
01071
01072 if (bound.assigned()) {
01073 IntArgs machine(n);
01074 for (int i = n; i--; ) machine[i] = 0;
01075 IntArgs limit(1, bound.val());
01076 IntVarArgs end(n);
01077 for (int i = n; i--; ) end[i] = IntVar(s, 0, Int::Limits::max);
01078 cumulatives(s, machine, start, duration, end, height, limit, true,
01079 ann2icl(ann));
01080 } else {
01081 int min = Gecode::Int::Limits::max;
01082 int max = Gecode::Int::Limits::min;
01083 IntVarArgs end(start.size());
01084 for (int i = start.size(); i--; ) {
01085 min = std::min(min, start[i].min());
01086 max = std::max(max, start[i].max() + duration[i].max());
01087 end[i] = post(s, start[i] + duration[i]);
01088 }
01089 for (int time = min; time < max; ++time) {
01090 IntVarArgs x(start.size());
01091 for (int i = start.size(); i--; ) {
01092 IntVar overlaps = channel(s, post(s, (~(start[i] <= time) &&
01093 ~(time < end[i]))));
01094 x[i] = mult(s, overlaps, height[i]);
01095 }
01096 linear(s, x, IRT_LQ, bound);
01097 }
01098 }
01099 }
01100
01101 void p_among_seq_int(FlatZincSpace& s, const ConExpr& ce,
01102 AST::Node* ann) {
01103 IntVarArgs x = arg2intvarargs(s, ce[0]);
01104 IntSet S = arg2intset(s, ce[1]);
01105 int q = ce[2]->getInt();
01106 int l = ce[3]->getInt();
01107 int u = ce[4]->getInt();
01108 sequence(s, x, S, q, l, u, ann2icl(ann));
01109 }
01110
01111 void p_among_seq_bool(FlatZincSpace& s, const ConExpr& ce,
01112 AST::Node* ann) {
01113 BoolVarArgs x = arg2boolvarargs(s, ce[0]);
01114 bool val = ce[1]->getBool();
01115 int q = ce[2]->getInt();
01116 int l = ce[3]->getInt();
01117 int u = ce[4]->getInt();
01118 IntSet S(val, val);
01119 sequence(s, x, S, q, l, u, ann2icl(ann));
01120 }
01121
01122 void p_schedule_unary(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
01123 IntVarArgs x = arg2intvarargs(s, ce[0]);
01124 IntArgs p = arg2intargs(ce[1]);
01125 unary(s, x, p);
01126 }
01127
01128 void p_schedule_unary_optional(FlatZincSpace& s, const ConExpr& ce,
01129 AST::Node*) {
01130 IntVarArgs x = arg2intvarargs(s, ce[0]);
01131 IntArgs p = arg2intargs(ce[1]);
01132 BoolVarArgs m = arg2boolvarargs(s, ce[2]);
01133 unary(s, x, p, m);
01134 }
01135
01136 void p_circuit(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01137 IntVarArgs xv = arg2intvarargs(s, ce[0]);
01138 circuit(s,xv,ann2icl(ann));
01139 }
01140 void p_circuit_cost_array(FlatZincSpace& s, const ConExpr& ce,
01141 AST::Node *ann) {
01142 IntArgs c = arg2intargs(ce[0]);
01143 IntVarArgs xv = arg2intvarargs(s, ce[1]);
01144 IntVarArgs yv = arg2intvarargs(s, ce[2]);
01145 IntVar z = getIntVar(s, ce[3]);
01146 circuit(s,c,xv,yv,z,ann2icl(ann));
01147 }
01148 void p_circuit_cost(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01149 IntArgs c = arg2intargs(ce[0]);
01150 IntVarArgs xv = arg2intvarargs(s, ce[1]);
01151 IntVar z = getIntVar(s, ce[2]);
01152 circuit(s,c,xv,z,ann2icl(ann));
01153 }
01154
01155 class IntPoster {
01156 public:
01157 IntPoster(void) {
01158 registry().add("all_different_int", &p_distinct);
01159 registry().add("all_different_offset", &p_distinctOffset);
01160 registry().add("all_equal_int", &p_all_equal);
01161 registry().add("int_eq", &p_int_eq);
01162 registry().add("int_ne", &p_int_ne);
01163 registry().add("int_ge", &p_int_ge);
01164 registry().add("int_gt", &p_int_gt);
01165 registry().add("int_le", &p_int_le);
01166 registry().add("int_lt", &p_int_lt);
01167 registry().add("int_eq_reif", &p_int_eq_reif);
01168 registry().add("int_ne_reif", &p_int_ne_reif);
01169 registry().add("int_ge_reif", &p_int_ge_reif);
01170 registry().add("int_gt_reif", &p_int_gt_reif);
01171 registry().add("int_le_reif", &p_int_le_reif);
01172 registry().add("int_lt_reif", &p_int_lt_reif);
01173 registry().add("int_lin_eq", &p_int_lin_eq);
01174 registry().add("int_lin_eq_reif", &p_int_lin_eq_reif);
01175 registry().add("int_lin_ne", &p_int_lin_ne);
01176 registry().add("int_lin_ne_reif", &p_int_lin_ne_reif);
01177 registry().add("int_lin_le", &p_int_lin_le);
01178 registry().add("int_lin_le_reif", &p_int_lin_le_reif);
01179 registry().add("int_lin_lt", &p_int_lin_lt);
01180 registry().add("int_lin_lt_reif", &p_int_lin_lt_reif);
01181 registry().add("int_lin_ge", &p_int_lin_ge);
01182 registry().add("int_lin_ge_reif", &p_int_lin_ge_reif);
01183 registry().add("int_lin_gt", &p_int_lin_gt);
01184 registry().add("int_lin_gt_reif", &p_int_lin_gt_reif);
01185 registry().add("int_plus", &p_int_plus);
01186 registry().add("int_minus", &p_int_minus);
01187 registry().add("int_times", &p_int_times);
01188 registry().add("int_div", &p_int_div);
01189 registry().add("int_mod", &p_int_mod);
01190 registry().add("int_min", &p_int_min);
01191 registry().add("int_max", &p_int_max);
01192 registry().add("int_abs", &p_abs);
01193 registry().add("int_negate", &p_int_negate);
01194 registry().add("bool_eq", &p_bool_eq);
01195 registry().add("bool_eq_reif", &p_bool_eq_reif);
01196 registry().add("bool_ne", &p_bool_ne);
01197 registry().add("bool_ne_reif", &p_bool_ne_reif);
01198 registry().add("bool_ge", &p_bool_ge);
01199 registry().add("bool_ge_reif", &p_bool_ge_reif);
01200 registry().add("bool_le", &p_bool_le);
01201 registry().add("bool_le_reif", &p_bool_le_reif);
01202 registry().add("bool_gt", &p_bool_gt);
01203 registry().add("bool_gt_reif", &p_bool_gt_reif);
01204 registry().add("bool_lt", &p_bool_lt);
01205 registry().add("bool_lt_reif", &p_bool_lt_reif);
01206 registry().add("bool_or", &p_bool_or);
01207 registry().add("bool_and", &p_bool_and);
01208 registry().add("bool_xor", &p_bool_xor);
01209 registry().add("array_bool_and", &p_array_bool_and);
01210 registry().add("array_bool_or", &p_array_bool_or);
01211 registry().add("bool_clause", &p_array_bool_clause);
01212 registry().add("bool_clause_reif", &p_array_bool_clause_reif);
01213 registry().add("bool_left_imp", &p_bool_l_imp);
01214 registry().add("bool_right_imp", &p_bool_r_imp);
01215 registry().add("bool_not", &p_bool_not);
01216 registry().add("array_int_element", &p_array_int_element);
01217 registry().add("array_var_int_element", &p_array_int_element);
01218 registry().add("array_bool_element", &p_array_bool_element);
01219 registry().add("array_var_bool_element", &p_array_bool_element);
01220 registry().add("bool2int", &p_bool2int);
01221 registry().add("int_in", &p_int_in);
01222
01223 registry().add("array_int_lt", &p_array_int_lt);
01224 registry().add("array_int_lq", &p_array_int_lq);
01225 registry().add("count", &p_count);
01226 registry().add("at_least_int", &p_at_least);
01227 registry().add("at_most_int", &p_at_most);
01228 registry().add("global_cardinality_gecode", &p_global_cardinality);
01229 registry().add("minimum_int", &p_minimum);
01230 registry().add("maximum_int", &p_maximum);
01231 registry().add("regular", &p_regular);
01232 registry().add("sort", &p_sort);
01233 registry().add("inverse_offsets", &p_inverse_offsets);
01234 registry().add("increasing_int", &p_increasing_int);
01235 registry().add("increasing_bool", &p_increasing_bool);
01236 registry().add("decreasing_int", &p_decreasing_int);
01237 registry().add("decreasing_bool", &p_decreasing_bool);
01238 registry().add("table_int", &p_table_int);
01239 registry().add("table_bool", &p_table_bool);
01240 registry().add("cumulatives", &p_cumulatives);
01241 registry().add("among_seq_int", &p_among_seq_int);
01242 registry().add("among_seq_bool", &p_among_seq_bool);
01243
01244 registry().add("bool_lin_eq", &p_bool_lin_eq);
01245 registry().add("bool_lin_ne", &p_bool_lin_ne);
01246 registry().add("bool_lin_le", &p_bool_lin_le);
01247 registry().add("bool_lin_lt", &p_bool_lin_lt);
01248 registry().add("bool_lin_ge", &p_bool_lin_ge);
01249 registry().add("bool_lin_gt", &p_bool_lin_gt);
01250
01251 registry().add("bool_lin_eq_reif", &p_bool_lin_eq_reif);
01252 registry().add("bool_lin_ne_reif", &p_bool_lin_ne_reif);
01253 registry().add("bool_lin_le_reif", &p_bool_lin_le_reif);
01254 registry().add("bool_lin_lt_reif", &p_bool_lin_lt_reif);
01255 registry().add("bool_lin_ge_reif", &p_bool_lin_ge_reif);
01256 registry().add("bool_lin_gt_reif", &p_bool_lin_gt_reif);
01257
01258 registry().add("schedule_unary", &p_schedule_unary);
01259 registry().add("schedule_unary_optional", &p_schedule_unary_optional);
01260
01261 registry().add("circuit", &p_circuit);
01262 registry().add("circuit_cost_array", &p_circuit_cost_array);
01263 registry().add("circuit_cost", &p_circuit_cost);
01264 }
01265 };
01266 IntPoster __int_poster;
01267
01268 #ifdef GECODE_HAS_SET_VARS
01269 void p_set_OP(FlatZincSpace& s, SetOpType op,
01270 const ConExpr& ce, AST::Node *) {
01271 rel(s, getSetVar(s, ce[0]), op, getSetVar(s, ce[1]),
01272 SRT_EQ, getSetVar(s, ce[2]));
01273 }
01274 void p_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01275 p_set_OP(s, SOT_UNION, ce, ann);
01276 }
01277 void p_set_intersect(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01278 p_set_OP(s, SOT_INTER, ce, ann);
01279 }
01280 void p_set_diff(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01281 p_set_OP(s, SOT_MINUS, ce, ann);
01282 }
01283
01284 void p_set_symdiff(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
01285 SetVar x = getSetVar(s, ce[0]);
01286 SetVar y = getSetVar(s, ce[1]);
01287
01288 SetVarLubRanges xub(x);
01289 IntSet xubs(xub);
01290 SetVar x_y(s,IntSet::empty,xubs);
01291 rel(s, x, SOT_MINUS, y, SRT_EQ, x_y);
01292
01293 SetVarLubRanges yub(y);
01294 IntSet yubs(yub);
01295 SetVar y_x(s,IntSet::empty,yubs);
01296 rel(s, y, SOT_MINUS, x, SRT_EQ, y_x);
01297
01298 rel(s, x_y, SOT_UNION, y_x, SRT_EQ, getSetVar(s, ce[2]));
01299 }
01300
01301 void p_array_set_OP(FlatZincSpace& s, SetOpType op,
01302 const ConExpr& ce, AST::Node *) {
01303 SetVarArgs xs = arg2setvarargs(s, ce[0]);
01304 rel(s, op, xs, getSetVar(s, ce[1]));
01305 }
01306 void p_array_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01307 p_array_set_OP(s, SOT_UNION, ce, ann);
01308 }
01309 void p_array_set_partition(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01310 p_array_set_OP(s, SOT_DUNION, ce, ann);
01311 }
01312
01313
01314 void p_set_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01315 rel(s, getSetVar(s, ce[0]), SRT_EQ, getSetVar(s, ce[1]));
01316 }
01317 void p_set_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01318 rel(s, getSetVar(s, ce[0]), SRT_NQ, getSetVar(s, ce[1]));
01319 }
01320 void p_set_subset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01321 rel(s, getSetVar(s, ce[0]), SRT_SUB, getSetVar(s, ce[1]));
01322 }
01323 void p_set_superset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01324 rel(s, getSetVar(s, ce[0]), SRT_SUP, getSetVar(s, ce[1]));
01325 }
01326 void p_set_card(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01327 if (!ce[1]->isIntVar()) {
01328 cardinality(s, getSetVar(s, ce[0]), ce[1]->getInt(),
01329 ce[1]->getInt());
01330 } else {
01331 cardinality(s, getSetVar(s, ce[0]), getIntVar(s, ce[1]));
01332 }
01333 }
01334 void p_set_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01335 if (!ce[1]->isSetVar()) {
01336 IntSet d = arg2intset(s,ce[1]);
01337 if (ce[0]->isBoolVar()) {
01338 IntSetRanges dr(d);
01339 Iter::Ranges::Singleton sr(0,1);
01340 Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
01341 IntSet d01(i);
01342 if (d01.size() == 0) {
01343 s.fail();
01344 } else {
01345 rel(s, getBoolVar(s, ce[0]), IRT_GQ, d01.min());
01346 rel(s, getBoolVar(s, ce[0]), IRT_LQ, d01.max());
01347 }
01348 } else {
01349 dom(s, getIntVar(s, ce[0]), d);
01350 }
01351 } else {
01352 if (!ce[0]->isIntVar()) {
01353 dom(s, getSetVar(s, ce[1]), SRT_SUP, ce[0]->getInt());
01354 } else {
01355 rel(s, getSetVar(s, ce[1]), SRT_SUP, getIntVar(s, ce[0]));
01356 }
01357 }
01358 }
01359 void p_set_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01360 rel(s, getSetVar(s, ce[0]), SRT_EQ, getSetVar(s, ce[1]),
01361 getBoolVar(s, ce[2]));
01362 }
01363 void p_set_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01364 rel(s, getSetVar(s, ce[0]), SRT_NQ, getSetVar(s, ce[1]),
01365 getBoolVar(s, ce[2]));
01366 }
01367 void p_set_subset_reif(FlatZincSpace& s, const ConExpr& ce,
01368 AST::Node *) {
01369 rel(s, getSetVar(s, ce[0]), SRT_SUB, getSetVar(s, ce[1]),
01370 getBoolVar(s, ce[2]));
01371 }
01372 void p_set_superset_reif(FlatZincSpace& s, const ConExpr& ce,
01373 AST::Node *) {
01374 rel(s, getSetVar(s, ce[0]), SRT_SUP, getSetVar(s, ce[1]),
01375 getBoolVar(s, ce[2]));
01376 }
01377 void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01378 if (!ce[1]->isSetVar()) {
01379 IntSet d = arg2intset(s,ce[1]);
01380 if (ce[0]->isBoolVar()) {
01381 IntSetRanges dr(d);
01382 Iter::Ranges::Singleton sr(0,1);
01383 Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
01384 IntSet d01(i);
01385 if (d01.size() == 0) {
01386 post(s, getBoolVar(s, ce[2]) == 0);
01387 } else if (d01.max() == 0) {
01388 post(s, tt(eqv(getBoolVar(s, ce[2]), !getBoolVar(s, ce[0]))));
01389 } else if (d01.min() == 1) {
01390 post(s, getBoolVar(s, ce[2]) == getBoolVar(s, ce[0]));
01391 } else {
01392 post(s, getBoolVar(s, ce[2]) == 1);
01393 }
01394 } else {
01395 dom(s, getIntVar(s, ce[0]), d, getBoolVar(s, ce[2]));
01396 }
01397 } else {
01398 if (!ce[0]->isIntVar()) {
01399 dom(s, getSetVar(s, ce[1]), SRT_SUP, ce[0]->getInt(),
01400 getBoolVar(s, ce[2]));
01401 } else {
01402 rel(s, getSetVar(s, ce[1]), SRT_SUP, getIntVar(s, ce[0]),
01403 getBoolVar(s, ce[2]));
01404 }
01405 }
01406 }
01407 void p_set_disjoint(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01408 rel(s, getSetVar(s, ce[0]), SRT_DISJ, getSetVar(s, ce[1]));
01409 }
01410
01411 void p_array_set_element(FlatZincSpace& s, const ConExpr& ce,
01412 AST::Node*) {
01413 bool isConstant = true;
01414 AST::Array* a = ce[1]->getArray();
01415 for (int i=a->a.size(); i--;) {
01416 if (a->a[i]->isSetVar()) {
01417 isConstant = false;
01418 break;
01419 }
01420 }
01421 IntVar selector = getIntVar(s, ce[0]);
01422 post(s, selector > 0);
01423 if (isConstant) {
01424 IntSetArgs sv = arg2intsetargs(s,ce[1],1);
01425 element(s, sv, selector, getSetVar(s, ce[2]));
01426 } else {
01427 SetVarArgs sv = arg2setvarargs(s, ce[1], 1);
01428 element(s, sv, selector, getSetVar(s, ce[2]));
01429 }
01430 }
01431
01432 void p_array_set_element_op(FlatZincSpace& s, const ConExpr& ce,
01433 AST::Node*, SetOpType op,
01434 const IntSet& universe =
01435 IntSet(Set::Limits::min,Set::Limits::max)) {
01436 bool isConstant = true;
01437 AST::Array* a = ce[1]->getArray();
01438 for (int i=a->a.size(); i--;) {
01439 if (a->a[i]->isSetVar()) {
01440 isConstant = false;
01441 break;
01442 }
01443 }
01444 SetVar selector = getSetVar(s, ce[0]);
01445 dom(s, selector, SRT_DISJ, 0);
01446 if (isConstant) {
01447 IntSetArgs sv = arg2intsetargs(s,ce[1], 1);
01448 element(s, op, sv, selector, getSetVar(s, ce[2]), universe);
01449 } else {
01450 SetVarArgs sv = arg2setvarargs(s, ce[1], 1);
01451 element(s, op, sv, selector, getSetVar(s, ce[2]), universe);
01452 }
01453 }
01454
01455 void p_array_set_element_union(FlatZincSpace& s, const ConExpr& ce,
01456 AST::Node* ann) {
01457 p_array_set_element_op(s, ce, ann, SOT_UNION);
01458 }
01459
01460 void p_array_set_element_intersect(FlatZincSpace& s, const ConExpr& ce,
01461 AST::Node* ann) {
01462 p_array_set_element_op(s, ce, ann, SOT_INTER);
01463 }
01464
01465 void p_array_set_element_intersect_in(FlatZincSpace& s,
01466 const ConExpr& ce,
01467 AST::Node* ann) {
01468 IntSet d = arg2intset(s, ce[3]);
01469 p_array_set_element_op(s, ce, ann, SOT_INTER, d);
01470 }
01471
01472 void p_array_set_element_partition(FlatZincSpace& s, const ConExpr& ce,
01473 AST::Node* ann) {
01474 p_array_set_element_op(s, ce, ann, SOT_DUNION);
01475 }
01476
01477 void p_set_convex(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01478 convex(s, getSetVar(s, ce[0]));
01479 }
01480
01481 void p_array_set_seq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01482 SetVarArgs sv = arg2setvarargs(s, ce[0]);
01483 sequence(s, sv);
01484 }
01485
01486 void p_array_set_seq_union(FlatZincSpace& s, const ConExpr& ce,
01487 AST::Node *) {
01488 SetVarArgs sv = arg2setvarargs(s, ce[0]);
01489 sequence(s, sv, getSetVar(s, ce[1]));
01490 }
01491
01492 class SetPoster {
01493 public:
01494 SetPoster(void) {
01495 registry().add("set_eq", &p_set_eq);
01496 registry().add("equal", &p_set_eq);
01497 registry().add("set_ne", &p_set_ne);
01498 registry().add("set_union", &p_set_union);
01499 registry().add("array_set_element", &p_array_set_element);
01500 registry().add("array_var_set_element", &p_array_set_element);
01501 registry().add("set_intersect", &p_set_intersect);
01502 registry().add("set_diff", &p_set_diff);
01503 registry().add("set_symdiff", &p_set_symdiff);
01504 registry().add("set_subset", &p_set_subset);
01505 registry().add("set_superset", &p_set_superset);
01506 registry().add("set_card", &p_set_card);
01507 registry().add("set_in", &p_set_in);
01508 registry().add("set_eq_reif", &p_set_eq_reif);
01509 registry().add("equal_reif", &p_set_eq_reif);
01510 registry().add("set_ne_reif", &p_set_ne_reif);
01511 registry().add("set_subset_reif", &p_set_subset_reif);
01512 registry().add("set_superset_reif", &p_set_superset_reif);
01513 registry().add("set_in_reif", &p_set_in_reif);
01514 registry().add("disjoint", &p_set_disjoint);
01515
01516 registry().add("array_set_union", &p_array_set_union);
01517 registry().add("array_set_partition", &p_array_set_partition);
01518 registry().add("set_convex", &p_set_convex);
01519 registry().add("array_set_seq", &p_array_set_seq);
01520 registry().add("array_set_seq_union", &p_array_set_seq_union);
01521 registry().add("array_set_element_union",
01522 &p_array_set_element_union);
01523 registry().add("array_set_element_intersect",
01524 &p_array_set_element_intersect);
01525 registry().add("array_set_element_intersect_in",
01526 &p_array_set_element_intersect_in);
01527 registry().add("array_set_element_partition",
01528 &p_array_set_element_partition);
01529 }
01530 };
01531 SetPoster __set_poster;
01532 #endif
01533
01534 }
01535 }}
01536
01537