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/minimodel.hh>
00047 #ifdef GECODE_HAS_SET_VARS
00048 #include <gecode/set.hh>
00049 #endif
00050 #include <gecode/flatzinc.hh>
00051
00052 namespace Gecode { namespace FlatZinc {
00053
00054 Registry& registry(void) {
00055 static Registry r;
00056 return r;
00057 }
00058
00059 void
00060 Registry::post(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00061 std::map<std::string,poster>::iterator i = r.find(ce.id);
00062 if (i == r.end()) {
00063 throw FlatZinc::Error("Registry",
00064 std::string("Constraint ")+ce.id+" not found");
00065 }
00066 i->second(s, ce, ann);
00067 }
00068
00069 void
00070 Registry::add(const std::string& id, poster p) {
00071 r[id] = p;
00072 }
00073
00074 namespace {
00075
00076 IntConLevel ann2icl(AST::Node* ann) {
00077 if (ann) {
00078 if (ann->hasAtom("val"))
00079 return ICL_VAL;
00080 if (ann->hasAtom("domain"))
00081 return ICL_DOM;
00082 if (ann->hasAtom("bounds") ||
00083 ann->hasAtom("boundsR") ||
00084 ann->hasAtom("boundsD") ||
00085 ann->hasAtom("boundsZ"))
00086 return ICL_BND;
00087 }
00088 return ICL_DEF;
00089 }
00090
00091 inline IntRelType
00092 swap(IntRelType irt) {
00093 switch (irt) {
00094 case IRT_LQ: return IRT_GQ;
00095 case IRT_LE: return IRT_GR;
00096 case IRT_GQ: return IRT_LQ;
00097 case IRT_GR: return IRT_LE;
00098 default: return irt;
00099 }
00100 }
00101
00102 inline IntRelType
00103 neg(IntRelType irt) {
00104 switch (irt) {
00105 case IRT_EQ: return IRT_NQ;
00106 case IRT_NQ: return IRT_EQ;
00107 case IRT_LQ: return IRT_GR;
00108 case IRT_LE: return IRT_GQ;
00109 case IRT_GQ: return IRT_LE;
00110 case IRT_GR:
00111 default:
00112 assert(irt == IRT_GR);
00113 }
00114 return IRT_LQ;
00115 }
00116
00117 inline IntArgs arg2intargs(AST::Node* arg, int offset = 0) {
00118 AST::Array* a = arg->getArray();
00119 IntArgs ia(a->a.size()+offset);
00120 for (int i=offset; i--;)
00121 ia[i] = 0;
00122 for (int i=a->a.size(); i--;)
00123 ia[i+offset] = a->a[i]->getInt();
00124 return ia;
00125 }
00126
00127 inline IntArgs arg2boolargs(AST::Node* arg, int offset = 0) {
00128 AST::Array* a = arg->getArray();
00129 IntArgs ia(a->a.size()+offset);
00130 for (int i=offset; i--;)
00131 ia[i] = 0;
00132 for (int i=a->a.size(); i--;)
00133 ia[i+offset] = a->a[i]->getBool();
00134 return ia;
00135 }
00136
00137 inline IntSetArgs arg2intsetargs(AST::Node* arg, int offset = 0) {
00138 AST::Array* a = arg->getArray();
00139 if (a->a.size() == 0) {
00140 IntSetArgs emptyIa(0);
00141 return emptyIa;
00142 }
00143 IntSetArgs ia(a->a.size()+offset);
00144 for (int i=offset; i--;)
00145 ia[i] = IntSet::empty;
00146 for (int i=a->a.size(); i--;) {
00147 AST::SetLit* sl = a->a[i]->getSet();
00148 if (sl->interval) {
00149 ia[i+offset] = IntSet(sl->min, sl->max);
00150 } else {
00151 int* is =
00152 heap.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
00153 for (int j=sl->s.size(); j--; )
00154 is[j] = sl->s[j];
00155 ia[i+offset] = IntSet(is, sl->s.size());
00156 heap.free(is,static_cast<unsigned long int>(sl->s.size()));
00157 }
00158 }
00159 return ia;
00160 }
00161
00162 inline IntVarArgs arg2intvarargs(FlatZincSpace& s, AST::Node* arg,
00163 int offset = 0) {
00164 AST::Array* a = arg->getArray();
00165 if (a->a.size() == 0) {
00166 IntVarArgs emptyIa(0);
00167 return emptyIa;
00168 }
00169 IntVarArgs ia(a->a.size()+offset);
00170 for (int i=offset; i--;)
00171 ia[i] = IntVar(s, 0, 0);
00172 for (int i=a->a.size(); i--;) {
00173 if (a->a[i]->isIntVar()) {
00174 ia[i+offset] = s.iv[a->a[i]->getIntVar()];
00175 } else {
00176 int value = a->a[i]->getInt();
00177 IntVar iv(s, value, value);
00178 ia[i+offset] = iv;
00179 }
00180 }
00181 return ia;
00182 }
00183
00184 inline BoolVarArgs arg2boolvarargs(FlatZincSpace& s, AST::Node* arg,
00185 int offset = 0) {
00186 AST::Array* a = arg->getArray();
00187 if (a->a.size() == 0) {
00188 BoolVarArgs emptyIa(0);
00189 return emptyIa;
00190 }
00191 BoolVarArgs ia(a->a.size()+offset);
00192 for (int i=offset; i--;)
00193 ia[i] = BoolVar(s, 0, 0);
00194 for (int i=a->a.size(); i--;) {
00195 if (a->a[i]->isBool()) {
00196 bool value = a->a[i]->getBool();
00197 BoolVar iv(s, value, value);
00198 ia[i+offset] = iv;
00199 } else {
00200 ia[i+offset] = s.bv[a->a[i]->getBoolVar()];
00201 }
00202 }
00203 return ia;
00204 }
00205
00206 #ifdef GECODE_HAS_SET_VARS
00207 SetVar getSetVar(FlatZincSpace& s, AST::Node* n) {
00208 SetVar x0;
00209 if (!n->isSetVar()) {
00210 AST::SetLit* sl = n->getSet();
00211 if (sl->interval) {
00212 IntSet d(sl->min, sl->max);
00213 x0 = SetVar(s, d, d);
00214 } else {
00215 Region re(s);
00216 int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
00217 for (int i=sl->s.size(); i--; )
00218 is[i] = sl->s[i];
00219 IntSet d(is, sl->s.size());
00220 x0 = SetVar(s, d, d);
00221 }
00222 } else {
00223 x0 = s.sv[n->getSetVar()];
00224 }
00225 return x0;
00226 }
00227
00228 inline SetVarArgs arg2setvarargs(FlatZincSpace& s, AST::Node* arg,
00229 int offset = 0) {
00230 AST::Array* a = arg->getArray();
00231 if (a->a.size() == 0) {
00232 SetVarArgs emptyIa(0);
00233 return emptyIa;
00234 }
00235 SetVarArgs ia(a->a.size()+offset);
00236 for (int i=offset; i--;)
00237 ia[i] = SetVar(s, IntSet::empty, IntSet::empty);
00238 for (int i=a->a.size(); i--;) {
00239 ia[i+offset] = getSetVar(s, a->a[i]);
00240 }
00241 return ia;
00242 }
00243 #endif
00244
00245 BoolVar getBoolVar(FlatZincSpace& s, AST::Node* n) {
00246 BoolVar x0;
00247 if (n->isBool()) {
00248 x0 = BoolVar(s, n->getBool(), n->getBool());
00249 }
00250 else {
00251 x0 = s.bv[n->getBoolVar()];
00252 }
00253 return x0;
00254 }
00255
00256 IntVar getIntVar(FlatZincSpace& s, AST::Node* n) {
00257 IntVar x0;
00258 if (n->isIntVar()) {
00259 x0 = s.iv[n->getIntVar()];
00260 } else {
00261 x0 = IntVar(s, n->getInt(), n->getInt());
00262 }
00263 return x0;
00264 }
00265
00266 void p_distinct(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00267 IntVarArgs va = arg2intvarargs(s, ce[0]);
00268 distinct(s, va, ann2icl(ann));
00269 }
00270 void p_distinctOffset(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00271 IntVarArgs va = arg2intvarargs(s, ce[1]);
00272 AST::Array* offs = ce.args->a[0]->getArray();
00273 IntArgs oa(offs->a.size());
00274 for (int i=offs->a.size(); i--; ) {
00275 oa[i] = offs->a[i]->getInt();
00276 }
00277 distinct(s, oa, va, ann2icl(ann));
00278 }
00279
00280 void p_int_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
00281 AST::Node* ann) {
00282 if (ce[0]->isIntVar()) {
00283 if (ce[1]->isIntVar()) {
00284 rel(s, getIntVar(s, ce[0]), irt, getIntVar(s, ce[1]),
00285 ann2icl(ann));
00286 } else {
00287 rel(s, getIntVar(s, ce[0]), irt, ce[1]->getInt(), ann2icl(ann));
00288 }
00289 } else {
00290 rel(s, getIntVar(s, ce[1]), swap(irt), ce[0]->getInt(),
00291 ann2icl(ann));
00292 }
00293 }
00294 void p_int_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00295 p_int_CMP(s, IRT_EQ, ce, ann);
00296 }
00297 void p_int_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00298 p_int_CMP(s, IRT_NQ, ce, ann);
00299 }
00300 void p_int_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00301 p_int_CMP(s, IRT_GQ, ce, ann);
00302 }
00303 void p_int_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00304 p_int_CMP(s, IRT_GR, ce, ann);
00305 }
00306 void p_int_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00307 p_int_CMP(s, IRT_LQ, ce, ann);
00308 }
00309 void p_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00310 p_int_CMP(s, IRT_LE, ce, ann);
00311 }
00312 void p_int_CMP_reif(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
00313 AST::Node* ann) {
00314 if (ce[2]->isBool()) {
00315 if (ce[2]->getBool()) {
00316 p_int_CMP(s, irt, ce, ann);
00317 } else {
00318 p_int_CMP(s, neg(irt), ce, ann);
00319 }
00320 return;
00321 }
00322 if (ce[0]->isIntVar()) {
00323 if (ce[1]->isIntVar()) {
00324 rel(s, getIntVar(s, ce[0]), irt, getIntVar(s, ce[1]),
00325 getBoolVar(s, ce[2]), ann2icl(ann));
00326 } else {
00327 rel(s, getIntVar(s, ce[0]), irt, ce[1]->getInt(),
00328 getBoolVar(s, ce[2]), ann2icl(ann));
00329 }
00330 } else {
00331 rel(s, getIntVar(s, ce[1]), swap(irt), ce[0]->getInt(),
00332 getBoolVar(s, ce[2]), ann2icl(ann));
00333 }
00334 }
00335
00336
00337 void p_int_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00338 p_int_CMP_reif(s, IRT_EQ, ce, ann);
00339 }
00340 void p_int_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00341 p_int_CMP_reif(s, IRT_NQ, ce, ann);
00342 }
00343 void p_int_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00344 p_int_CMP_reif(s, IRT_GQ, ce, ann);
00345 }
00346 void p_int_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00347 p_int_CMP_reif(s, IRT_GR, ce, ann);
00348 }
00349 void p_int_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00350 p_int_CMP_reif(s, IRT_LQ, ce, ann);
00351 }
00352 void p_int_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00353 p_int_CMP_reif(s, IRT_LE, ce, ann);
00354 }
00355
00356
00357 void p_int_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
00358 AST::Node* ann) {
00359 IntArgs ia = arg2intargs(ce[0]);
00360 IntVarArgs iv = arg2intvarargs(s, ce[1]);
00361 linear(s, ia, iv, irt, ce[2]->getInt(), ann2icl(ann));
00362 }
00363 void p_int_lin_CMP_reif(FlatZincSpace& s, IntRelType irt,
00364 const ConExpr& ce, AST::Node* ann) {
00365 if (ce[2]->isBool()) {
00366 if (ce[2]->getBool()) {
00367 p_int_lin_CMP(s, irt, ce, ann);
00368 } else {
00369 p_int_lin_CMP(s, neg(irt), ce, ann);
00370 }
00371 return;
00372 }
00373 IntArgs ia = arg2intargs(ce[0]);
00374 IntVarArgs iv = arg2intvarargs(s, ce[1]);
00375 linear(s, ia, iv, irt, ce[2]->getInt(), getBoolVar(s, ce[3]),
00376 ann2icl(ann));
00377 }
00378 void p_int_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00379 p_int_lin_CMP(s, IRT_EQ, ce, ann);
00380 }
00381 void p_int_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00382 p_int_lin_CMP_reif(s, IRT_EQ, ce, ann);
00383 }
00384 void p_int_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00385 p_int_lin_CMP(s, IRT_NQ, ce, ann);
00386 }
00387 void p_int_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00388 p_int_lin_CMP_reif(s, IRT_NQ, ce, ann);
00389 }
00390 void p_int_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00391 p_int_lin_CMP(s, IRT_LQ, ce, ann);
00392 }
00393 void p_int_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00394 p_int_lin_CMP_reif(s, IRT_LQ, ce, ann);
00395 }
00396 void p_int_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00397 p_int_lin_CMP(s, IRT_LE, ce, ann);
00398 }
00399 void p_int_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00400 p_int_lin_CMP_reif(s, IRT_LE, ce, ann);
00401 }
00402 void p_int_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00403 p_int_lin_CMP(s, IRT_GQ, ce, ann);
00404 }
00405 void p_int_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00406 p_int_lin_CMP_reif(s, IRT_GQ, ce, ann);
00407 }
00408 void p_int_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00409 p_int_lin_CMP(s, IRT_GR, ce, ann);
00410 }
00411 void p_int_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00412 p_int_lin_CMP_reif(s, IRT_GR, ce, ann);
00413 }
00414
00415 void p_bool_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
00416 AST::Node* ann) {
00417 IntArgs ia = arg2intargs(ce[0]);
00418 BoolVarArgs iv = arg2boolvarargs(s, ce[1]);
00419 if (ce[2]->isIntVar())
00420 linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()], ann2icl(ann));
00421 else
00422 linear(s, ia, iv, irt, ce[2]->getInt(), ann2icl(ann));
00423 }
00424 void p_bool_lin_CMP_reif(FlatZincSpace& s, IntRelType irt,
00425 const ConExpr& ce, AST::Node* ann) {
00426 if (ce[2]->isBool()) {
00427 if (ce[2]->getBool()) {
00428 p_bool_lin_CMP(s, irt, ce, ann);
00429 } else {
00430 p_bool_lin_CMP(s, neg(irt), ce, ann);
00431 }
00432 return;
00433 }
00434 IntArgs ia = arg2intargs(ce[0]);
00435 BoolVarArgs iv = arg2boolvarargs(s, ce[1]);
00436 if (ce[2]->isIntVar())
00437 linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()], getBoolVar(s, ce[3]),
00438 ann2icl(ann));
00439 else
00440 linear(s, ia, iv, irt, ce[2]->getInt(), getBoolVar(s, ce[3]),
00441 ann2icl(ann));
00442 }
00443 void p_bool_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00444 p_bool_lin_CMP(s, IRT_EQ, ce, ann);
00445 }
00446 void p_bool_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00447 {
00448 p_bool_lin_CMP_reif(s, IRT_EQ, ce, ann);
00449 }
00450 void p_bool_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00451 p_bool_lin_CMP(s, IRT_NQ, ce, ann);
00452 }
00453 void p_bool_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00454 {
00455 p_bool_lin_CMP_reif(s, IRT_NQ, ce, ann);
00456 }
00457 void p_bool_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00458 p_bool_lin_CMP(s, IRT_LQ, ce, ann);
00459 }
00460 void p_bool_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00461 {
00462 p_bool_lin_CMP_reif(s, IRT_LQ, ce, ann);
00463 }
00464 void p_bool_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00465 {
00466 p_bool_lin_CMP(s, IRT_LE, ce, ann);
00467 }
00468 void p_bool_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00469 {
00470 p_bool_lin_CMP_reif(s, IRT_LE, ce, ann);
00471 }
00472 void p_bool_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00473 p_bool_lin_CMP(s, IRT_GQ, ce, ann);
00474 }
00475 void p_bool_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00476 {
00477 p_bool_lin_CMP_reif(s, IRT_GQ, ce, ann);
00478 }
00479 void p_bool_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00480 p_bool_lin_CMP(s, IRT_GR, ce, ann);
00481 }
00482 void p_bool_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00483 {
00484 p_bool_lin_CMP_reif(s, IRT_GR, ce, ann);
00485 }
00486
00487
00488
00489 void p_int_plus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00490 if (!ce[0]->isIntVar()) {
00491 post(s, ce[0]->getInt() + getIntVar(s, ce[1])
00492 == getIntVar(s,ce[2]), ann2icl(ann));
00493 } else if (!ce[1]->isIntVar()) {
00494 post(s, getIntVar(s,ce[0]) + ce[1]->getInt()
00495 == getIntVar(s,ce[2]), ann2icl(ann));
00496 } else if (!ce[2]->isIntVar()) {
00497 post(s, getIntVar(s,ce[0]) + getIntVar(s,ce[1])
00498 == ce[2]->getInt(), ann2icl(ann));
00499 } else {
00500 post(s, getIntVar(s,ce[0]) + getIntVar(s,ce[1])
00501 == getIntVar(s,ce[2]), ann2icl(ann));
00502 }
00503 }
00504
00505 void p_int_minus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00506 if (!ce[0]->isIntVar()) {
00507 post(s, ce[0]->getInt() - getIntVar(s, ce[1])
00508 == getIntVar(s,ce[2]), ann2icl(ann));
00509 } else if (!ce[1]->isIntVar()) {
00510 post(s, getIntVar(s,ce[0]) - ce[1]->getInt()
00511 == getIntVar(s,ce[2]), ann2icl(ann));
00512 } else if (!ce[2]->isIntVar()) {
00513 post(s, getIntVar(s,ce[0]) - getIntVar(s,ce[1])
00514 == ce[2]->getInt(), ann2icl(ann));
00515 } else {
00516 post(s, getIntVar(s,ce[0]) - getIntVar(s,ce[1])
00517 == getIntVar(s,ce[2]), ann2icl(ann));
00518 }
00519 }
00520
00521 void p_int_times(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00522 IntVar x0 = getIntVar(s, ce[0]);
00523 IntVar x1 = getIntVar(s, ce[1]);
00524 IntVar x2 = getIntVar(s, ce[2]);
00525 mult(s, x0, x1, x2, ann2icl(ann));
00526 }
00527 void p_int_div(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00528 IntVar x0 = getIntVar(s, ce[0]);
00529 IntVar x1 = getIntVar(s, ce[1]);
00530 IntVar x2 = getIntVar(s, ce[2]);
00531 div(s,x0,x1,x2, ann2icl(ann));
00532 }
00533 void p_int_mod(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00534 IntVar x0 = getIntVar(s, ce[0]);
00535 IntVar x1 = getIntVar(s, ce[1]);
00536 IntVar x2 = getIntVar(s, ce[2]);
00537 mod(s,x0,x1,x2, ann2icl(ann));
00538 }
00539
00540 void p_int_min(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00541 IntVar x0 = getIntVar(s, ce[0]);
00542 IntVar x1 = getIntVar(s, ce[1]);
00543 IntVar x2 = getIntVar(s, ce[2]);
00544 min(s, x0, x1, x2, ann2icl(ann));
00545 }
00546 void p_int_max(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00547 IntVar x0 = getIntVar(s, ce[0]);
00548 IntVar x1 = getIntVar(s, ce[1]);
00549 IntVar x2 = getIntVar(s, ce[2]);
00550 max(s, x0, x1, x2, ann2icl(ann));
00551 }
00552 void p_int_negate(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00553 IntVar x0 = getIntVar(s, ce[0]);
00554 IntVar x1 = getIntVar(s, ce[1]);
00555 post(s, x0 == -x1, ann2icl(ann));
00556 }
00557
00558
00559 void p_bool_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
00560 AST::Node* ann) {
00561 if (ce[0]->isBoolVar()) {
00562 if (ce[1]->isBoolVar()) {
00563 rel(s, getBoolVar(s, ce[0]), irt, getBoolVar(s, ce[1]),
00564 ann2icl(ann));
00565 } else {
00566 rel(s, getBoolVar(s, ce[0]), irt, ce[1]->getBool(), ann2icl(ann));
00567 }
00568 } else {
00569 rel(s, getBoolVar(s, ce[1]), swap(irt), ce[0]->getBool(),
00570 ann2icl(ann));
00571 }
00572 }
00573 void p_bool_CMP_reif(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
00574 AST::Node* ann) {
00575 rel(s, getBoolVar(s, ce[0]), irt, getBoolVar(s, ce[1]),
00576 getBoolVar(s, ce[2]), ann2icl(ann));
00577 }
00578 void p_bool_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00579 p_bool_CMP(s, IRT_EQ, ce, ann);
00580 }
00581 void p_bool_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00582 p_bool_CMP_reif(s, IRT_EQ, ce, ann);
00583 }
00584 void p_bool_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00585 p_bool_CMP(s, IRT_NQ, ce, ann);
00586 }
00587 void p_bool_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00588 p_bool_CMP_reif(s, IRT_NQ, ce, ann);
00589 }
00590 void p_bool_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00591 p_bool_CMP(s, IRT_GQ, ce, ann);
00592 }
00593 void p_bool_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00594 p_bool_CMP_reif(s, IRT_GQ, ce, ann);
00595 }
00596 void p_bool_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00597 p_bool_CMP(s, IRT_LQ, ce, ann);
00598 }
00599 void p_bool_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00600 p_bool_CMP_reif(s, IRT_LQ, ce, ann);
00601 }
00602 void p_bool_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00603 p_bool_CMP(s, IRT_GR, ce, ann);
00604 }
00605 void p_bool_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00606 p_bool_CMP_reif(s, IRT_GR, ce, ann);
00607 }
00608 void p_bool_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00609 p_bool_CMP(s, IRT_LE, ce, ann);
00610 }
00611 void p_bool_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00612 p_bool_CMP_reif(s, IRT_LE, ce, ann);
00613 }
00614
00615 #define BOOL_OP(op) \
00616 BoolVar b0 = getBoolVar(s, ce[0]); \
00617 BoolVar b1 = getBoolVar(s, ce[1]); \
00618 if (ce[2]->isBool()) { \
00619 rel(s, b0, op, b1, ce[2]->getBool(), ann2icl(ann)); \
00620 } else { \
00621 rel(s, b0, op, b1, s.bv[ce[2]->getBoolVar()], ann2icl(ann)); \
00622 }
00623
00624 #define BOOL_ARRAY_OP(op) \
00625 BoolVarArgs bv = arg2boolvarargs(s, ce[0]); \
00626 if (ce[1]->isBool()) { \
00627 rel(s, op, bv, ce[1]->getBool(), ann2icl(ann)); \
00628 } else { \
00629 rel(s, op, bv, s.bv[ce[1]->getBoolVar()], ann2icl(ann)); \
00630 }
00631
00632 void p_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00633 BOOL_OP(BOT_OR);
00634 }
00635 void p_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00636 BOOL_OP(BOT_AND);
00637 }
00638 void p_array_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00639 {
00640 BOOL_ARRAY_OP(BOT_AND);
00641 }
00642 void p_array_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00643 {
00644 BOOL_ARRAY_OP(BOT_OR);
00645 }
00646 void p_array_bool_clause(FlatZincSpace& s, const ConExpr& ce,
00647 AST::Node* ann) {
00648 BoolVarArgs bvp = arg2boolvarargs(s, ce[0]);
00649 BoolVarArgs bvn = arg2boolvarargs(s, ce[1]);
00650 clause(s, BOT_OR, bvp, bvn, 1, ann2icl(ann));
00651 }
00652 void p_array_bool_clause_reif(FlatZincSpace& s, const ConExpr& ce,
00653 AST::Node* ann) {
00654 BoolVarArgs bvp = arg2boolvarargs(s, ce[0]);
00655 BoolVarArgs bvn = arg2boolvarargs(s, ce[1]);
00656 BoolVar b0 = getBoolVar(s, ce[2]);
00657 clause(s, BOT_OR, bvp, bvn, b0, ann2icl(ann));
00658 }
00659 void p_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00660 BOOL_OP(BOT_XOR);
00661 }
00662 void p_bool_l_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00663 BoolVar b0 = getBoolVar(s, ce[0]);
00664 BoolVar b1 = getBoolVar(s, ce[1]);
00665 if (ce[2]->isBool()) {
00666 rel(s, b1, BOT_IMP, b0, ce[2]->getBool(), ann2icl(ann));
00667 } else {
00668 rel(s, b1, BOT_IMP, b0, s.bv[ce[2]->getBoolVar()], ann2icl(ann));
00669 }
00670 }
00671 void p_bool_r_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00672 BOOL_OP(BOT_IMP);
00673 }
00674 void p_bool_not(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00675 BoolVar x0 = getBoolVar(s, ce[0]);
00676 BoolVar x1 = getBoolVar(s, ce[1]);
00677 rel(s, x0, BOT_XOR, x1, 1, ann2icl(ann));
00678 }
00679
00680
00681 void p_array_int_element(FlatZincSpace& s, const ConExpr& ce,
00682 AST::Node* ann) {
00683 bool isConstant = true;
00684 AST::Array* a = ce[1]->getArray();
00685 for (int i=a->a.size(); i--;) {
00686 if (!a->a[i]->isInt()) {
00687 isConstant = false;
00688 break;
00689 }
00690 }
00691 IntVar selector = getIntVar(s, ce[0]);
00692 post(s, selector > 0);
00693 if (isConstant) {
00694 IntArgs ia = arg2intargs(ce[1], 1);
00695 element(s, ia, selector, getIntVar(s, ce[2]), ann2icl(ann));
00696 } else {
00697 IntVarArgs iv = arg2intvarargs(s, ce[1], 1);
00698 element(s, iv, selector, getIntVar(s, ce[2]), ann2icl(ann));
00699 }
00700 }
00701 void p_array_bool_element(FlatZincSpace& s, const ConExpr& ce,
00702 AST::Node* ann) {
00703 bool isConstant = true;
00704 AST::Array* a = ce[1]->getArray();
00705 for (int i=a->a.size(); i--;) {
00706 if (!a->a[i]->isBool()) {
00707 isConstant = false;
00708 break;
00709 }
00710 }
00711 IntVar selector = getIntVar(s, ce[0]);
00712 post(s, selector > 0);
00713 if (isConstant) {
00714 IntArgs ia = arg2boolargs(ce[1], 1);
00715 element(s, ia, selector, getBoolVar(s, ce[2]), ann2icl(ann));
00716 } else {
00717 BoolVarArgs iv = arg2boolvarargs(s, ce[1], 1);
00718 element(s, iv, selector, getBoolVar(s, ce[2]), ann2icl(ann));
00719 }
00720 }
00721
00722
00723 void p_bool2int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00724 BoolVar x0 = getBoolVar(s, ce[0]);
00725 IntVar x1 = getIntVar(s, ce[1]);
00726 channel(s, x0, x1, ann2icl(ann));
00727 }
00728
00729
00730
00731 void p_abs(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00732 IntVar x0 = getIntVar(s, ce[0]);
00733 IntVar x1 = getIntVar(s, ce[1]);
00734 abs(s, x0, x1, ann2icl(ann));
00735 }
00736
00737 void p_array_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00738 IntVarArgs iv0 = arg2intvarargs(s, ce[0]);
00739 IntVarArgs iv1 = arg2intvarargs(s, ce[1]);
00740 rel(s, iv0, IRT_LE, iv1, ann2icl(ann));
00741 }
00742
00743 void p_array_int_lq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00744 IntVarArgs iv0 = arg2intvarargs(s, ce[0]);
00745 IntVarArgs iv1 = arg2intvarargs(s, ce[1]);
00746 rel(s, iv0, IRT_LQ, iv1, ann2icl(ann));
00747 }
00748
00749 void p_count(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00750 IntVarArgs iv = arg2intvarargs(s, ce[0]);
00751 if (!ce[1]->isIntVar()) {
00752 if (!ce[2]->isIntVar()) {
00753 count(s, iv, ce[1]->getInt(), IRT_EQ, ce[2]->getInt(),
00754 ann2icl(ann));
00755 } else {
00756 count(s, iv, ce[1]->getInt(), IRT_EQ, getIntVar(s, ce[2]),
00757 ann2icl(ann));
00758 }
00759 } else if (!ce[2]->isIntVar()) {
00760 count(s, iv, getIntVar(s, ce[1]), IRT_EQ, ce[2]->getInt(),
00761 ann2icl(ann));
00762 } else {
00763 count(s, iv, getIntVar(s, ce[1]), IRT_EQ, getIntVar(s, ce[2]),
00764 ann2icl(ann));
00765 }
00766 }
00767
00768 void count_rel(IntRelType irt,
00769 FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00770 IntVarArgs iv = arg2intvarargs(s, ce[1]);
00771 count(s, iv, ce[2]->getInt(), irt, ce[0]->getInt(), ann2icl(ann));
00772 }
00773
00774 void p_at_most(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00775 count_rel(IRT_LQ, s, ce, ann);
00776 }
00777
00778 void p_at_least(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00779 count_rel(IRT_GQ, s, ce, ann);
00780 }
00781
00782 void p_global_cardinality(FlatZincSpace& s, const ConExpr& ce,
00783 AST::Node* ann) {
00784 IntVarArgs iv0 = arg2intvarargs(s, ce[0]);
00785 IntVarArgs iv1 = arg2intvarargs(s, ce[1]);
00786 int cmin = ce[2]->getInt();
00787 if (cmin == 0) {
00788 count(s, iv0, iv1, ann2icl(ann));
00789 } else {
00790 IntArgs values(iv1.size());
00791 for (int i=values.size(); i--;)
00792 values[i] = i+cmin;
00793 count(s, iv0, iv1, values, ann2icl(ann));
00794 }
00795 }
00796
00797 void p_minimum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00798 IntVarArgs iv = arg2intvarargs(s, ce[1]);
00799 min(s, iv, getIntVar(s, ce[0]), ann2icl(ann));
00800 }
00801
00802 void p_maximum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00803 IntVarArgs iv = arg2intvarargs(s, ce[1]);
00804 max(s, iv, getIntVar(s, ce[0]), ann2icl(ann));
00805 }
00806
00807 void p_regular(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00808 IntVarArgs iv = arg2intvarargs(s, ce[0]);
00809 int q = ce[1]->getInt();
00810 int symbols = ce[2]->getInt();
00811 IntArgs d = arg2intargs(ce[3]);
00812 int q0 = ce[4]->getInt();
00813
00814 int noOfTrans = 0;
00815 for (int i=1; i<=q; i++) {
00816 for (int j=1; j<=symbols; j++) {
00817 if (d[(i-1)*symbols+(j-1)] > 0)
00818 noOfTrans++;
00819 }
00820 }
00821
00822 Region re(s);
00823 DFA::Transition* t = re.alloc<DFA::Transition>(noOfTrans+1);
00824 noOfTrans = 0;
00825 for (int i=1; i<=q; i++) {
00826 for (int j=1; j<=symbols; j++) {
00827 if (d[(i-1)*symbols+(j-1)] > 0) {
00828 t[noOfTrans].i_state = i;
00829 t[noOfTrans].symbol = j;
00830 t[noOfTrans].o_state = d[(i-1)*symbols+(j-1)];
00831 noOfTrans++;
00832 }
00833 }
00834 }
00835 t[noOfTrans].i_state = -1;
00836
00837
00838 AST::SetLit* sl = ce[5]->getSet();
00839 int* f;
00840 if (sl->interval) {
00841 f = static_cast<int*>(malloc(sizeof(int)*(sl->max-sl->min+2)));
00842 for (int i=sl->min; i<=sl->max; i++)
00843 f[i-sl->min] = i;
00844 f[sl->max-sl->min+1] = -1;
00845 } else {
00846 f = static_cast<int*>(malloc(sizeof(int)*(sl->s.size()+1)));
00847 for (int j=sl->s.size(); j--; )
00848 f[j] = sl->s[j];
00849 f[sl->s.size()] = -1;
00850 }
00851
00852 DFA dfa(q0,t,f);
00853 free(f);
00854 extensional(s, iv, dfa, ann2icl(ann));
00855 }
00856
00857 void
00858 p_sort(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00859 IntVarArgs x = arg2intvarargs(s, ce[0]);
00860 IntVarArgs y = arg2intvarargs(s, ce[1]);
00861 IntVarArgs xy(x.size()+y.size());
00862 for (int i=x.size(); i--;)
00863 xy[i] = x[i];
00864 for (int i=y.size(); i--;)
00865 xy[i+x.size()] = y[i];
00866 unshare(s, xy);
00867 for (int i=x.size(); i--;)
00868 x[i] = xy[i];
00869 for (int i=y.size(); i--;)
00870 y[i] = xy[i+x.size()];
00871 sorted(s, x, y, ann2icl(ann));
00872 }
00873
00874 void
00875 p_inverse_offsets(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00876 IntVarArgs x = arg2intvarargs(s, ce[0]);
00877 int xoff = ce[1]->getInt();
00878 IntVarArgs y = arg2intvarargs(s, ce[2]);
00879 int yoff = ce[3]->getInt();
00880 channel(s, x, xoff, y, yoff, ann2icl(ann));
00881 }
00882
00883 void
00884 p_increasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00885 IntVarArgs x = arg2intvarargs(s, ce[0]);
00886 rel(s,x,IRT_LQ,ann2icl(ann));
00887 }
00888
00889 void
00890 p_increasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00891 BoolVarArgs x = arg2boolvarargs(s, ce[0]);
00892 rel(s,x,IRT_LQ,ann2icl(ann));
00893 }
00894
00895 void
00896 p_table_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00897 IntVarArgs x = arg2intvarargs(s, ce[0]);
00898 IntArgs tuples = arg2intargs(ce[1]);
00899 int noOfVars = x.size();
00900 int noOfTuples = tuples.size()/noOfVars;
00901 TupleSet ts;
00902 for (int i=0; i<noOfTuples; i++) {
00903 IntArgs t(noOfVars);
00904 for (int j=0; j<x.size(); j++) {
00905 t[j] = tuples[i*noOfVars+j];
00906 }
00907 ts.add(t);
00908 }
00909 ts.finalize();
00910 extensional(s,x,ts,EPK_DEF,ann2icl(ann));
00911 }
00912 void
00913 p_table_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00914 BoolVarArgs x = arg2boolvarargs(s, ce[0]);
00915 IntArgs tuples = arg2boolargs(ce[1]);
00916 int noOfVars = x.size();
00917 int noOfTuples = tuples.size()/noOfVars;
00918 TupleSet ts;
00919 for (int i=0; i<noOfTuples; i++) {
00920 IntArgs t(noOfVars);
00921 for (int j=0; j<x.size(); j++) {
00922 t[j] = tuples[i*noOfVars+j];
00923 }
00924 ts.add(t);
00925 }
00926 ts.finalize();
00927 extensional(s,x,ts,EPK_DEF,ann2icl(ann));
00928 }
00929
00930 void p_cumulatives(FlatZincSpace& s, const ConExpr& ce,
00931 AST::Node* ann) {
00932 IntVarArgs start = arg2intvarargs(s, ce[0]);
00933 IntVarArgs duration = arg2intvarargs(s, ce[1]);
00934 IntVarArgs height = arg2intvarargs(s, ce[2]);
00935 int n = start.size();
00936 IntVar bound = getIntVar(s, ce[3]);
00937
00938 if (bound.assigned()) {
00939 IntArgs machine(n);
00940 for (int i = n; i--; ) machine[i] = 0;
00941 IntArgs limit(1, bound.val());
00942 IntVarArgs end(n);
00943 for (int i = n; i--; ) end[i] = IntVar(s, 0, Int::Limits::max);
00944 cumulatives(s, machine, start, duration, end, height, limit, true,
00945 ann2icl(ann));
00946 } else {
00947 int min = Gecode::Int::Limits::max;
00948 int max = Gecode::Int::Limits::min;
00949 IntVarArgs end(start.size());
00950 for (int i = start.size(); i--; ) {
00951 min = std::min(min, start[i].min());
00952 max = std::max(max, start[i].max() + duration[i].max());
00953 end[i] = post(s, start[i] + duration[i]);
00954 }
00955 for (int time = min; time < max; ++time) {
00956 IntVarArgs x(start.size());
00957 for (int i = start.size(); i--; ) {
00958 IntVar overlaps = channel(s, post(s, (~(start[i] <= time) &&
00959 ~(time < end[i]))));
00960 x[i] = mult(s, overlaps, height[i]);
00961 }
00962 linear(s, x, IRT_LQ, bound);
00963 }
00964 }
00965 }
00966
00967 class IntPoster {
00968 public:
00969 IntPoster(void) {
00970 registry().add("all_different_int", &p_distinct);
00971 registry().add("all_different_offset", &p_distinctOffset);
00972 registry().add("int_eq", &p_int_eq);
00973 registry().add("int_ne", &p_int_ne);
00974 registry().add("int_ge", &p_int_ge);
00975 registry().add("int_gt", &p_int_gt);
00976 registry().add("int_le", &p_int_le);
00977 registry().add("int_lt", &p_int_lt);
00978 registry().add("int_eq_reif", &p_int_eq_reif);
00979 registry().add("int_ne_reif", &p_int_ne_reif);
00980 registry().add("int_ge_reif", &p_int_ge_reif);
00981 registry().add("int_gt_reif", &p_int_gt_reif);
00982 registry().add("int_le_reif", &p_int_le_reif);
00983 registry().add("int_lt_reif", &p_int_lt_reif);
00984 registry().add("int_lin_eq", &p_int_lin_eq);
00985 registry().add("int_lin_eq_reif", &p_int_lin_eq_reif);
00986 registry().add("int_lin_ne", &p_int_lin_ne);
00987 registry().add("int_lin_ne_reif", &p_int_lin_ne_reif);
00988 registry().add("int_lin_le", &p_int_lin_le);
00989 registry().add("int_lin_le_reif", &p_int_lin_le_reif);
00990 registry().add("int_lin_lt", &p_int_lin_lt);
00991 registry().add("int_lin_lt_reif", &p_int_lin_lt_reif);
00992 registry().add("int_lin_ge", &p_int_lin_ge);
00993 registry().add("int_lin_ge_reif", &p_int_lin_ge_reif);
00994 registry().add("int_lin_gt", &p_int_lin_gt);
00995 registry().add("int_lin_gt_reif", &p_int_lin_gt_reif);
00996 registry().add("int_plus", &p_int_plus);
00997 registry().add("int_minus", &p_int_minus);
00998 registry().add("int_times", &p_int_times);
00999 registry().add("int_div", &p_int_div);
01000 registry().add("int_mod", &p_int_mod);
01001 registry().add("int_min", &p_int_min);
01002 registry().add("int_max", &p_int_max);
01003 registry().add("int_abs", &p_abs);
01004 registry().add("int_negate", &p_int_negate);
01005 registry().add("bool_eq", &p_bool_eq);
01006 registry().add("bool_eq_reif", &p_bool_eq_reif);
01007 registry().add("bool_ne", &p_bool_ne);
01008 registry().add("bool_ne_reif", &p_bool_ne_reif);
01009 registry().add("bool_ge", &p_bool_ge);
01010 registry().add("bool_ge_reif", &p_bool_ge_reif);
01011 registry().add("bool_le", &p_bool_le);
01012 registry().add("bool_le_reif", &p_bool_le_reif);
01013 registry().add("bool_gt", &p_bool_gt);
01014 registry().add("bool_gt_reif", &p_bool_gt_reif);
01015 registry().add("bool_lt", &p_bool_lt);
01016 registry().add("bool_lt_reif", &p_bool_lt_reif);
01017 registry().add("bool_or", &p_bool_or);
01018 registry().add("bool_and", &p_bool_and);
01019 registry().add("bool_xor", &p_bool_xor);
01020 registry().add("array_bool_and", &p_array_bool_and);
01021 registry().add("array_bool_or", &p_array_bool_or);
01022 registry().add("bool_clause", &p_array_bool_clause);
01023 registry().add("bool_clause_reif", &p_array_bool_clause_reif);
01024 registry().add("bool_left_imp", &p_bool_l_imp);
01025 registry().add("bool_right_imp", &p_bool_r_imp);
01026 registry().add("bool_not", &p_bool_not);
01027 registry().add("array_int_element", &p_array_int_element);
01028 registry().add("array_bool_element", &p_array_bool_element);
01029 registry().add("bool2int", &p_bool2int);
01030
01031 registry().add("array_int_lt", &p_array_int_lt);
01032 registry().add("array_int_lq", &p_array_int_lq);
01033 registry().add("count", &p_count);
01034 registry().add("at_least_int", &p_at_least);
01035 registry().add("at_most_int", &p_at_most);
01036 registry().add("global_cardinality_gecode", &p_global_cardinality);
01037 registry().add("minimum_int", &p_minimum);
01038 registry().add("maximum_int", &p_maximum);
01039 registry().add("regular", &p_regular);
01040 registry().add("sort", &p_sort);
01041 registry().add("inverse_offsets", &p_inverse_offsets);
01042 registry().add("increasing_int", &p_increasing_int);
01043 registry().add("increasing_bool", &p_increasing_bool);
01044 registry().add("table_int", &p_table_int);
01045 registry().add("table_bool", &p_table_bool);
01046 registry().add("cumulatives", &p_cumulatives);
01047
01048 registry().add("bool_lin_eq", &p_bool_lin_eq);
01049 registry().add("bool_lin_ne", &p_bool_lin_ne);
01050 registry().add("bool_lin_le", &p_bool_lin_le);
01051 registry().add("bool_lin_lt", &p_bool_lin_lt);
01052 registry().add("bool_lin_ge", &p_bool_lin_ge);
01053 registry().add("bool_lin_gt", &p_bool_lin_gt);
01054
01055 registry().add("bool_lin_eq_reif", &p_bool_lin_eq_reif);
01056 registry().add("bool_lin_ne_reif", &p_bool_lin_ne_reif);
01057 registry().add("bool_lin_le_reif", &p_bool_lin_le_reif);
01058 registry().add("bool_lin_lt_reif", &p_bool_lin_lt_reif);
01059 registry().add("bool_lin_ge_reif", &p_bool_lin_ge_reif);
01060 registry().add("bool_lin_gt_reif", &p_bool_lin_gt_reif);
01061 }
01062 };
01063 IntPoster __int_poster;
01064
01065 #ifdef GECODE_HAS_SET_VARS
01066 void p_set_OP(FlatZincSpace& s, SetOpType op,
01067 const ConExpr& ce, AST::Node *) {
01068 rel(s, getSetVar(s, ce[0]), op, getSetVar(s, ce[1]),
01069 SRT_EQ, getSetVar(s, ce[2]));
01070 }
01071 void p_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01072 p_set_OP(s, SOT_UNION, ce, ann);
01073 }
01074 void p_set_intersect(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01075 p_set_OP(s, SOT_INTER, ce, ann);
01076 }
01077 void p_set_diff(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01078 p_set_OP(s, SOT_MINUS, ce, ann);
01079 }
01080
01081 void p_set_symdiff(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
01082 SetVar x = getSetVar(s, ce[0]);
01083 SetVar y = getSetVar(s, ce[1]);
01084
01085 SetVarLubRanges xub(x);
01086 IntSet xubs(xub);
01087 SetVar x_y(s,IntSet::empty,xubs);
01088 rel(s, x, SOT_MINUS, y, SRT_EQ, x_y);
01089
01090 SetVarLubRanges yub(y);
01091 IntSet yubs(yub);
01092 SetVar y_x(s,IntSet::empty,yubs);
01093 rel(s, y, SOT_MINUS, x, SRT_EQ, y_x);
01094
01095 rel(s, x_y, SOT_UNION, y_x, SRT_EQ, getSetVar(s, ce[2]));
01096 }
01097
01098 void p_array_set_OP(FlatZincSpace& s, SetOpType op,
01099 const ConExpr& ce, AST::Node *) {
01100 SetVarArgs xs = arg2setvarargs(s, ce[0]);
01101 rel(s, op, xs, getSetVar(s, ce[1]));
01102 }
01103 void p_array_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01104 p_array_set_OP(s, SOT_UNION, ce, ann);
01105 }
01106 void p_array_set_partition(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01107 p_array_set_OP(s, SOT_DUNION, ce, ann);
01108 }
01109
01110
01111 void p_set_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01112 rel(s, getSetVar(s, ce[0]), SRT_EQ, getSetVar(s, ce[1]));
01113 }
01114 void p_set_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01115 rel(s, getSetVar(s, ce[0]), SRT_NQ, getSetVar(s, ce[1]));
01116 }
01117 void p_set_subset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01118 rel(s, getSetVar(s, ce[0]), SRT_SUB, getSetVar(s, ce[1]));
01119 }
01120 void p_set_superset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01121 rel(s, getSetVar(s, ce[0]), SRT_SUP, getSetVar(s, ce[1]));
01122 }
01123 void p_set_card(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01124 if (!ce[1]->isIntVar()) {
01125 cardinality(s, getSetVar(s, ce[0]), ce[1]->getInt(),
01126 ce[1]->getInt());
01127 } else {
01128 cardinality(s, getSetVar(s, ce[0]), getIntVar(s, ce[1]));
01129 }
01130 }
01131 void p_set_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01132 if (!ce[1]->isSetVar()) {
01133 AST::SetLit* sl = ce[1]->getSet();
01134 IntSet d;
01135 if (sl->interval) {
01136 d = IntSet(sl->min, sl->max);
01137 } else {
01138 Region re(s);
01139 int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
01140 for (int i=sl->s.size(); i--; )
01141 is[i] = sl->s[i];
01142 d = IntSet(is, sl->s.size());
01143 }
01144 if (ce[0]->isBoolVar()) {
01145 assert(sl->interval);
01146 rel(s, getBoolVar(s, ce[0]), IRT_GQ, sl->min);
01147 rel(s, getBoolVar(s, ce[0]), IRT_LQ, sl->max);
01148 } else {
01149 dom(s, getIntVar(s, ce[0]), d);
01150 }
01151 } else {
01152 if (!ce[0]->isIntVar()) {
01153 dom(s, getSetVar(s, ce[1]), SRT_SUP, ce[0]->getInt());
01154 } else {
01155 rel(s, getSetVar(s, ce[1]), SRT_SUP, getIntVar(s, ce[0]));
01156 }
01157 }
01158 }
01159 void p_set_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01160 rel(s, getSetVar(s, ce[0]), SRT_EQ, getSetVar(s, ce[1]),
01161 getBoolVar(s, ce[2]));
01162 }
01163 void p_set_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01164 rel(s, getSetVar(s, ce[0]), SRT_NQ, getSetVar(s, ce[1]),
01165 getBoolVar(s, ce[2]));
01166 }
01167 void p_set_subset_reif(FlatZincSpace& s, const ConExpr& ce,
01168 AST::Node *) {
01169 rel(s, getSetVar(s, ce[0]), SRT_SUB, getSetVar(s, ce[1]),
01170 getBoolVar(s, ce[2]));
01171 }
01172 void p_set_superset_reif(FlatZincSpace& s, const ConExpr& ce,
01173 AST::Node *) {
01174 rel(s, getSetVar(s, ce[0]), SRT_SUP, getSetVar(s, ce[1]),
01175 getBoolVar(s, ce[2]));
01176 }
01177 void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01178 if (!ce[1]->isSetVar()) {
01179 AST::SetLit* sl = ce[1]->getSet();
01180 IntSet d;
01181 if (sl->interval) {
01182 d = IntSet(sl->min, sl->max);
01183 } else {
01184 Region re(s);
01185 int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
01186 for (int i=sl->s.size(); i--; )
01187 is[i] = sl->s[i];
01188 d = IntSet(is, sl->s.size());
01189 }
01190 if (ce[0]->isBoolVar()) {
01191 assert(sl->interval);
01192 rel(s, getBoolVar(s, ce[0]), IRT_GQ, sl->min, getBoolVar(s, ce[2]));
01193 rel(s, getBoolVar(s, ce[0]), IRT_LQ, sl->max, getBoolVar(s, ce[2]));
01194 } else {
01195 dom(s, getIntVar(s, ce[0]), d, getBoolVar(s, ce[2]));
01196 }
01197 } else {
01198 if (!ce[0]->isIntVar()) {
01199 dom(s, getSetVar(s, ce[1]), SRT_SUP, ce[0]->getInt(),
01200 getBoolVar(s, ce[2]));
01201 } else {
01202 rel(s, getSetVar(s, ce[1]), SRT_SUP, getIntVar(s, ce[0]),
01203 getBoolVar(s, ce[2]));
01204 }
01205 }
01206 }
01207 void p_set_disjoint(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01208 rel(s, getSetVar(s, ce[0]), SRT_DISJ, getSetVar(s, ce[1]));
01209 }
01210
01211 void p_array_set_element(FlatZincSpace& s, const ConExpr& ce,
01212 AST::Node*) {
01213 bool isConstant = true;
01214 AST::Array* a = ce[1]->getArray();
01215 for (int i=a->a.size(); i--;) {
01216 if (a->a[i]->isSetVar()) {
01217 isConstant = false;
01218 break;
01219 }
01220 }
01221 IntVar selector = getIntVar(s, ce[0]);
01222 post(s, selector > 0);
01223 if (isConstant) {
01224 IntSetArgs sv = arg2intsetargs(ce[1],1);
01225 element(s, sv, selector, getSetVar(s, ce[2]));
01226 } else {
01227 SetVarArgs sv = arg2setvarargs(s, ce[1], 1);
01228 element(s, sv, selector, getSetVar(s, ce[2]));
01229 }
01230 }
01231
01232 void p_array_set_element_op(FlatZincSpace& s, const ConExpr& ce,
01233 AST::Node*, SetOpType op,
01234 const IntSet& universe =
01235 IntSet(Set::Limits::min,Set::Limits::max)) {
01236 bool isConstant = true;
01237 AST::Array* a = ce[1]->getArray();
01238 for (int i=a->a.size(); i--;) {
01239 if (a->a[i]->isSetVar()) {
01240 isConstant = false;
01241 break;
01242 }
01243 }
01244 SetVar selector = getSetVar(s, ce[0]);
01245 dom(s, selector, SRT_DISJ, 0);
01246 if (isConstant) {
01247 IntSetArgs sv = arg2intsetargs(ce[1], 1);
01248 element(s, op, sv, selector, getSetVar(s, ce[2]), universe);
01249 } else {
01250 SetVarArgs sv = arg2setvarargs(s, ce[1], 1);
01251 element(s, op, sv, selector, getSetVar(s, ce[2]), universe);
01252 }
01253 }
01254
01255 void p_array_set_element_union(FlatZincSpace& s, const ConExpr& ce,
01256 AST::Node* ann) {
01257 p_array_set_element_op(s, ce, ann, SOT_UNION);
01258 }
01259
01260 void p_array_set_element_intersect(FlatZincSpace& s, const ConExpr& ce,
01261 AST::Node* ann) {
01262 p_array_set_element_op(s, ce, ann, SOT_INTER);
01263 }
01264
01265 void p_array_set_element_intersect_in(FlatZincSpace& s,
01266 const ConExpr& ce,
01267 AST::Node* ann) {
01268 AST::SetLit* sl = ce[3]->getSet();
01269 IntSet d;
01270 if (sl->interval) {
01271 d = IntSet(sl->min, sl->max);
01272 } else {
01273 Region re(s);
01274 int* is = re.alloc<int>(static_cast<unsigned long int>(sl->s.size()));
01275 for (int i=sl->s.size(); i--; )
01276 is[i] = sl->s[i];
01277 d = IntSet(is, sl->s.size());
01278 }
01279 p_array_set_element_op(s, ce, ann, SOT_INTER, d);
01280 }
01281
01282 void p_array_set_element_partition(FlatZincSpace& s, const ConExpr& ce,
01283 AST::Node* ann) {
01284 p_array_set_element_op(s, ce, ann, SOT_DUNION);
01285 }
01286
01287 void p_set_convex(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01288 convex(s, getSetVar(s, ce[0]));
01289 }
01290
01291 void p_array_set_seq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01292 SetVarArgs sv = arg2setvarargs(s, ce[0]);
01293 sequence(s, sv);
01294 }
01295
01296 void p_array_set_seq_union(FlatZincSpace& s, const ConExpr& ce,
01297 AST::Node *) {
01298 SetVarArgs sv = arg2setvarargs(s, ce[0]);
01299 sequence(s, sv, getSetVar(s, ce[1]));
01300 }
01301
01302 class SetPoster {
01303 public:
01304 SetPoster(void) {
01305 registry().add("set_eq", &p_set_eq);
01306 registry().add("equal", &p_set_eq);
01307 registry().add("set_ne", &p_set_ne);
01308 registry().add("set_union", &p_set_union);
01309 registry().add("array_set_element", &p_array_set_element);
01310 registry().add("set_intersect", &p_set_intersect);
01311 registry().add("set_diff", &p_set_diff);
01312 registry().add("set_symdiff", &p_set_symdiff);
01313 registry().add("set_subset", &p_set_subset);
01314 registry().add("set_superset", &p_set_superset);
01315 registry().add("set_card", &p_set_card);
01316 registry().add("set_in", &p_set_in);
01317 registry().add("set_eq_reif", &p_set_eq_reif);
01318 registry().add("equal_reif", &p_set_eq_reif);
01319 registry().add("set_ne_reif", &p_set_ne_reif);
01320 registry().add("set_subset_reif", &p_set_subset_reif);
01321 registry().add("set_superset_reif", &p_set_superset_reif);
01322 registry().add("set_in_reif", &p_set_in_reif);
01323 registry().add("disjoint", &p_set_disjoint);
01324
01325 registry().add("array_set_union", &p_array_set_union);
01326 registry().add("array_set_partition", &p_array_set_partition);
01327 registry().add("set_convex", &p_set_convex);
01328 registry().add("array_set_seq", &p_array_set_seq);
01329 registry().add("array_set_seq_union", &p_array_set_seq_union);
01330 registry().add("array_set_element_union",
01331 &p_array_set_element_union);
01332 registry().add("array_set_element_intersect",
01333 &p_array_set_element_intersect);
01334 registry().add("array_set_element_intersect_in",
01335 &p_array_set_element_intersect_in);
01336 registry().add("array_set_element_partition",
01337 &p_array_set_element_partition);
01338 }
01339 };
01340 SetPoster __set_poster;
01341 #endif
01342
01343 }
01344 }}
01345
01346