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