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 #include <gecode/flatzinc/registry.hh>
00039 #include <gecode/kernel.hh>
00040 #include <gecode/int.hh>
00041 #include <gecode/minimodel.hh>
00042
00043 #ifdef GECODE_HAS_SET_VARS
00044 #include <gecode/set.hh>
00045 #endif
00046 #ifdef GECODE_HAS_FLOAT_VARS
00047 #include <gecode/float.hh>
00048 #endif
00049 #include <gecode/flatzinc.hh>
00050
00051 namespace Gecode { namespace FlatZinc {
00052
00053 Registry& registry(void) {
00054 static Registry r;
00055 return r;
00056 }
00057
00058 void
00059 Registry::post(FlatZincSpace& s, const ConExpr& ce) {
00060 std::map<std::string,poster>::iterator i = r.find(ce.id);
00061 if (i == r.end()) {
00062 throw FlatZinc::Error("Registry",
00063 std::string("Constraint ")+ce.id+" not found");
00064 }
00065 i->second(s, ce, ce.ann);
00066 }
00067
00068 void
00069 Registry::add(const std::string& id, poster p) {
00070 r[id] = p;
00071 r["gecode_" + id] = p;
00072 }
00073
00074 namespace {
00075
00076 void p_distinct(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00077 IntVarArgs va = s.arg2intvarargs(ce[0]);
00078 IntPropLevel ipl = s.ann2ipl(ann);
00079 unshare(s, va);
00080 distinct(s, va, ipl == IPL_DEF ? IPL_BND : ipl);
00081 }
00082
00083 void p_distinctOffset(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00084 IntVarArgs va = s.arg2intvarargs(ce[1]);
00085 unshare(s, va);
00086 AST::Array* offs = ce.args->a[0]->getArray();
00087 IntArgs oa(offs->a.size());
00088 for (int i=offs->a.size(); i--; ) {
00089 oa[i] = offs->a[i]->getInt();
00090 }
00091 IntPropLevel ipl = s.ann2ipl(ann);
00092 distinct(s, oa, va, ipl == IPL_DEF ? IPL_BND : ipl);
00093 }
00094
00095 void p_all_equal(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00096 IntVarArgs va = s.arg2intvarargs(ce[0]);
00097 rel(s, va, IRT_EQ, s.ann2ipl(ann));
00098 }
00099
00100 void p_int_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
00101 AST::Node* ann) {
00102 if (ce[0]->isIntVar()) {
00103 if (ce[1]->isIntVar()) {
00104 rel(s, s.arg2IntVar(ce[0]), irt, s.arg2IntVar(ce[1]),
00105 s.ann2ipl(ann));
00106 } else {
00107 rel(s, s.arg2IntVar(ce[0]), irt, ce[1]->getInt(), s.ann2ipl(ann));
00108 }
00109 } else {
00110 rel(s, s.arg2IntVar(ce[1]), swap(irt), ce[0]->getInt(),
00111 s.ann2ipl(ann));
00112 }
00113 }
00114 void p_int_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00115 p_int_CMP(s, IRT_EQ, ce, ann);
00116 }
00117 void p_int_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00118 p_int_CMP(s, IRT_NQ, ce, ann);
00119 }
00120 void p_int_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00121 p_int_CMP(s, IRT_GQ, ce, ann);
00122 }
00123 void p_int_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00124 p_int_CMP(s, IRT_GR, ce, ann);
00125 }
00126 void p_int_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00127 p_int_CMP(s, IRT_LQ, ce, ann);
00128 }
00129 void p_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00130 p_int_CMP(s, IRT_LE, ce, ann);
00131 }
00132 void p_int_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm,
00133 const ConExpr& ce, AST::Node* ann) {
00134 if (rm == RM_EQV && ce[2]->isBool()) {
00135 if (ce[2]->getBool()) {
00136 p_int_CMP(s, irt, ce, ann);
00137 } else {
00138 p_int_CMP(s, neg(irt), ce, ann);
00139 }
00140 return;
00141 }
00142 if (ce[0]->isIntVar()) {
00143 if (ce[1]->isIntVar()) {
00144 rel(s, s.arg2IntVar(ce[0]), irt, s.arg2IntVar(ce[1]),
00145 Reify(s.arg2BoolVar(ce[2]), rm), s.ann2ipl(ann));
00146 } else {
00147 rel(s, s.arg2IntVar(ce[0]), irt, ce[1]->getInt(),
00148 Reify(s.arg2BoolVar(ce[2]), rm), s.ann2ipl(ann));
00149 }
00150 } else {
00151 rel(s, s.arg2IntVar(ce[1]), swap(irt), ce[0]->getInt(),
00152 Reify(s.arg2BoolVar(ce[2]), rm), s.ann2ipl(ann));
00153 }
00154 }
00155
00156
00157 void p_int_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00158 p_int_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann);
00159 }
00160 void p_int_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00161 p_int_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann);
00162 }
00163 void p_int_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00164 p_int_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann);
00165 }
00166 void p_int_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00167 p_int_CMP_reif(s, IRT_GR, RM_EQV, ce, ann);
00168 }
00169 void p_int_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00170 p_int_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann);
00171 }
00172 void p_int_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00173 p_int_CMP_reif(s, IRT_LE, RM_EQV, ce, ann);
00174 }
00175
00176 void p_int_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00177 p_int_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann);
00178 }
00179 void p_int_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00180 p_int_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann);
00181 }
00182 void p_int_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00183 p_int_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann);
00184 }
00185 void p_int_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00186 p_int_CMP_reif(s, IRT_GR, RM_IMP, ce, ann);
00187 }
00188 void p_int_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00189 p_int_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann);
00190 }
00191 void p_int_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00192 p_int_CMP_reif(s, IRT_LE, RM_IMP, ce, ann);
00193 }
00194
00195
00196 void p_int_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
00197 AST::Node* ann) {
00198 IntArgs ia = s.arg2intargs(ce[0]);
00199 int singleIntVar;
00200 if (s.isBoolArray(ce[1],singleIntVar)) {
00201 if (singleIntVar != -1) {
00202 if (std::abs(ia[singleIntVar]) == 1 && ce[2]->getInt() == 0) {
00203 IntVar siv = s.arg2IntVar(ce[1]->getArray()->a[singleIntVar]);
00204 BoolVarArgs iv = s.arg2boolvarargs(ce[1], 0, singleIntVar);
00205 IntArgs ia_tmp(ia.size()-1);
00206 int count = 0;
00207 for (int i=0; i<ia.size(); i++) {
00208 if (i != singleIntVar)
00209 ia_tmp[count++] = ia[singleIntVar] == -1 ? ia[i] : -ia[i];
00210 }
00211 IntRelType t = (ia[singleIntVar] == -1 ? irt : swap(irt));
00212 linear(s, ia_tmp, iv, t, siv, s.ann2ipl(ann));
00213 } else {
00214 IntVarArgs iv = s.arg2intvarargs(ce[1]);
00215 linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2ipl(ann));
00216 }
00217 } else {
00218 BoolVarArgs iv = s.arg2boolvarargs(ce[1]);
00219 linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2ipl(ann));
00220 }
00221 } else {
00222 IntVarArgs iv = s.arg2intvarargs(ce[1]);
00223 linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2ipl(ann));
00224 }
00225 }
00226 void p_int_lin_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm,
00227 const ConExpr& ce, AST::Node* ann) {
00228 if (rm == RM_EQV && ce[2]->isBool()) {
00229 if (ce[2]->getBool()) {
00230 p_int_lin_CMP(s, irt, ce, ann);
00231 } else {
00232 p_int_lin_CMP(s, neg(irt), ce, ann);
00233 }
00234 return;
00235 }
00236 IntArgs ia = s.arg2intargs(ce[0]);
00237 int singleIntVar;
00238 if (s.isBoolArray(ce[1],singleIntVar)) {
00239 if (singleIntVar != -1) {
00240 if (std::abs(ia[singleIntVar]) == 1 && ce[2]->getInt() == 0) {
00241 IntVar siv = s.arg2IntVar(ce[1]->getArray()->a[singleIntVar]);
00242 BoolVarArgs iv = s.arg2boolvarargs(ce[1], 0, singleIntVar);
00243 IntArgs ia_tmp(ia.size()-1);
00244 int count = 0;
00245 for (int i=0; i<ia.size(); i++) {
00246 if (i != singleIntVar)
00247 ia_tmp[count++] = ia[singleIntVar] == -1 ? ia[i] : -ia[i];
00248 }
00249 IntRelType t = (ia[singleIntVar] == -1 ? irt : swap(irt));
00250 linear(s, ia_tmp, iv, t, siv, Reify(s.arg2BoolVar(ce[3]), rm),
00251 s.ann2ipl(ann));
00252 } else {
00253 IntVarArgs iv = s.arg2intvarargs(ce[1]);
00254 linear(s, ia, iv, irt, ce[2]->getInt(),
00255 Reify(s.arg2BoolVar(ce[3]), rm), s.ann2ipl(ann));
00256 }
00257 } else {
00258 BoolVarArgs iv = s.arg2boolvarargs(ce[1]);
00259 linear(s, ia, iv, irt, ce[2]->getInt(),
00260 Reify(s.arg2BoolVar(ce[3]), rm), s.ann2ipl(ann));
00261 }
00262 } else {
00263 IntVarArgs iv = s.arg2intvarargs(ce[1]);
00264 linear(s, ia, iv, irt, ce[2]->getInt(),
00265 Reify(s.arg2BoolVar(ce[3]), rm),
00266 s.ann2ipl(ann));
00267 }
00268 }
00269 void p_int_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00270 p_int_lin_CMP(s, IRT_EQ, ce, ann);
00271 }
00272 void p_int_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00273 p_int_lin_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann);
00274 }
00275 void p_int_lin_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00276 p_int_lin_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann);
00277 }
00278 void p_int_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00279 p_int_lin_CMP(s, IRT_NQ, ce, ann);
00280 }
00281 void p_int_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00282 p_int_lin_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann);
00283 }
00284 void p_int_lin_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00285 p_int_lin_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann);
00286 }
00287 void p_int_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00288 p_int_lin_CMP(s, IRT_LQ, ce, ann);
00289 }
00290 void p_int_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00291 p_int_lin_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann);
00292 }
00293 void p_int_lin_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00294 p_int_lin_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann);
00295 }
00296 void p_int_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00297 p_int_lin_CMP(s, IRT_LE, ce, ann);
00298 }
00299 void p_int_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00300 p_int_lin_CMP_reif(s, IRT_LE, RM_EQV, ce, ann);
00301 }
00302 void p_int_lin_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00303 p_int_lin_CMP_reif(s, IRT_LE, RM_IMP, ce, ann);
00304 }
00305 void p_int_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00306 p_int_lin_CMP(s, IRT_GQ, ce, ann);
00307 }
00308 void p_int_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00309 p_int_lin_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann);
00310 }
00311 void p_int_lin_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00312 p_int_lin_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann);
00313 }
00314 void p_int_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00315 p_int_lin_CMP(s, IRT_GR, ce, ann);
00316 }
00317 void p_int_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00318 p_int_lin_CMP_reif(s, IRT_GR, RM_EQV, ce, ann);
00319 }
00320 void p_int_lin_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00321 p_int_lin_CMP_reif(s, IRT_GR, RM_IMP, ce, ann);
00322 }
00323
00324 void p_bool_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
00325 AST::Node* ann) {
00326 IntArgs ia = s.arg2intargs(ce[0]);
00327 BoolVarArgs iv = s.arg2boolvarargs(ce[1]);
00328 if (ce[2]->isIntVar())
00329 linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()], s.ann2ipl(ann));
00330 else
00331 linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2ipl(ann));
00332 }
00333 void p_bool_lin_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm,
00334 const ConExpr& ce, AST::Node* ann) {
00335 if (rm == RM_EQV && ce[2]->isBool()) {
00336 if (ce[2]->getBool()) {
00337 p_bool_lin_CMP(s, irt, ce, ann);
00338 } else {
00339 p_bool_lin_CMP(s, neg(irt), ce, ann);
00340 }
00341 return;
00342 }
00343 IntArgs ia = s.arg2intargs(ce[0]);
00344 BoolVarArgs iv = s.arg2boolvarargs(ce[1]);
00345 if (ce[2]->isIntVar())
00346 linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()],
00347 Reify(s.arg2BoolVar(ce[3]), rm),
00348 s.ann2ipl(ann));
00349 else
00350 linear(s, ia, iv, irt, ce[2]->getInt(),
00351 Reify(s.arg2BoolVar(ce[3]), rm),
00352 s.ann2ipl(ann));
00353 }
00354 void p_bool_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00355 p_bool_lin_CMP(s, IRT_EQ, ce, ann);
00356 }
00357 void p_bool_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00358 {
00359 p_bool_lin_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann);
00360 }
00361 void p_bool_lin_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00362 {
00363 p_bool_lin_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann);
00364 }
00365 void p_bool_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00366 p_bool_lin_CMP(s, IRT_NQ, ce, ann);
00367 }
00368 void p_bool_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00369 {
00370 p_bool_lin_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann);
00371 }
00372 void p_bool_lin_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00373 {
00374 p_bool_lin_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann);
00375 }
00376 void p_bool_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00377 p_bool_lin_CMP(s, IRT_LQ, ce, ann);
00378 }
00379 void p_bool_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00380 {
00381 p_bool_lin_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann);
00382 }
00383 void p_bool_lin_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00384 {
00385 p_bool_lin_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann);
00386 }
00387 void p_bool_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00388 {
00389 p_bool_lin_CMP(s, IRT_LE, ce, ann);
00390 }
00391 void p_bool_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00392 {
00393 p_bool_lin_CMP_reif(s, IRT_LE, RM_EQV, ce, ann);
00394 }
00395 void p_bool_lin_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00396 {
00397 p_bool_lin_CMP_reif(s, IRT_LE, RM_IMP, ce, ann);
00398 }
00399 void p_bool_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00400 p_bool_lin_CMP(s, IRT_GQ, ce, ann);
00401 }
00402 void p_bool_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00403 {
00404 p_bool_lin_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann);
00405 }
00406 void p_bool_lin_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00407 {
00408 p_bool_lin_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann);
00409 }
00410 void p_bool_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00411 p_bool_lin_CMP(s, IRT_GR, ce, ann);
00412 }
00413 void p_bool_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00414 {
00415 p_bool_lin_CMP_reif(s, IRT_GR, RM_EQV, ce, ann);
00416 }
00417 void p_bool_lin_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00418 {
00419 p_bool_lin_CMP_reif(s, IRT_GR, RM_IMP, ce, ann);
00420 }
00421
00422
00423
00424 void p_int_plus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00425 if (!ce[0]->isIntVar()) {
00426 rel(s, ce[0]->getInt() + s.arg2IntVar(ce[1])
00427 == s.arg2IntVar(ce[2]), s.ann2ipl(ann));
00428 } else if (!ce[1]->isIntVar()) {
00429 rel(s, s.arg2IntVar(ce[0]) + ce[1]->getInt()
00430 == s.arg2IntVar(ce[2]), s.ann2ipl(ann));
00431 } else if (!ce[2]->isIntVar()) {
00432 rel(s, s.arg2IntVar(ce[0]) + s.arg2IntVar(ce[1])
00433 == ce[2]->getInt(), s.ann2ipl(ann));
00434 } else {
00435 rel(s, s.arg2IntVar(ce[0]) + s.arg2IntVar(ce[1])
00436 == s.arg2IntVar(ce[2]), s.ann2ipl(ann));
00437 }
00438 }
00439
00440 void p_int_minus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00441 if (!ce[0]->isIntVar()) {
00442 rel(s, ce[0]->getInt() - s.arg2IntVar(ce[1])
00443 == s.arg2IntVar(ce[2]), s.ann2ipl(ann));
00444 } else if (!ce[1]->isIntVar()) {
00445 rel(s, s.arg2IntVar(ce[0]) - ce[1]->getInt()
00446 == s.arg2IntVar(ce[2]), s.ann2ipl(ann));
00447 } else if (!ce[2]->isIntVar()) {
00448 rel(s, s.arg2IntVar(ce[0]) - s.arg2IntVar(ce[1])
00449 == ce[2]->getInt(), s.ann2ipl(ann));
00450 } else {
00451 rel(s, s.arg2IntVar(ce[0]) - s.arg2IntVar(ce[1])
00452 == s.arg2IntVar(ce[2]), s.ann2ipl(ann));
00453 }
00454 }
00455
00456 void p_int_times(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00457 IntVar x0 = s.arg2IntVar(ce[0]);
00458 IntVar x1 = s.arg2IntVar(ce[1]);
00459 IntVar x2 = s.arg2IntVar(ce[2]);
00460 mult(s, x0, x1, x2, s.ann2ipl(ann));
00461 }
00462 void p_int_pow(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00463 IntVar x0 = s.arg2IntVar(ce[0]);
00464 IntVar x2 = s.arg2IntVar(ce[2]);
00465 pow(s, x0, ce[1]->getInt(), x2, s.ann2ipl(ann));
00466 }
00467 void p_int_div(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00468 IntVar x0 = s.arg2IntVar(ce[0]);
00469 IntVar x1 = s.arg2IntVar(ce[1]);
00470 IntVar x2 = s.arg2IntVar(ce[2]);
00471 div(s,x0,x1,x2, s.ann2ipl(ann));
00472 }
00473 void p_int_mod(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00474 IntVar x0 = s.arg2IntVar(ce[0]);
00475 IntVar x1 = s.arg2IntVar(ce[1]);
00476 IntVar x2 = s.arg2IntVar(ce[2]);
00477 mod(s,x0,x1,x2, s.ann2ipl(ann));
00478 }
00479
00480 void p_int_min(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00481 IntVar x0 = s.arg2IntVar(ce[0]);
00482 IntVar x1 = s.arg2IntVar(ce[1]);
00483 IntVar x2 = s.arg2IntVar(ce[2]);
00484 min(s, x0, x1, x2, s.ann2ipl(ann));
00485 }
00486 void p_int_max(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00487 IntVar x0 = s.arg2IntVar(ce[0]);
00488 IntVar x1 = s.arg2IntVar(ce[1]);
00489 IntVar x2 = s.arg2IntVar(ce[2]);
00490 max(s, x0, x1, x2, s.ann2ipl(ann));
00491 }
00492 void p_int_negate(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00493 IntVar x0 = s.arg2IntVar(ce[0]);
00494 IntVar x1 = s.arg2IntVar(ce[1]);
00495 rel(s, x0 == -x1, s.ann2ipl(ann));
00496 }
00497
00498
00499 void p_bool_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
00500 AST::Node* ann) {
00501 rel(s, s.arg2BoolVar(ce[0]), irt, s.arg2BoolVar(ce[1]),
00502 s.ann2ipl(ann));
00503 }
00504 void p_bool_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm,
00505 const ConExpr& ce, AST::Node* ann) {
00506 rel(s, s.arg2BoolVar(ce[0]), irt, s.arg2BoolVar(ce[1]),
00507 Reify(s.arg2BoolVar(ce[2]), rm), s.ann2ipl(ann));
00508 }
00509 void p_bool_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00510 p_bool_CMP(s, IRT_EQ, ce, ann);
00511 }
00512 void p_bool_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00513 p_bool_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann);
00514 }
00515 void p_bool_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00516 p_bool_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann);
00517 }
00518 void p_bool_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00519 p_bool_CMP(s, IRT_NQ, ce, ann);
00520 }
00521 void p_bool_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00522 p_bool_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann);
00523 }
00524 void p_bool_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00525 p_bool_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann);
00526 }
00527 void p_bool_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00528 p_bool_CMP(s, IRT_GQ, ce, ann);
00529 }
00530 void p_bool_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00531 p_bool_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann);
00532 }
00533 void p_bool_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00534 p_bool_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann);
00535 }
00536 void p_bool_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00537 p_bool_CMP(s, IRT_LQ, ce, ann);
00538 }
00539 void p_bool_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00540 p_bool_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann);
00541 }
00542 void p_bool_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00543 p_bool_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann);
00544 }
00545 void p_bool_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00546 p_bool_CMP(s, IRT_GR, ce, ann);
00547 }
00548 void p_bool_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00549 p_bool_CMP_reif(s, IRT_GR, RM_EQV, ce, ann);
00550 }
00551 void p_bool_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00552 p_bool_CMP_reif(s, IRT_GR, RM_IMP, ce, ann);
00553 }
00554 void p_bool_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00555 p_bool_CMP(s, IRT_LE, ce, ann);
00556 }
00557 void p_bool_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00558 p_bool_CMP_reif(s, IRT_LE, RM_EQV, ce, ann);
00559 }
00560 void p_bool_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00561 p_bool_CMP_reif(s, IRT_LE, RM_IMP, ce, ann);
00562 }
00563
00564 #define BOOL_OP(op) \
00565 BoolVar b0 = s.arg2BoolVar(ce[0]); \
00566 BoolVar b1 = s.arg2BoolVar(ce[1]); \
00567 if (ce[2]->isBool()) { \
00568 rel(s, b0, op, b1, ce[2]->getBool(), s.ann2ipl(ann)); \
00569 } else { \
00570 rel(s, b0, op, b1, s.bv[ce[2]->getBoolVar()], s.ann2ipl(ann)); \
00571 }
00572
00573 #define BOOL_ARRAY_OP(op) \
00574 BoolVarArgs bv = s.arg2boolvarargs(ce[0]); \
00575 if (ce.size()==1) { \
00576 rel(s, op, bv, 1, s.ann2ipl(ann)); \
00577 } else if (ce[1]->isBool()) { \
00578 rel(s, op, bv, ce[1]->getBool(), s.ann2ipl(ann)); \
00579 } else { \
00580 rel(s, op, bv, s.bv[ce[1]->getBoolVar()], s.ann2ipl(ann)); \
00581 }
00582
00583 void p_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00584 BOOL_OP(BOT_OR);
00585 }
00586 void p_bool_or_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00587 BoolVar b0 = s.arg2BoolVar(ce[0]);
00588 BoolVar b1 = s.arg2BoolVar(ce[1]);
00589 BoolVar b2 = s.arg2BoolVar(ce[2]);
00590 clause(s, BOT_OR, BoolVarArgs()<<b0<<b1, BoolVarArgs()<<b2, 1,
00591 s.ann2ipl(ann));
00592 }
00593 void p_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00594 BOOL_OP(BOT_AND);
00595 }
00596 void p_bool_and_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00597 BoolVar b0 = s.arg2BoolVar(ce[0]);
00598 BoolVar b1 = s.arg2BoolVar(ce[1]);
00599 BoolVar b2 = s.arg2BoolVar(ce[2]);
00600 rel(s, b2, BOT_IMP, b0, 1, s.ann2ipl(ann));
00601 rel(s, b2, BOT_IMP, b1, 1, s.ann2ipl(ann));
00602 }
00603 void p_array_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00604 {
00605 BOOL_ARRAY_OP(BOT_AND);
00606 }
00607 void p_array_bool_and_imp(FlatZincSpace& s, const ConExpr& ce,
00608 AST::Node* ann)
00609 {
00610 BoolVarArgs bv = s.arg2boolvarargs(ce[0]);
00611 BoolVar b1 = s.arg2BoolVar(ce[1]);
00612 for (unsigned int i=bv.size(); i--;)
00613 rel(s, b1, BOT_IMP, bv[i], 1, s.ann2ipl(ann));
00614 }
00615 void p_array_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00616 {
00617 BOOL_ARRAY_OP(BOT_OR);
00618 }
00619 void p_array_bool_or_imp(FlatZincSpace& s, const ConExpr& ce,
00620 AST::Node* ann)
00621 {
00622 BoolVarArgs bv = s.arg2boolvarargs(ce[0]);
00623 BoolVar b1 = s.arg2BoolVar(ce[1]);
00624 clause(s, BOT_OR, bv, BoolVarArgs()<<b1, 1, s.ann2ipl(ann));
00625 }
00626 void p_array_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
00627 {
00628 BOOL_ARRAY_OP(BOT_XOR);
00629 }
00630 void p_array_bool_xor_imp(FlatZincSpace& s, const ConExpr& ce,
00631 AST::Node* ann)
00632 {
00633 BoolVarArgs bv = s.arg2boolvarargs(ce[0]);
00634 BoolVar tmp(s,0,1);
00635 rel(s, BOT_XOR, bv, tmp, s.ann2ipl(ann));
00636 rel(s, s.arg2BoolVar(ce[1]), BOT_IMP, tmp, 1);
00637 }
00638 void p_array_bool_clause(FlatZincSpace& s, const ConExpr& ce,
00639 AST::Node* ann) {
00640 BoolVarArgs bvp = s.arg2boolvarargs(ce[0]);
00641 BoolVarArgs bvn = s.arg2boolvarargs(ce[1]);
00642 clause(s, BOT_OR, bvp, bvn, 1, s.ann2ipl(ann));
00643 }
00644 void p_array_bool_clause_reif(FlatZincSpace& s, const ConExpr& ce,
00645 AST::Node* ann) {
00646 BoolVarArgs bvp = s.arg2boolvarargs(ce[0]);
00647 BoolVarArgs bvn = s.arg2boolvarargs(ce[1]);
00648 BoolVar b0 = s.arg2BoolVar(ce[2]);
00649 clause(s, BOT_OR, bvp, bvn, b0, s.ann2ipl(ann));
00650 }
00651 void p_array_bool_clause_imp(FlatZincSpace& s, const ConExpr& ce,
00652 AST::Node* ann) {
00653 BoolVarArgs bvp = s.arg2boolvarargs(ce[0]);
00654 BoolVarArgs bvn = s.arg2boolvarargs(ce[1]);
00655 BoolVar b0 = s.arg2BoolVar(ce[2]);
00656 clause(s, BOT_OR, bvp, bvn, b0, s.ann2ipl(ann));
00657 }
00658 void p_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00659 BOOL_OP(BOT_XOR);
00660 }
00661 void p_bool_xor_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00662 BoolVar b0 = s.arg2BoolVar(ce[0]);
00663 BoolVar b1 = s.arg2BoolVar(ce[1]);
00664 BoolVar b2 = s.arg2BoolVar(ce[2]);
00665 clause(s, BOT_OR, BoolVarArgs()<<b0<<b1, BoolVarArgs()<<b2, 1,
00666 s.ann2ipl(ann));
00667 clause(s, BOT_OR, BoolVarArgs(), BoolVarArgs()<<b0<<b1<<b2, 1,
00668 s.ann2ipl(ann));
00669 }
00670 void p_bool_l_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00671 BoolVar b0 = s.arg2BoolVar(ce[0]);
00672 BoolVar b1 = s.arg2BoolVar(ce[1]);
00673 if (ce[2]->isBool()) {
00674 rel(s, b1, BOT_IMP, b0, ce[2]->getBool(), s.ann2ipl(ann));
00675 } else {
00676 rel(s, b1, BOT_IMP, b0, s.bv[ce[2]->getBoolVar()], s.ann2ipl(ann));
00677 }
00678 }
00679 void p_bool_r_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00680 BOOL_OP(BOT_IMP);
00681 }
00682 void p_bool_not(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00683 BoolVar x0 = s.arg2BoolVar(ce[0]);
00684 BoolVar x1 = s.arg2BoolVar(ce[1]);
00685 rel(s, x0, BOT_XOR, x1, 1, s.ann2ipl(ann));
00686 }
00687
00688
00689 void p_array_int_element(FlatZincSpace& s, const ConExpr& ce,
00690 AST::Node* ann) {
00691 bool isConstant = true;
00692 AST::Array* a = ce[1]->getArray();
00693 for (int i=a->a.size(); i--;) {
00694 if (!a->a[i]->isInt()) {
00695 isConstant = false;
00696 break;
00697 }
00698 }
00699 IntVar selector = s.arg2IntVar(ce[0]);
00700 rel(s, selector > 0);
00701 if (isConstant) {
00702 IntSharedArray sia = s.arg2intsharedarray(ce[1], 1);
00703 element(s, sia, selector, s.arg2IntVar(ce[2]), s.ann2ipl(ann));
00704 } else {
00705 IntVarArgs iv = s.arg2intvarargs(ce[1], 1);
00706 element(s, iv, selector, s.arg2IntVar(ce[2]), s.ann2ipl(ann));
00707 }
00708 }
00709 void p_array_bool_element(FlatZincSpace& s, const ConExpr& ce,
00710 AST::Node* ann) {
00711 bool isConstant = true;
00712 AST::Array* a = ce[1]->getArray();
00713 for (int i=a->a.size(); i--;) {
00714 if (!a->a[i]->isBool()) {
00715 isConstant = false;
00716 break;
00717 }
00718 }
00719 IntVar selector = s.arg2IntVar(ce[0]);
00720 rel(s, selector > 0);
00721 if (isConstant) {
00722 IntSharedArray sia = s.arg2boolsharedarray(ce[1], 1);
00723 element(s, sia, selector, s.arg2BoolVar(ce[2]), s.ann2ipl(ann));
00724 } else {
00725 BoolVarArgs iv = s.arg2boolvarargs(ce[1], 1);
00726 element(s, iv, selector, s.arg2BoolVar(ce[2]), s.ann2ipl(ann));
00727 }
00728 }
00729
00730
00731 void p_bool2int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00732 BoolVar x0 = s.arg2BoolVar(ce[0]);
00733 IntVar x1 = s.arg2IntVar(ce[1]);
00734 if (ce[0]->isBoolVar() && ce[1]->isIntVar()) {
00735 s.aliasBool2Int(ce[1]->getIntVar(), ce[0]->getBoolVar());
00736 }
00737 channel(s, x0, x1, s.ann2ipl(ann));
00738 }
00739
00740 void p_int_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
00741 IntSet d = s.arg2intset(ce[1]);
00742 if (ce[0]->isBoolVar()) {
00743 IntSetRanges dr(d);
00744 Iter::Ranges::Singleton sr(0,1);
00745 Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
00746 IntSet d01(i);
00747 if (d01.size() == 0) {
00748 s.fail();
00749 } else {
00750 rel(s, s.arg2BoolVar(ce[0]), IRT_GQ, d01.min());
00751 rel(s, s.arg2BoolVar(ce[0]), IRT_LQ, d01.max());
00752 }
00753 } else {
00754 dom(s, s.arg2IntVar(ce[0]), d);
00755 }
00756 }
00757 void p_int_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
00758 IntSet d = s.arg2intset(ce[1]);
00759 if (ce[0]->isBoolVar()) {
00760 IntSetRanges dr(d);
00761 Iter::Ranges::Singleton sr(0,1);
00762 Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
00763 IntSet d01(i);
00764 if (d01.size() == 0) {
00765 rel(s, s.arg2BoolVar(ce[2]) == 0);
00766 } else if (d01.max() == 0) {
00767 rel(s, s.arg2BoolVar(ce[2]) == !s.arg2BoolVar(ce[0]));
00768 } else if (d01.min() == 1) {
00769 rel(s, s.arg2BoolVar(ce[2]) == s.arg2BoolVar(ce[0]));
00770 } else {
00771 rel(s, s.arg2BoolVar(ce[2]) == 1);
00772 }
00773 } else {
00774 dom(s, s.arg2IntVar(ce[0]), d, s.arg2BoolVar(ce[2]));
00775 }
00776 }
00777 void p_int_in_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
00778 IntSet d = s.arg2intset(ce[1]);
00779 if (ce[0]->isBoolVar()) {
00780 IntSetRanges dr(d);
00781 Iter::Ranges::Singleton sr(0,1);
00782 Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
00783 IntSet d01(i);
00784 if (d01.size() == 0) {
00785 rel(s, s.arg2BoolVar(ce[2]) == 0);
00786 } else if (d01.max() == 0) {
00787 rel(s, s.arg2BoolVar(ce[2]) >> !s.arg2BoolVar(ce[0]));
00788 } else if (d01.min() == 1) {
00789 rel(s, s.arg2BoolVar(ce[2]) >> s.arg2BoolVar(ce[0]));
00790 }
00791 } else {
00792 dom(s, s.arg2IntVar(ce[0]), d, Reify(s.arg2BoolVar(ce[2]),RM_IMP));
00793 }
00794 }
00795
00796
00797
00798 void p_abs(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00799 IntVar x0 = s.arg2IntVar(ce[0]);
00800 IntVar x1 = s.arg2IntVar(ce[1]);
00801 abs(s, x0, x1, s.ann2ipl(ann));
00802 }
00803
00804 void p_array_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00805 IntVarArgs iv0 = s.arg2intvarargs(ce[0]);
00806 IntVarArgs iv1 = s.arg2intvarargs(ce[1]);
00807 rel(s, iv0, IRT_LE, iv1, s.ann2ipl(ann));
00808 }
00809
00810 void p_array_int_lq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00811 IntVarArgs iv0 = s.arg2intvarargs(ce[0]);
00812 IntVarArgs iv1 = s.arg2intvarargs(ce[1]);
00813 rel(s, iv0, IRT_LQ, iv1, s.ann2ipl(ann));
00814 }
00815
00816 void p_array_bool_lt(FlatZincSpace& s, const ConExpr& ce,
00817 AST::Node* ann) {
00818 BoolVarArgs bv0 = s.arg2boolvarargs(ce[0]);
00819 BoolVarArgs bv1 = s.arg2boolvarargs(ce[1]);
00820 rel(s, bv0, IRT_LE, bv1, s.ann2ipl(ann));
00821 }
00822
00823 void p_array_bool_lq(FlatZincSpace& s, const ConExpr& ce,
00824 AST::Node* ann) {
00825 BoolVarArgs bv0 = s.arg2boolvarargs(ce[0]);
00826 BoolVarArgs bv1 = s.arg2boolvarargs(ce[1]);
00827 rel(s, bv0, IRT_LQ, bv1, s.ann2ipl(ann));
00828 }
00829
00830 void p_count(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00831 IntVarArgs iv = s.arg2intvarargs(ce[0]);
00832 if (!ce[1]->isIntVar()) {
00833 if (!ce[2]->isIntVar()) {
00834 count(s, iv, ce[1]->getInt(), IRT_EQ, ce[2]->getInt(),
00835 s.ann2ipl(ann));
00836 } else {
00837 count(s, iv, ce[1]->getInt(), IRT_EQ, s.arg2IntVar(ce[2]),
00838 s.ann2ipl(ann));
00839 }
00840 } else if (!ce[2]->isIntVar()) {
00841 count(s, iv, s.arg2IntVar(ce[1]), IRT_EQ, ce[2]->getInt(),
00842 s.ann2ipl(ann));
00843 } else {
00844 count(s, iv, s.arg2IntVar(ce[1]), IRT_EQ, s.arg2IntVar(ce[2]),
00845 s.ann2ipl(ann));
00846 }
00847 }
00848
00849 void p_count_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00850 IntVarArgs iv = s.arg2intvarargs(ce[0]);
00851 IntVar x = s.arg2IntVar(ce[1]);
00852 IntVar y = s.arg2IntVar(ce[2]);
00853 BoolVar b = s.arg2BoolVar(ce[3]);
00854 IntVar c(s,0,Int::Limits::max);
00855 count(s,iv,x,IRT_EQ,c,s.ann2ipl(ann));
00856 rel(s, b == (c==y));
00857 }
00858 void p_count_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00859 IntVarArgs iv = s.arg2intvarargs(ce[0]);
00860 IntVar x = s.arg2IntVar(ce[1]);
00861 IntVar y = s.arg2IntVar(ce[2]);
00862 BoolVar b = s.arg2BoolVar(ce[3]);
00863 IntVar c(s,0,Int::Limits::max);
00864 count(s,iv,x,IRT_EQ,c,s.ann2ipl(ann));
00865 rel(s, b >> (c==y));
00866 }
00867
00868 void count_rel(IntRelType irt,
00869 FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00870 IntVarArgs iv = s.arg2intvarargs(ce[1]);
00871 count(s, iv, ce[2]->getInt(), irt, ce[0]->getInt(), s.ann2ipl(ann));
00872 }
00873
00874 void p_at_most(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00875 count_rel(IRT_LQ, s, ce, ann);
00876 }
00877
00878 void p_at_least(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
00879 count_rel(IRT_GQ, s, ce, ann);
00880 }
00881
00882 void p_bin_packing_load(FlatZincSpace& s, const ConExpr& ce,
00883 AST::Node* ann) {
00884 int minIdx = ce[3]->getInt();
00885 IntVarArgs load = s.arg2intvarargs(ce[0]);
00886 IntVarArgs l;
00887 IntVarArgs bin = s.arg2intvarargs(ce[1]);
00888 for (int i=bin.size(); i--;)
00889 rel(s, bin[i] >= minIdx);
00890 if (minIdx > 0) {
00891 for (int i=minIdx; i--;)
00892 l << IntVar(s,0,0);
00893 } else if (minIdx < 0) {
00894 IntVarArgs bin2(bin.size());
00895 for (int i=bin.size(); i--;)
00896 bin2[i] = expr(s, bin[i]-minIdx, s.ann2ipl(ann));
00897 bin = bin2;
00898 }
00899 l << load;
00900 IntArgs sizes = s.arg2intargs(ce[2]);
00901
00902 IntVarArgs allvars = l + bin;
00903 unshare(s, allvars);
00904 binpacking(s, allvars.slice(0,1,l.size()), allvars.slice(l.size(),1,bin.size()),
00905 sizes, s.ann2ipl(ann));
00906 }
00907
00908 void p_global_cardinality(FlatZincSpace& s, const ConExpr& ce,
00909 AST::Node* ann) {
00910 IntVarArgs iv0 = s.arg2intvarargs(ce[0]);
00911 IntArgs cover = s.arg2intargs(ce[1]);
00912 IntVarArgs iv1 = s.arg2intvarargs(ce[2]);
00913
00914 Region re;
00915 IntSet cover_s(cover);
00916 IntSetRanges cover_r(cover_s);
00917 IntVarRanges* iv0_ri = re.alloc<IntVarRanges>(iv0.size());
00918 for (int i=iv0.size(); i--;)
00919 iv0_ri[i] = IntVarRanges(iv0[i]);
00920 Iter::Ranges::NaryUnion iv0_r(re,iv0_ri,iv0.size());
00921 Iter::Ranges::Diff<Iter::Ranges::NaryUnion,IntSetRanges>
00922 extra_r(iv0_r,cover_r);
00923 Iter::Ranges::ToValues<Iter::Ranges::Diff<
00924 Iter::Ranges::NaryUnion,IntSetRanges> > extra(extra_r);
00925 for (; extra(); ++extra) {
00926 cover << extra.val();
00927 iv1 << IntVar(s,0,iv0.size());
00928 }
00929 IntPropLevel ipl = s.ann2ipl(ann);
00930 if (ipl==IPL_DEF)
00931 ipl=IPL_BND;
00932 if (ipl==IPL_DOM) {
00933 IntVarArgs allvars = iv0+iv1;
00934 unshare(s, allvars);
00935 count(s, allvars.slice(0,1,iv0.size()),
00936 allvars.slice(iv0.size(),1,iv1.size()),
00937 cover, ipl);
00938 } else {
00939 unshare(s, iv0);
00940 count(s, iv0, iv1, cover, ipl);
00941 }
00942 }
00943
00944 void p_global_cardinality_closed(FlatZincSpace& s, const ConExpr& ce,
00945 AST::Node* ann) {
00946 IntVarArgs iv0 = s.arg2intvarargs(ce[0]);
00947 IntArgs cover = s.arg2intargs(ce[1]);
00948 IntVarArgs iv1 = s.arg2intvarargs(ce[2]);
00949 IntPropLevel ipl = s.ann2ipl(ann);
00950 if (ipl==IPL_DEF)
00951 ipl=IPL_BND;
00952 if (ipl==IPL_DOM) {
00953 IntVarArgs allvars = iv0+iv1;
00954 unshare(s, allvars);
00955 count(s, allvars.slice(0,1,iv0.size()),
00956 allvars.slice(iv0.size(),1,iv1.size()),
00957 cover, ipl);
00958 } else {
00959 unshare(s, iv0);
00960 count(s, iv0, iv1, cover, ipl);
00961 }
00962 }
00963
00964 void p_global_cardinality_low_up(FlatZincSpace& s, const ConExpr& ce,
00965 AST::Node* ann) {
00966 IntVarArgs x = s.arg2intvarargs(ce[0]);
00967 IntArgs cover = s.arg2intargs(ce[1]);
00968
00969 IntArgs lbound = s.arg2intargs(ce[2]);
00970 IntArgs ubound = s.arg2intargs(ce[3]);
00971 IntSetArgs y(cover.size());
00972 for (int i=cover.size(); i--;)
00973 y[i] = IntSet(lbound[i],ubound[i]);
00974
00975 IntSet cover_s(cover);
00976 Region re;
00977 IntVarRanges* xrs = re.alloc<IntVarRanges>(x.size());
00978 for (int i=x.size(); i--;)
00979 xrs[i].init(x[i]);
00980 Iter::Ranges::NaryUnion u(re, xrs, x.size());
00981 Iter::Ranges::ToValues<Iter::Ranges::NaryUnion> uv(u);
00982 for (; uv(); ++uv) {
00983 if (!cover_s.in(uv.val())) {
00984 cover << uv.val();
00985 y << IntSet(0,x.size());
00986 }
00987 }
00988 unshare(s, x);
00989 IntPropLevel ipl = s.ann2ipl(ann);
00990 if (ipl==IPL_DEF)
00991 ipl=IPL_BND;
00992 count(s, x, y, cover, ipl);
00993 }
00994
00995 void p_global_cardinality_low_up_closed(FlatZincSpace& s,
00996 const ConExpr& ce,
00997 AST::Node* ann) {
00998 IntVarArgs x = s.arg2intvarargs(ce[0]);
00999 IntArgs cover = s.arg2intargs(ce[1]);
01000
01001 IntArgs lbound = s.arg2intargs(ce[2]);
01002 IntArgs ubound = s.arg2intargs(ce[3]);
01003 IntSetArgs y(cover.size());
01004 for (int i=cover.size(); i--;)
01005 y[i] = IntSet(lbound[i],ubound[i]);
01006 unshare(s, x);
01007 IntPropLevel ipl = s.ann2ipl(ann);
01008 if (ipl==IPL_DEF)
01009 ipl=IPL_BND;
01010 count(s, x, y, cover, ipl);
01011 }
01012
01013 void p_minimum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01014 IntVarArgs iv = s.arg2intvarargs(ce[1]);
01015 min(s, iv, s.arg2IntVar(ce[0]), s.ann2ipl(ann));
01016 }
01017
01018 void p_maximum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01019 IntVarArgs iv = s.arg2intvarargs(ce[1]);
01020 max(s, iv, s.arg2IntVar(ce[0]), s.ann2ipl(ann));
01021 }
01022
01023 void p_minimum_arg(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01024 IntVarArgs iv = s.arg2intvarargs(ce[0]);
01025 int offset = ce[1]->getInt();
01026 argmin(s, iv, offset, s.arg2IntVar(ce[2]), true, s.ann2ipl(ann));
01027 }
01028
01029 void p_maximum_arg(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01030 IntVarArgs iv = s.arg2intvarargs(ce[0]);
01031 int offset = ce[1]->getInt();
01032 argmax(s, iv, offset, s.arg2IntVar(ce[2]), true, s.ann2ipl(ann));
01033 }
01034
01035 void p_minimum_arg_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01036 BoolVarArgs bv = s.arg2boolvarargs(ce[0]);
01037 int offset = ce[1]->getInt();
01038 argmin(s, bv, offset, s.arg2IntVar(ce[2]), true, s.ann2ipl(ann));
01039 }
01040
01041 void p_maximum_arg_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01042 BoolVarArgs bv = s.arg2boolvarargs(ce[0]);
01043 int offset = ce[1]->getInt();
01044 argmax(s, bv, offset, s.arg2IntVar(ce[2]), true, s.ann2ipl(ann));
01045 }
01046
01047 void p_regular(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01048 IntVarArgs iv = s.arg2intvarargs(ce[0]);
01049 int q = ce[1]->getInt();
01050 int symbols = ce[2]->getInt();
01051 IntArgs d = s.arg2intargs(ce[3]);
01052 int q0 = ce[4]->getInt();
01053
01054 int noOfTrans = 0;
01055 for (int i=1; i<=q; i++) {
01056 for (int j=1; j<=symbols; j++) {
01057 if (d[(i-1)*symbols+(j-1)] > 0)
01058 noOfTrans++;
01059 }
01060 }
01061
01062 Region re;
01063 DFA::Transition* t = re.alloc<DFA::Transition>(noOfTrans+1);
01064 noOfTrans = 0;
01065 for (int i=1; i<=q; i++) {
01066 for (int j=1; j<=symbols; j++) {
01067 if (d[(i-1)*symbols+(j-1)] > 0) {
01068 t[noOfTrans].i_state = i;
01069 t[noOfTrans].symbol = j;
01070 t[noOfTrans].o_state = d[(i-1)*symbols+(j-1)];
01071 noOfTrans++;
01072 }
01073 }
01074 }
01075 t[noOfTrans].i_state = -1;
01076
01077
01078 AST::SetLit* sl = ce[5]->getSet();
01079 int* f;
01080 if (sl->interval) {
01081 f = static_cast<int*>(heap.ralloc(sizeof(int)*(sl->max-sl->min+2)));
01082 for (int i=sl->min; i<=sl->max; i++)
01083 f[i-sl->min] = i;
01084 f[sl->max-sl->min+1] = -1;
01085 } else {
01086 f = static_cast<int*>(heap.ralloc(sizeof(int)*(sl->s.size()+1)));
01087 for (int j=sl->s.size(); j--; )
01088 f[j] = sl->s[j];
01089 f[sl->s.size()] = -1;
01090 }
01091
01092 DFA dfa(q0,t,f);
01093 free(f);
01094 unshare(s, iv);
01095 extensional(s, iv, s.getSharedDFA(dfa), s.ann2ipl(ann));
01096 }
01097
01098 void
01099 p_sort(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01100 IntVarArgs x = s.arg2intvarargs(ce[0]);
01101 IntVarArgs y = s.arg2intvarargs(ce[1]);
01102 IntVarArgs xy(x.size()+y.size());
01103 for (int i=x.size(); i--;)
01104 xy[i] = x[i];
01105 for (int i=y.size(); i--;)
01106 xy[i+x.size()] = y[i];
01107 unshare(s, xy);
01108 for (int i=x.size(); i--;)
01109 x[i] = xy[i];
01110 for (int i=y.size(); i--;)
01111 y[i] = xy[i+x.size()];
01112 sorted(s, x, y, s.ann2ipl(ann));
01113 }
01114
01115 void
01116 p_inverse_offsets(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01117 IntVarArgs x = s.arg2intvarargs(ce[0]);
01118 unshare(s, x);
01119 int xoff = ce[1]->getInt();
01120 IntVarArgs y = s.arg2intvarargs(ce[2]);
01121 unshare(s, y);
01122 int yoff = ce[3]->getInt();
01123 channel(s, x, xoff, y, yoff, s.ann2ipl(ann));
01124 }
01125
01126 void
01127 p_increasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01128 IntVarArgs x = s.arg2intvarargs(ce[0]);
01129 rel(s,x,IRT_LQ,s.ann2ipl(ann));
01130 }
01131
01132 void
01133 p_increasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01134 BoolVarArgs x = s.arg2boolvarargs(ce[0]);
01135 rel(s,x,IRT_LQ,s.ann2ipl(ann));
01136 }
01137
01138 void
01139 p_decreasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01140 IntVarArgs x = s.arg2intvarargs(ce[0]);
01141 rel(s,x,IRT_GQ,s.ann2ipl(ann));
01142 }
01143
01144 void
01145 p_decreasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01146 BoolVarArgs x = s.arg2boolvarargs(ce[0]);
01147 rel(s,x,IRT_GQ,s.ann2ipl(ann));
01148 }
01149
01150 void
01151 p_table_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01152 IntVarArgs x = s.arg2intvarargs(ce[0]);
01153 IntArgs tuples = s.arg2intargs(ce[1]);
01154 TupleSet ts = s.arg2tupleset(tuples,x.size());
01155 extensional(s,x,ts,s.ann2ipl(ann));
01156 }
01157
01158 void
01159 p_table_int_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01160 IntVarArgs x = s.arg2intvarargs(ce[0]);
01161 IntArgs tuples = s.arg2intargs(ce[1]);
01162 TupleSet ts = s.arg2tupleset(tuples,x.size());
01163 extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_EQV),s.ann2ipl(ann));
01164 }
01165
01166 void
01167 p_table_int_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01168 IntVarArgs x = s.arg2intvarargs(ce[0]);
01169 IntArgs tuples = s.arg2intargs(ce[1]);
01170 TupleSet ts = s.arg2tupleset(tuples,x.size());
01171 extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_IMP),s.ann2ipl(ann));
01172 }
01173
01174 void
01175 p_table_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01176 BoolVarArgs x = s.arg2boolvarargs(ce[0]);
01177 IntArgs tuples = s.arg2boolargs(ce[1]);
01178 TupleSet ts = s.arg2tupleset(tuples,x.size());
01179 extensional(s,x,ts,s.ann2ipl(ann));
01180 }
01181
01182 void
01183 p_table_bool_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01184 BoolVarArgs x = s.arg2boolvarargs(ce[0]);
01185 IntArgs tuples = s.arg2boolargs(ce[1]);
01186 TupleSet ts = s.arg2tupleset(tuples,x.size());
01187 extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_EQV),s.ann2ipl(ann));
01188 }
01189
01190 void
01191 p_table_bool_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01192 BoolVarArgs x = s.arg2boolvarargs(ce[0]);
01193 IntArgs tuples = s.arg2boolargs(ce[1]);
01194 TupleSet ts = s.arg2tupleset(tuples,x.size());
01195 extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_IMP),s.ann2ipl(ann));
01196 }
01197
01198 void p_cumulative_opt(FlatZincSpace& s, const ConExpr& ce,
01199 AST::Node* ann) {
01200 IntVarArgs start = s.arg2intvarargs(ce[0]);
01201 IntArgs duration = s.arg2intargs(ce[1]);
01202 IntArgs height = s.arg2intargs(ce[2]);
01203 BoolVarArgs opt = s.arg2boolvarargs(ce[3]);
01204 int bound = ce[4]->getInt();
01205 unshare(s,start);
01206 cumulative(s,bound,start,duration,height,opt,s.ann2ipl(ann));
01207 }
01208
01209 void p_cumulatives(FlatZincSpace& s, const ConExpr& ce,
01210 AST::Node* ann) {
01211 IntVarArgs start = s.arg2intvarargs(ce[0]);
01212 IntVarArgs duration = s.arg2intvarargs(ce[1]);
01213 IntVarArgs height = s.arg2intvarargs(ce[2]);
01214 int n = start.size();
01215 IntVar bound = s.arg2IntVar(ce[3]);
01216
01217 if (n==0)
01218 return;
01219
01220 if (n == 1) {
01221 rel(s, height[0] <= bound);
01222 return;
01223 }
01224
01225 int minHeight = std::min(height[0].min(),height[1].min());
01226 int minHeight2 = std::max(height[0].min(),height[1].min());
01227 for (int i=2; i<n; i++) {
01228 if (height[i].min() < minHeight) {
01229 minHeight2 = minHeight;
01230 minHeight = height[i].min();
01231 } else if (height[i].min() < minHeight2) {
01232 minHeight2 = height[i].min();
01233 }
01234 }
01235 bool disjunctive =
01236 (minHeight > bound.max()/2) ||
01237 (minHeight2 > bound.max()/2 && minHeight+minHeight2>bound.max());
01238 if (disjunctive) {
01239 rel(s, bound >= max(height));
01240
01241 if (duration.assigned()) {
01242 IntArgs durationI(n);
01243 for (int i=n; i--;)
01244 durationI[i] = duration[i].val();
01245 unshare(s,start);
01246 unary(s,start,durationI);
01247 } else {
01248 IntVarArgs end(n);
01249 for (int i=n; i--;)
01250 end[i] = expr(s,start[i]+duration[i]);
01251 unshare(s,start);
01252 unary(s,start,duration,end);
01253 }
01254 } else if (height.assigned()) {
01255 IntArgs heightI(n);
01256 for (int i=n; i--;)
01257 heightI[i] = height[i].val();
01258 if (duration.assigned()) {
01259 IntArgs durationI(n);
01260 for (int i=n; i--;)
01261 durationI[i] = duration[i].val();
01262 cumulative(s, bound, start, durationI, heightI);
01263 } else {
01264 IntVarArgs end(n);
01265 for (int i = n; i--; )
01266 end[i] = expr(s,start[i]+duration[i]);
01267 cumulative(s, bound, start, duration, end, heightI);
01268 }
01269 } else if (bound.assigned()) {
01270 IntArgs machine = IntArgs::create(n,0,0);
01271 IntArgs limit({bound.val()});
01272 IntVarArgs end(n);
01273 for (int i=n; i--;)
01274 end[i] = expr(s,start[i]+duration[i]);
01275 cumulatives(s, machine, start, duration, end, height, limit, true,
01276 s.ann2ipl(ann));
01277 } else {
01278 int min = Gecode::Int::Limits::max;
01279 int max = Gecode::Int::Limits::min;
01280 IntVarArgs end(start.size());
01281 for (int i = start.size(); i--; ) {
01282 min = std::min(min, start[i].min());
01283 max = std::max(max, start[i].max() + duration[i].max());
01284 end[i] = expr(s, start[i] + duration[i]);
01285 }
01286 for (int time = min; time < max; ++time) {
01287 IntVarArgs x(start.size());
01288 for (int i = start.size(); i--; ) {
01289 IntVar overlaps = channel(s, expr(s, (start[i] <= time) &&
01290 (time < end[i])));
01291 x[i] = expr(s, overlaps * height[i]);
01292 }
01293 linear(s, x, IRT_LQ, bound);
01294 }
01295 }
01296 }
01297
01298 void p_among_seq_int(FlatZincSpace& s, const ConExpr& ce,
01299 AST::Node* ann) {
01300 IntVarArgs x = s.arg2intvarargs(ce[0]);
01301 IntSet S = s.arg2intset(ce[1]);
01302 int q = ce[2]->getInt();
01303 int l = ce[3]->getInt();
01304 int u = ce[4]->getInt();
01305 unshare(s, x);
01306 sequence(s, x, S, q, l, u, s.ann2ipl(ann));
01307 }
01308
01309 void p_among_seq_bool(FlatZincSpace& s, const ConExpr& ce,
01310 AST::Node* ann) {
01311 BoolVarArgs x = s.arg2boolvarargs(ce[0]);
01312 bool val = ce[1]->getBool();
01313 int q = ce[2]->getInt();
01314 int l = ce[3]->getInt();
01315 int u = ce[4]->getInt();
01316 IntSet S(val, val);
01317 unshare(s, x);
01318 sequence(s, x, S, q, l, u, s.ann2ipl(ann));
01319 }
01320
01321 void p_schedule_unary(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
01322 IntVarArgs x = s.arg2intvarargs(ce[0]);
01323 IntArgs p = s.arg2intargs(ce[1]);
01324 unshare(s,x);
01325 unary(s, x, p);
01326 }
01327
01328 void p_schedule_unary_optional(FlatZincSpace& s, const ConExpr& ce,
01329 AST::Node*) {
01330 IntVarArgs x = s.arg2intvarargs(ce[0]);
01331 IntArgs p = s.arg2intargs(ce[1]);
01332 BoolVarArgs m = s.arg2boolvarargs(ce[2]);
01333 unshare(s,x);
01334 unary(s, x, p, m);
01335 }
01336
01337 void p_circuit(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01338 int off = ce[0]->getInt();
01339 IntVarArgs xv = s.arg2intvarargs(ce[1]);
01340 unshare(s,xv);
01341 circuit(s,off,xv,s.ann2ipl(ann));
01342 }
01343 void p_circuit_cost_array(FlatZincSpace& s, const ConExpr& ce,
01344 AST::Node *ann) {
01345 IntArgs c = s.arg2intargs(ce[0]);
01346 IntVarArgs xv = s.arg2intvarargs(ce[1]);
01347 IntVarArgs yv = s.arg2intvarargs(ce[2]);
01348 IntVar z = s.arg2IntVar(ce[3]);
01349 unshare(s,xv);
01350 circuit(s,c,xv,yv,z,s.ann2ipl(ann));
01351 }
01352 void p_circuit_cost(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01353 IntArgs c = s.arg2intargs(ce[0]);
01354 IntVarArgs xv = s.arg2intvarargs(ce[1]);
01355 IntVar z = s.arg2IntVar(ce[2]);
01356 unshare(s,xv);
01357 circuit(s,c,xv,z,s.ann2ipl(ann));
01358 }
01359
01360 void p_nooverlap(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01361 IntVarArgs x0 = s.arg2intvarargs(ce[0]);
01362 IntVarArgs w = s.arg2intvarargs(ce[1]);
01363 IntVarArgs y0 = s.arg2intvarargs(ce[2]);
01364 IntVarArgs h = s.arg2intvarargs(ce[3]);
01365 if (w.assigned() && h.assigned()) {
01366 IntArgs iw(w.size());
01367 for (int i=w.size(); i--;)
01368 iw[i] = w[i].val();
01369 IntArgs ih(h.size());
01370 for (int i=h.size(); i--;)
01371 ih[i] = h[i].val();
01372 nooverlap(s,x0,iw,y0,ih,s.ann2ipl(ann));
01373
01374 int miny = y0[0].min();
01375 int maxy = y0[0].max();
01376 int maxdy = ih[0];
01377 for (int i=1; i<y0.size(); i++) {
01378 miny = std::min(miny,y0[i].min());
01379 maxy = std::max(maxy,y0[i].max());
01380 maxdy = std::max(maxdy,ih[i]);
01381 }
01382 int minx = x0[0].min();
01383 int maxx = x0[0].max();
01384 int maxdx = iw[0];
01385 for (int i=1; i<x0.size(); i++) {
01386 minx = std::min(minx,x0[i].min());
01387 maxx = std::max(maxx,x0[i].max());
01388 maxdx = std::max(maxdx,iw[i]);
01389 }
01390 if (miny > Int::Limits::min && maxy < Int::Limits::max) {
01391 cumulative(s,maxdy+maxy-miny,x0,iw,ih);
01392 cumulative(s,maxdx+maxx-minx,y0,ih,iw);
01393 }
01394 } else {
01395 IntVarArgs x1(x0.size()), y1(y0.size());
01396 for (int i=x0.size(); i--; )
01397 x1[i] = expr(s, x0[i] + w[i]);
01398 for (int i=y0.size(); i--; )
01399 y1[i] = expr(s, y0[i] + h[i]);
01400 nooverlap(s,x0,w,x1,y0,h,y1,s.ann2ipl(ann));
01401 }
01402 }
01403
01404 void p_precede(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01405 IntVarArgs x = s.arg2intvarargs(ce[0]);
01406 int p_s = ce[1]->getInt();
01407 int p_t = ce[2]->getInt();
01408 precede(s,x,p_s,p_t,s.ann2ipl(ann));
01409 }
01410
01411 void p_nvalue(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01412 IntVarArgs x = s.arg2intvarargs(ce[1]);
01413 if (ce[0]->isIntVar()) {
01414 IntVar y = s.arg2IntVar(ce[0]);
01415 nvalues(s,x,IRT_EQ,y,s.ann2ipl(ann));
01416 } else {
01417 nvalues(s,x,IRT_EQ,ce[0]->getInt(),s.ann2ipl(ann));
01418 }
01419 }
01420
01421 void p_among(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01422 IntVarArgs x = s.arg2intvarargs(ce[1]);
01423 IntSet v = s.arg2intset(ce[2]);
01424 if (ce[0]->isIntVar()) {
01425 IntVar n = s.arg2IntVar(ce[0]);
01426 unshare(s, x);
01427 count(s,x,v,IRT_EQ,n,s.ann2ipl(ann));
01428 } else {
01429 unshare(s, x);
01430 count(s,x,v,IRT_EQ,ce[0]->getInt(),s.ann2ipl(ann));
01431 }
01432 }
01433
01434 void p_member_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01435 IntVarArgs x = s.arg2intvarargs(ce[0]);
01436 IntVar y = s.arg2IntVar(ce[1]);
01437 member(s,x,y,s.ann2ipl(ann));
01438 }
01439 void p_member_int_reif(FlatZincSpace& s, const ConExpr& ce,
01440 AST::Node* ann) {
01441 IntVarArgs x = s.arg2intvarargs(ce[0]);
01442 IntVar y = s.arg2IntVar(ce[1]);
01443 BoolVar b = s.arg2BoolVar(ce[2]);
01444 member(s,x,y,b,s.ann2ipl(ann));
01445 }
01446 void p_member_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01447 BoolVarArgs x = s.arg2boolvarargs(ce[0]);
01448 BoolVar y = s.arg2BoolVar(ce[1]);
01449 member(s,x,y,s.ann2ipl(ann));
01450 }
01451 void p_member_bool_reif(FlatZincSpace& s, const ConExpr& ce,
01452 AST::Node* ann) {
01453 BoolVarArgs x = s.arg2boolvarargs(ce[0]);
01454 BoolVar y = s.arg2BoolVar(ce[1]);
01455 member(s,x,y,s.arg2BoolVar(ce[2]),s.ann2ipl(ann));
01456 }
01457
01458 class IntPoster {
01459 public:
01460 IntPoster(void) {
01461 registry().add("all_different_int", &p_distinct);
01462 registry().add("all_different_offset", &p_distinctOffset);
01463 registry().add("all_equal_int", &p_all_equal);
01464 registry().add("int_eq", &p_int_eq);
01465 registry().add("int_ne", &p_int_ne);
01466 registry().add("int_ge", &p_int_ge);
01467 registry().add("int_gt", &p_int_gt);
01468 registry().add("int_le", &p_int_le);
01469 registry().add("int_lt", &p_int_lt);
01470 registry().add("int_eq_reif", &p_int_eq_reif);
01471 registry().add("int_ne_reif", &p_int_ne_reif);
01472 registry().add("int_ge_reif", &p_int_ge_reif);
01473 registry().add("int_gt_reif", &p_int_gt_reif);
01474 registry().add("int_le_reif", &p_int_le_reif);
01475 registry().add("int_lt_reif", &p_int_lt_reif);
01476 registry().add("int_eq_imp", &p_int_eq_imp);
01477 registry().add("int_ne_imp", &p_int_ne_imp);
01478 registry().add("int_ge_imp", &p_int_ge_imp);
01479 registry().add("int_gt_imp", &p_int_gt_imp);
01480 registry().add("int_le_imp", &p_int_le_imp);
01481 registry().add("int_lt_imp", &p_int_lt_imp);
01482 registry().add("int_lin_eq", &p_int_lin_eq);
01483 registry().add("int_lin_eq_reif", &p_int_lin_eq_reif);
01484 registry().add("int_lin_eq_imp", &p_int_lin_eq_imp);
01485 registry().add("int_lin_ne", &p_int_lin_ne);
01486 registry().add("int_lin_ne_reif", &p_int_lin_ne_reif);
01487 registry().add("int_lin_ne_imp", &p_int_lin_ne_imp);
01488 registry().add("int_lin_le", &p_int_lin_le);
01489 registry().add("int_lin_le_reif", &p_int_lin_le_reif);
01490 registry().add("int_lin_le_imp", &p_int_lin_le_imp);
01491 registry().add("int_lin_lt", &p_int_lin_lt);
01492 registry().add("int_lin_lt_reif", &p_int_lin_lt_reif);
01493 registry().add("int_lin_lt_imp", &p_int_lin_lt_imp);
01494 registry().add("int_lin_ge", &p_int_lin_ge);
01495 registry().add("int_lin_ge_reif", &p_int_lin_ge_reif);
01496 registry().add("int_lin_ge_imp", &p_int_lin_ge_imp);
01497 registry().add("int_lin_gt", &p_int_lin_gt);
01498 registry().add("int_lin_gt_reif", &p_int_lin_gt_reif);
01499 registry().add("int_lin_gt_imp", &p_int_lin_gt_imp);
01500 registry().add("int_plus", &p_int_plus);
01501 registry().add("int_minus", &p_int_minus);
01502 registry().add("int_times", &p_int_times);
01503 registry().add("gecode_int_pow", &p_int_pow);
01504 registry().add("int_div", &p_int_div);
01505 registry().add("int_mod", &p_int_mod);
01506 registry().add("int_min", &p_int_min);
01507 registry().add("int_max", &p_int_max);
01508 registry().add("int_abs", &p_abs);
01509 registry().add("int_negate", &p_int_negate);
01510 registry().add("bool_eq", &p_bool_eq);
01511 registry().add("bool_eq_reif", &p_bool_eq_reif);
01512 registry().add("bool_eq_imp", &p_bool_eq_imp);
01513 registry().add("bool_ne", &p_bool_ne);
01514 registry().add("bool_ne_reif", &p_bool_ne_reif);
01515 registry().add("bool_ne_imp", &p_bool_ne_imp);
01516 registry().add("bool_ge", &p_bool_ge);
01517 registry().add("bool_ge_reif", &p_bool_ge_reif);
01518 registry().add("bool_ge_imp", &p_bool_ge_imp);
01519 registry().add("bool_le", &p_bool_le);
01520 registry().add("bool_le_reif", &p_bool_le_reif);
01521 registry().add("bool_le_imp", &p_bool_le_imp);
01522 registry().add("bool_gt", &p_bool_gt);
01523 registry().add("bool_gt_reif", &p_bool_gt_reif);
01524 registry().add("bool_gt_imp", &p_bool_gt_imp);
01525 registry().add("bool_lt", &p_bool_lt);
01526 registry().add("bool_lt_reif", &p_bool_lt_reif);
01527 registry().add("bool_lt_imp", &p_bool_lt_imp);
01528 registry().add("bool_or", &p_bool_or);
01529 registry().add("bool_or_imp", &p_bool_or_imp);
01530 registry().add("bool_and", &p_bool_and);
01531 registry().add("bool_and_imp", &p_bool_and_imp);
01532 registry().add("bool_xor", &p_bool_xor);
01533 registry().add("bool_xor_imp", &p_bool_xor_imp);
01534 registry().add("array_bool_and", &p_array_bool_and);
01535 registry().add("array_bool_and_imp", &p_array_bool_and_imp);
01536 registry().add("array_bool_or", &p_array_bool_or);
01537 registry().add("array_bool_or_imp", &p_array_bool_or_imp);
01538 registry().add("array_bool_xor", &p_array_bool_xor);
01539 registry().add("array_bool_xor_imp", &p_array_bool_xor_imp);
01540 registry().add("bool_clause", &p_array_bool_clause);
01541 registry().add("bool_clause_reif", &p_array_bool_clause_reif);
01542 registry().add("bool_clause_imp", &p_array_bool_clause_imp);
01543 registry().add("bool_left_imp", &p_bool_l_imp);
01544 registry().add("bool_right_imp", &p_bool_r_imp);
01545 registry().add("bool_not", &p_bool_not);
01546 registry().add("array_int_element", &p_array_int_element);
01547 registry().add("array_var_int_element", &p_array_int_element);
01548 registry().add("array_bool_element", &p_array_bool_element);
01549 registry().add("array_var_bool_element", &p_array_bool_element);
01550 registry().add("bool2int", &p_bool2int);
01551 registry().add("int_in", &p_int_in);
01552 registry().add("int_in_reif", &p_int_in_reif);
01553 registry().add("int_in_imp", &p_int_in_imp);
01554 #ifndef GECODE_HAS_SET_VARS
01555 registry().add("set_in", &p_int_in);
01556 registry().add("set_in_reif", &p_int_in_reif);
01557 registry().add("set_in_imp", &p_int_in_imp);
01558 #endif
01559
01560 registry().add("array_int_lt", &p_array_int_lt);
01561 registry().add("array_int_lq", &p_array_int_lq);
01562 registry().add("array_bool_lt", &p_array_bool_lt);
01563 registry().add("array_bool_lq", &p_array_bool_lq);
01564 registry().add("count", &p_count);
01565 registry().add("count_reif", &p_count_reif);
01566 registry().add("count_imp", &p_count_imp);
01567 registry().add("at_least_int", &p_at_least);
01568 registry().add("at_most_int", &p_at_most);
01569 registry().add("gecode_bin_packing_load", &p_bin_packing_load);
01570 registry().add("gecode_global_cardinality", &p_global_cardinality);
01571 registry().add("gecode_global_cardinality_closed",
01572 &p_global_cardinality_closed);
01573 registry().add("global_cardinality_low_up",
01574 &p_global_cardinality_low_up);
01575 registry().add("global_cardinality_low_up_closed",
01576 &p_global_cardinality_low_up_closed);
01577 registry().add("array_int_minimum", &p_minimum);
01578 registry().add("array_int_maximum", &p_maximum);
01579 registry().add("gecode_minimum_arg_int_offset", &p_minimum_arg);
01580 registry().add("gecode_maximum_arg_int_offset", &p_maximum_arg);
01581 registry().add("gecode_minimum_arg_bool_offset", &p_minimum_arg_bool);
01582 registry().add("gecode_maximum_arg_bool_offset", &p_maximum_arg_bool);
01583 registry().add("array_int_maximum", &p_maximum);
01584 registry().add("gecode_regular", &p_regular);
01585 registry().add("sort", &p_sort);
01586 registry().add("inverse_offsets", &p_inverse_offsets);
01587 registry().add("increasing_int", &p_increasing_int);
01588 registry().add("increasing_bool", &p_increasing_bool);
01589 registry().add("decreasing_int", &p_decreasing_int);
01590 registry().add("decreasing_bool", &p_decreasing_bool);
01591 registry().add("gecode_table_int", &p_table_int);
01592 registry().add("gecode_table_int_reif", &p_table_int_reif);
01593 registry().add("gecode_table_int_imp", &p_table_int_imp);
01594 registry().add("gecode_table_bool", &p_table_bool);
01595 registry().add("gecode_table_bool_reif", &p_table_bool_reif);
01596 registry().add("gecode_table_bool_imp", &p_table_bool_imp);
01597 registry().add("cumulatives", &p_cumulatives);
01598 registry().add("gecode_among_seq_int", &p_among_seq_int);
01599 registry().add("gecode_among_seq_bool", &p_among_seq_bool);
01600
01601 registry().add("bool_lin_eq", &p_bool_lin_eq);
01602 registry().add("bool_lin_ne", &p_bool_lin_ne);
01603 registry().add("bool_lin_le", &p_bool_lin_le);
01604 registry().add("bool_lin_lt", &p_bool_lin_lt);
01605 registry().add("bool_lin_ge", &p_bool_lin_ge);
01606 registry().add("bool_lin_gt", &p_bool_lin_gt);
01607
01608 registry().add("bool_lin_eq_reif", &p_bool_lin_eq_reif);
01609 registry().add("bool_lin_eq_imp", &p_bool_lin_eq_imp);
01610 registry().add("bool_lin_ne_reif", &p_bool_lin_ne_reif);
01611 registry().add("bool_lin_ne_imp", &p_bool_lin_ne_imp);
01612 registry().add("bool_lin_le_reif", &p_bool_lin_le_reif);
01613 registry().add("bool_lin_le_imp", &p_bool_lin_le_imp);
01614 registry().add("bool_lin_lt_reif", &p_bool_lin_lt_reif);
01615 registry().add("bool_lin_lt_imp", &p_bool_lin_lt_imp);
01616 registry().add("bool_lin_ge_reif", &p_bool_lin_ge_reif);
01617 registry().add("bool_lin_ge_imp", &p_bool_lin_ge_imp);
01618 registry().add("bool_lin_gt_reif", &p_bool_lin_gt_reif);
01619 registry().add("bool_lin_gt_imp", &p_bool_lin_gt_imp);
01620
01621 registry().add("gecode_schedule_unary", &p_schedule_unary);
01622 registry().add("gecode_schedule_unary_optional", &p_schedule_unary_optional);
01623 registry().add("gecode_schedule_cumulative_optional", &p_cumulative_opt);
01624
01625 registry().add("gecode_circuit", &p_circuit);
01626 registry().add("gecode_circuit_cost_array", &p_circuit_cost_array);
01627 registry().add("gecode_circuit_cost", &p_circuit_cost);
01628 registry().add("gecode_nooverlap", &p_nooverlap);
01629 registry().add("gecode_precede", &p_precede);
01630 registry().add("nvalue",&p_nvalue);
01631 registry().add("among",&p_among);
01632 registry().add("member_int",&p_member_int);
01633 registry().add("gecode_member_int_reif",&p_member_int_reif);
01634 registry().add("member_bool",&p_member_bool);
01635 registry().add("gecode_member_bool_reif",&p_member_bool_reif);
01636 }
01637 };
01638 IntPoster __int_poster;
01639
01640 #ifdef GECODE_HAS_SET_VARS
01641 void p_set_OP(FlatZincSpace& s, SetOpType op,
01642 const ConExpr& ce, AST::Node *) {
01643 rel(s, s.arg2SetVar(ce[0]), op, s.arg2SetVar(ce[1]),
01644 SRT_EQ, s.arg2SetVar(ce[2]));
01645 }
01646 void p_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01647 p_set_OP(s, SOT_UNION, ce, ann);
01648 }
01649 void p_set_intersect(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01650 p_set_OP(s, SOT_INTER, ce, ann);
01651 }
01652 void p_set_diff(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01653 p_set_OP(s, SOT_MINUS, ce, ann);
01654 }
01655
01656 void p_set_symdiff(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
01657 SetVar x = s.arg2SetVar(ce[0]);
01658 SetVar y = s.arg2SetVar(ce[1]);
01659
01660 SetVarLubRanges xub(x);
01661 IntSet xubs(xub);
01662 SetVar x_y(s,IntSet::empty,xubs);
01663 rel(s, x, SOT_MINUS, y, SRT_EQ, x_y);
01664
01665 SetVarLubRanges yub(y);
01666 IntSet yubs(yub);
01667 SetVar y_x(s,IntSet::empty,yubs);
01668 rel(s, y, SOT_MINUS, x, SRT_EQ, y_x);
01669
01670 rel(s, x_y, SOT_UNION, y_x, SRT_EQ, s.arg2SetVar(ce[2]));
01671 }
01672
01673 void p_array_set_OP(FlatZincSpace& s, SetOpType op,
01674 const ConExpr& ce, AST::Node *) {
01675 SetVarArgs xs = s.arg2setvarargs(ce[0]);
01676 rel(s, op, xs, s.arg2SetVar(ce[1]));
01677 }
01678 void p_array_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01679 p_array_set_OP(s, SOT_UNION, ce, ann);
01680 }
01681 void p_array_set_partition(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
01682 p_array_set_OP(s, SOT_DUNION, ce, ann);
01683 }
01684
01685
01686 void p_set_rel(FlatZincSpace& s, SetRelType srt, const ConExpr& ce) {
01687 rel(s, s.arg2SetVar(ce[0]), srt, s.arg2SetVar(ce[1]));
01688 }
01689
01690 void p_set_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01691 p_set_rel(s, SRT_EQ, ce);
01692 }
01693 void p_set_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01694 p_set_rel(s, SRT_NQ, ce);
01695 }
01696 void p_set_subset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01697 p_set_rel(s, SRT_SUB, ce);
01698 }
01699 void p_set_superset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01700 p_set_rel(s, SRT_SUP, ce);
01701 }
01702 void p_set_le(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01703 p_set_rel(s, SRT_LQ, ce);
01704 }
01705 void p_set_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01706 p_set_rel(s, SRT_LE, ce);
01707 }
01708 void p_set_card(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01709 if (!ce[1]->isIntVar()) {
01710 cardinality(s, s.arg2SetVar(ce[0]), ce[1]->getInt(),
01711 ce[1]->getInt());
01712 } else {
01713 cardinality(s, s.arg2SetVar(ce[0]), s.arg2IntVar(ce[1]));
01714 }
01715 }
01716 void p_set_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01717 if (!ce[1]->isSetVar()) {
01718 IntSet d = s.arg2intset(ce[1]);
01719 if (ce[0]->isBoolVar()) {
01720 IntSetRanges dr(d);
01721 Iter::Ranges::Singleton sr(0,1);
01722 Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
01723 IntSet d01(i);
01724 if (d01.size() == 0) {
01725 s.fail();
01726 } else {
01727 rel(s, s.arg2BoolVar(ce[0]), IRT_GQ, d01.min());
01728 rel(s, s.arg2BoolVar(ce[0]), IRT_LQ, d01.max());
01729 }
01730 } else {
01731 dom(s, s.arg2IntVar(ce[0]), d);
01732 }
01733 } else {
01734 if (!ce[0]->isIntVar()) {
01735 dom(s, s.arg2SetVar(ce[1]), SRT_SUP, ce[0]->getInt());
01736 } else {
01737 rel(s, s.arg2SetVar(ce[1]), SRT_SUP, s.arg2IntVar(ce[0]));
01738 }
01739 }
01740 }
01741 void p_set_rel_reif(FlatZincSpace& s, SetRelType srt, const ConExpr& ce) {
01742 rel(s, s.arg2SetVar(ce[0]), srt, s.arg2SetVar(ce[1]),
01743 s.arg2BoolVar(ce[2]));
01744 }
01745
01746 void p_set_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01747 p_set_rel_reif(s,SRT_EQ,ce);
01748 }
01749 void p_set_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01750 p_set_rel_reif(s,SRT_LQ,ce);
01751 }
01752 void p_set_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01753 p_set_rel_reif(s,SRT_LE,ce);
01754 }
01755 void p_set_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01756 p_set_rel_reif(s,SRT_NQ,ce);
01757 }
01758 void p_set_subset_reif(FlatZincSpace& s, const ConExpr& ce,
01759 AST::Node *) {
01760 p_set_rel_reif(s,SRT_SUB,ce);
01761 }
01762 void p_set_superset_reif(FlatZincSpace& s, const ConExpr& ce,
01763 AST::Node *) {
01764 p_set_rel_reif(s,SRT_SUP,ce);
01765 }
01766 void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann, ReifyMode rm) {
01767 if (!ce[1]->isSetVar()) {
01768 if (rm==RM_EQV) {
01769 p_int_in_reif(s,ce,ann);
01770 } else {
01771 assert(rm==RM_IMP);
01772 p_int_in_imp(s,ce,ann);
01773 }
01774 } else {
01775 if (!ce[0]->isIntVar()) {
01776 dom(s, s.arg2SetVar(ce[1]), SRT_SUP, ce[0]->getInt(),
01777 Reify(s.arg2BoolVar(ce[2]),rm));
01778 } else {
01779 rel(s, s.arg2SetVar(ce[1]), SRT_SUP, s.arg2IntVar(ce[0]),
01780 Reify(s.arg2BoolVar(ce[2]),rm));
01781 }
01782 }
01783 }
01784 void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01785 p_set_in_reif(s,ce,ann,RM_EQV);
01786 }
01787 void p_set_in_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
01788 p_set_in_reif(s,ce,ann,RM_IMP);
01789 }
01790 void p_set_disjoint(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01791 rel(s, s.arg2SetVar(ce[0]), SRT_DISJ, s.arg2SetVar(ce[1]));
01792 }
01793
01794 void p_link_set_to_booleans(FlatZincSpace& s, const ConExpr& ce,
01795 AST::Node *) {
01796 SetVar x = s.arg2SetVar(ce[0]);
01797 int idx = ce[2]->getInt();
01798 assert(idx >= 0);
01799 rel(s, x || IntSet(Set::Limits::min,idx-1));
01800 BoolVarArgs y = s.arg2boolvarargs(ce[1],idx);
01801 unshare(s, y);
01802 channel(s, y, x);
01803 }
01804
01805 void p_array_set_element(FlatZincSpace& s, const ConExpr& ce,
01806 AST::Node*) {
01807 bool isConstant = true;
01808 AST::Array* a = ce[1]->getArray();
01809 for (int i=a->a.size(); i--;) {
01810 if (a->a[i]->isSetVar()) {
01811 isConstant = false;
01812 break;
01813 }
01814 }
01815 IntVar selector = s.arg2IntVar(ce[0]);
01816 rel(s, selector > 0);
01817 if (isConstant) {
01818 IntSetArgs sv = s.arg2intsetargs(ce[1],1);
01819 element(s, sv, selector, s.arg2SetVar(ce[2]));
01820 } else {
01821 SetVarArgs sv = s.arg2setvarargs(ce[1], 1);
01822 element(s, sv, selector, s.arg2SetVar(ce[2]));
01823 }
01824 }
01825
01826 void p_array_set_element_op(FlatZincSpace& s, const ConExpr& ce,
01827 AST::Node*, SetOpType op,
01828 const IntSet& universe =
01829 IntSet(Set::Limits::min,Set::Limits::max)) {
01830 bool isConstant = true;
01831 AST::Array* a = ce[1]->getArray();
01832 for (int i=a->a.size(); i--;) {
01833 if (a->a[i]->isSetVar()) {
01834 isConstant = false;
01835 break;
01836 }
01837 }
01838 SetVar selector = s.arg2SetVar(ce[0]);
01839 dom(s, selector, SRT_DISJ, 0);
01840 if (isConstant) {
01841 IntSetArgs sv = s.arg2intsetargs(ce[1], 1);
01842 element(s, op, sv, selector, s.arg2SetVar(ce[2]), universe);
01843 } else {
01844 SetVarArgs sv = s.arg2setvarargs(ce[1], 1);
01845 element(s, op, sv, selector, s.arg2SetVar(ce[2]), universe);
01846 }
01847 }
01848
01849 void p_array_set_element_union(FlatZincSpace& s, const ConExpr& ce,
01850 AST::Node* ann) {
01851 p_array_set_element_op(s, ce, ann, SOT_UNION);
01852 }
01853
01854 void p_array_set_element_intersect(FlatZincSpace& s, const ConExpr& ce,
01855 AST::Node* ann) {
01856 p_array_set_element_op(s, ce, ann, SOT_INTER);
01857 }
01858
01859 void p_array_set_element_intersect_in(FlatZincSpace& s,
01860 const ConExpr& ce,
01861 AST::Node* ann) {
01862 IntSet d = s.arg2intset(ce[3]);
01863 p_array_set_element_op(s, ce, ann, SOT_INTER, d);
01864 }
01865
01866 void p_array_set_element_partition(FlatZincSpace& s, const ConExpr& ce,
01867 AST::Node* ann) {
01868 p_array_set_element_op(s, ce, ann, SOT_DUNION);
01869 }
01870
01871 void p_set_convex(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01872 convex(s, s.arg2SetVar(ce[0]));
01873 }
01874
01875 void p_array_set_seq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
01876 SetVarArgs sv = s.arg2setvarargs(ce[0]);
01877 sequence(s, sv);
01878 }
01879
01880 void p_array_set_seq_union(FlatZincSpace& s, const ConExpr& ce,
01881 AST::Node *) {
01882 SetVarArgs sv = s.arg2setvarargs(ce[0]);
01883 sequence(s, sv, s.arg2SetVar(ce[1]));
01884 }
01885
01886 void p_int_set_channel(FlatZincSpace& s, const ConExpr& ce,
01887 AST::Node *) {
01888 int xoff=ce[1]->getInt();
01889 assert(xoff >= 0);
01890 int yoff=ce[3]->getInt();
01891 assert(yoff >= 0);
01892 IntVarArgs xv = s.arg2intvarargs(ce[0], xoff);
01893 SetVarArgs yv = s.arg2setvarargs(ce[2], yoff, 1, IntSet(0, xoff-1));
01894 IntSet xd(yoff,yv.size()-1);
01895 for (int i=xoff; i<xv.size(); i++) {
01896 dom(s, xv[i], xd);
01897 }
01898 IntSet yd(xoff,xv.size()-1);
01899 for (int i=yoff; i<yv.size(); i++) {
01900 dom(s, yv[i], SRT_SUB, yd);
01901 }
01902 channel(s,xv,yv);
01903 }
01904
01905 void p_range(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
01906 int xoff=ce[1]->getInt();
01907 assert(xoff >= 0);
01908 IntVarArgs xv = s.arg2intvarargs(ce[0],xoff);
01909 element(s, SOT_UNION, xv, s.arg2SetVar(ce[2]), s.arg2SetVar(ce[3]));
01910 }
01911
01912 void p_weights(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
01913 IntArgs e = s.arg2intargs(ce[0]);
01914 IntArgs w = s.arg2intargs(ce[1]);
01915 SetVar x = s.arg2SetVar(ce[2]);
01916 IntVar y = s.arg2IntVar(ce[3]);
01917 weights(s,e,w,x,y);
01918 }
01919
01920 void p_inverse_set(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
01921 int xoff = ce[2]->getInt();
01922 int yoff = ce[3]->getInt();
01923 SetVarArgs x = s.arg2setvarargs(ce[0],xoff);
01924 SetVarArgs y = s.arg2setvarargs(ce[1],yoff);
01925 channel(s, x, y);
01926 }
01927
01928 void p_precede_set(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
01929 SetVarArgs x = s.arg2setvarargs(ce[0]);
01930 int p_s = ce[1]->getInt();
01931 int p_t = ce[2]->getInt();
01932 precede(s,x,p_s,p_t);
01933 }
01934
01935 class SetPoster {
01936 public:
01937 SetPoster(void) {
01938 registry().add("set_eq", &p_set_eq);
01939 registry().add("set_le", &p_set_le);
01940 registry().add("set_lt", &p_set_lt);
01941 registry().add("equal", &p_set_eq);
01942 registry().add("set_ne", &p_set_ne);
01943 registry().add("set_union", &p_set_union);
01944 registry().add("array_set_element", &p_array_set_element);
01945 registry().add("array_var_set_element", &p_array_set_element);
01946 registry().add("set_intersect", &p_set_intersect);
01947 registry().add("set_diff", &p_set_diff);
01948 registry().add("set_symdiff", &p_set_symdiff);
01949 registry().add("set_subset", &p_set_subset);
01950 registry().add("set_superset", &p_set_superset);
01951 registry().add("set_card", &p_set_card);
01952 registry().add("set_in", &p_set_in);
01953 registry().add("set_eq_reif", &p_set_eq_reif);
01954 registry().add("set_le_reif", &p_set_le_reif);
01955 registry().add("set_lt_reif", &p_set_lt_reif);
01956 registry().add("equal_reif", &p_set_eq_reif);
01957 registry().add("set_ne_reif", &p_set_ne_reif);
01958 registry().add("set_subset_reif", &p_set_subset_reif);
01959 registry().add("set_superset_reif", &p_set_superset_reif);
01960 registry().add("set_in_reif", &p_set_in_reif);
01961 registry().add("set_in_imp", &p_set_in_imp);
01962 registry().add("disjoint", &p_set_disjoint);
01963 registry().add("gecode_link_set_to_booleans",
01964 &p_link_set_to_booleans);
01965
01966 registry().add("array_set_union", &p_array_set_union);
01967 registry().add("array_set_partition", &p_array_set_partition);
01968 registry().add("set_convex", &p_set_convex);
01969 registry().add("array_set_seq", &p_array_set_seq);
01970 registry().add("array_set_seq_union", &p_array_set_seq_union);
01971 registry().add("gecode_array_set_element_union",
01972 &p_array_set_element_union);
01973 registry().add("gecode_array_set_element_intersect",
01974 &p_array_set_element_intersect);
01975 registry().add("gecode_array_set_element_intersect_in",
01976 &p_array_set_element_intersect_in);
01977 registry().add("gecode_array_set_element_partition",
01978 &p_array_set_element_partition);
01979 registry().add("gecode_int_set_channel",
01980 &p_int_set_channel);
01981 registry().add("gecode_range",
01982 &p_range);
01983 registry().add("gecode_set_weights",
01984 &p_weights);
01985 registry().add("gecode_inverse_set", &p_inverse_set);
01986 registry().add("gecode_precede_set", &p_precede_set);
01987 }
01988 };
01989 SetPoster __set_poster;
01990 #endif
01991
01992 #ifdef GECODE_HAS_FLOAT_VARS
01993
01994 void p_int2float(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
01995 IntVar x0 = s.arg2IntVar(ce[0]);
01996 FloatVar x1 = s.arg2FloatVar(ce[1]);
01997 channel(s, x0, x1);
01998 }
01999
02000 void p_float_lin_cmp(FlatZincSpace& s, FloatRelType frt,
02001 const ConExpr& ce, AST::Node*) {
02002 FloatValArgs fa = s.arg2floatargs(ce[0]);
02003 FloatVarArgs fv = s.arg2floatvarargs(ce[1]);
02004 linear(s, fa, fv, frt, ce[2]->getFloat());
02005 }
02006 void p_float_lin_cmp_reif(FlatZincSpace& s, FloatRelType frt,
02007 const ConExpr& ce, AST::Node*) {
02008 FloatValArgs fa = s.arg2floatargs(ce[0]);
02009 FloatVarArgs fv = s.arg2floatvarargs(ce[1]);
02010 linear(s, fa, fv, frt, ce[2]->getFloat(), s.arg2BoolVar(ce[3]));
02011 }
02012 void p_float_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
02013 p_float_lin_cmp(s,FRT_EQ,ce,ann);
02014 }
02015 void p_float_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce,
02016 AST::Node* ann) {
02017 p_float_lin_cmp_reif(s,FRT_EQ,ce,ann);
02018 }
02019 void p_float_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
02020 p_float_lin_cmp(s,FRT_LQ,ce,ann);
02021 }
02022 void p_float_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
02023 p_float_lin_cmp(s,FRT_LE,ce,ann);
02024 }
02025 void p_float_lin_le_reif(FlatZincSpace& s, const ConExpr& ce,
02026 AST::Node* ann) {
02027 p_float_lin_cmp_reif(s,FRT_LQ,ce,ann);
02028 }
02029 void p_float_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce,
02030 AST::Node* ann) {
02031 p_float_lin_cmp_reif(s,FRT_LE,ce,ann);
02032 }
02033
02034 void p_float_times(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02035 FloatVar x = s.arg2FloatVar(ce[0]);
02036 FloatVar y = s.arg2FloatVar(ce[1]);
02037 FloatVar z = s.arg2FloatVar(ce[2]);
02038 mult(s,x,y,z);
02039 }
02040
02041 void p_float_div(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02042 FloatVar x = s.arg2FloatVar(ce[0]);
02043 FloatVar y = s.arg2FloatVar(ce[1]);
02044 FloatVar z = s.arg2FloatVar(ce[2]);
02045 div(s,x,y,z);
02046 }
02047
02048 void p_float_plus(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02049 FloatVar x = s.arg2FloatVar(ce[0]);
02050 FloatVar y = s.arg2FloatVar(ce[1]);
02051 FloatVar z = s.arg2FloatVar(ce[2]);
02052 rel(s,x+y==z);
02053 }
02054
02055 void p_float_sqrt(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02056 FloatVar x = s.arg2FloatVar(ce[0]);
02057 FloatVar y = s.arg2FloatVar(ce[1]);
02058 sqrt(s,x,y);
02059 }
02060
02061 void p_float_abs(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02062 FloatVar x = s.arg2FloatVar(ce[0]);
02063 FloatVar y = s.arg2FloatVar(ce[1]);
02064 abs(s,x,y);
02065 }
02066
02067 void p_float_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02068 FloatVar x = s.arg2FloatVar(ce[0]);
02069 FloatVar y = s.arg2FloatVar(ce[1]);
02070 rel(s,x,FRT_EQ,y);
02071 }
02072 void p_float_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02073 FloatVar x = s.arg2FloatVar(ce[0]);
02074 FloatVar y = s.arg2FloatVar(ce[1]);
02075 BoolVar b = s.arg2BoolVar(ce[2]);
02076 rel(s,x,FRT_EQ,y,b);
02077 }
02078 void p_float_le(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02079 FloatVar x = s.arg2FloatVar(ce[0]);
02080 FloatVar y = s.arg2FloatVar(ce[1]);
02081 rel(s,x,FRT_LQ,y);
02082 }
02083 void p_float_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02084 FloatVar x = s.arg2FloatVar(ce[0]);
02085 FloatVar y = s.arg2FloatVar(ce[1]);
02086 BoolVar b = s.arg2BoolVar(ce[2]);
02087 rel(s,x,FRT_LQ,y,b);
02088 }
02089 void p_float_max(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02090 FloatVar x = s.arg2FloatVar(ce[0]);
02091 FloatVar y = s.arg2FloatVar(ce[1]);
02092 FloatVar z = s.arg2FloatVar(ce[2]);
02093 max(s,x,y,z);
02094 }
02095 void p_float_min(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02096 FloatVar x = s.arg2FloatVar(ce[0]);
02097 FloatVar y = s.arg2FloatVar(ce[1]);
02098 FloatVar z = s.arg2FloatVar(ce[2]);
02099 min(s,x,y,z);
02100 }
02101 void p_float_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02102 FloatVar x = s.arg2FloatVar(ce[0]);
02103 FloatVar y = s.arg2FloatVar(ce[1]);
02104 rel(s, x, FRT_LQ, y);
02105 rel(s, x, FRT_EQ, y, BoolVar(s,0,0));
02106 }
02107
02108 void p_float_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02109 FloatVar x = s.arg2FloatVar(ce[0]);
02110 FloatVar y = s.arg2FloatVar(ce[1]);
02111 BoolVar b = s.arg2BoolVar(ce[2]);
02112 BoolVar b0(s,0,1);
02113 BoolVar b1(s,0,1);
02114 rel(s, b == (b0 && !b1));
02115 rel(s, x, FRT_LQ, y, b0);
02116 rel(s, x, FRT_EQ, y, b1);
02117 }
02118
02119 void p_float_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02120 FloatVar x = s.arg2FloatVar(ce[0]);
02121 FloatVar y = s.arg2FloatVar(ce[1]);
02122 rel(s, x, FRT_EQ, y, BoolVar(s,0,0));
02123 }
02124
02125 #ifdef GECODE_HAS_MPFR
02126 #define P_FLOAT_OP(Op) \
02127 void p_float_ ## Op (FlatZincSpace& s, const ConExpr& ce, AST::Node*) {\
02128 FloatVar x = s.arg2FloatVar(ce[0]);\
02129 FloatVar y = s.arg2FloatVar(ce[1]);\
02130 Op(s,x,y);\
02131 }
02132 P_FLOAT_OP(acos)
02133 P_FLOAT_OP(asin)
02134 P_FLOAT_OP(atan)
02135 P_FLOAT_OP(cos)
02136 P_FLOAT_OP(exp)
02137 P_FLOAT_OP(sin)
02138 P_FLOAT_OP(tan)
02139
02140
02141
02142 #undef P_FLOAT_OP
02143
02144 void p_float_ln(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02145 FloatVar x = s.arg2FloatVar(ce[0]);
02146 FloatVar y = s.arg2FloatVar(ce[1]);
02147 log(s,x,y);
02148 }
02149 void p_float_log10(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02150 FloatVar x = s.arg2FloatVar(ce[0]);
02151 FloatVar y = s.arg2FloatVar(ce[1]);
02152 log(s,10.0,x,y);
02153 }
02154 void p_float_log2(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
02155 FloatVar x = s.arg2FloatVar(ce[0]);
02156 FloatVar y = s.arg2FloatVar(ce[1]);
02157 log(s,2.0,x,y);
02158 }
02159
02160 #endif
02161
02162 class FloatPoster {
02163 public:
02164 FloatPoster(void) {
02165 registry().add("int2float",&p_int2float);
02166 registry().add("float_abs",&p_float_abs);
02167 registry().add("float_sqrt",&p_float_sqrt);
02168 registry().add("float_eq",&p_float_eq);
02169 registry().add("float_eq_reif",&p_float_eq_reif);
02170 registry().add("float_le",&p_float_le);
02171 registry().add("float_le_reif",&p_float_le_reif);
02172 registry().add("float_lt",&p_float_lt);
02173 registry().add("float_lt_reif",&p_float_lt_reif);
02174 registry().add("float_ne",&p_float_ne);
02175 registry().add("float_times",&p_float_times);
02176 registry().add("float_div",&p_float_div);
02177 registry().add("float_plus",&p_float_plus);
02178 registry().add("float_max",&p_float_max);
02179 registry().add("float_min",&p_float_min);
02180
02181 registry().add("float_lin_eq",&p_float_lin_eq);
02182 registry().add("float_lin_eq_reif",&p_float_lin_eq_reif);
02183 registry().add("float_lin_le",&p_float_lin_le);
02184 registry().add("float_lin_lt",&p_float_lin_lt);
02185 registry().add("float_lin_le_reif",&p_float_lin_le_reif);
02186 registry().add("float_lin_lt_reif",&p_float_lin_lt_reif);
02187
02188 #ifdef GECODE_HAS_MPFR
02189 registry().add("float_acos",&p_float_acos);
02190 registry().add("float_asin",&p_float_asin);
02191 registry().add("float_atan",&p_float_atan);
02192 registry().add("float_cos",&p_float_cos);
02193
02194 registry().add("float_exp",&p_float_exp);
02195 registry().add("float_ln",&p_float_ln);
02196 registry().add("float_log10",&p_float_log10);
02197 registry().add("float_log2",&p_float_log2);
02198 registry().add("float_sin",&p_float_sin);
02199
02200 registry().add("float_tan",&p_float_tan);
02201
02202 #endif
02203 }
02204 } __float_poster;
02205 #endif
02206
02207 }
02208 }}
02209
02210