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