registry.cpp
Go to the documentation of this file.
/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
/*
* Main authors:
* Guido Tack <tack@gecode.org>
*
* Contributing authors:
* Mikael Lagerkvist <lagerkvist@gmail.com>
*
* Copyright:
* Guido Tack, 2007
* Mikael Lagerkvist, 2009
*
* This file is part of Gecode, the generic constraint
* development environment:
* http://www.gecode.org
*
* Permission is hereby granted, free of charge, to any person obtaining
* a copy of this software and associated documentation files (the
* "Software"), to deal in the Software without restriction, including
* without limitation the rights to use, copy, modify, merge, publish,
* distribute, sublicense, and/or sell copies of the Software, and to
* permit persons to whom the Software is furnished to do so, subject to
* the following conditions:
*
* The above copyright notice and this permission notice shall be
* included in all copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
* EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
* MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
* NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
* LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
* OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
* WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*
*/
#include <gecode/flatzinc/registry.hh>
#include <gecode/kernel.hh>
#include <gecode/int.hh>
#include <gecode/minimodel.hh>
#ifdef GECODE_HAS_SET_VARS
#include <gecode/set.hh>
#endif
#ifdef GECODE_HAS_FLOAT_VARS
#include <gecode/float.hh>
#endif
#include <gecode/flatzinc.hh>
namespace Gecode { namespace FlatZinc {
Registry& registry(void) {
static Registry r;
return r;
}
void
Registry::post(FlatZincSpace& s, const ConExpr& ce) {
std::map<std::string,poster>::iterator i = r.find(ce.id);
if (i == r.end()) {
throw FlatZinc::Error("Registry",
std::string("Constraint ")+ce.id+" not found");
}
i->second(s, ce, ce.ann);
}
void
Registry::add(const std::string& id, poster p) {
r[id] = p;
r["gecode_" + id] = p;
}
namespace {
void p_distinct(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs va = s.arg2intvarargs(ce[0]);
IntPropLevel ipl = s.ann2ipl(ann);
unshare(s, va);
distinct(s, va, ipl == IPL_DEF ? IPL_BND : ipl);
}
void p_distinctOffset(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs va = s.arg2intvarargs(ce[1]);
unshare(s, va);
AST::Array* offs = ce.args->a[0]->getArray();
IntArgs oa(offs->a.size());
for (int i=offs->a.size(); i--; ) {
oa[i] = offs->a[i]->getInt();
}
IntPropLevel ipl = s.ann2ipl(ann);
distinct(s, oa, va, ipl == IPL_DEF ? IPL_BND : ipl);
}
void p_all_equal(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs va = s.arg2intvarargs(ce[0]);
rel(s, va, IRT_EQ, s.ann2ipl(ann));
}
void p_int_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
AST::Node* ann) {
if (ce[0]->isIntVar()) {
if (ce[1]->isIntVar()) {
rel(s, s.arg2IntVar(ce[0]), irt, s.arg2IntVar(ce[1]),
s.ann2ipl(ann));
} else {
rel(s, s.arg2IntVar(ce[0]), irt, ce[1]->getInt(), s.ann2ipl(ann));
}
} else {
rel(s, s.arg2IntVar(ce[1]), swap(irt), ce[0]->getInt(),
s.ann2ipl(ann));
}
}
void p_int_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP(s, IRT_EQ, ce, ann);
}
void p_int_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP(s, IRT_NQ, ce, ann);
}
void p_int_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP(s, IRT_GQ, ce, ann);
}
void p_int_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP(s, IRT_GR, ce, ann);
}
void p_int_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP(s, IRT_LQ, ce, ann);
}
void p_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP(s, IRT_LE, ce, ann);
}
void p_int_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm,
const ConExpr& ce, AST::Node* ann) {
if (rm == RM_EQV && ce[2]->isBool()) {
if (ce[2]->getBool()) {
p_int_CMP(s, irt, ce, ann);
} else {
p_int_CMP(s, neg(irt), ce, ann);
}
return;
}
if (ce[0]->isIntVar()) {
if (ce[1]->isIntVar()) {
rel(s, s.arg2IntVar(ce[0]), irt, s.arg2IntVar(ce[1]),
Reify(s.arg2BoolVar(ce[2]), rm), s.ann2ipl(ann));
} else {
rel(s, s.arg2IntVar(ce[0]), irt, ce[1]->getInt(),
Reify(s.arg2BoolVar(ce[2]), rm), s.ann2ipl(ann));
}
} else {
rel(s, s.arg2IntVar(ce[1]), swap(irt), ce[0]->getInt(),
Reify(s.arg2BoolVar(ce[2]), rm), s.ann2ipl(ann));
}
}
/* Comparisons */
void p_int_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann);
}
void p_int_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann);
}
void p_int_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann);
}
void p_int_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP_reif(s, IRT_GR, RM_EQV, ce, ann);
}
void p_int_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann);
}
void p_int_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP_reif(s, IRT_LE, RM_EQV, ce, ann);
}
void p_int_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann);
}
void p_int_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann);
}
void p_int_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann);
}
void p_int_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP_reif(s, IRT_GR, RM_IMP, ce, ann);
}
void p_int_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann);
}
void p_int_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_CMP_reif(s, IRT_LE, RM_IMP, ce, ann);
}
/* linear (in-)equations */
void p_int_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
AST::Node* ann) {
IntArgs ia = s.arg2intargs(ce[0]);
int singleIntVar;
if (s.isBoolArray(ce[1],singleIntVar)) {
if (singleIntVar != -1) {
if (std::abs(ia[singleIntVar]) == 1 && ce[2]->getInt() == 0) {
IntVar siv = s.arg2IntVar(ce[1]->getArray()->a[singleIntVar]);
BoolVarArgs iv = s.arg2boolvarargs(ce[1], 0, singleIntVar);
IntArgs ia_tmp(ia.size()-1);
int count = 0;
for (int i=0; i<ia.size(); i++) {
if (i != singleIntVar)
ia_tmp[count++] = ia[singleIntVar] == -1 ? ia[i] : -ia[i];
}
IntRelType t = (ia[singleIntVar] == -1 ? irt : swap(irt));
linear(s, ia_tmp, iv, t, siv, s.ann2ipl(ann));
} else {
IntVarArgs iv = s.arg2intvarargs(ce[1]);
linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2ipl(ann));
}
} else {
BoolVarArgs iv = s.arg2boolvarargs(ce[1]);
linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2ipl(ann));
}
} else {
IntVarArgs iv = s.arg2intvarargs(ce[1]);
linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2ipl(ann));
}
}
void p_int_lin_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm,
const ConExpr& ce, AST::Node* ann) {
if (rm == RM_EQV && ce[2]->isBool()) {
if (ce[2]->getBool()) {
p_int_lin_CMP(s, irt, ce, ann);
} else {
p_int_lin_CMP(s, neg(irt), ce, ann);
}
return;
}
IntArgs ia = s.arg2intargs(ce[0]);
int singleIntVar;
if (s.isBoolArray(ce[1],singleIntVar)) {
if (singleIntVar != -1) {
if (std::abs(ia[singleIntVar]) == 1 && ce[2]->getInt() == 0) {
IntVar siv = s.arg2IntVar(ce[1]->getArray()->a[singleIntVar]);
BoolVarArgs iv = s.arg2boolvarargs(ce[1], 0, singleIntVar);
IntArgs ia_tmp(ia.size()-1);
int count = 0;
for (int i=0; i<ia.size(); i++) {
if (i != singleIntVar)
ia_tmp[count++] = ia[singleIntVar] == -1 ? ia[i] : -ia[i];
}
IntRelType t = (ia[singleIntVar] == -1 ? irt : swap(irt));
linear(s, ia_tmp, iv, t, siv, Reify(s.arg2BoolVar(ce[3]), rm),
s.ann2ipl(ann));
} else {
IntVarArgs iv = s.arg2intvarargs(ce[1]);
linear(s, ia, iv, irt, ce[2]->getInt(),
Reify(s.arg2BoolVar(ce[3]), rm), s.ann2ipl(ann));
}
} else {
BoolVarArgs iv = s.arg2boolvarargs(ce[1]);
linear(s, ia, iv, irt, ce[2]->getInt(),
Reify(s.arg2BoolVar(ce[3]), rm), s.ann2ipl(ann));
}
} else {
IntVarArgs iv = s.arg2intvarargs(ce[1]);
linear(s, ia, iv, irt, ce[2]->getInt(),
Reify(s.arg2BoolVar(ce[3]), rm),
s.ann2ipl(ann));
}
}
void p_int_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP(s, IRT_EQ, ce, ann);
}
void p_int_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann);
}
void p_int_lin_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann);
}
void p_int_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP(s, IRT_NQ, ce, ann);
}
void p_int_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann);
}
void p_int_lin_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann);
}
void p_int_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP(s, IRT_LQ, ce, ann);
}
void p_int_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann);
}
void p_int_lin_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann);
}
void p_int_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP(s, IRT_LE, ce, ann);
}
void p_int_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP_reif(s, IRT_LE, RM_EQV, ce, ann);
}
void p_int_lin_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP_reif(s, IRT_LE, RM_IMP, ce, ann);
}
void p_int_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP(s, IRT_GQ, ce, ann);
}
void p_int_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann);
}
void p_int_lin_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann);
}
void p_int_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP(s, IRT_GR, ce, ann);
}
void p_int_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP_reif(s, IRT_GR, RM_EQV, ce, ann);
}
void p_int_lin_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_int_lin_CMP_reif(s, IRT_GR, RM_IMP, ce, ann);
}
void p_bool_lin_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
AST::Node* ann) {
IntArgs ia = s.arg2intargs(ce[0]);
BoolVarArgs iv = s.arg2boolvarargs(ce[1]);
if (ce[2]->isIntVar())
linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()], s.ann2ipl(ann));
else
linear(s, ia, iv, irt, ce[2]->getInt(), s.ann2ipl(ann));
}
void p_bool_lin_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm,
const ConExpr& ce, AST::Node* ann) {
if (rm == RM_EQV && ce[2]->isBool()) {
if (ce[2]->getBool()) {
p_bool_lin_CMP(s, irt, ce, ann);
} else {
p_bool_lin_CMP(s, neg(irt), ce, ann);
}
return;
}
IntArgs ia = s.arg2intargs(ce[0]);
BoolVarArgs iv = s.arg2boolvarargs(ce[1]);
if (ce[2]->isIntVar())
linear(s, ia, iv, irt, s.iv[ce[2]->getIntVar()],
Reify(s.arg2BoolVar(ce[3]), rm),
s.ann2ipl(ann));
else
linear(s, ia, iv, irt, ce[2]->getInt(),
Reify(s.arg2BoolVar(ce[3]), rm),
s.ann2ipl(ann));
}
void p_bool_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_lin_CMP(s, IRT_EQ, ce, ann);
}
void p_bool_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
p_bool_lin_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann);
}
void p_bool_lin_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
p_bool_lin_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann);
}
void p_bool_lin_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_lin_CMP(s, IRT_NQ, ce, ann);
}
void p_bool_lin_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
p_bool_lin_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann);
}
void p_bool_lin_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
p_bool_lin_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann);
}
void p_bool_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_lin_CMP(s, IRT_LQ, ce, ann);
}
void p_bool_lin_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
p_bool_lin_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann);
}
void p_bool_lin_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
p_bool_lin_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann);
}
void p_bool_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
p_bool_lin_CMP(s, IRT_LE, ce, ann);
}
void p_bool_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
p_bool_lin_CMP_reif(s, IRT_LE, RM_EQV, ce, ann);
}
void p_bool_lin_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
p_bool_lin_CMP_reif(s, IRT_LE, RM_IMP, ce, ann);
}
void p_bool_lin_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_lin_CMP(s, IRT_GQ, ce, ann);
}
void p_bool_lin_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
p_bool_lin_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann);
}
void p_bool_lin_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
p_bool_lin_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann);
}
void p_bool_lin_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_lin_CMP(s, IRT_GR, ce, ann);
}
void p_bool_lin_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
p_bool_lin_CMP_reif(s, IRT_GR, RM_EQV, ce, ann);
}
void p_bool_lin_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
p_bool_lin_CMP_reif(s, IRT_GR, RM_IMP, ce, ann);
}
/* arithmetic constraints */
void p_int_plus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
if (!ce[0]->isIntVar()) {
rel(s, ce[0]->getInt() + s.arg2IntVar(ce[1])
== s.arg2IntVar(ce[2]), s.ann2ipl(ann));
} else if (!ce[1]->isIntVar()) {
rel(s, s.arg2IntVar(ce[0]) + ce[1]->getInt()
== s.arg2IntVar(ce[2]), s.ann2ipl(ann));
} else if (!ce[2]->isIntVar()) {
rel(s, s.arg2IntVar(ce[0]) + s.arg2IntVar(ce[1])
== ce[2]->getInt(), s.ann2ipl(ann));
} else {
rel(s, s.arg2IntVar(ce[0]) + s.arg2IntVar(ce[1])
== s.arg2IntVar(ce[2]), s.ann2ipl(ann));
}
}
void p_int_minus(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
if (!ce[0]->isIntVar()) {
rel(s, ce[0]->getInt() - s.arg2IntVar(ce[1])
== s.arg2IntVar(ce[2]), s.ann2ipl(ann));
} else if (!ce[1]->isIntVar()) {
rel(s, s.arg2IntVar(ce[0]) - ce[1]->getInt()
== s.arg2IntVar(ce[2]), s.ann2ipl(ann));
} else if (!ce[2]->isIntVar()) {
rel(s, s.arg2IntVar(ce[0]) - s.arg2IntVar(ce[1])
== ce[2]->getInt(), s.ann2ipl(ann));
} else {
rel(s, s.arg2IntVar(ce[0]) - s.arg2IntVar(ce[1])
== s.arg2IntVar(ce[2]), s.ann2ipl(ann));
}
}
void p_int_times(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVar x0 = s.arg2IntVar(ce[0]);
IntVar x1 = s.arg2IntVar(ce[1]);
IntVar x2 = s.arg2IntVar(ce[2]);
mult(s, x0, x1, x2, s.ann2ipl(ann));
}
void p_int_pow(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVar x0 = s.arg2IntVar(ce[0]);
IntVar x2 = s.arg2IntVar(ce[2]);
pow(s, x0, ce[1]->getInt(), x2, s.ann2ipl(ann));
}
void p_int_div(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVar x0 = s.arg2IntVar(ce[0]);
IntVar x1 = s.arg2IntVar(ce[1]);
IntVar x2 = s.arg2IntVar(ce[2]);
div(s,x0,x1,x2, s.ann2ipl(ann));
}
void p_int_mod(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVar x0 = s.arg2IntVar(ce[0]);
IntVar x1 = s.arg2IntVar(ce[1]);
IntVar x2 = s.arg2IntVar(ce[2]);
mod(s,x0,x1,x2, s.ann2ipl(ann));
}
void p_int_min(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVar x0 = s.arg2IntVar(ce[0]);
IntVar x1 = s.arg2IntVar(ce[1]);
IntVar x2 = s.arg2IntVar(ce[2]);
min(s, x0, x1, x2, s.ann2ipl(ann));
}
void p_int_max(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVar x0 = s.arg2IntVar(ce[0]);
IntVar x1 = s.arg2IntVar(ce[1]);
IntVar x2 = s.arg2IntVar(ce[2]);
max(s, x0, x1, x2, s.ann2ipl(ann));
}
void p_int_negate(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVar x0 = s.arg2IntVar(ce[0]);
IntVar x1 = s.arg2IntVar(ce[1]);
rel(s, x0 == -x1, s.ann2ipl(ann));
}
/* Boolean constraints */
void p_bool_CMP(FlatZincSpace& s, IntRelType irt, const ConExpr& ce,
AST::Node* ann) {
rel(s, s.arg2BoolVar(ce[0]), irt, s.arg2BoolVar(ce[1]),
s.ann2ipl(ann));
}
void p_bool_CMP_reif(FlatZincSpace& s, IntRelType irt, ReifyMode rm,
const ConExpr& ce, AST::Node* ann) {
rel(s, s.arg2BoolVar(ce[0]), irt, s.arg2BoolVar(ce[1]),
Reify(s.arg2BoolVar(ce[2]), rm), s.ann2ipl(ann));
}
void p_bool_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP(s, IRT_EQ, ce, ann);
}
void p_bool_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP_reif(s, IRT_EQ, RM_EQV, ce, ann);
}
void p_bool_eq_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP_reif(s, IRT_EQ, RM_IMP, ce, ann);
}
void p_bool_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP(s, IRT_NQ, ce, ann);
}
void p_bool_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP_reif(s, IRT_NQ, RM_EQV, ce, ann);
}
void p_bool_ne_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP_reif(s, IRT_NQ, RM_IMP, ce, ann);
}
void p_bool_ge(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP(s, IRT_GQ, ce, ann);
}
void p_bool_ge_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP_reif(s, IRT_GQ, RM_EQV, ce, ann);
}
void p_bool_ge_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP_reif(s, IRT_GQ, RM_IMP, ce, ann);
}
void p_bool_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP(s, IRT_LQ, ce, ann);
}
void p_bool_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP_reif(s, IRT_LQ, RM_EQV, ce, ann);
}
void p_bool_le_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP_reif(s, IRT_LQ, RM_IMP, ce, ann);
}
void p_bool_gt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP(s, IRT_GR, ce, ann);
}
void p_bool_gt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP_reif(s, IRT_GR, RM_EQV, ce, ann);
}
void p_bool_gt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP_reif(s, IRT_GR, RM_IMP, ce, ann);
}
void p_bool_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP(s, IRT_LE, ce, ann);
}
void p_bool_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP_reif(s, IRT_LE, RM_EQV, ce, ann);
}
void p_bool_lt_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_bool_CMP_reif(s, IRT_LE, RM_IMP, ce, ann);
}
#define BOOL_OP(op) \
BoolVar b0 = s.arg2BoolVar(ce[0]); \
BoolVar b1 = s.arg2BoolVar(ce[1]); \
if (ce[2]->isBool()) { \
rel(s, b0, op, b1, ce[2]->getBool(), s.ann2ipl(ann)); \
} else { \
rel(s, b0, op, b1, s.bv[ce[2]->getBoolVar()], s.ann2ipl(ann)); \
}
#define BOOL_ARRAY_OP(op) \
BoolVarArgs bv = s.arg2boolvarargs(ce[0]); \
if (ce.size()==1) { \
rel(s, op, bv, 1, s.ann2ipl(ann)); \
} else if (ce[1]->isBool()) { \
rel(s, op, bv, ce[1]->getBool(), s.ann2ipl(ann)); \
} else { \
rel(s, op, bv, s.bv[ce[1]->getBoolVar()], s.ann2ipl(ann)); \
}
void p_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BOOL_OP(BOT_OR);
}
void p_bool_or_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BoolVar b0 = s.arg2BoolVar(ce[0]);
BoolVar b1 = s.arg2BoolVar(ce[1]);
BoolVar b2 = s.arg2BoolVar(ce[2]);
clause(s, BOT_OR, BoolVarArgs()<<b0<<b1, BoolVarArgs()<<b2, 1,
s.ann2ipl(ann));
}
void p_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BOOL_OP(BOT_AND);
}
void p_bool_and_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BoolVar b0 = s.arg2BoolVar(ce[0]);
BoolVar b1 = s.arg2BoolVar(ce[1]);
BoolVar b2 = s.arg2BoolVar(ce[2]);
rel(s, b2, BOT_IMP, b0, 1, s.ann2ipl(ann));
rel(s, b2, BOT_IMP, b1, 1, s.ann2ipl(ann));
}
void p_array_bool_and(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
BOOL_ARRAY_OP(BOT_AND);
}
void p_array_bool_and_imp(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann)
{
BoolVarArgs bv = s.arg2boolvarargs(ce[0]);
BoolVar b1 = s.arg2BoolVar(ce[1]);
for (unsigned int i=bv.size(); i--;)
rel(s, b1, BOT_IMP, bv[i], 1, s.ann2ipl(ann));
}
void p_array_bool_or(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
BOOL_ARRAY_OP(BOT_OR);
}
void p_array_bool_or_imp(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann)
{
BoolVarArgs bv = s.arg2boolvarargs(ce[0]);
BoolVar b1 = s.arg2BoolVar(ce[1]);
clause(s, BOT_OR, bv, BoolVarArgs()<<b1, 1, s.ann2ipl(ann));
}
void p_array_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann)
{
BOOL_ARRAY_OP(BOT_XOR);
}
void p_array_bool_xor_imp(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann)
{
BoolVarArgs bv = s.arg2boolvarargs(ce[0]);
BoolVar tmp(s,0,1);
rel(s, BOT_XOR, bv, tmp, s.ann2ipl(ann));
rel(s, s.arg2BoolVar(ce[1]), BOT_IMP, tmp, 1);
}
void p_array_bool_clause(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
BoolVarArgs bvp = s.arg2boolvarargs(ce[0]);
BoolVarArgs bvn = s.arg2boolvarargs(ce[1]);
clause(s, BOT_OR, bvp, bvn, 1, s.ann2ipl(ann));
}
void p_array_bool_clause_reif(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
BoolVarArgs bvp = s.arg2boolvarargs(ce[0]);
BoolVarArgs bvn = s.arg2boolvarargs(ce[1]);
BoolVar b0 = s.arg2BoolVar(ce[2]);
clause(s, BOT_OR, bvp, bvn, b0, s.ann2ipl(ann));
}
void p_array_bool_clause_imp(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
BoolVarArgs bvp = s.arg2boolvarargs(ce[0]);
BoolVarArgs bvn = s.arg2boolvarargs(ce[1]);
BoolVar b0 = s.arg2BoolVar(ce[2]);
clause(s, BOT_OR, bvp, bvn, b0, s.ann2ipl(ann));
}
void p_bool_xor(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BOOL_OP(BOT_XOR);
}
void p_bool_xor_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BoolVar b0 = s.arg2BoolVar(ce[0]);
BoolVar b1 = s.arg2BoolVar(ce[1]);
BoolVar b2 = s.arg2BoolVar(ce[2]);
clause(s, BOT_OR, BoolVarArgs()<<b0<<b1, BoolVarArgs()<<b2, 1,
s.ann2ipl(ann));
clause(s, BOT_OR, BoolVarArgs(), BoolVarArgs()<<b0<<b1<<b2, 1,
s.ann2ipl(ann));
}
void p_bool_l_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BoolVar b0 = s.arg2BoolVar(ce[0]);
BoolVar b1 = s.arg2BoolVar(ce[1]);
if (ce[2]->isBool()) {
rel(s, b1, BOT_IMP, b0, ce[2]->getBool(), s.ann2ipl(ann));
} else {
rel(s, b1, BOT_IMP, b0, s.bv[ce[2]->getBoolVar()], s.ann2ipl(ann));
}
}
void p_bool_r_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BOOL_OP(BOT_IMP);
}
void p_bool_not(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BoolVar x0 = s.arg2BoolVar(ce[0]);
BoolVar x1 = s.arg2BoolVar(ce[1]);
rel(s, x0, BOT_XOR, x1, 1, s.ann2ipl(ann));
}
/* element constraints */
void p_array_int_element(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
bool isConstant = true;
AST::Array* a = ce[1]->getArray();
for (int i=a->a.size(); i--;) {
if (!a->a[i]->isInt()) {
isConstant = false;
break;
}
}
IntVar selector = s.arg2IntVar(ce[0]);
rel(s, selector > 0);
if (isConstant) {
IntSharedArray sia = s.arg2intsharedarray(ce[1], 1);
element(s, sia, selector, s.arg2IntVar(ce[2]), s.ann2ipl(ann));
} else {
IntVarArgs iv = s.arg2intvarargs(ce[1], 1);
element(s, iv, selector, s.arg2IntVar(ce[2]), s.ann2ipl(ann));
}
}
void p_array_bool_element(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
bool isConstant = true;
AST::Array* a = ce[1]->getArray();
for (int i=a->a.size(); i--;) {
if (!a->a[i]->isBool()) {
isConstant = false;
break;
}
}
IntVar selector = s.arg2IntVar(ce[0]);
rel(s, selector > 0);
if (isConstant) {
IntSharedArray sia = s.arg2boolsharedarray(ce[1], 1);
element(s, sia, selector, s.arg2BoolVar(ce[2]), s.ann2ipl(ann));
} else {
BoolVarArgs iv = s.arg2boolvarargs(ce[1], 1);
element(s, iv, selector, s.arg2BoolVar(ce[2]), s.ann2ipl(ann));
}
}
/* coercion constraints */
void p_bool2int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BoolVar x0 = s.arg2BoolVar(ce[0]);
IntVar x1 = s.arg2IntVar(ce[1]);
if (ce[0]->isBoolVar() && ce[1]->isIntVar()) {
s.aliasBool2Int(ce[1]->getIntVar(), ce[0]->getBoolVar());
}
channel(s, x0, x1, s.ann2ipl(ann));
}
void p_int_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
IntSet d = s.arg2intset(ce[1]);
if (ce[0]->isBoolVar()) {
IntSetRanges dr(d);
Iter::Ranges::Singleton sr(0,1);
Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
IntSet d01(i);
if (d01.size() == 0) {
s.fail();
} else {
rel(s, s.arg2BoolVar(ce[0]), IRT_GQ, d01.min());
rel(s, s.arg2BoolVar(ce[0]), IRT_LQ, d01.max());
}
} else {
dom(s, s.arg2IntVar(ce[0]), d);
}
}
void p_int_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
IntSet d = s.arg2intset(ce[1]);
if (ce[0]->isBoolVar()) {
IntSetRanges dr(d);
Iter::Ranges::Singleton sr(0,1);
Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
IntSet d01(i);
if (d01.size() == 0) {
rel(s, s.arg2BoolVar(ce[2]) == 0);
} else if (d01.max() == 0) {
rel(s, s.arg2BoolVar(ce[2]) == !s.arg2BoolVar(ce[0]));
} else if (d01.min() == 1) {
rel(s, s.arg2BoolVar(ce[2]) == s.arg2BoolVar(ce[0]));
} else {
rel(s, s.arg2BoolVar(ce[2]) == 1);
}
} else {
dom(s, s.arg2IntVar(ce[0]), d, s.arg2BoolVar(ce[2]));
}
}
void p_int_in_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
IntSet d = s.arg2intset(ce[1]);
if (ce[0]->isBoolVar()) {
IntSetRanges dr(d);
Iter::Ranges::Singleton sr(0,1);
Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
IntSet d01(i);
if (d01.size() == 0) {
rel(s, s.arg2BoolVar(ce[2]) == 0);
} else if (d01.max() == 0) {
rel(s, s.arg2BoolVar(ce[2]) >> !s.arg2BoolVar(ce[0]));
} else if (d01.min() == 1) {
rel(s, s.arg2BoolVar(ce[2]) >> s.arg2BoolVar(ce[0]));
}
} else {
dom(s, s.arg2IntVar(ce[0]), d, Reify(s.arg2BoolVar(ce[2]),RM_IMP));
}
}
/* constraints from the standard library */
void p_abs(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVar x0 = s.arg2IntVar(ce[0]);
IntVar x1 = s.arg2IntVar(ce[1]);
abs(s, x0, x1, s.ann2ipl(ann));
}
void p_array_int_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs iv0 = s.arg2intvarargs(ce[0]);
IntVarArgs iv1 = s.arg2intvarargs(ce[1]);
rel(s, iv0, IRT_LE, iv1, s.ann2ipl(ann));
}
void p_array_int_lq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs iv0 = s.arg2intvarargs(ce[0]);
IntVarArgs iv1 = s.arg2intvarargs(ce[1]);
rel(s, iv0, IRT_LQ, iv1, s.ann2ipl(ann));
}
void p_array_bool_lt(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
BoolVarArgs bv0 = s.arg2boolvarargs(ce[0]);
BoolVarArgs bv1 = s.arg2boolvarargs(ce[1]);
rel(s, bv0, IRT_LE, bv1, s.ann2ipl(ann));
}
void p_array_bool_lq(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
BoolVarArgs bv0 = s.arg2boolvarargs(ce[0]);
BoolVarArgs bv1 = s.arg2boolvarargs(ce[1]);
rel(s, bv0, IRT_LQ, bv1, s.ann2ipl(ann));
}
void p_count(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs iv = s.arg2intvarargs(ce[0]);
if (!ce[1]->isIntVar()) {
if (!ce[2]->isIntVar()) {
count(s, iv, ce[1]->getInt(), IRT_EQ, ce[2]->getInt(),
s.ann2ipl(ann));
} else {
count(s, iv, ce[1]->getInt(), IRT_EQ, s.arg2IntVar(ce[2]),
s.ann2ipl(ann));
}
} else if (!ce[2]->isIntVar()) {
count(s, iv, s.arg2IntVar(ce[1]), IRT_EQ, ce[2]->getInt(),
s.ann2ipl(ann));
} else {
count(s, iv, s.arg2IntVar(ce[1]), IRT_EQ, s.arg2IntVar(ce[2]),
s.ann2ipl(ann));
}
}
void p_count_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs iv = s.arg2intvarargs(ce[0]);
IntVar x = s.arg2IntVar(ce[1]);
IntVar y = s.arg2IntVar(ce[2]);
BoolVar b = s.arg2BoolVar(ce[3]);
IntVar c(s,0,Int::Limits::max);
count(s,iv,x,IRT_EQ,c,s.ann2ipl(ann));
rel(s, b == (c==y));
}
void p_count_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs iv = s.arg2intvarargs(ce[0]);
IntVar x = s.arg2IntVar(ce[1]);
IntVar y = s.arg2IntVar(ce[2]);
BoolVar b = s.arg2BoolVar(ce[3]);
IntVar c(s,0,Int::Limits::max);
count(s,iv,x,IRT_EQ,c,s.ann2ipl(ann));
rel(s, b >> (c==y));
}
void count_rel(IntRelType irt,
FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs iv = s.arg2intvarargs(ce[1]);
count(s, iv, ce[2]->getInt(), irt, ce[0]->getInt(), s.ann2ipl(ann));
}
void p_at_most(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
count_rel(IRT_LQ, s, ce, ann);
}
void p_at_least(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
count_rel(IRT_GQ, s, ce, ann);
}
void p_bin_packing_load(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
int minIdx = ce[3]->getInt();
IntVarArgs load = s.arg2intvarargs(ce[0]);
IntVarArgs l;
IntVarArgs bin = s.arg2intvarargs(ce[1]);
for (int i=bin.size(); i--;)
rel(s, bin[i] >= minIdx);
if (minIdx > 0) {
for (int i=minIdx; i--;)
l << IntVar(s,0,0);
} else if (minIdx < 0) {
IntVarArgs bin2(bin.size());
for (int i=bin.size(); i--;)
bin2[i] = expr(s, bin[i]-minIdx, s.ann2ipl(ann));
bin = bin2;
}
l << load;
IntArgs sizes = s.arg2intargs(ce[2]);
IntVarArgs allvars = l + bin;
unshare(s, allvars);
binpacking(s, allvars.slice(0,1,l.size()), allvars.slice(l.size(),1,bin.size()),
sizes, s.ann2ipl(ann));
}
void p_global_cardinality(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
IntVarArgs iv0 = s.arg2intvarargs(ce[0]);
IntArgs cover = s.arg2intargs(ce[1]);
IntVarArgs iv1 = s.arg2intvarargs(ce[2]);
Region re;
IntSet cover_s(cover);
IntSetRanges cover_r(cover_s);
IntVarRanges* iv0_ri = re.alloc<IntVarRanges>(iv0.size());
for (int i=iv0.size(); i--;)
iv0_ri[i] = IntVarRanges(iv0[i]);
Iter::Ranges::NaryUnion iv0_r(re,iv0_ri,iv0.size());
Iter::Ranges::Diff<Iter::Ranges::NaryUnion,IntSetRanges>
extra_r(iv0_r,cover_r);
Iter::Ranges::ToValues<Iter::Ranges::Diff<
Iter::Ranges::NaryUnion,IntSetRanges> > extra(extra_r);
for (; extra(); ++extra) {
cover << extra.val();
iv1 << IntVar(s,0,iv0.size());
}
IntPropLevel ipl = s.ann2ipl(ann);
if (ipl==IPL_DEF)
ipl=IPL_BND;
if (ipl==IPL_DOM) {
IntVarArgs allvars = iv0+iv1;
unshare(s, allvars);
count(s, allvars.slice(0,1,iv0.size()),
allvars.slice(iv0.size(),1,iv1.size()),
cover, ipl);
} else {
unshare(s, iv0);
count(s, iv0, iv1, cover, ipl);
}
}
void p_global_cardinality_closed(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
IntVarArgs iv0 = s.arg2intvarargs(ce[0]);
IntArgs cover = s.arg2intargs(ce[1]);
IntVarArgs iv1 = s.arg2intvarargs(ce[2]);
IntPropLevel ipl = s.ann2ipl(ann);
if (ipl==IPL_DEF)
ipl=IPL_BND;
if (ipl==IPL_DOM) {
IntVarArgs allvars = iv0+iv1;
unshare(s, allvars);
count(s, allvars.slice(0,1,iv0.size()),
allvars.slice(iv0.size(),1,iv1.size()),
cover, ipl);
} else {
unshare(s, iv0);
count(s, iv0, iv1, cover, ipl);
}
}
void p_global_cardinality_low_up(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
IntArgs cover = s.arg2intargs(ce[1]);
IntArgs lbound = s.arg2intargs(ce[2]);
IntArgs ubound = s.arg2intargs(ce[3]);
IntSetArgs y(cover.size());
for (int i=cover.size(); i--;)
y[i] = IntSet(lbound[i],ubound[i]);
IntSet cover_s(cover);
Region re;
IntVarRanges* xrs = re.alloc<IntVarRanges>(x.size());
for (int i=x.size(); i--;)
xrs[i].init(x[i]);
Iter::Ranges::NaryUnion u(re, xrs, x.size());
Iter::Ranges::ToValues<Iter::Ranges::NaryUnion> uv(u);
for (; uv(); ++uv) {
if (!cover_s.in(uv.val())) {
cover << uv.val();
y << IntSet(0,x.size());
}
}
unshare(s, x);
IntPropLevel ipl = s.ann2ipl(ann);
if (ipl==IPL_DEF)
ipl=IPL_BND;
count(s, x, y, cover, ipl);
}
void p_global_cardinality_low_up_closed(FlatZincSpace& s,
const ConExpr& ce,
AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
IntArgs cover = s.arg2intargs(ce[1]);
IntArgs lbound = s.arg2intargs(ce[2]);
IntArgs ubound = s.arg2intargs(ce[3]);
IntSetArgs y(cover.size());
for (int i=cover.size(); i--;)
y[i] = IntSet(lbound[i],ubound[i]);
unshare(s, x);
IntPropLevel ipl = s.ann2ipl(ann);
if (ipl==IPL_DEF)
ipl=IPL_BND;
count(s, x, y, cover, ipl);
}
void p_minimum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs iv = s.arg2intvarargs(ce[1]);
min(s, iv, s.arg2IntVar(ce[0]), s.ann2ipl(ann));
}
void p_maximum(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs iv = s.arg2intvarargs(ce[1]);
max(s, iv, s.arg2IntVar(ce[0]), s.ann2ipl(ann));
}
void p_minimum_arg(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs iv = s.arg2intvarargs(ce[0]);
int offset = ce[1]->getInt();
argmin(s, iv, offset, s.arg2IntVar(ce[2]), true, s.ann2ipl(ann));
}
void p_maximum_arg(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs iv = s.arg2intvarargs(ce[0]);
int offset = ce[1]->getInt();
argmax(s, iv, offset, s.arg2IntVar(ce[2]), true, s.ann2ipl(ann));
}
void p_minimum_arg_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BoolVarArgs bv = s.arg2boolvarargs(ce[0]);
int offset = ce[1]->getInt();
argmin(s, bv, offset, s.arg2IntVar(ce[2]), true, s.ann2ipl(ann));
}
void p_maximum_arg_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BoolVarArgs bv = s.arg2boolvarargs(ce[0]);
int offset = ce[1]->getInt();
argmax(s, bv, offset, s.arg2IntVar(ce[2]), true, s.ann2ipl(ann));
}
void p_regular(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs iv = s.arg2intvarargs(ce[0]);
int q = ce[1]->getInt();
int symbols = ce[2]->getInt();
IntArgs d = s.arg2intargs(ce[3]);
int q0 = ce[4]->getInt();
int noOfTrans = 0;
for (int i=1; i<=q; i++) {
for (int j=1; j<=symbols; j++) {
if (d[(i-1)*symbols+(j-1)] > 0)
noOfTrans++;
}
}
Region re;
DFA::Transition* t = re.alloc<DFA::Transition>(noOfTrans+1);
noOfTrans = 0;
for (int i=1; i<=q; i++) {
for (int j=1; j<=symbols; j++) {
if (d[(i-1)*symbols+(j-1)] > 0) {
t[noOfTrans].i_state = i;
t[noOfTrans].symbol = j;
t[noOfTrans].o_state = d[(i-1)*symbols+(j-1)];
noOfTrans++;
}
}
}
t[noOfTrans].i_state = -1;
// Final states
AST::SetLit* sl = ce[5]->getSet();
int* f;
if (sl->interval) {
f = static_cast<int*>(heap.ralloc(sizeof(int)*(sl->max-sl->min+2)));
for (int i=sl->min; i<=sl->max; i++)
f[i-sl->min] = i;
f[sl->max-sl->min+1] = -1;
} else {
f = static_cast<int*>(heap.ralloc(sizeof(int)*(sl->s.size()+1)));
for (int j=sl->s.size(); j--; )
f[j] = sl->s[j];
f[sl->s.size()] = -1;
}
DFA dfa(q0,t,f);
free(f);
unshare(s, iv);
extensional(s, iv, s.getSharedDFA(dfa), s.ann2ipl(ann));
}
void
p_sort(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
IntVarArgs y = s.arg2intvarargs(ce[1]);
IntVarArgs xy(x.size()+y.size());
for (int i=x.size(); i--;)
xy[i] = x[i];
for (int i=y.size(); i--;)
xy[i+x.size()] = y[i];
unshare(s, xy);
for (int i=x.size(); i--;)
x[i] = xy[i];
for (int i=y.size(); i--;)
y[i] = xy[i+x.size()];
sorted(s, x, y, s.ann2ipl(ann));
}
void
p_inverse_offsets(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
unshare(s, x);
int xoff = ce[1]->getInt();
IntVarArgs y = s.arg2intvarargs(ce[2]);
unshare(s, y);
int yoff = ce[3]->getInt();
channel(s, x, xoff, y, yoff, s.ann2ipl(ann));
}
void
p_increasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
rel(s,x,IRT_LQ,s.ann2ipl(ann));
}
void
p_increasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BoolVarArgs x = s.arg2boolvarargs(ce[0]);
rel(s,x,IRT_LQ,s.ann2ipl(ann));
}
void
p_decreasing_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
rel(s,x,IRT_GQ,s.ann2ipl(ann));
}
void
p_decreasing_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BoolVarArgs x = s.arg2boolvarargs(ce[0]);
rel(s,x,IRT_GQ,s.ann2ipl(ann));
}
void
p_table_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
IntArgs tuples = s.arg2intargs(ce[1]);
TupleSet ts = s.arg2tupleset(tuples,x.size());
extensional(s,x,ts,s.ann2ipl(ann));
}
void
p_table_int_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
IntArgs tuples = s.arg2intargs(ce[1]);
TupleSet ts = s.arg2tupleset(tuples,x.size());
extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_EQV),s.ann2ipl(ann));
}
void
p_table_int_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
IntArgs tuples = s.arg2intargs(ce[1]);
TupleSet ts = s.arg2tupleset(tuples,x.size());
extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_IMP),s.ann2ipl(ann));
}
void
p_table_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BoolVarArgs x = s.arg2boolvarargs(ce[0]);
IntArgs tuples = s.arg2boolargs(ce[1]);
TupleSet ts = s.arg2tupleset(tuples,x.size());
extensional(s,x,ts,s.ann2ipl(ann));
}
void
p_table_bool_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BoolVarArgs x = s.arg2boolvarargs(ce[0]);
IntArgs tuples = s.arg2boolargs(ce[1]);
TupleSet ts = s.arg2tupleset(tuples,x.size());
extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_EQV),s.ann2ipl(ann));
}
void
p_table_bool_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BoolVarArgs x = s.arg2boolvarargs(ce[0]);
IntArgs tuples = s.arg2boolargs(ce[1]);
TupleSet ts = s.arg2tupleset(tuples,x.size());
extensional(s,x,ts,Reify(s.arg2BoolVar(ce[2]),RM_IMP),s.ann2ipl(ann));
}
void p_cumulative_opt(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
IntVarArgs start = s.arg2intvarargs(ce[0]);
IntArgs duration = s.arg2intargs(ce[1]);
IntArgs height = s.arg2intargs(ce[2]);
BoolVarArgs opt = s.arg2boolvarargs(ce[3]);
int bound = ce[4]->getInt();
unshare(s,start);
cumulative(s,bound,start,duration,height,opt,s.ann2ipl(ann));
}
void p_cumulatives(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
IntVarArgs start = s.arg2intvarargs(ce[0]);
IntVarArgs duration = s.arg2intvarargs(ce[1]);
IntVarArgs height = s.arg2intvarargs(ce[2]);
int n = start.size();
IntVar bound = s.arg2IntVar(ce[3]);
if (n==0)
return;
if (n == 1) {
rel(s, height[0] <= bound);
return;
}
int minHeight = std::min(height[0].min(),height[1].min());
int minHeight2 = std::max(height[0].min(),height[1].min());
for (int i=2; i<n; i++) {
if (height[i].min() < minHeight) {
minHeight2 = minHeight;
minHeight = height[i].min();
} else if (height[i].min() < minHeight2) {
minHeight2 = height[i].min();
}
}
bool disjunctive =
(minHeight > bound.max()/2) ||
(minHeight2 > bound.max()/2 && minHeight+minHeight2>bound.max());
if (disjunctive) {
rel(s, bound >= max(height));
// Unary
if (duration.assigned()) {
IntArgs durationI(n);
for (int i=n; i--;)
durationI[i] = duration[i].val();
unshare(s,start);
unary(s,start,durationI);
} else {
IntVarArgs end(n);
for (int i=n; i--;)
end[i] = expr(s,start[i]+duration[i]);
unshare(s,start);
unary(s,start,duration,end);
}
} else if (height.assigned()) {
IntArgs heightI(n);
for (int i=n; i--;)
heightI[i] = height[i].val();
if (duration.assigned()) {
IntArgs durationI(n);
for (int i=n; i--;)
durationI[i] = duration[i].val();
cumulative(s, bound, start, durationI, heightI);
} else {
IntVarArgs end(n);
for (int i = n; i--; )
end[i] = expr(s,start[i]+duration[i]);
cumulative(s, bound, start, duration, end, heightI);
}
} else if (bound.assigned()) {
IntArgs machine = IntArgs::create(n,0,0);
IntArgs limit({bound.val()});
IntVarArgs end(n);
for (int i=n; i--;)
end[i] = expr(s,start[i]+duration[i]);
cumulatives(s, machine, start, duration, end, height, limit, true,
s.ann2ipl(ann));
} else {
int min = Gecode::Int::Limits::max;
int max = Gecode::Int::Limits::min;
IntVarArgs end(start.size());
for (int i = start.size(); i--; ) {
min = std::min(min, start[i].min());
max = std::max(max, start[i].max() + duration[i].max());
end[i] = expr(s, start[i] + duration[i]);
}
for (int time = min; time < max; ++time) {
IntVarArgs x(start.size());
for (int i = start.size(); i--; ) {
IntVar overlaps = channel(s, expr(s, (start[i] <= time) &&
(time < end[i])));
x[i] = expr(s, overlaps * height[i]);
}
linear(s, x, IRT_LQ, bound);
}
}
}
void p_among_seq_int(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
IntSet S = s.arg2intset(ce[1]);
int q = ce[2]->getInt();
int l = ce[3]->getInt();
int u = ce[4]->getInt();
unshare(s, x);
sequence(s, x, S, q, l, u, s.ann2ipl(ann));
}
void p_among_seq_bool(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
BoolVarArgs x = s.arg2boolvarargs(ce[0]);
bool val = ce[1]->getBool();
int q = ce[2]->getInt();
int l = ce[3]->getInt();
int u = ce[4]->getInt();
IntSet S(val, val);
unshare(s, x);
sequence(s, x, S, q, l, u, s.ann2ipl(ann));
}
void p_schedule_unary(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
IntArgs p = s.arg2intargs(ce[1]);
unshare(s,x);
unary(s, x, p);
}
void p_schedule_unary_optional(FlatZincSpace& s, const ConExpr& ce,
AST::Node*) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
IntArgs p = s.arg2intargs(ce[1]);
BoolVarArgs m = s.arg2boolvarargs(ce[2]);
unshare(s,x);
unary(s, x, p, m);
}
void p_circuit(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
int off = ce[0]->getInt();
IntVarArgs xv = s.arg2intvarargs(ce[1]);
unshare(s,xv);
circuit(s,off,xv,s.ann2ipl(ann));
}
void p_circuit_cost_array(FlatZincSpace& s, const ConExpr& ce,
AST::Node *ann) {
IntArgs c = s.arg2intargs(ce[0]);
IntVarArgs xv = s.arg2intvarargs(ce[1]);
IntVarArgs yv = s.arg2intvarargs(ce[2]);
IntVar z = s.arg2IntVar(ce[3]);
unshare(s,xv);
circuit(s,c,xv,yv,z,s.ann2ipl(ann));
}
void p_circuit_cost(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
IntArgs c = s.arg2intargs(ce[0]);
IntVarArgs xv = s.arg2intvarargs(ce[1]);
IntVar z = s.arg2IntVar(ce[2]);
unshare(s,xv);
circuit(s,c,xv,z,s.ann2ipl(ann));
}
void p_nooverlap(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
IntVarArgs x0 = s.arg2intvarargs(ce[0]);
IntVarArgs w = s.arg2intvarargs(ce[1]);
IntVarArgs y0 = s.arg2intvarargs(ce[2]);
IntVarArgs h = s.arg2intvarargs(ce[3]);
if (w.assigned() && h.assigned()) {
IntArgs iw(w.size());
for (int i=w.size(); i--;)
iw[i] = w[i].val();
IntArgs ih(h.size());
for (int i=h.size(); i--;)
ih[i] = h[i].val();
nooverlap(s,x0,iw,y0,ih,s.ann2ipl(ann));
int miny = y0[0].min();
int maxy = y0[0].max();
int maxdy = ih[0];
for (int i=1; i<y0.size(); i++) {
miny = std::min(miny,y0[i].min());
maxy = std::max(maxy,y0[i].max());
maxdy = std::max(maxdy,ih[i]);
}
int minx = x0[0].min();
int maxx = x0[0].max();
int maxdx = iw[0];
for (int i=1; i<x0.size(); i++) {
minx = std::min(minx,x0[i].min());
maxx = std::max(maxx,x0[i].max());
maxdx = std::max(maxdx,iw[i]);
}
if (miny > Int::Limits::min && maxy < Int::Limits::max) {
cumulative(s,maxdy+maxy-miny,x0,iw,ih);
cumulative(s,maxdx+maxx-minx,y0,ih,iw);
}
} else {
IntVarArgs x1(x0.size()), y1(y0.size());
for (int i=x0.size(); i--; )
x1[i] = expr(s, x0[i] + w[i]);
for (int i=y0.size(); i--; )
y1[i] = expr(s, y0[i] + h[i]);
nooverlap(s,x0,w,x1,y0,h,y1,s.ann2ipl(ann));
}
}
void p_precede(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
int p_s = ce[1]->getInt();
int p_t = ce[2]->getInt();
precede(s,x,p_s,p_t,s.ann2ipl(ann));
}
void p_nvalue(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[1]);
if (ce[0]->isIntVar()) {
IntVar y = s.arg2IntVar(ce[0]);
nvalues(s,x,IRT_EQ,y,s.ann2ipl(ann));
} else {
nvalues(s,x,IRT_EQ,ce[0]->getInt(),s.ann2ipl(ann));
}
}
void p_among(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[1]);
IntSet v = s.arg2intset(ce[2]);
if (ce[0]->isIntVar()) {
IntVar n = s.arg2IntVar(ce[0]);
unshare(s, x);
count(s,x,v,IRT_EQ,n,s.ann2ipl(ann));
} else {
unshare(s, x);
count(s,x,v,IRT_EQ,ce[0]->getInt(),s.ann2ipl(ann));
}
}
void p_member_int(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
IntVar y = s.arg2IntVar(ce[1]);
member(s,x,y,s.ann2ipl(ann));
}
void p_member_int_reif(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
IntVarArgs x = s.arg2intvarargs(ce[0]);
IntVar y = s.arg2IntVar(ce[1]);
BoolVar b = s.arg2BoolVar(ce[2]);
member(s,x,y,b,s.ann2ipl(ann));
}
void p_member_bool(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
BoolVarArgs x = s.arg2boolvarargs(ce[0]);
BoolVar y = s.arg2BoolVar(ce[1]);
member(s,x,y,s.ann2ipl(ann));
}
void p_member_bool_reif(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
BoolVarArgs x = s.arg2boolvarargs(ce[0]);
BoolVar y = s.arg2BoolVar(ce[1]);
member(s,x,y,s.arg2BoolVar(ce[2]),s.ann2ipl(ann));
}
class IntPoster {
public:
IntPoster(void) {
registry().add("all_different_int", &p_distinct);
registry().add("all_different_offset", &p_distinctOffset);
registry().add("all_equal_int", &p_all_equal);
registry().add("int_eq", &p_int_eq);
registry().add("int_ne", &p_int_ne);
registry().add("int_ge", &p_int_ge);
registry().add("int_gt", &p_int_gt);
registry().add("int_le", &p_int_le);
registry().add("int_lt", &p_int_lt);
registry().add("int_eq_reif", &p_int_eq_reif);
registry().add("int_ne_reif", &p_int_ne_reif);
registry().add("int_ge_reif", &p_int_ge_reif);
registry().add("int_gt_reif", &p_int_gt_reif);
registry().add("int_le_reif", &p_int_le_reif);
registry().add("int_lt_reif", &p_int_lt_reif);
registry().add("int_eq_imp", &p_int_eq_imp);
registry().add("int_ne_imp", &p_int_ne_imp);
registry().add("int_ge_imp", &p_int_ge_imp);
registry().add("int_gt_imp", &p_int_gt_imp);
registry().add("int_le_imp", &p_int_le_imp);
registry().add("int_lt_imp", &p_int_lt_imp);
registry().add("int_lin_eq", &p_int_lin_eq);
registry().add("int_lin_eq_reif", &p_int_lin_eq_reif);
registry().add("int_lin_eq_imp", &p_int_lin_eq_imp);
registry().add("int_lin_ne", &p_int_lin_ne);
registry().add("int_lin_ne_reif", &p_int_lin_ne_reif);
registry().add("int_lin_ne_imp", &p_int_lin_ne_imp);
registry().add("int_lin_le", &p_int_lin_le);
registry().add("int_lin_le_reif", &p_int_lin_le_reif);
registry().add("int_lin_le_imp", &p_int_lin_le_imp);
registry().add("int_lin_lt", &p_int_lin_lt);
registry().add("int_lin_lt_reif", &p_int_lin_lt_reif);
registry().add("int_lin_lt_imp", &p_int_lin_lt_imp);
registry().add("int_lin_ge", &p_int_lin_ge);
registry().add("int_lin_ge_reif", &p_int_lin_ge_reif);
registry().add("int_lin_ge_imp", &p_int_lin_ge_imp);
registry().add("int_lin_gt", &p_int_lin_gt);
registry().add("int_lin_gt_reif", &p_int_lin_gt_reif);
registry().add("int_lin_gt_imp", &p_int_lin_gt_imp);
registry().add("int_plus", &p_int_plus);
registry().add("int_minus", &p_int_minus);
registry().add("int_times", &p_int_times);
registry().add("gecode_int_pow", &p_int_pow);
registry().add("int_div", &p_int_div);
registry().add("int_mod", &p_int_mod);
registry().add("int_min", &p_int_min);
registry().add("int_max", &p_int_max);
registry().add("int_abs", &p_abs);
registry().add("int_negate", &p_int_negate);
registry().add("bool_eq", &p_bool_eq);
registry().add("bool_eq_reif", &p_bool_eq_reif);
registry().add("bool_eq_imp", &p_bool_eq_imp);
registry().add("bool_ne", &p_bool_ne);
registry().add("bool_ne_reif", &p_bool_ne_reif);
registry().add("bool_ne_imp", &p_bool_ne_imp);
registry().add("bool_ge", &p_bool_ge);
registry().add("bool_ge_reif", &p_bool_ge_reif);
registry().add("bool_ge_imp", &p_bool_ge_imp);
registry().add("bool_le", &p_bool_le);
registry().add("bool_le_reif", &p_bool_le_reif);
registry().add("bool_le_imp", &p_bool_le_imp);
registry().add("bool_gt", &p_bool_gt);
registry().add("bool_gt_reif", &p_bool_gt_reif);
registry().add("bool_gt_imp", &p_bool_gt_imp);
registry().add("bool_lt", &p_bool_lt);
registry().add("bool_lt_reif", &p_bool_lt_reif);
registry().add("bool_lt_imp", &p_bool_lt_imp);
registry().add("bool_or", &p_bool_or);
registry().add("bool_or_imp", &p_bool_or_imp);
registry().add("bool_and", &p_bool_and);
registry().add("bool_and_imp", &p_bool_and_imp);
registry().add("bool_xor", &p_bool_xor);
registry().add("bool_xor_imp", &p_bool_xor_imp);
registry().add("array_bool_and", &p_array_bool_and);
registry().add("array_bool_and_imp", &p_array_bool_and_imp);
registry().add("array_bool_or", &p_array_bool_or);
registry().add("array_bool_or_imp", &p_array_bool_or_imp);
registry().add("array_bool_xor", &p_array_bool_xor);
registry().add("array_bool_xor_imp", &p_array_bool_xor_imp);
registry().add("bool_clause", &p_array_bool_clause);
registry().add("bool_clause_reif", &p_array_bool_clause_reif);
registry().add("bool_clause_imp", &p_array_bool_clause_imp);
registry().add("bool_left_imp", &p_bool_l_imp);
registry().add("bool_right_imp", &p_bool_r_imp);
registry().add("bool_not", &p_bool_not);
registry().add("array_int_element", &p_array_int_element);
registry().add("array_var_int_element", &p_array_int_element);
registry().add("array_bool_element", &p_array_bool_element);
registry().add("array_var_bool_element", &p_array_bool_element);
registry().add("bool2int", &p_bool2int);
registry().add("int_in", &p_int_in);
registry().add("int_in_reif", &p_int_in_reif);
registry().add("int_in_imp", &p_int_in_imp);
#ifndef GECODE_HAS_SET_VARS
registry().add("set_in", &p_int_in);
registry().add("set_in_reif", &p_int_in_reif);
registry().add("set_in_imp", &p_int_in_imp);
#endif
registry().add("array_int_lt", &p_array_int_lt);
registry().add("array_int_lq", &p_array_int_lq);
registry().add("array_bool_lt", &p_array_bool_lt);
registry().add("array_bool_lq", &p_array_bool_lq);
registry().add("count", &p_count);
registry().add("count_reif", &p_count_reif);
registry().add("count_imp", &p_count_imp);
registry().add("at_least_int", &p_at_least);
registry().add("at_most_int", &p_at_most);
registry().add("gecode_bin_packing_load", &p_bin_packing_load);
registry().add("gecode_global_cardinality", &p_global_cardinality);
registry().add("gecode_global_cardinality_closed",
&p_global_cardinality_closed);
registry().add("global_cardinality_low_up",
&p_global_cardinality_low_up);
registry().add("global_cardinality_low_up_closed",
&p_global_cardinality_low_up_closed);
registry().add("array_int_minimum", &p_minimum);
registry().add("array_int_maximum", &p_maximum);
registry().add("gecode_minimum_arg_int_offset", &p_minimum_arg);
registry().add("gecode_maximum_arg_int_offset", &p_maximum_arg);
registry().add("gecode_minimum_arg_bool_offset", &p_minimum_arg_bool);
registry().add("gecode_maximum_arg_bool_offset", &p_maximum_arg_bool);
registry().add("array_int_maximum", &p_maximum);
registry().add("gecode_regular", &p_regular);
registry().add("sort", &p_sort);
registry().add("inverse_offsets", &p_inverse_offsets);
registry().add("increasing_int", &p_increasing_int);
registry().add("increasing_bool", &p_increasing_bool);
registry().add("decreasing_int", &p_decreasing_int);
registry().add("decreasing_bool", &p_decreasing_bool);
registry().add("gecode_table_int", &p_table_int);
registry().add("gecode_table_int_reif", &p_table_int_reif);
registry().add("gecode_table_int_imp", &p_table_int_imp);
registry().add("gecode_table_bool", &p_table_bool);
registry().add("gecode_table_bool_reif", &p_table_bool_reif);
registry().add("gecode_table_bool_imp", &p_table_bool_imp);
registry().add("cumulatives", &p_cumulatives);
registry().add("gecode_among_seq_int", &p_among_seq_int);
registry().add("gecode_among_seq_bool", &p_among_seq_bool);
registry().add("bool_lin_eq", &p_bool_lin_eq);
registry().add("bool_lin_ne", &p_bool_lin_ne);
registry().add("bool_lin_le", &p_bool_lin_le);
registry().add("bool_lin_lt", &p_bool_lin_lt);
registry().add("bool_lin_ge", &p_bool_lin_ge);
registry().add("bool_lin_gt", &p_bool_lin_gt);
registry().add("bool_lin_eq_reif", &p_bool_lin_eq_reif);
registry().add("bool_lin_eq_imp", &p_bool_lin_eq_imp);
registry().add("bool_lin_ne_reif", &p_bool_lin_ne_reif);
registry().add("bool_lin_ne_imp", &p_bool_lin_ne_imp);
registry().add("bool_lin_le_reif", &p_bool_lin_le_reif);
registry().add("bool_lin_le_imp", &p_bool_lin_le_imp);
registry().add("bool_lin_lt_reif", &p_bool_lin_lt_reif);
registry().add("bool_lin_lt_imp", &p_bool_lin_lt_imp);
registry().add("bool_lin_ge_reif", &p_bool_lin_ge_reif);
registry().add("bool_lin_ge_imp", &p_bool_lin_ge_imp);
registry().add("bool_lin_gt_reif", &p_bool_lin_gt_reif);
registry().add("bool_lin_gt_imp", &p_bool_lin_gt_imp);
registry().add("gecode_schedule_unary", &p_schedule_unary);
registry().add("gecode_schedule_unary_optional", &p_schedule_unary_optional);
registry().add("gecode_schedule_cumulative_optional", &p_cumulative_opt);
registry().add("gecode_circuit", &p_circuit);
registry().add("gecode_circuit_cost_array", &p_circuit_cost_array);
registry().add("gecode_circuit_cost", &p_circuit_cost);
registry().add("gecode_nooverlap", &p_nooverlap);
registry().add("gecode_precede", &p_precede);
registry().add("nvalue",&p_nvalue);
registry().add("among",&p_among);
registry().add("member_int",&p_member_int);
registry().add("gecode_member_int_reif",&p_member_int_reif);
registry().add("member_bool",&p_member_bool);
registry().add("gecode_member_bool_reif",&p_member_bool_reif);
}
};
IntPoster __int_poster;
#ifdef GECODE_HAS_SET_VARS
void p_set_OP(FlatZincSpace& s, SetOpType op,
const ConExpr& ce, AST::Node *) {
rel(s, s.arg2SetVar(ce[0]), op, s.arg2SetVar(ce[1]),
SRT_EQ, s.arg2SetVar(ce[2]));
}
void p_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
p_set_OP(s, SOT_UNION, ce, ann);
}
void p_set_intersect(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
p_set_OP(s, SOT_INTER, ce, ann);
}
void p_set_diff(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
p_set_OP(s, SOT_MINUS, ce, ann);
}
void p_set_symdiff(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
SetVar x = s.arg2SetVar(ce[0]);
SetVar y = s.arg2SetVar(ce[1]);
SetVarLubRanges xub(x);
IntSet xubs(xub);
SetVar x_y(s,IntSet::empty,xubs);
rel(s, x, SOT_MINUS, y, SRT_EQ, x_y);
SetVarLubRanges yub(y);
IntSet yubs(yub);
SetVar y_x(s,IntSet::empty,yubs);
rel(s, y, SOT_MINUS, x, SRT_EQ, y_x);
rel(s, x_y, SOT_UNION, y_x, SRT_EQ, s.arg2SetVar(ce[2]));
}
void p_array_set_OP(FlatZincSpace& s, SetOpType op,
const ConExpr& ce, AST::Node *) {
SetVarArgs xs = s.arg2setvarargs(ce[0]);
rel(s, op, xs, s.arg2SetVar(ce[1]));
}
void p_array_set_union(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
p_array_set_OP(s, SOT_UNION, ce, ann);
}
void p_array_set_partition(FlatZincSpace& s, const ConExpr& ce, AST::Node *ann) {
p_array_set_OP(s, SOT_DUNION, ce, ann);
}
void p_set_rel(FlatZincSpace& s, SetRelType srt, const ConExpr& ce) {
rel(s, s.arg2SetVar(ce[0]), srt, s.arg2SetVar(ce[1]));
}
void p_set_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
p_set_rel(s, SRT_EQ, ce);
}
void p_set_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
p_set_rel(s, SRT_NQ, ce);
}
void p_set_subset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
p_set_rel(s, SRT_SUB, ce);
}
void p_set_superset(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
p_set_rel(s, SRT_SUP, ce);
}
void p_set_le(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
p_set_rel(s, SRT_LQ, ce);
}
void p_set_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
p_set_rel(s, SRT_LE, ce);
}
void p_set_card(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
if (!ce[1]->isIntVar()) {
cardinality(s, s.arg2SetVar(ce[0]), ce[1]->getInt(),
ce[1]->getInt());
} else {
cardinality(s, s.arg2SetVar(ce[0]), s.arg2IntVar(ce[1]));
}
}
void p_set_in(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
if (!ce[1]->isSetVar()) {
IntSet d = s.arg2intset(ce[1]);
if (ce[0]->isBoolVar()) {
IntSetRanges dr(d);
Iter::Ranges::Singleton sr(0,1);
Iter::Ranges::Inter<IntSetRanges,Iter::Ranges::Singleton> i(dr,sr);
IntSet d01(i);
if (d01.size() == 0) {
s.fail();
} else {
rel(s, s.arg2BoolVar(ce[0]), IRT_GQ, d01.min());
rel(s, s.arg2BoolVar(ce[0]), IRT_LQ, d01.max());
}
} else {
dom(s, s.arg2IntVar(ce[0]), d);
}
} else {
if (!ce[0]->isIntVar()) {
dom(s, s.arg2SetVar(ce[1]), SRT_SUP, ce[0]->getInt());
} else {
rel(s, s.arg2SetVar(ce[1]), SRT_SUP, s.arg2IntVar(ce[0]));
}
}
}
void p_set_rel_reif(FlatZincSpace& s, SetRelType srt, const ConExpr& ce) {
rel(s, s.arg2SetVar(ce[0]), srt, s.arg2SetVar(ce[1]),
s.arg2BoolVar(ce[2]));
}
void p_set_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
p_set_rel_reif(s,SRT_EQ,ce);
}
void p_set_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
p_set_rel_reif(s,SRT_LQ,ce);
}
void p_set_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
p_set_rel_reif(s,SRT_LE,ce);
}
void p_set_ne_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
p_set_rel_reif(s,SRT_NQ,ce);
}
void p_set_subset_reif(FlatZincSpace& s, const ConExpr& ce,
AST::Node *) {
p_set_rel_reif(s,SRT_SUB,ce);
}
void p_set_superset_reif(FlatZincSpace& s, const ConExpr& ce,
AST::Node *) {
p_set_rel_reif(s,SRT_SUP,ce);
}
void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann, ReifyMode rm) {
if (!ce[1]->isSetVar()) {
if (rm==RM_EQV) {
p_int_in_reif(s,ce,ann);
} else {
assert(rm==RM_IMP);
p_int_in_imp(s,ce,ann);
}
} else {
if (!ce[0]->isIntVar()) {
dom(s, s.arg2SetVar(ce[1]), SRT_SUP, ce[0]->getInt(),
Reify(s.arg2BoolVar(ce[2]),rm));
} else {
rel(s, s.arg2SetVar(ce[1]), SRT_SUP, s.arg2IntVar(ce[0]),
Reify(s.arg2BoolVar(ce[2]),rm));
}
}
}
void p_set_in_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_set_in_reif(s,ce,ann,RM_EQV);
}
void p_set_in_imp(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_set_in_reif(s,ce,ann,RM_IMP);
}
void p_set_disjoint(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
rel(s, s.arg2SetVar(ce[0]), SRT_DISJ, s.arg2SetVar(ce[1]));
}
void p_link_set_to_booleans(FlatZincSpace& s, const ConExpr& ce,
AST::Node *) {
SetVar x = s.arg2SetVar(ce[0]);
int idx = ce[2]->getInt();
assert(idx >= 0);
rel(s, x || IntSet(Set::Limits::min,idx-1));
BoolVarArgs y = s.arg2boolvarargs(ce[1],idx);
unshare(s, y);
channel(s, y, x);
}
void p_array_set_element(FlatZincSpace& s, const ConExpr& ce,
AST::Node*) {
bool isConstant = true;
AST::Array* a = ce[1]->getArray();
for (int i=a->a.size(); i--;) {
if (a->a[i]->isSetVar()) {
isConstant = false;
break;
}
}
IntVar selector = s.arg2IntVar(ce[0]);
rel(s, selector > 0);
if (isConstant) {
IntSetArgs sv = s.arg2intsetargs(ce[1],1);
element(s, sv, selector, s.arg2SetVar(ce[2]));
} else {
SetVarArgs sv = s.arg2setvarargs(ce[1], 1);
element(s, sv, selector, s.arg2SetVar(ce[2]));
}
}
void p_array_set_element_op(FlatZincSpace& s, const ConExpr& ce,
AST::Node*, SetOpType op,
const IntSet& universe =
IntSet(Set::Limits::min,Set::Limits::max)) {
bool isConstant = true;
AST::Array* a = ce[1]->getArray();
for (int i=a->a.size(); i--;) {
if (a->a[i]->isSetVar()) {
isConstant = false;
break;
}
}
SetVar selector = s.arg2SetVar(ce[0]);
dom(s, selector, SRT_DISJ, 0);
if (isConstant) {
IntSetArgs sv = s.arg2intsetargs(ce[1], 1);
element(s, op, sv, selector, s.arg2SetVar(ce[2]), universe);
} else {
SetVarArgs sv = s.arg2setvarargs(ce[1], 1);
element(s, op, sv, selector, s.arg2SetVar(ce[2]), universe);
}
}
void p_array_set_element_union(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
p_array_set_element_op(s, ce, ann, SOT_UNION);
}
void p_array_set_element_intersect(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
p_array_set_element_op(s, ce, ann, SOT_INTER);
}
void p_array_set_element_intersect_in(FlatZincSpace& s,
const ConExpr& ce,
AST::Node* ann) {
IntSet d = s.arg2intset(ce[3]);
p_array_set_element_op(s, ce, ann, SOT_INTER, d);
}
void p_array_set_element_partition(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
p_array_set_element_op(s, ce, ann, SOT_DUNION);
}
void p_set_convex(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
convex(s, s.arg2SetVar(ce[0]));
}
void p_array_set_seq(FlatZincSpace& s, const ConExpr& ce, AST::Node *) {
SetVarArgs sv = s.arg2setvarargs(ce[0]);
sequence(s, sv);
}
void p_array_set_seq_union(FlatZincSpace& s, const ConExpr& ce,
AST::Node *) {
SetVarArgs sv = s.arg2setvarargs(ce[0]);
sequence(s, sv, s.arg2SetVar(ce[1]));
}
void p_int_set_channel(FlatZincSpace& s, const ConExpr& ce,
AST::Node *) {
int xoff=ce[1]->getInt();
assert(xoff >= 0);
int yoff=ce[3]->getInt();
assert(yoff >= 0);
IntVarArgs xv = s.arg2intvarargs(ce[0], xoff);
SetVarArgs yv = s.arg2setvarargs(ce[2], yoff, 1, IntSet(0, xoff-1));
IntSet xd(yoff,yv.size()-1);
for (int i=xoff; i<xv.size(); i++) {
dom(s, xv[i], xd);
}
IntSet yd(xoff,xv.size()-1);
for (int i=yoff; i<yv.size(); i++) {
dom(s, yv[i], SRT_SUB, yd);
}
channel(s,xv,yv);
}
void p_range(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
int xoff=ce[1]->getInt();
assert(xoff >= 0);
IntVarArgs xv = s.arg2intvarargs(ce[0],xoff);
element(s, SOT_UNION, xv, s.arg2SetVar(ce[2]), s.arg2SetVar(ce[3]));
}
void p_weights(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
IntArgs e = s.arg2intargs(ce[0]);
IntArgs w = s.arg2intargs(ce[1]);
SetVar x = s.arg2SetVar(ce[2]);
IntVar y = s.arg2IntVar(ce[3]);
weights(s,e,w,x,y);
}
void p_inverse_set(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
int xoff = ce[2]->getInt();
int yoff = ce[3]->getInt();
SetVarArgs x = s.arg2setvarargs(ce[0],xoff);
SetVarArgs y = s.arg2setvarargs(ce[1],yoff);
channel(s, x, y);
}
void p_precede_set(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
SetVarArgs x = s.arg2setvarargs(ce[0]);
int p_s = ce[1]->getInt();
int p_t = ce[2]->getInt();
precede(s,x,p_s,p_t);
}
class SetPoster {
public:
SetPoster(void) {
registry().add("set_eq", &p_set_eq);
registry().add("set_le", &p_set_le);
registry().add("set_lt", &p_set_lt);
registry().add("equal", &p_set_eq);
registry().add("set_ne", &p_set_ne);
registry().add("set_union", &p_set_union);
registry().add("array_set_element", &p_array_set_element);
registry().add("array_var_set_element", &p_array_set_element);
registry().add("set_intersect", &p_set_intersect);
registry().add("set_diff", &p_set_diff);
registry().add("set_symdiff", &p_set_symdiff);
registry().add("set_subset", &p_set_subset);
registry().add("set_superset", &p_set_superset);
registry().add("set_card", &p_set_card);
registry().add("set_in", &p_set_in);
registry().add("set_eq_reif", &p_set_eq_reif);
registry().add("set_le_reif", &p_set_le_reif);
registry().add("set_lt_reif", &p_set_lt_reif);
registry().add("equal_reif", &p_set_eq_reif);
registry().add("set_ne_reif", &p_set_ne_reif);
registry().add("set_subset_reif", &p_set_subset_reif);
registry().add("set_superset_reif", &p_set_superset_reif);
registry().add("set_in_reif", &p_set_in_reif);
registry().add("set_in_imp", &p_set_in_imp);
registry().add("disjoint", &p_set_disjoint);
registry().add("gecode_link_set_to_booleans",
&p_link_set_to_booleans);
registry().add("array_set_union", &p_array_set_union);
registry().add("array_set_partition", &p_array_set_partition);
registry().add("set_convex", &p_set_convex);
registry().add("array_set_seq", &p_array_set_seq);
registry().add("array_set_seq_union", &p_array_set_seq_union);
registry().add("gecode_array_set_element_union",
&p_array_set_element_union);
registry().add("gecode_array_set_element_intersect",
&p_array_set_element_intersect);
registry().add("gecode_array_set_element_intersect_in",
&p_array_set_element_intersect_in);
registry().add("gecode_array_set_element_partition",
&p_array_set_element_partition);
registry().add("gecode_int_set_channel",
&p_int_set_channel);
registry().add("gecode_range",
&p_range);
registry().add("gecode_set_weights",
&p_weights);
registry().add("gecode_inverse_set", &p_inverse_set);
registry().add("gecode_precede_set", &p_precede_set);
}
};
SetPoster __set_poster;
#endif
#ifdef GECODE_HAS_FLOAT_VARS
void p_int2float(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
IntVar x0 = s.arg2IntVar(ce[0]);
FloatVar x1 = s.arg2FloatVar(ce[1]);
channel(s, x0, x1);
}
void p_float_lin_cmp(FlatZincSpace& s, FloatRelType frt,
const ConExpr& ce, AST::Node*) {
FloatValArgs fa = s.arg2floatargs(ce[0]);
FloatVarArgs fv = s.arg2floatvarargs(ce[1]);
linear(s, fa, fv, frt, ce[2]->getFloat());
}
void p_float_lin_cmp_reif(FlatZincSpace& s, FloatRelType frt,
const ConExpr& ce, AST::Node*) {
FloatValArgs fa = s.arg2floatargs(ce[0]);
FloatVarArgs fv = s.arg2floatvarargs(ce[1]);
linear(s, fa, fv, frt, ce[2]->getFloat(), s.arg2BoolVar(ce[3]));
}
void p_float_lin_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_float_lin_cmp(s,FRT_EQ,ce,ann);
}
void p_float_lin_eq_reif(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
p_float_lin_cmp_reif(s,FRT_EQ,ce,ann);
}
void p_float_lin_le(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_float_lin_cmp(s,FRT_LQ,ce,ann);
}
void p_float_lin_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node* ann) {
p_float_lin_cmp(s,FRT_LE,ce,ann);
}
void p_float_lin_le_reif(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
p_float_lin_cmp_reif(s,FRT_LQ,ce,ann);
}
void p_float_lin_lt_reif(FlatZincSpace& s, const ConExpr& ce,
AST::Node* ann) {
p_float_lin_cmp_reif(s,FRT_LE,ce,ann);
}
void p_float_times(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
FloatVar z = s.arg2FloatVar(ce[2]);
mult(s,x,y,z);
}
void p_float_div(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
FloatVar z = s.arg2FloatVar(ce[2]);
div(s,x,y,z);
}
void p_float_plus(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
FloatVar z = s.arg2FloatVar(ce[2]);
rel(s,x+y==z);
}
void p_float_sqrt(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
sqrt(s,x,y);
}
void p_float_abs(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
abs(s,x,y);
}
void p_float_eq(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
rel(s,x,FRT_EQ,y);
}
void p_float_eq_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
BoolVar b = s.arg2BoolVar(ce[2]);
rel(s,x,FRT_EQ,y,b);
}
void p_float_le(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
rel(s,x,FRT_LQ,y);
}
void p_float_le_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
BoolVar b = s.arg2BoolVar(ce[2]);
rel(s,x,FRT_LQ,y,b);
}
void p_float_max(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
FloatVar z = s.arg2FloatVar(ce[2]);
max(s,x,y,z);
}
void p_float_min(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
FloatVar z = s.arg2FloatVar(ce[2]);
min(s,x,y,z);
}
void p_float_lt(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
rel(s, x, FRT_LQ, y);
rel(s, x, FRT_EQ, y, BoolVar(s,0,0));
}
void p_float_lt_reif(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
BoolVar b = s.arg2BoolVar(ce[2]);
BoolVar b0(s,0,1);
BoolVar b1(s,0,1);
rel(s, b == (b0 && !b1));
rel(s, x, FRT_LQ, y, b0);
rel(s, x, FRT_EQ, y, b1);
}
void p_float_ne(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
rel(s, x, FRT_EQ, y, BoolVar(s,0,0));
}
#ifdef GECODE_HAS_MPFR
#define P_FLOAT_OP(Op) \
void p_float_ ## Op (FlatZincSpace& s, const ConExpr& ce, AST::Node*) {\
FloatVar x = s.arg2FloatVar(ce[0]);\
FloatVar y = s.arg2FloatVar(ce[1]);\
Op(s,x,y);\
}
P_FLOAT_OP(acos)
P_FLOAT_OP(asin)
P_FLOAT_OP(atan)
P_FLOAT_OP(cos)
P_FLOAT_OP(exp)
P_FLOAT_OP(sin)
P_FLOAT_OP(tan)
// P_FLOAT_OP(sinh)
// P_FLOAT_OP(tanh)
// P_FLOAT_OP(cosh)
#undef P_FLOAT_OP
void p_float_ln(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
log(s,x,y);
}
void p_float_log10(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
log(s,10.0,x,y);
}
void p_float_log2(FlatZincSpace& s, const ConExpr& ce, AST::Node*) {
FloatVar x = s.arg2FloatVar(ce[0]);
FloatVar y = s.arg2FloatVar(ce[1]);
log(s,2.0,x,y);
}
#endif
class FloatPoster {
public:
FloatPoster(void) {
registry().add("int2float",&p_int2float);
registry().add("float_abs",&p_float_abs);
registry().add("float_sqrt",&p_float_sqrt);
registry().add("float_eq",&p_float_eq);
registry().add("float_eq_reif",&p_float_eq_reif);
registry().add("float_le",&p_float_le);
registry().add("float_le_reif",&p_float_le_reif);
registry().add("float_lt",&p_float_lt);
registry().add("float_lt_reif",&p_float_lt_reif);
registry().add("float_ne",&p_float_ne);
registry().add("float_times",&p_float_times);
registry().add("float_div",&p_float_div);
registry().add("float_plus",&p_float_plus);
registry().add("float_max",&p_float_max);
registry().add("float_min",&p_float_min);
registry().add("float_lin_eq",&p_float_lin_eq);
registry().add("float_lin_eq_reif",&p_float_lin_eq_reif);
registry().add("float_lin_le",&p_float_lin_le);
registry().add("float_lin_lt",&p_float_lin_lt);
registry().add("float_lin_le_reif",&p_float_lin_le_reif);
registry().add("float_lin_lt_reif",&p_float_lin_lt_reif);
#ifdef GECODE_HAS_MPFR
registry().add("float_acos",&p_float_acos);
registry().add("float_asin",&p_float_asin);
registry().add("float_atan",&p_float_atan);
registry().add("float_cos",&p_float_cos);
// registry().add("float_cosh",&p_float_cosh);
registry().add("float_exp",&p_float_exp);
registry().add("float_ln",&p_float_ln);
registry().add("float_log10",&p_float_log10);
registry().add("float_log2",&p_float_log2);
registry().add("float_sin",&p_float_sin);
// registry().add("float_sinh",&p_float_sinh);
registry().add("float_tan",&p_float_tan);
// registry().add("float_tanh",&p_float_tanh);
#endif
}
} __float_poster;
#endif
}
}}
// STATISTICS: flatzinc-any
Gecode::ArgArrayBase::end
iterator end(void)
Return an iterator past the end of the array.
Definition array.hpp:1639
Gecode::ArgArrayBase::size
int size(void) const
Return size of array (number of elements).
Definition array.hpp:1607
Gecode::FlatZinc::AST::Array
Array node
Definition ast.hh:231
Gecode::FlatZinc::AST::Node
A node in a FlatZinc abstract syntax tree.
Definition ast.hh:67
Gecode::FlatZinc::AST::Node::getSet
SetLit * getSet(void)
Cast this node to a set literal node.
Definition ast.hh:458
Gecode::FlatZinc::AST::SetLit
Set literal node
Definition ast.hh:171
Gecode::FlatZinc::ConExpr
Abstract representation of a constraint.
Definition conexpr.hh:43
Gecode::FlatZinc::ConExpr::id
std::string id
Identifier for the constraint.
Definition conexpr.hh:46
Gecode::FlatZinc::ConExpr::ann
AST::Array * ann
Constraint annotations.
Definition conexpr.hh:50
Gecode::FlatZinc::Error
Exception class for FlatZinc errors
Definition flatzinc.hh:665
Gecode::FlatZinc::FlatZincSpace
A space that can be initialized with a FlatZinc model.
Definition flatzinc.hh:428
Gecode::FlatZinc::FlatZincSpace::arg2intvarargs
IntVarArgs arg2intvarargs(AST::Node *arg, int offset=0)
Convert arg to IntVarArgs.
Definition flatzinc.cpp:2227
Gecode::FlatZinc::FlatZincSpace::ann2ipl
IntPropLevel ann2ipl(AST::Node *ann)
Convert ann to integer propagation level.
Definition flatzinc.cpp:2386
Gecode::FlatZinc::Registry
Map from constraint identifier to constraint posting functions.
Definition registry.hh:44
Gecode::FlatZinc::Registry::poster
void(* poster)(FlatZincSpace &, const ConExpr &, AST::Node *)
Type of constraint posting function.
Definition registry.hh:47
Gecode::FlatZinc::Registry::add
void add(const std::string &id, poster p)
Add posting function p with identifier id.
Definition registry.cpp:69
Gecode::FlatZinc::Registry::post
void post(FlatZincSpace &s, const ConExpr &ce)
Post constraint specified by ce.
Definition registry.cpp:59
Gecode::FloatVal::size
FloatNum size(void) const
Return size of float value (distance between maximum and minimum).
Definition val.hpp:78
Gecode::Heap::ralloc
void * ralloc(size_t s)
Allocate s bytes from heap.
Definition heap.hpp:357
Gecode::IntArgs
Passing integer arguments.
Definition int.hh:628
Gecode::IntArgs::create
static IntArgs create(int n, int start, int inc=1)
Allocate array with n elements such that for all .
Definition array.hpp:76
Gecode::IntSet::empty
static const IntSet empty
Empty set.
Definition int.hh:283
Gecode::IntVarArgs
Passing integer variables.
Definition int.hh:656
flatzinc.hh
float.hh
int.hh
set.hh
Gecode::heap
Heap heap
The single global heap.
Definition heap.cpp:44
Gecode::Int::OffsetView::offset
int offset(void) const
Integer-precision integer scale view.
Definition view.hpp:642
Gecode::linear
void linear(Home home, const FloatVarArgs &x, FloatRelType frt, FloatVal c)
Post propagator for .
Definition linear.cpp:41
Gecode::rel
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVar x1)
Post propagator for .
Definition rel.cpp:68
Gecode::FloatRelType
FloatRelType
Relation types for floats.
Definition float.hh:1068
Gecode::FRT_EQ
@ FRT_EQ
Equality ( ).
Definition float.hh:1069
Gecode::FRT_LE
@ FRT_LE
Less ( ).
Definition float.hh:1072
Gecode::FRT_LQ
@ FRT_LQ
Less or equal ( ).
Definition float.hh:1071
Gecode::binpacking
void binpacking(Home home, const IntVarArgs &l, const IntVarArgs &b, const IntArgs &s, IntPropLevel ipl=IPL_DEF)
Post propagator for bin packing.
Definition bin-packing.cpp:41
Gecode::extensional
void extensional(Home home, const IntVarArgs &x, DFA d, IntPropLevel ipl=IPL_DEF)
Post domain consistent propagator for extensional constraint described by a DFA.
Definition extensional-regular.cpp:39
Gecode::nooverlap
void nooverlap(Home home, const IntVarArgs &x, const IntArgs &w, const IntVarArgs &y, const IntArgs &h, IntPropLevel ipl=IPL_DEF)
Post propagator for rectangle packing.
Definition no-overlap.cpp:51
Gecode::precede
void precede(Home home, const IntVarArgs &x, int s, int t, IntPropLevel=IPL_DEF)
Post propagator that s precedes t in x.
Definition precede.cpp:43
Gecode::clause
void clause(Home home, BoolOpType o, const BoolVarArgs &x, const BoolVarArgs &y, BoolVar z, IntPropLevel ipl=IPL_DEF)
Post domain consistent propagator for Boolean clause with positive variables x and negative variables...
Definition bool.cpp:955
Gecode::IntRelType
IntRelType
Relation types for integers.
Definition int.hh:925
Gecode::ReifyMode
ReifyMode
Mode for reification.
Definition int.hh:848
Gecode::IntPropLevel
IntPropLevel
Propagation levels for integer propagators.
Definition int.hh:974
Gecode::IRT_EQ
@ IRT_EQ
Equality ( ).
Definition int.hh:926
Gecode::IRT_NQ
@ IRT_NQ
Disequality ( ).
Definition int.hh:927
Gecode::IRT_GQ
@ IRT_GQ
Greater or equal ( ).
Definition int.hh:930
Gecode::IRT_LE
@ IRT_LE
Less ( ).
Definition int.hh:929
Gecode::IRT_GR
@ IRT_GR
Greater ( ).
Definition int.hh:931
Gecode::IRT_LQ
@ IRT_LQ
Less or equal ( ).
Definition int.hh:928
Gecode::RM_IMP
@ RM_IMP
Implication for reification.
Definition int.hh:862
Gecode::RM_EQV
@ RM_EQV
Equivalence for reification (default).
Definition int.hh:855
Gecode::BOT_OR
@ BOT_OR
Disjunction.
Definition int.hh:952
Gecode::BOT_IMP
@ BOT_IMP
Implication.
Definition int.hh:953
Gecode::BOT_XOR
@ BOT_XOR
Exclusive or.
Definition int.hh:955
Gecode::BOT_AND
@ BOT_AND
Conjunction.
Definition int.hh:951
Gecode::IPL_DOM
@ IPL_DOM
Domain propagation Options: basic versus advanced propagation.
Definition int.hh:979
Gecode::IPL_DEF
@ IPL_DEF
Simple propagation levels.
Definition int.hh:976
Gecode::IPL_BND
@ IPL_BND
Bounds propagation.
Definition int.hh:978
Gecode::weights
void weights(Home home, IntSharedArray elements, IntSharedArray weights, SetVar x, IntVar y)
Post propagator for .
Definition int.cpp:292
Gecode::SetOpType
SetOpType
Common operations for sets.
Definition set.hh:660
Gecode::SetRelType
SetRelType
Common relation types for sets.
Definition set.hh:643
Gecode::SOT_MINUS
@ SOT_MINUS
Difference.
Definition set.hh:664
Gecode::SOT_DUNION
@ SOT_DUNION
Disjoint union.
Definition set.hh:662
Gecode::SOT_UNION
@ SOT_UNION
Union.
Definition set.hh:661
Gecode::SOT_INTER
@ SOT_INTER
Intersection
Definition set.hh:663
Gecode::SRT_LQ
@ SRT_LQ
Less or equal ( ).
Definition set.hh:650
Gecode::SRT_NQ
@ SRT_NQ
Disequality ( ).
Definition set.hh:645
Gecode::SRT_LE
@ SRT_LE
Less ( ).
Definition set.hh:651
Gecode::SRT_EQ
@ SRT_EQ
Equality ( ).
Definition set.hh:644
Gecode::SRT_SUP
@ SRT_SUP
Superset ( ).
Definition set.hh:647
Gecode::SRT_DISJ
@ SRT_DISJ
Disjoint ( ).
Definition set.hh:648
Gecode::SRT_SUB
@ SRT_SUB
Subset ( ).
Definition set.hh:646
kernel.hh
minimodel.hh
Gecode::FlatZinc
Interpreter for the FlatZinc language.
Gecode::FlatZinc::registry
Registry & registry(void)
Return global registry object.
Definition registry.cpp:53
Gecode::Int::Limits::min
const int min
Smallest allowed integer value.
Definition int.hh:118
Gecode::Int::Limits::max
const int max
Largest allowed integer value.
Definition int.hh:116
Gecode::Set::Limits::min
const int min
Smallest allowed integer in integer set.
Definition set.hh:99
Gecode::Set::Limits::max
const int max
Largest allowed integer in integer set.
Definition set.hh:97
Gecode
Gecode toplevel namespace
Gecode::IntSetArgs
ArgArray< IntSet > IntSetArgs
Passing set arguments.
Definition int.hh:619
Gecode::sin
void sin(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition trigonometric.cpp:52
Gecode::count
void count(Home home, const IntVarArgs &x, int n, IntRelType irt, int m, IntPropLevel ipl=IPL_DEF)
Post propagator for .
Definition count.cpp:40
Gecode::channel
void channel(Home home, FloatVar x0, IntVar x1)
Post propagator for channeling a float and an integer variable .
Definition channel.cpp:41
Gecode::mod
void mod(Home home, IntVar x0, IntVar x1, IntVar x2, IntPropLevel ipl=IPL_DEF)
Post propagator for .
Definition arithmetic.cpp:360
Gecode::sequence
void sequence(Home home, const IntVarArgs &x, const IntSet &s, int q, int l, int u, IntPropLevel ipl=IPL_DEF)
Post propagator for .
Definition sequence.cpp:47
Gecode::IntSharedArray
SharedArray< int > IntSharedArray
Arrays of integers that can be shared among several element constraints.
Definition int.hh:1477
Gecode::expr
IntVar expr(Home home, const LinIntExpr &e, const IntPropLevels &ipls=IntPropLevels::def)
Post linear expression and return its value.
Definition int-expr.cpp:915
Gecode::sorted
void sorted(Home home, const IntVarArgs &x, const IntVarArgs &y, IntPropLevel ipl=IPL_DEF)
Post propagator that y is x sorted in increasing order.
Definition sorted.cpp:58
Gecode::distinct
void distinct(Home home, const IntVarArgs &x, IntPropLevel ipl=IPL_DEF)
Post propagator for for all .
Definition distinct.cpp:46
Gecode::cos
void cos(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition trigonometric.cpp:66
Gecode::min
void min(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition arithmetic.cpp:67
Gecode::neg
IntRelType neg(IntRelType irt)
Return negated relation type of irt.
Definition irt.hpp:52
Gecode::dom
void dom(Home home, FloatVar x, FloatVal n)
Propagates .
Definition dom.cpp:40
Gecode::abs
void abs(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition arithmetic.cpp:41
Gecode::div
void div(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition arithmetic.cpp:127
Gecode::element
void element(Home home, IntSharedArray n, IntVar x0, IntVar x1, IntPropLevel ipl=IPL_DEF)
Post domain consistent propagator for .
Definition element.cpp:39
Gecode::argmax
void argmax(Home home, const IntVarArgs &x, IntVar y, bool tiebreak=true, IntPropLevel ipl=IPL_DEF)
Post propagator for .
Definition arithmetic.cpp:110
Gecode::mult
void mult(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition arithmetic.cpp:88
Gecode::swap
IntRelType swap(IntRelType irt)
Return swapped relation type of irt.
Definition irt.hpp:37
Gecode::sqrt
void sqrt(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition arithmetic.cpp:102
Gecode::acos
void acos(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition trigonometric.cpp:59
Gecode::cumulative
void cumulative(Home home, int c, const TaskTypeArgs &t, const IntVarArgs &flex, const IntArgs &fix, const IntArgs &u, IntPropLevel ipl=IPL_DEF)
Post propagators for scheduling tasks on cumulative resources.
Definition cumulative.cpp:354
Gecode::cumulatives
void cumulatives(Home home, const IntVarArgs &m, const IntVarArgs &s, const IntVarArgs &p, const IntVarArgs &e, const IntVarArgs &u, const IntArgs &c, bool at_most, IntPropLevel ipl=IPL_DEF)
Post propagators for the cumulatives constraint.
Definition cumulatives.cpp:110
Gecode::log
void log(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition transcendental.cpp:53
Gecode::convex
void convex(Home home, SetVar x)
Post propagator that propagates that x is convex.
Definition convex.cpp:41
Gecode::exp
void exp(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition transcendental.cpp:45
Gecode::atan
void atan(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition trigonometric.cpp:73
Gecode::unshare
void unshare(Home home, IntVarArgs &x, IntPropLevel ipl=IPL_DEF)
Replace multiple variable occurences in x by fresh variables.
Definition unshare.cpp:136
Gecode::max
void max(Home home, FloatVar x0, FloatVar x1, FloatVar x2)
Post propagator for .
Definition arithmetic.cpp:49
Gecode::argmin
void argmin(Home home, const IntVarArgs &x, IntVar y, bool tiebreak=true, IntPropLevel ipl=IPL_DEF)
Post propagator for .
Definition arithmetic.cpp:163
Gecode::nvalues
void nvalues(Home home, const IntVarArgs &x, IntRelType irt, int y, IntPropLevel ipl=IPL_DEF)
Post propagator for .
Definition nvalues.cpp:40
Gecode::unary
void unary(Home home, const IntVarArgs &s, const IntArgs &p, IntPropLevel ipl=IPL_DEF)
Post propagators for scheduling tasks on unary resources.
Definition unary.cpp:44
Gecode::asin
void asin(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition trigonometric.cpp:45
Gecode::member
void member(Home home, const IntVarArgs &x, IntVar y, IntPropLevel ipl=IPL_DEF)
Post domain consistent propagator for .
Definition member.cpp:39
Gecode::pow
void pow(Home home, FloatVar x0, int n, FloatVar x1)
Post propagator for for $n\geq 0$.
Definition arithmetic.cpp:109
Gecode::cardinality
LinIntExpr cardinality(const SetExpr &)
Cardinality of set expression.
Definition set-expr.cpp:817
Gecode::circuit
void circuit(Home home, const IntVarArgs &x, IntPropLevel ipl=IPL_DEF)
Post propagator such that x forms a circuit.
Definition circuit.cpp:73
Gecode::tan
void tan(Home home, FloatVar x0, FloatVar x1)
Post propagator for .
Definition trigonometric.cpp:80
Test::Float::Arithmetic::c
Gecode::FloatVal c(-8, 8)
Test::Float::Arithmetic::b
Gecode::FloatVal b(9, 12)
Test::Float::Arithmetic::a
Gecode::FloatVal a(-8, 5)
Test::Int::Basic::b2
Basic b2(i)
Test::Int::Basic::b1
Basic b1(3)
Test::Int::Basic::i
Gecode::IntArgs i({1, 2, 3, 4})
Test::Int::Distinct::d
Gecode::IntSet d(v, 7)
Test::Int::Distinct::v
const int v[7]
Definition distinct.cpp:259
Test::Int::Unshare::f
Failed f
Definition unshare.cpp:124
Test::opt
Options opt
The options.
Definition test.cpp:97
BOOL_ARRAY_OP
#define BOOL_ARRAY_OP(op)
Definition registry.cpp:573
BOOL_OP
#define BOOL_OP(op)
Definition registry.cpp:564
P_FLOAT_OP
#define P_FLOAT_OP(Op)
Definition registry.cpp:2126
registry.hh