Generated on Mon May 10 06:46:39 2010 for Gecode by doxygen 1.6.3

int-post.cpp

Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
00002 /*
00003  *  Main authors:
00004  *     Christian Schulte <schulte@gecode.org>
00005  *
00006  *  Copyright:
00007  *     Christian Schulte, 2002
00008  *
00009  *  Last modified:
00010  *     $Date: 2010-03-03 17:40:32 +0100 (Wed, 03 Mar 2010) $ by $Author: schulte $
00011  *     $Revision: 10365 $
00012  *
00013  *  This file is part of Gecode, the generic constraint
00014  *  development environment:
00015  *     http://www.gecode.org
00016  *
00017  *  Permission is hereby granted, free of charge, to any person obtaining
00018  *  a copy of this software and associated documentation files (the
00019  *  "Software"), to deal in the Software without restriction, including
00020  *  without limitation the rights to use, copy, modify, merge, publish,
00021  *  distribute, sublicense, and/or sell copies of the Software, and to
00022  *  permit persons to whom the Software is furnished to do so, subject to
00023  *  the following conditions:
00024  *
00025  *  The above copyright notice and this permission notice shall be
00026  *  included in all copies or substantial portions of the Software.
00027  *
00028  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00029  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00030  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00031  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00032  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00033  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00034  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00035  *
00036  */
00037 
00038 #include <cfloat>
00039 #include <algorithm>
00040 
00041 #include <gecode/int/rel.hh>
00042 #include <gecode/int/linear.hh>
00043 
00044 namespace Gecode { namespace Int { namespace Linear {
00045 
00047   inline void
00048   eliminate(Term<IntView>* t, int &n, double& d) {
00049     for (int i=n; i--; )
00050       if (t[i].x.assigned()) {
00051         d -= t[i].a * static_cast<double>(t[i].x.val());
00052         t[i]=t[--n];
00053       }
00054     if ((d < Limits::double_min) || (d > Limits::double_max))
00055       throw OutOfLimits("Int::linear");
00056   }
00057 
00059   inline void
00060   rewrite(IntRelType &r, double &d,
00061           Term<IntView>* &t_p, int &n_p,
00062           Term<IntView>* &t_n, int &n_n) {
00063     switch (r) {
00064     case IRT_EQ: case IRT_NQ: case IRT_LQ:
00065       break;
00066     case IRT_LE:
00067       d--; r = IRT_LQ; break;
00068     case IRT_GR:
00069       d++; /* fall through */
00070     case IRT_GQ:
00071       r = IRT_LQ;
00072       std::swap(n_p,n_n); std::swap(t_p,t_n); d = -d;
00073       break;
00074     default:
00075       throw UnknownRelation("Int::linear");
00076     }
00077   }
00078 
00080   inline bool
00081   precision(Term<IntView>* t_p, int n_p,
00082             Term<IntView>* t_n, int n_n,
00083             double d) {
00084     double sl = 0.0;
00085     double su = 0.0;
00086 
00087     for (int i = n_p; i--; ) {
00088       sl += t_p[i].a * static_cast<double>(t_p[i].x.min());
00089       su += t_p[i].a * static_cast<double>(t_p[i].x.max());
00090     }
00091     for (int i = n_n; i--; ) {
00092       sl -= t_n[i].a * static_cast<double>(t_n[i].x.max());
00093       su -= t_n[i].a * static_cast<double>(t_n[i].x.min());
00094     }
00095     sl -= d;
00096     su -= d;
00097 
00098     if ((sl < Limits::double_min) || (su > Limits::double_max))
00099       throw OutOfLimits("Int::linear");
00100 
00101     bool is_ip = (sl >= Limits::min) && (su <= Limits::max);
00102 
00103     for (int i = n_p; i--; ) {
00104       if (sl - t_p[i].a * static_cast<double>(t_p[i].x.min()) 
00105           < Limits::double_min)
00106         throw OutOfLimits("Int::linear");
00107       if (sl - t_p[i].a * static_cast<double>(t_p[i].x.min()) < Limits::min)
00108         is_ip = false;
00109       if (su - t_p[i].a * static_cast<double>(t_p[i].x.max()) 
00110           > Limits::double_max)
00111         throw OutOfLimits("Int::linear");
00112       if (su - t_p[i].a * static_cast<double>(t_p[i].x.max()) > Limits::max)
00113         is_ip = false;
00114     }
00115     for (int i = n_n; i--; ) {
00116       if (sl + t_n[i].a * static_cast<double>(t_n[i].x.min()) 
00117           < Limits::double_min)
00118         throw OutOfLimits("Int::linear");
00119       if (sl + t_n[i].a * static_cast<double>(t_n[i].x.min()) < Limits::min)
00120         is_ip = false;
00121       if (su + t_n[i].a * static_cast<double>(t_n[i].x.max()) 
00122           > Limits::double_max)
00123         throw OutOfLimits("Int::linear");
00124       if (su + t_n[i].a * static_cast<double>(t_n[i].x.max()) > Limits::max)
00125         is_ip = false;
00126     }
00127     return is_ip;
00128   }
00129 
00134   template<class Val, class View>
00135   forceinline void
00136   post_nary(Home home,
00137             ViewArray<View>& x, ViewArray<View>& y, IntRelType r, Val c) {
00138     switch (r) {
00139     case IRT_EQ:
00140       GECODE_ES_FAIL((Eq<Val,View,View >::post(home,x,y,c)));
00141       break;
00142     case IRT_NQ:
00143       GECODE_ES_FAIL((Nq<Val,View,View >::post(home,x,y,c)));
00144       break;
00145     case IRT_LQ:
00146       GECODE_ES_FAIL((Lq<Val,View,View >::post(home,x,y,c)));
00147       break;
00148     default: GECODE_NEVER;
00149     }
00150   }
00151 
00152 
00154 #define GECODE_INT_PL_BIN(CLASS)                                             \
00155   switch (n_p) {                                                             \
00156   case 2:                                                                    \
00157     GECODE_ES_FAIL((CLASS<int,IntView,IntView>::post                    \
00158                          (home,t_p[0].x,t_p[1].x,c)));                       \
00159     break;                                                                   \
00160   case 1:                                                                    \
00161     GECODE_ES_FAIL((CLASS<int,IntView,MinusView>::post                  \
00162                          (home,t_p[0].x,MinusView(t_n[0].x),c)));            \
00163     break;                                                                   \
00164   case 0:                                                                    \
00165     GECODE_ES_FAIL((CLASS<int,MinusView,MinusView>::post                \
00166                          (home,MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
00167     break;                                                                   \
00168   default: GECODE_NEVER;                                                     \
00169   }
00170 
00172 #define GECODE_INT_PL_TER(CLASS)                                        \
00173   switch (n_p) {                                                        \
00174   case 3:                                                               \
00175     GECODE_ES_FAIL((CLASS<int,IntView,IntView,IntView>::post       \
00176                          (home,t_p[0].x,t_p[1].x,t_p[2].x,c)));         \
00177     break;                                                              \
00178   case 2:                                                               \
00179     GECODE_ES_FAIL((CLASS<int,IntView,IntView,MinusView>::post     \
00180                          (home,t_p[0].x,t_p[1].x,                       \
00181                           MinusView(t_n[0].x),c)));                     \
00182     break;                                                              \
00183   case 1:                                                               \
00184     GECODE_ES_FAIL((CLASS<int,IntView,MinusView,MinusView>::post   \
00185                          (home,t_p[0].x,                                \
00186                           MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
00187     break;                                                              \
00188   case 0:                                                               \
00189     GECODE_ES_FAIL((CLASS<int,MinusView,MinusView,MinusView>::post \
00190                          (home,MinusView(t_n[0].x),                     \
00191                           MinusView(t_n[1].x),MinusView(t_n[2].x),c))); \
00192     break;                                                              \
00193   default: GECODE_NEVER;                                                \
00194   }
00195 
00196   void
00197   post(Home home, Term<IntView>* t, int n, IntRelType r, int c,
00198        IntConLevel icl) {
00199 
00200     Limits::check(c,"Int::linear");
00201 
00202     double d = c;
00203 
00204     eliminate(t,n,d);
00205 
00206     Term<IntView> *t_p, *t_n;
00207     int n_p, n_n;
00208     bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n);
00209 
00210     rewrite(r,d,t_p,n_p,t_n,n_n);
00211 
00212     if (n == 0) {
00213       switch (r) {
00214       case IRT_EQ: if (d != 0.0) home.fail(); break;
00215       case IRT_NQ: if (d == 0.0) home.fail(); break;
00216       case IRT_LQ: if (d < 0.0)  home.fail(); break;
00217       default: GECODE_NEVER;
00218       }
00219       return;
00220     }
00221 
00222     if (n == 1) {
00223       if (n_p == 1) {
00224         DoubleScaleView y(t_p[0].a,t_p[0].x);
00225         switch (r) {
00226         case IRT_EQ: GECODE_ME_FAIL(y.eq(home,d)); break;
00227         case IRT_NQ: GECODE_ME_FAIL(y.nq(home,d)); break;
00228         case IRT_LQ: GECODE_ME_FAIL(y.lq(home,d)); break;
00229         default: GECODE_NEVER;
00230         }
00231       } else {
00232         DoubleScaleView y(t_n[0].a,t_n[0].x);
00233         switch (r) {
00234         case IRT_EQ: GECODE_ME_FAIL(y.eq(home,-d)); break;
00235         case IRT_NQ: GECODE_ME_FAIL(y.nq(home,-d)); break;
00236         case IRT_LQ: GECODE_ME_FAIL(y.gq(home,-d)); break;
00237         default: GECODE_NEVER;
00238         }
00239       }
00240       return;
00241     }
00242 
00243     bool is_ip = precision(t_p,n_p,t_n,n_n,d);
00244 
00245     if (is_unit && is_ip && (icl != ICL_DOM)) {
00246       // Unit coefficients with integer precision
00247       c = static_cast<int>(d);
00248       if (n == 2) {
00249         switch (r) {
00250         case IRT_EQ: GECODE_INT_PL_BIN(EqBin); break;
00251         case IRT_NQ: GECODE_INT_PL_BIN(NqBin); break;
00252         case IRT_LQ: GECODE_INT_PL_BIN(LqBin); break;
00253         default: GECODE_NEVER;
00254         }
00255       } else if (n == 3) {
00256         switch (r) {
00257         case IRT_EQ: GECODE_INT_PL_TER(EqTer); break;
00258         case IRT_NQ: GECODE_INT_PL_TER(NqTer); break;
00259         case IRT_LQ: GECODE_INT_PL_TER(LqTer); break;
00260         default: GECODE_NEVER;
00261         }
00262       } else {
00263         ViewArray<IntView> x(home,n_p);
00264         for (int i = n_p; i--; )
00265           x[i] = t_p[i].x;
00266         ViewArray<IntView> y(home,n_n);
00267         for (int i = n_n; i--; )
00268           y[i] = t_n[i].x;
00269         post_nary<int,IntView>(home,x,y,r,c);
00270       }
00271     } else if (is_ip) {
00272       // Arbitrary coefficients with integer precision
00273       c = static_cast<int>(d);
00274       ViewArray<IntScaleView> x(home,n_p);
00275       for (int i = n_p; i--; )
00276         x[i].init(t_p[i].a,t_p[i].x);
00277       ViewArray<IntScaleView> y(home,n_n);
00278       for (int i = n_n; i--; )
00279         y[i].init(t_n[i].a,t_n[i].x);
00280       if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00281         GECODE_ES_FAIL((DomEq<int,IntScaleView>::post(home,x,y,c)));
00282       } else {
00283         post_nary<int,IntScaleView>(home,x,y,r,c);
00284       }
00285     } else {
00286       // Arbitrary coefficients with double precision
00287       ViewArray<DoubleScaleView> x(home,n_p);
00288       for (int i = n_p; i--; )
00289         x[i].init(t_p[i].a,t_p[i].x);
00290       ViewArray<DoubleScaleView> y(home,n_n);
00291       for (int i = n_n; i--; )
00292         y[i].init(t_n[i].a,t_n[i].x);
00293       if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00294         GECODE_ES_FAIL((DomEq<double,DoubleScaleView>::post(home,x,y,d)));
00295       } else {
00296         post_nary<double,DoubleScaleView>(home,x,y,r,d);
00297       }
00298     }
00299   }
00300 
00301 #undef GECODE_INT_PL_BIN
00302 #undef GECODE_INT_PL_TER
00303 
00304 
00309   template<class Val, class View>
00310   forceinline void
00311   post_nary(Home home,
00312             ViewArray<View>& x, ViewArray<View>& y,
00313             IntRelType r, Val c, BoolView b) {
00314     switch (r) {
00315     case IRT_EQ:
00316       GECODE_ES_FAIL((ReEq<Val,View,View,BoolView>::post(home,x,y,c,b)));
00317       break;
00318     case IRT_NQ:
00319       {
00320         NegBoolView n(b);
00321         GECODE_ES_FAIL((ReEq<Val,View,View,NegBoolView>::post
00322                              (home,x,y,c,n)));
00323       }
00324       break;
00325     case IRT_LQ:
00326       GECODE_ES_FAIL((ReLq<Val,View,View>::post(home,x,y,c,b)));
00327       break;
00328     default: GECODE_NEVER;
00329     }
00330   }
00331 
00332   void
00333   post(Home home,
00334        Term<IntView>* t, int n, IntRelType r, int c, BoolView b,
00335        IntConLevel) {
00336 
00337     Limits::check(c,"Int::linear");
00338 
00339     double d = c;
00340 
00341     eliminate(t,n,d);
00342 
00343     Term<IntView> *t_p, *t_n;
00344     int n_p, n_n;
00345     bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n);
00346 
00347     rewrite(r,d,t_p,n_p,t_n,n_n);
00348 
00349     if (n == 0) {
00350       bool fail = false;
00351       switch (r) {
00352       case IRT_EQ: fail = (d != 0.0); break;
00353       case IRT_NQ: fail = (d == 0.0); break;
00354       case IRT_LQ: fail = (0.0 > d); break;
00355       default: GECODE_NEVER;
00356       }
00357       if ((fail ? b.zero(home) : b.one(home)) == ME_INT_FAILED)
00358         home.fail();
00359       return;
00360     }
00361 
00362     bool is_ip = precision(t_p,n_p,t_n,n_n,d);
00363 
00364     if (is_unit && is_ip) {
00365       c = static_cast<int>(d);
00366       if (n == 1) {
00367         switch (r) {
00368         case IRT_EQ:
00369           if (n_p == 1) {
00370             GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,BoolView>::post
00371                                  (home,t_p[0].x,c,b)));
00372           } else {
00373             GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,BoolView>::post
00374                                  (home,t_n[0].x,-c,b)));
00375           }
00376           break;
00377         case IRT_NQ:
00378           {
00379             NegBoolView nb(b);
00380             if (n_p == 1) {
00381               GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,NegBoolView>::post
00382                                    (home,t_p[0].x,c,nb)));
00383             } else {
00384               GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,NegBoolView>::post
00385                                    (home,t_n[0].x,-c,nb)));
00386             }
00387           }
00388           break;
00389         case IRT_LQ:
00390           if (n_p == 1) {
00391             GECODE_ES_FAIL((Rel::ReLqInt<IntView,BoolView>::post
00392                                  (home,t_p[0].x,c,b)));
00393           } else {
00394             NegBoolView nb(b);
00395             GECODE_ES_FAIL((Rel::ReLqInt<IntView,NegBoolView>::post
00396                                  (home,t_n[0].x,-c-1,nb)));
00397           }
00398           break;
00399         default: GECODE_NEVER;
00400         }
00401       } else if (n == 2) {
00402         switch (r) {
00403         case IRT_EQ:
00404           switch (n_p) {
00405           case 2:
00406             GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView>::post
00407                                  (home,t_p[0].x,t_p[1].x,c,b)));
00408             break;
00409           case 1:
00410             GECODE_ES_FAIL((ReEqBin<int,IntView,MinusView,BoolView>::post
00411                                  (home,t_p[0].x,MinusView(t_n[0].x),c,b)));
00412             break;
00413           case 0:
00414             GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView>::post
00415                                  (home,t_n[0].x,t_n[1].x,-c,b)));
00416             break;
00417           default: GECODE_NEVER;
00418           }
00419           break;
00420         case IRT_NQ:
00421           {
00422             NegBoolView nb(b);
00423             switch (n_p) {
00424             case 2:
00425               GECODE_ES_FAIL(
00426                              (ReEqBin<int,IntView,IntView,NegBoolView>::post
00427                               (home,t_p[0].x,t_p[1].x,c,nb)));
00428               break;
00429             case 1:
00430               GECODE_ES_FAIL(
00431                              (ReEqBin<int,IntView,MinusView,NegBoolView>::post
00432                               (home,t_p[0].x,MinusView(t_n[0].x),c,
00433                                NegBoolView(b))));
00434               break;
00435             case 0:
00436               GECODE_ES_FAIL(
00437                              (ReEqBin<int,IntView,IntView,NegBoolView>::post
00438                               (home,t_p[0].x,t_p[1].x,-c,NegBoolView(b))));
00439               break;
00440             default: GECODE_NEVER;
00441             }
00442           }
00443           break;
00444         case IRT_LQ:
00445           switch (n_p) {
00446           case 2:
00447             GECODE_ES_FAIL((ReLqBin<int,IntView,IntView>::post
00448                                  (home,t_p[0].x,t_p[1].x,c,b)));
00449             break;
00450           case 1:
00451             GECODE_ES_FAIL((ReLqBin<int,IntView,MinusView>::post
00452                                  (home,t_p[0].x,MinusView(t_n[0].x),c,b)));
00453             break;
00454           case 0:
00455             GECODE_ES_FAIL((ReLqBin<int,MinusView,MinusView>::post
00456                                  (home,MinusView(t_n[0].x),
00457                                   MinusView(t_n[1].x),c,b)));
00458             break;
00459           default: GECODE_NEVER;
00460           }
00461           break;
00462         default: GECODE_NEVER;
00463         }
00464       } else {
00465         ViewArray<IntView> x(home,n_p);
00466         for (int i = n_p; i--; )
00467           x[i] = t_p[i].x;
00468         ViewArray<IntView> y(home,n_n);
00469         for (int i = n_n; i--; )
00470           y[i] = t_n[i].x;
00471         post_nary<int,IntView>(home,x,y,r,c,b);
00472       }
00473     } else if (is_ip) {
00474       // Arbitrary coefficients with integer precision
00475       c = static_cast<int>(d);
00476       ViewArray<IntScaleView> x(home,n_p);
00477       for (int i = n_p; i--; )
00478         x[i].init(t_p[i].a,t_p[i].x);
00479       ViewArray<IntScaleView> y(home,n_n);
00480       for (int i = n_n; i--; )
00481         y[i].init(t_n[i].a,t_n[i].x);
00482       post_nary<int,IntScaleView>(home,x,y,r,c,b);
00483     } else {
00484       // Arbitrary coefficients with double precision
00485       ViewArray<DoubleScaleView> x(home,n_p);
00486       for (int i = n_p; i--; )
00487         x[i].init(t_p[i].a,t_p[i].x);
00488       ViewArray<DoubleScaleView> y(home,n_n);
00489       for (int i = n_n; i--; )
00490         y[i].init(t_n[i].a,t_n[i].x);
00491       post_nary<double,DoubleScaleView>(home,x,y,r,d,b);
00492     }
00493   }
00494 
00495 }}}
00496 
00497 // STATISTICS: int-post