int-post.cpp
Go to the documentation of this file.
/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
/*
* Main authors:
* Christian Schulte <schulte@gecode.org>
*
* Copyright:
* Christian Schulte, 2002
*
* 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 <algorithm>
#include <gecode/int/rel.hh>
#include <gecode/int/linear.hh>
#include <gecode/int/div.hh>
namespace Gecode { namespace Int { namespace Linear {
forceinline void
eliminate(Term<IntView>* t, int &n, long long int& d) {
for (int i=n; i--; )
if (t[i].x.assigned()) {
long long int ax = t[i].a * static_cast<long long int>(t[i].x.val());
if (Limits::overflow_sub(d,ax))
throw OutOfLimits("Int::linear");
d=d-ax; t[i]=t[--n];
}
}
forceinline void
rewrite(IntRelType &irt, long long int &d,
Term<IntView>* &t_p, int &n_p,
Term<IntView>* &t_n, int &n_n) {
switch (irt) {
case IRT_EQ: case IRT_NQ: case IRT_LQ:
break;
case IRT_LE:
d--; irt = IRT_LQ;
break;
case IRT_GR:
d++;
/* fall through */
case IRT_GQ:
irt = IRT_LQ;
std::swap(n_p,n_n); std::swap(t_p,t_n); d = -d;
break;
default:
throw UnknownRelation("Int::linear");
}
}
forceinline bool
precision(Term<IntView>* t_p, int n_p,
Term<IntView>* t_n, int n_n,
long long int d) {
long long int sl = 0;
long long int su = 0;
for (int i=0; i<n_p; i++) {
long long int axmin =
t_p[i].a * static_cast<long long int>(t_p[i].x.min());
if (Limits::overflow_add(sl,axmin))
throw OutOfLimits("Int::linear");
sl = sl + axmin;
long long int axmax =
t_p[i].a * static_cast<long long int>(t_p[i].x.max());
if (Limits::overflow_add(sl,axmax))
throw OutOfLimits("Int::linear");
su = su + axmax;
}
for (int i=0; i<n_n; i++) {
long long int axmax =
t_n[i].a * static_cast<long long int>(t_n[i].x.max());
if (Limits::overflow_sub(sl,axmax))
throw OutOfLimits("Int::linear");
sl = sl - axmax;
long long int axmin =
t_n[i].a * static_cast<long long int>(t_n[i].x.min());
if (Limits::overflow_sub(su,axmin))
throw OutOfLimits("Int::linear");
su = su - axmin;
}
bool is_ip = (sl >= Limits::min) && (su <= Limits::max);
if (Limits::overflow_sub(sl,d))
throw OutOfLimits("Int::linear");
sl = sl - d;
if (Limits::overflow_sub(su,d))
throw OutOfLimits("Int::linear");
su = su - d;
is_ip = is_ip && (sl >= Limits::min) && (su <= Limits::max);
for (int i=0; i<n_p; i++) {
long long int axmin =
t_p[i].a * static_cast<long long int>(t_p[i].x.min());
if (Limits::overflow_sub(sl,axmin))
throw OutOfLimits("Int::linear");
if (sl - axmin < Limits::min)
is_ip = false;
long long int axmax =
t_p[i].a * static_cast<long long int>(t_p[i].x.max());
if (Limits::overflow_sub(su,axmax))
throw OutOfLimits("Int::linear");
if (su - axmax > Limits::max)
is_ip = false;
}
for (int i=0; i<n_n; i++) {
long long int axmin =
t_n[i].a * static_cast<long long int>(t_n[i].x.min());
if (Limits::overflow_add(sl,axmin))
throw OutOfLimits("Int::linear");
if (sl + axmin < Limits::min)
is_ip = false;
long long int axmax =
t_n[i].a * static_cast<long long int>(t_n[i].x.max());
if (Limits::overflow_add(su,axmax))
throw OutOfLimits("Int::linear");
if (su + axmax > Limits::max)
is_ip = false;
}
return is_ip;
}
template<class Val, class View>
forceinline void
post_nary(Home home,
ViewArray<View>& x, ViewArray<View>& y, IntRelType irt, Val c) {
switch (irt) {
case IRT_EQ:
GECODE_ES_FAIL((Eq<Val,View,View >::post(home,x,y,c)));
break;
case IRT_NQ:
GECODE_ES_FAIL((Nq<Val,View,View >::post(home,x,y,c)));
break;
case IRT_LQ:
GECODE_ES_FAIL((Lq<Val,View,View >::post(home,x,y,c)));
break;
default: GECODE_NEVER;
}
}
#define GECODE_INT_PL_BIN(CLASS) \
switch (n_p) { \
case 2: \
GECODE_ES_FAIL((CLASS<int,IntView,IntView>::post \
(home,t_p[0].x,t_p[1].x,c))); \
break; \
case 1: \
GECODE_ES_FAIL((CLASS<int,IntView,MinusView>::post \
(home,t_p[0].x,MinusView(t_n[0].x),c))); \
break; \
case 0: \
GECODE_ES_FAIL((CLASS<int,MinusView,MinusView>::post \
(home,MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
break; \
default: GECODE_NEVER; \
}
#define GECODE_INT_PL_TER(CLASS) \
switch (n_p) { \
case 3: \
GECODE_ES_FAIL((CLASS<int,IntView,IntView,IntView>::post \
(home,t_p[0].x,t_p[1].x,t_p[2].x,c))); \
break; \
case 2: \
GECODE_ES_FAIL((CLASS<int,IntView,IntView,MinusView>::post \
(home,t_p[0].x,t_p[1].x, \
MinusView(t_n[0].x),c))); \
break; \
case 1: \
GECODE_ES_FAIL((CLASS<int,IntView,MinusView,MinusView>::post \
(home,t_p[0].x, \
MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
break; \
case 0: \
GECODE_ES_FAIL((CLASS<int,MinusView,MinusView,MinusView>::post \
(home,MinusView(t_n[0].x), \
MinusView(t_n[1].x),MinusView(t_n[2].x),c))); \
break; \
default: GECODE_NEVER; \
}
void
post(Home home, Term<IntView>* t, int n, IntRelType irt, int c,
IntPropLevel ipl) {
Limits::check(c,"Int::linear");
long long int d = c;
eliminate(t,n,d);
Term<IntView> *t_p, *t_n;
int n_p, n_n, gcd=1;
bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n,gcd);
rewrite(irt,d,t_p,n_p,t_n,n_n);
// Divide by gcd
if (gcd > 1) {
switch (irt) {
case IRT_EQ:
if ((d % gcd) != 0) {
home.fail();
return;
}
d /= gcd;
break;
case IRT_NQ:
if ((d % gcd) != 0)
return;
d /= gcd;
break;
case IRT_LQ:
d = floor_div_xp(d,static_cast<long long int>(gcd));
break;
default: GECODE_NEVER;
}
}
if (n == 0) {
switch (irt) {
case IRT_EQ: if (d != 0) home.fail(); break;
case IRT_NQ: if (d == 0) home.fail(); break;
case IRT_LQ: if (d < 0) home.fail(); break;
default: GECODE_NEVER;
}
return;
}
if (n == 1) {
if (n_p == 1) {
LLongScaleView y(t_p[0].a,t_p[0].x);
switch (irt) {
case IRT_EQ: GECODE_ME_FAIL(y.eq(home,d)); break;
case IRT_NQ: GECODE_ME_FAIL(y.nq(home,d)); break;
case IRT_LQ: GECODE_ME_FAIL(y.lq(home,d)); break;
default: GECODE_NEVER;
}
} else {
LLongScaleView y(t_n[0].a,t_n[0].x);
switch (irt) {
case IRT_EQ: GECODE_ME_FAIL(y.eq(home,-d)); break;
case IRT_NQ: GECODE_ME_FAIL(y.nq(home,-d)); break;
case IRT_LQ: GECODE_ME_FAIL(y.gq(home,-d)); break;
default: GECODE_NEVER;
}
}
return;
}
// Check this special case here, as there can be no overflow
if ((n == 2) && is_unit &&
((vbd(ipl) == IPL_DOM) || (vbd(ipl) == IPL_DEF)) &&
(irt == IRT_EQ) && (d == 0)) {
switch (n_p) {
case 2: {
IntView x(t_p[0].x);
MinusView y(t_p[1].x);
GECODE_ES_FAIL((Rel::EqDom<IntView,MinusView>::post(home,x,y)));
break;
}
case 1: {
IntView x(t_p[0].x);
IntView y(t_n[0].x);
GECODE_ES_FAIL((Rel::EqDom<IntView,IntView>::post(home,x,y)));
break;
}
case 0: {
IntView x(t_n[0].x);
MinusView y(t_n[1].x);
GECODE_ES_FAIL((Rel::EqDom<IntView,MinusView>::post(home,x,y)));
break;
}
default:
GECODE_NEVER;
}
return;
}
bool is_ip = precision(t_p,n_p,t_n,n_n,d);
if (is_unit && is_ip &&
(vbd(ipl) != IPL_DOM) && (vbd(ipl) != IPL_DEF)) {
// Unit coefficients with integer precision
c = static_cast<int>(d);
if (n == 2) {
switch (irt) {
case IRT_EQ: GECODE_INT_PL_BIN(EqBin); break;
case IRT_NQ: GECODE_INT_PL_BIN(NqBin); break;
case IRT_LQ: GECODE_INT_PL_BIN(LqBin); break;
default: GECODE_NEVER;
}
} else if (n == 3) {
switch (irt) {
case IRT_EQ: GECODE_INT_PL_TER(EqTer); break;
case IRT_NQ: GECODE_INT_PL_TER(NqTer); break;
case IRT_LQ: GECODE_INT_PL_TER(LqTer); break;
default: GECODE_NEVER;
}
} else {
ViewArray<IntView> x(home,n_p);
for (int i=0; i<n_p; i++)
x[i] = t_p[i].x;
ViewArray<IntView> y(home,n_n);
for (int i=0; i<n_n; i++)
y[i] = t_n[i].x;
post_nary<int,IntView>(home,x,y,irt,c);
}
} else if (is_ip) {
if ((n==2) && is_unit &&
((vbd(ipl) == IPL_DOM) || (vbd(ipl) == IPL_DEF)) &&
(irt == IRT_EQ)) {
// Binary domain-consistent equality
c = static_cast<int>(d);
assert(c != 0);
switch (n_p) {
case 2: {
MinusView x(t_p[0].x);
OffsetView y(t_p[1].x, -c);
GECODE_ES_FAIL((Rel::EqDom<MinusView,OffsetView>::post(home,x,y)));
break;
}
case 1: {
IntView x(t_p[0].x);
OffsetView y(t_n[0].x, c);
GECODE_ES_FAIL((Rel::EqDom<IntView,OffsetView>::post(home,x,y)));
break;
}
case 0: {
MinusView x(t_n[0].x);
OffsetView y(t_n[1].x, c);
GECODE_ES_FAIL((Rel::EqDom<MinusView,OffsetView>::post(home,x,y)));
break;
}
default:
GECODE_NEVER;
}
} else {
// Arbitrary coefficients with integer precision
c = static_cast<int>(d);
ViewArray<IntScaleView> x(home,n_p);
for (int i=0; i<n_p; i++)
x[i] = IntScaleView(t_p[i].a,t_p[i].x);
ViewArray<IntScaleView> y(home,n_n);
for (int i=0; i<n_n; i++)
y[i] = IntScaleView(t_n[i].a,t_n[i].x);
if ((vbd(ipl) == IPL_DOM) && (irt == IRT_EQ)) {
GECODE_ES_FAIL((DomEq<int,IntScaleView>::post(home,x,y,c)));
} else {
post_nary<int,IntScaleView>(home,x,y,irt,c);
}
}
} else {
// Arbitrary coefficients with long long precision
ViewArray<LLongScaleView> x(home,n_p);
for (int i=0; i<n_p; i++)
x[i] = LLongScaleView(t_p[i].a,t_p[i].x);
ViewArray<LLongScaleView> y(home,n_n);
for (int i=0; i<n_n; i++)
y[i] = LLongScaleView(t_n[i].a,t_n[i].x);
if ((vbd(ipl) == IPL_DOM) && (irt == IRT_EQ)) {
GECODE_ES_FAIL((DomEq<long long int,LLongScaleView>
::post(home,x,y,d)));
} else {
post_nary<long long int,LLongScaleView>(home,x,y,irt,d);
}
}
}
#undef GECODE_INT_PL_BIN
#undef GECODE_INT_PL_TER
template<class Val, class View>
forceinline void
post_nary(Home home,
ViewArray<View>& x, ViewArray<View>& y,
IntRelType irt, Val c, Reify r) {
switch (irt) {
case IRT_EQ:
switch (r.mode()) {
case RM_EQV:
GECODE_ES_FAIL((ReEq<Val,View,View,BoolView,RM_EQV>::
post(home,x,y,c,r.var())));
break;
case RM_IMP:
GECODE_ES_FAIL((ReEq<Val,View,View,BoolView,RM_IMP>::
post(home,x,y,c,r.var())));
break;
case RM_PMI:
GECODE_ES_FAIL((ReEq<Val,View,View,BoolView,RM_PMI>::
post(home,x,y,c,r.var())));
break;
default: GECODE_NEVER;
}
break;
case IRT_NQ:
{
NegBoolView n(r.var());
switch (r.mode()) {
case RM_EQV:
GECODE_ES_FAIL((ReEq<Val,View,View,NegBoolView,RM_EQV>::
post(home,x,y,c,n)));
break;
case RM_IMP:
GECODE_ES_FAIL((ReEq<Val,View,View,NegBoolView,RM_PMI>::
post(home,x,y,c,n)));
break;
case RM_PMI:
GECODE_ES_FAIL((ReEq<Val,View,View,NegBoolView,RM_IMP>::
post(home,x,y,c,n)));
break;
default: GECODE_NEVER;
}
}
break;
case IRT_LQ:
switch (r.mode()) {
case RM_EQV:
GECODE_ES_FAIL((ReLq<Val,View,View,RM_EQV>::
post(home,x,y,c,r.var())));
break;
case RM_IMP:
GECODE_ES_FAIL((ReLq<Val,View,View,RM_IMP>::
post(home,x,y,c,r.var())));
break;
case RM_PMI:
GECODE_ES_FAIL((ReLq<Val,View,View,RM_PMI>::
post(home,x,y,c,r.var())));
break;
default: GECODE_NEVER;
}
break;
default: GECODE_NEVER;
}
}
template<class CtrlView>
forceinline void
posteqint(Home home, IntView& x, int c, CtrlView b, ReifyMode rm,
IntPropLevel ipl) {
if ((vbd(ipl) == IPL_DOM) || (vbd(ipl) == IPL_DEF)) {
switch (rm) {
case RM_EQV:
GECODE_ES_FAIL((Rel::ReEqDomInt<IntView,CtrlView,RM_EQV>::
post(home,x,c,b)));
break;
case RM_IMP:
GECODE_ES_FAIL((Rel::ReEqDomInt<IntView,CtrlView,RM_IMP>::
post(home,x,c,b)));
break;
case RM_PMI:
GECODE_ES_FAIL((Rel::ReEqDomInt<IntView,CtrlView,RM_PMI>::
post(home,x,c,b)));
break;
default: GECODE_NEVER;
}
} else {
switch (rm) {
case RM_EQV:
GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,CtrlView,RM_EQV>::
post(home,x,c,b)));
break;
case RM_IMP:
GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,CtrlView,RM_IMP>::
post(home,x,c,b)));
break;
case RM_PMI:
GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,CtrlView,RM_PMI>::
post(home,x,c,b)));
break;
default: GECODE_NEVER;
}
}
}
void
post(Home home,
Term<IntView>* t, int n, IntRelType irt, int c, Reify r,
IntPropLevel ipl) {
Limits::check(c,"Int::linear");
long long int d = c;
eliminate(t,n,d);
Term<IntView> *t_p, *t_n;
int n_p, n_n, gcd=1;
bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n,gcd);
rewrite(irt,d,t_p,n_p,t_n,n_n);
// Divide by gcd
if (gcd > 1) {
switch (irt) {
case IRT_EQ:
if ((d % gcd) != 0) {
if (r.mode() != RM_PMI)
GECODE_ME_FAIL(BoolView(r.var()).zero(home));
return;
}
d /= gcd;
break;
case IRT_NQ:
if ((d % gcd) != 0) {
if (r.mode() != RM_IMP)
GECODE_ME_FAIL(BoolView(r.var()).one(home));
return;
}
d /= gcd;
break;
case IRT_LQ:
d = floor_div_xp(d,static_cast<long long int>(gcd));
break;
default: GECODE_NEVER;
}
}
if (n == 0) {
bool fail = false;
switch (irt) {
case IRT_EQ: fail = (d != 0); break;
case IRT_NQ: fail = (d == 0); break;
case IRT_LQ: fail = (0 > d); break;
default: GECODE_NEVER;
}
if (fail) {
if (r.mode() != RM_PMI)
GECODE_ME_FAIL(BoolView(r.var()).zero(home));
} else {
if (r.mode() != RM_IMP)
GECODE_ME_FAIL(BoolView(r.var()).one(home));
}
return;
}
bool is_ip = precision(t_p,n_p,t_n,n_n,d);
if (is_unit && is_ip) {
c = static_cast<int>(d);
if (n == 1) {
switch (irt) {
case IRT_EQ:
if (n_p == 1) {
posteqint<BoolView>(home,t_p[0].x,c,r.var(),r.mode(),ipl);
} else {
posteqint<BoolView>(home,t_p[0].x,-c,r.var(),r.mode(),ipl);
}
break;
case IRT_NQ:
{
NegBoolView nb(r.var());
ReifyMode rm = r.mode();
switch (rm) {
case RM_IMP: rm = RM_PMI; break;
case RM_PMI: rm = RM_IMP; break;
default: ;
}
if (n_p == 1) {
posteqint<NegBoolView>(home,t_p[0].x,c,nb,rm,ipl);
} else {
posteqint<NegBoolView>(home,t_p[0].x,-c,nb,rm,ipl);
}
}
break;
case IRT_LQ:
if (n_p == 1) {
switch (r.mode()) {
case RM_EQV:
GECODE_ES_FAIL((Rel::ReLqInt<IntView,BoolView,RM_EQV>::
post(home,t_p[0].x,c,r.var())));
break;
case RM_IMP:
GECODE_ES_FAIL((Rel::ReLqInt<IntView,BoolView,RM_IMP>::
post(home,t_p[0].x,c,r.var())));
break;
case RM_PMI:
GECODE_ES_FAIL((Rel::ReLqInt<IntView,BoolView,RM_PMI>::
post(home,t_p[0].x,c,r.var())));
break;
default: GECODE_NEVER;
}
} else {
NegBoolView nb(r.var());
switch (r.mode()) {
case RM_EQV:
GECODE_ES_FAIL((Rel::ReLqInt<IntView,NegBoolView,RM_EQV>::
post(home,t_n[0].x,-c-1,nb)));
break;
case RM_IMP:
GECODE_ES_FAIL((Rel::ReLqInt<IntView,NegBoolView,RM_PMI>::
post(home,t_n[0].x,-c-1,nb)));
break;
case RM_PMI:
GECODE_ES_FAIL((Rel::ReLqInt<IntView,NegBoolView,RM_IMP>::
post(home,t_n[0].x,-c-1,nb)));
break;
default: GECODE_NEVER;
}
}
break;
default: GECODE_NEVER;
}
} else if (n == 2) {
switch (irt) {
case IRT_EQ:
switch (n_p) {
case 2:
switch (r.mode()) {
case RM_EQV:
GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView,RM_EQV>::
post(home,t_p[0].x,t_p[1].x,c,r.var())));
break;
case RM_IMP:
GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView,RM_IMP>::
post(home,t_p[0].x,t_p[1].x,c,r.var())));
break;
case RM_PMI:
GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView,RM_PMI>::
post(home,t_p[0].x,t_p[1].x,c,r.var())));
break;
default: GECODE_NEVER;
}
break;
case 1:
switch (r.mode()) {
case RM_EQV:
GECODE_ES_FAIL((ReEqBin<int,IntView,MinusView,BoolView,RM_EQV>::
post(home,t_p[0].x,MinusView(t_n[0].x),c,
r.var())));
break;
case RM_IMP:
GECODE_ES_FAIL((ReEqBin<int,IntView,MinusView,BoolView,RM_IMP>::
post(home,t_p[0].x,MinusView(t_n[0].x),c,
r.var())));
break;
case RM_PMI:
GECODE_ES_FAIL((ReEqBin<int,IntView,MinusView,BoolView,RM_PMI>::
post(home,t_p[0].x,MinusView(t_n[0].x),c,
r.var())));
break;
default: GECODE_NEVER;
}
break;
case 0:
switch (r.mode()) {
case RM_EQV:
GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView,RM_EQV>::
post(home,t_n[0].x,t_n[1].x,-c,r.var())));
break;
case RM_IMP:
GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView,RM_IMP>::
post(home,t_n[0].x,t_n[1].x,-c,r.var())));
break;
case RM_PMI:
GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView,RM_PMI>::
post(home,t_n[0].x,t_n[1].x,-c,r.var())));
break;
default: GECODE_NEVER;
}
break;
default: GECODE_NEVER;
}
break;
case IRT_NQ:
{
NegBoolView nb(r.var());
switch (n_p) {
case 2:
switch (r.mode()) {
case RM_EQV:
GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,NegBoolView,RM_EQV>::
post(home,t_p[0].x,t_p[1].x,c,nb)));
break;
case RM_IMP:
GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,NegBoolView,RM_PMI>::
post(home,t_p[0].x,t_p[1].x,c,nb)));
break;
case RM_PMI:
GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,NegBoolView,RM_IMP>::
post(home,t_p[0].x,t_p[1].x,c,nb)));
break;
default: GECODE_NEVER;
}
break;
case 1:
switch (r.mode()) {
case RM_EQV:
GECODE_ES_FAIL((ReEqBin<int,IntView,MinusView,NegBoolView,RM_EQV>::
post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
break;
case RM_IMP:
GECODE_ES_FAIL((ReEqBin<int,IntView,MinusView,NegBoolView,RM_PMI>::
post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
break;
case RM_PMI:
GECODE_ES_FAIL((ReEqBin<int,IntView,MinusView,NegBoolView,RM_IMP>::
post(home,t_p[0].x,MinusView(t_n[0].x),c,nb)));
break;
default: GECODE_NEVER;
}
break;
case 0:
switch (r.mode()) {
case RM_EQV:
GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,NegBoolView,RM_EQV>::
post(home,t_p[0].x,t_p[1].x,-c,nb)));
break;
case RM_IMP:
GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,NegBoolView,RM_PMI>::
post(home,t_p[0].x,t_p[1].x,-c,nb)));
break;
case RM_PMI:
GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,NegBoolView,RM_IMP>::
post(home,t_p[0].x,t_p[1].x,-c,nb)));
break;
default: GECODE_NEVER;
}
break;
default: GECODE_NEVER;
}
}
break;
case IRT_LQ:
switch (n_p) {
case 2:
switch (r.mode()) {
case RM_EQV:
GECODE_ES_FAIL((ReLqBin<int,IntView,IntView,RM_EQV>::
post(home,t_p[0].x,t_p[1].x,c,r.var())));
break;
case RM_IMP:
GECODE_ES_FAIL((ReLqBin<int,IntView,IntView,RM_IMP>::
post(home,t_p[0].x,t_p[1].x,c,r.var())));
break;
case RM_PMI:
GECODE_ES_FAIL((ReLqBin<int,IntView,IntView,RM_PMI>::
post(home,t_p[0].x,t_p[1].x,c,r.var())));
break;
default: GECODE_NEVER;
}
break;
case 1:
switch (r.mode()) {
case RM_EQV:
GECODE_ES_FAIL((ReLqBin<int,IntView,MinusView,RM_EQV>::
post(home,t_p[0].x,MinusView(t_n[0].x),c,
r.var())));
break;
case RM_IMP:
GECODE_ES_FAIL((ReLqBin<int,IntView,MinusView,RM_IMP>::
post(home,t_p[0].x,MinusView(t_n[0].x),c,
r.var())));
break;
case RM_PMI:
GECODE_ES_FAIL((ReLqBin<int,IntView,MinusView,RM_PMI>::
post(home,t_p[0].x,MinusView(t_n[0].x),c,
r.var())));
break;
default: GECODE_NEVER;
}
break;
case 0:
switch (r.mode()) {
case RM_EQV:
GECODE_ES_FAIL((ReLqBin<int,MinusView,MinusView,RM_EQV>::
post(home,MinusView(t_n[0].x),
MinusView(t_n[1].x),c,r.var())));
break;
case RM_IMP:
GECODE_ES_FAIL((ReLqBin<int,MinusView,MinusView,RM_IMP>::
post(home,MinusView(t_n[0].x),
MinusView(t_n[1].x),c,r.var())));
break;
case RM_PMI:
GECODE_ES_FAIL((ReLqBin<int,MinusView,MinusView,RM_PMI>::
post(home,MinusView(t_n[0].x),
MinusView(t_n[1].x),c,r.var())));
break;
default: GECODE_NEVER;
}
break;
default: GECODE_NEVER;
}
break;
default: GECODE_NEVER;
}
} else {
ViewArray<IntView> x(home,n_p);
for (int i=0; i<n_p; i++)
x[i] = t_p[i].x;
ViewArray<IntView> y(home,n_n);
for (int i=0; i<n_n; i++)
y[i] = t_n[i].x;
post_nary<int,IntView>(home,x,y,irt,c,r);
}
} else if (is_ip) {
// Arbitrary coefficients with integer precision
c = static_cast<int>(d);
ViewArray<IntScaleView> x(home,n_p);
for (int i=0; i<n_p; i++)
x[i] = IntScaleView(t_p[i].a,t_p[i].x);
ViewArray<IntScaleView> y(home,n_n);
for (int i=0; i<n_n; i++)
y[i] = IntScaleView(t_n[i].a,t_n[i].x);
post_nary<int,IntScaleView>(home,x,y,irt,c,r);
} else {
// Arbitrary coefficients with long long precision
ViewArray<LLongScaleView> x(home,n_p);
for (int i=0; i<n_p; i++)
x[i] = LLongScaleView(t_p[i].a,t_p[i].x);
ViewArray<LLongScaleView> y(home,n_n);
for (int i=0; i<n_n; i++)
y[i] = LLongScaleView(t_n[i].a,t_n[i].x);
post_nary<long long int,LLongScaleView>(home,x,y,irt,d,r);
}
}
}}}
// STATISTICS: int-post
Gecode::Home
Home class for posting propagators
Definition core.hpp:856
Gecode::Home::fail
void fail(void)
Mark space as failed.
Definition core.hpp:4039
Gecode::Int::BoolView
Boolean view for Boolean variables.
Definition view.hpp:1380
Gecode::Int::BoolView::zero
bool zero(void) const
Test whether view is assigned to be zero.
Definition bool.hpp:220
Gecode::Int::BoolView::one
bool one(void) const
Test whether view is assigned to be one.
Definition bool.hpp:224
Gecode::Int::IntView
Integer view for integer variables.
Definition view.hpp:129
Gecode::Int::Linear::DomEq
Propagator for domain consistent n-ary linear equality
Definition linear.hh:609
Gecode::Int::Linear::DomEq::post
static ExecStatus post(Home home, ViewArray< View > &x, ViewArray< View > &y, Val c)
Post propagator for .
Definition int-dom.hpp:362
Gecode::Int::Linear::EqBin
Propagator for bounds consistent binary linear equality
Definition linear.hh:134
Gecode::Int::Linear::EqTer
Propagator for bounds consistent ternary linear equality
Definition linear.hh:384
Gecode::Int::Linear::Eq::post
static ExecStatus post(Home home, ViewArray< P > &x, ViewArray< N > &y, Val c)
Post propagator for .
Definition int-nary.hpp:280
Gecode::Int::Linear::LqBin
Propagator for bounds consistent binary linear less or equal
Definition linear.hh:237
Gecode::Int::Linear::LqTer
Propagator for bounds consistent ternary linear less or equal
Definition linear.hh:454
Gecode::Int::Linear::Lq::post
static ExecStatus post(Home home, ViewArray< P > &x, ViewArray< N > &y, Val c)
Post propagator for .
Definition int-nary.hpp:631
Gecode::Int::Linear::NqBin
Propagator for bounds consistent binary linear disequality
Definition linear.hh:201
Gecode::Int::Linear::NqTer
Propagator for bounds consistent ternary linear disquality
Definition linear.hh:419
Gecode::Int::Linear::Nq::post
static ExecStatus post(Home home, ViewArray< P > &x, ViewArray< N > &y, Val c)
Post propagator for .
Definition int-nary.hpp:482
Gecode::Int::Linear::ReEqBin
Propagator for reified bounds consistent binary linear equality
Definition linear.hh:168
Gecode::Int::Linear::ReEq
Propagator for reified bounds consistent n-ary linear equality
Definition linear.hh:649
Gecode::Int::Linear::ReLqBin
Propagator for reified bounds consistent binary linear less or equal
Definition linear.hh:305
Gecode::Int::Linear::ReLq
Propagator for reified bounds consistent n-ary linear less or equal
Definition linear.hh:749
Gecode::Int::Linear::Term
Class for describing linear term .
Definition linear.hh:1336
Gecode::Int::Linear::Term::x
View x
View.
Definition linear.hh:1341
Gecode::Int::Linear::Term::a
int a
Coefficient.
Definition linear.hh:1339
Gecode::Int::MinusView
Minus integer view.
Definition view.hpp:282
Gecode::Int::NegBoolView
Negated Boolean view.
Definition view.hpp:1574
Gecode::Int::OffsetView
Offset integer view.
Definition view.hpp:443
Gecode::Int::OutOfLimits
Exception: Value out of limits
Definition exception.hpp:44
Gecode::Int::Rel::EqDom::post
static ExecStatus post(Home home, View0 x0, View1 x1)
Post domain consistent propagator .
Definition eq.hpp:176
Gecode::Int::Rel::ReEqBndInt
Reified bounds consistent equality with integer propagator.
Definition rel.hh:425
Gecode::Int::Rel::ReEqDomInt
Reified domain consistent equality with integer propagator.
Definition rel.hh:398
Gecode::Int::Rel::ReLqInt
Reified less or equal with integer propagator.
Definition rel.hh:575
Gecode::Int::UnknownRelation
Exception: Unknown relation passed as argument
Definition exception.hpp:87
Gecode::Reify
Reification specification.
Definition int.hh:876
Gecode::Val
Gecode::ValSelCommitBase::val
virtual Val val(const Space &home, View x, int i)=0
Return value of view x at position i.
Gecode::ViewArray
View arrays.
Definition array.hpp:253
div.hh
Gecode::Int::Linear::post
void post(Home home, Term< IntView > *t, int n, IntRelType irt, int c, IntPropLevel=IPL_DEF)
Post propagator for linear constraint over integers.
Definition int-post.cpp:219
GECODE_ES_FAIL
#define GECODE_ES_FAIL(es)
Check whether execution status es is failed, and fail space home.
Definition macros.hpp:103
GECODE_ME_FAIL
#define GECODE_ME_FAIL(me)
Check whether modification event me is failed, and fail space home.
Definition macros.hpp:77
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_PMI
@ RM_PMI
Inverse implication for reification.
Definition int.hh:869
Gecode::RM_EQV
@ RM_EQV
Equivalence for reification (default).
Definition int.hh:855
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_INT_PL_TER
#define GECODE_INT_PL_TER(CLASS)
Macro for posting ternary special cases for linear constraints.
Definition int-post.cpp:194
GECODE_INT_PL_BIN
#define GECODE_INT_PL_BIN(CLASS)
Macro for posting binary special cases for linear constraints.
Definition int-post.cpp:176
linear.hh
rel.hh
Gecode::Int::Limits::overflow_add
bool overflow_add(int n, int m)
Check whether adding n and m would overflow.
Definition limits.hpp:79
Gecode::Int::Limits::check
void check(int n, const char *l)
Check whether n is in range, otherwise throw out of limits with information l.
Definition limits.hpp:46
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::Int::Limits::overflow_sub
bool overflow_sub(int n, int m)
Check whether subtracting m from n would overflow.
Definition limits.hpp:93
Gecode::Int::Linear
Linear propagators
Gecode::Int::Linear::eliminate
void eliminate(Term< BoolView > *t, int &n, long long int &d)
Eliminate assigned views.
Definition bool-post.cpp:43
Gecode::Int::Linear::precision
bool precision(Term< IntView > *t_p, int n_p, Term< IntView > *t_n, int n_n, long long int d)
Decide the required precision and check for overflow.
Definition int-post.cpp:79
Gecode::Int::Linear::posteqint
void posteqint(Home home, IntView &x, int c, CtrlView b, ReifyMode rm, IntPropLevel ipl)
Definition int-post.cpp:480
Gecode::Int::Linear::rewrite
void rewrite(IntRelType &r, long long int &d)
Rewrite non-strict relations.
Definition bool-post.cpp:55
Gecode::Int::Linear::gcd
int gcd(int a, int b)
Compute the greatest common divisor of a and b.
Definition post.hpp:89
Gecode::Int::Linear::normalize
bool normalize(Term< View > *t, int &n, Term< View > *&t_p, int &n_p, Term< View > *&t_n, int &n_n, int &g)
Normalize linear integer constraints.
Definition post.hpp:126
Gecode::Int::Linear::post_nary
void post_nary(Home home, ViewArray< View > &x, ViewArray< View > &y, IntRelType irt, Val c)
Posting n-ary propagators.
Definition int-post.cpp:158
Gecode::Int
Finite domain integers.
Gecode::Int::floor_div_xp
IntType floor_div_xp(IntType x, IntType y)
Compute where y is non-negative.
Definition div.hpp:75
Gecode
Gecode toplevel namespace
Gecode::vbd
IntPropLevel vbd(IntPropLevel ipl)
Extract value, bounds, or domain propagation from propagation level.
Definition ipl.hpp:37
forceinline
#define forceinline
Definition config.hpp:187
GECODE_NEVER
#define GECODE_NEVER
Assert that this command is never executed.
Definition macros.hpp:56