int-post.cpp

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: 2011-09-02 11:52:00 +0200 (Fri, 02 Sep 2011) $ by $Author: tack $
00011  *     $Revision: 12388 $
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       if ((sl < Limits::double_min) || (su > Limits::double_max))
00091         throw OutOfLimits("Int::linear");
00092     }
00093     for (int i = n_n; i--; ) {
00094       sl -= t_n[i].a * static_cast<double>(t_n[i].x.max());
00095       su -= t_n[i].a * static_cast<double>(t_n[i].x.min());
00096       if ((sl < Limits::double_min) || (su > Limits::double_max))
00097         throw OutOfLimits("Int::linear");
00098     }
00099 
00100     bool is_ip = (sl >= Limits::min) && (su <= Limits::max);
00101 
00102     sl -= d;
00103     su -= d;
00104     if ((sl < Limits::double_min) || (su > Limits::double_max))
00105       throw OutOfLimits("Int::linear");
00106 
00107     is_ip = is_ip && (sl >= Limits::min) && (su <= Limits::max);
00108 
00109     for (int i = n_p; i--; ) {
00110       if (sl - t_p[i].a * static_cast<double>(t_p[i].x.min()) 
00111           < Limits::double_min)
00112         throw OutOfLimits("Int::linear");
00113       if (sl - t_p[i].a * static_cast<double>(t_p[i].x.min()) < Limits::min)
00114         is_ip = false;
00115       if (su - t_p[i].a * static_cast<double>(t_p[i].x.max()) 
00116           > Limits::double_max)
00117         throw OutOfLimits("Int::linear");
00118       if (su - t_p[i].a * static_cast<double>(t_p[i].x.max()) > Limits::max)
00119         is_ip = false;
00120     }
00121     for (int i = n_n; i--; ) {
00122       if (sl + t_n[i].a * static_cast<double>(t_n[i].x.min()) 
00123           < Limits::double_min)
00124         throw OutOfLimits("Int::linear");
00125       if (sl + t_n[i].a * static_cast<double>(t_n[i].x.min()) < Limits::min)
00126         is_ip = false;
00127       if (su + t_n[i].a * static_cast<double>(t_n[i].x.max()) 
00128           > Limits::double_max)
00129         throw OutOfLimits("Int::linear");
00130       if (su + t_n[i].a * static_cast<double>(t_n[i].x.max()) > Limits::max)
00131         is_ip = false;
00132     }
00133     return is_ip;
00134   }
00135 
00140   template<class Val, class View>
00141   forceinline void
00142   post_nary(Home home,
00143             ViewArray<View>& x, ViewArray<View>& y, IntRelType r, Val c) {
00144     switch (r) {
00145     case IRT_EQ:
00146       GECODE_ES_FAIL((Eq<Val,View,View >::post(home,x,y,c)));
00147       break;
00148     case IRT_NQ:
00149       GECODE_ES_FAIL((Nq<Val,View,View >::post(home,x,y,c)));
00150       break;
00151     case IRT_LQ:
00152       GECODE_ES_FAIL((Lq<Val,View,View >::post(home,x,y,c)));
00153       break;
00154     default: GECODE_NEVER;
00155     }
00156   }
00157 
00158 
00160 #define GECODE_INT_PL_BIN(CLASS)                                             \
00161   switch (n_p) {                                                             \
00162   case 2:                                                                    \
00163     GECODE_ES_FAIL((CLASS<int,IntView,IntView>::post                    \
00164                          (home,t_p[0].x,t_p[1].x,c)));                       \
00165     break;                                                                   \
00166   case 1:                                                                    \
00167     GECODE_ES_FAIL((CLASS<int,IntView,MinusView>::post                  \
00168                          (home,t_p[0].x,MinusView(t_n[0].x),c)));            \
00169     break;                                                                   \
00170   case 0:                                                                    \
00171     GECODE_ES_FAIL((CLASS<int,MinusView,MinusView>::post                \
00172                          (home,MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
00173     break;                                                                   \
00174   default: GECODE_NEVER;                                                     \
00175   }
00176 
00178 #define GECODE_INT_PL_TER(CLASS)                                        \
00179   switch (n_p) {                                                        \
00180   case 3:                                                               \
00181     GECODE_ES_FAIL((CLASS<int,IntView,IntView,IntView>::post       \
00182                          (home,t_p[0].x,t_p[1].x,t_p[2].x,c)));         \
00183     break;                                                              \
00184   case 2:                                                               \
00185     GECODE_ES_FAIL((CLASS<int,IntView,IntView,MinusView>::post     \
00186                          (home,t_p[0].x,t_p[1].x,                       \
00187                           MinusView(t_n[0].x),c)));                     \
00188     break;                                                              \
00189   case 1:                                                               \
00190     GECODE_ES_FAIL((CLASS<int,IntView,MinusView,MinusView>::post   \
00191                          (home,t_p[0].x,                                \
00192                           MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
00193     break;                                                              \
00194   case 0:                                                               \
00195     GECODE_ES_FAIL((CLASS<int,MinusView,MinusView,MinusView>::post \
00196                          (home,MinusView(t_n[0].x),                     \
00197                           MinusView(t_n[1].x),MinusView(t_n[2].x),c))); \
00198     break;                                                              \
00199   default: GECODE_NEVER;                                                \
00200   }
00201 
00202   void
00203   post(Home home, Term<IntView>* t, int n, IntRelType r, int c,
00204        IntConLevel icl) {
00205 
00206     Limits::check(c,"Int::linear");
00207 
00208     double d = c;
00209 
00210     eliminate(t,n,d);
00211 
00212     Term<IntView> *t_p, *t_n;
00213     int n_p, n_n;
00214     bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n);
00215 
00216     rewrite(r,d,t_p,n_p,t_n,n_n);
00217 
00218     if (n == 0) {
00219       switch (r) {
00220       case IRT_EQ: if (d != 0.0) home.fail(); break;
00221       case IRT_NQ: if (d == 0.0) home.fail(); break;
00222       case IRT_LQ: if (d < 0.0)  home.fail(); break;
00223       default: GECODE_NEVER;
00224       }
00225       return;
00226     }
00227 
00228     if (n == 1) {
00229       if (n_p == 1) {
00230         DoubleScaleView y(t_p[0].a,t_p[0].x);
00231         switch (r) {
00232         case IRT_EQ: GECODE_ME_FAIL(y.eq(home,d)); break;
00233         case IRT_NQ: GECODE_ME_FAIL(y.nq(home,d)); break;
00234         case IRT_LQ: GECODE_ME_FAIL(y.lq(home,d)); break;
00235         default: GECODE_NEVER;
00236         }
00237       } else {
00238         DoubleScaleView y(t_n[0].a,t_n[0].x);
00239         switch (r) {
00240         case IRT_EQ: GECODE_ME_FAIL(y.eq(home,-d)); break;
00241         case IRT_NQ: GECODE_ME_FAIL(y.nq(home,-d)); break;
00242         case IRT_LQ: GECODE_ME_FAIL(y.gq(home,-d)); break;
00243         default: GECODE_NEVER;
00244         }
00245       }
00246       return;
00247     }
00248 
00249     bool is_ip = precision(t_p,n_p,t_n,n_n,d);
00250 
00251     if (is_unit && is_ip && (icl != ICL_DOM)) {
00252       // Unit coefficients with integer precision
00253       c = static_cast<int>(d);
00254       if (n == 2) {
00255         switch (r) {
00256         case IRT_EQ: GECODE_INT_PL_BIN(EqBin); break;
00257         case IRT_NQ: GECODE_INT_PL_BIN(NqBin); break;
00258         case IRT_LQ: GECODE_INT_PL_BIN(LqBin); break;
00259         default: GECODE_NEVER;
00260         }
00261       } else if (n == 3) {
00262         switch (r) {
00263         case IRT_EQ: GECODE_INT_PL_TER(EqTer); break;
00264         case IRT_NQ: GECODE_INT_PL_TER(NqTer); break;
00265         case IRT_LQ: GECODE_INT_PL_TER(LqTer); break;
00266         default: GECODE_NEVER;
00267         }
00268       } else {
00269         ViewArray<IntView> x(home,n_p);
00270         for (int i = n_p; i--; )
00271           x[i] = t_p[i].x;
00272         ViewArray<IntView> y(home,n_n);
00273         for (int i = n_n; i--; )
00274           y[i] = t_n[i].x;
00275         post_nary<int,IntView>(home,x,y,r,c);
00276       }
00277     } else if (is_ip) {
00278       if (n==2 && is_unit && icl == ICL_DOM && r == IRT_EQ) {
00279         // Binary domain-consistent equality
00280         c = static_cast<int>(d);
00281         if (c==0) {
00282           switch (n_p) {
00283           case 2: {
00284             IntView x(t_p[0].x);
00285             MinusView y(t_p[1].x);
00286             GECODE_ES_FAIL(
00287               (Rel::EqDom<IntView,MinusView>::post(home,x,y)));
00288             break;
00289           }
00290           case 1: {
00291             IntView x(t_p[0].x);
00292             IntView y(t_n[0].x);
00293             GECODE_ES_FAIL(
00294               (Rel::EqDom<IntView,IntView>::post(home,x,y)));
00295             break;
00296           }
00297           case 0: {
00298             IntView x(t_n[0].x);
00299             MinusView y(t_n[1].x);
00300             GECODE_ES_FAIL(
00301               (Rel::EqDom<IntView,MinusView>::post(home,x,y)));
00302             break;
00303           }
00304           default:
00305             GECODE_NEVER;
00306           }
00307         } else {
00308           switch (n_p) {
00309           case 2: {
00310             MinusView x(t_p[0].x);
00311             OffsetView y(t_p[1].x, -c);
00312             GECODE_ES_FAIL(
00313               (Rel::EqDom<MinusView,OffsetView>::post(home,x,y)));
00314             break;
00315           }
00316           case 1: {
00317             IntView x(t_p[0].x);
00318             OffsetView y(t_n[0].x, c);
00319             GECODE_ES_FAIL(
00320               (Rel::EqDom<IntView,OffsetView>::post(home,x,y)));
00321             break;
00322           }
00323           case 0: {
00324             MinusView x(t_n[0].x);
00325             OffsetView y(t_n[1].x, c);
00326             GECODE_ES_FAIL(
00327               (Rel::EqDom<MinusView,OffsetView>::post(home,x,y)));
00328             break;
00329           }
00330           default:
00331             GECODE_NEVER;
00332           }          
00333         }
00334       } else {
00335         // Arbitrary coefficients with integer precision
00336         c = static_cast<int>(d);
00337         ViewArray<IntScaleView> x(home,n_p);
00338         for (int i = n_p; i--; )
00339           x[i] = IntScaleView(t_p[i].a,t_p[i].x);
00340         ViewArray<IntScaleView> y(home,n_n);
00341         for (int i = n_n; i--; )
00342           y[i] = IntScaleView(t_n[i].a,t_n[i].x);
00343         if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00344           GECODE_ES_FAIL((DomEq<int,IntScaleView>::post(home,x,y,c)));
00345         } else {
00346           post_nary<int,IntScaleView>(home,x,y,r,c);
00347         }
00348       }
00349     } else {
00350       // Arbitrary coefficients with double precision
00351       ViewArray<DoubleScaleView> x(home,n_p);
00352       for (int i = n_p; i--; )
00353         x[i] = DoubleScaleView(t_p[i].a,t_p[i].x);
00354       ViewArray<DoubleScaleView> y(home,n_n);
00355       for (int i = n_n; i--; )
00356         y[i] = DoubleScaleView(t_n[i].a,t_n[i].x);
00357       if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00358         GECODE_ES_FAIL((DomEq<double,DoubleScaleView>::post(home,x,y,d)));
00359       } else {
00360         post_nary<double,DoubleScaleView>(home,x,y,r,d);
00361       }
00362     }
00363   }
00364 
00365 #undef GECODE_INT_PL_BIN
00366 #undef GECODE_INT_PL_TER
00367 
00368 
00373   template<class Val, class View>
00374   forceinline void
00375   post_nary(Home home,
00376             ViewArray<View>& x, ViewArray<View>& y,
00377             IntRelType r, Val c, BoolView b) {
00378     switch (r) {
00379     case IRT_EQ:
00380       GECODE_ES_FAIL((ReEq<Val,View,View,BoolView>::post(home,x,y,c,b)));
00381       break;
00382     case IRT_NQ:
00383       {
00384         NegBoolView n(b);
00385         GECODE_ES_FAIL((ReEq<Val,View,View,NegBoolView>::post
00386                              (home,x,y,c,n)));
00387       }
00388       break;
00389     case IRT_LQ:
00390       GECODE_ES_FAIL((ReLq<Val,View,View>::post(home,x,y,c,b)));
00391       break;
00392     default: GECODE_NEVER;
00393     }
00394   }
00395 
00396   void
00397   post(Home home,
00398        Term<IntView>* t, int n, IntRelType r, int c, BoolView b,
00399        IntConLevel) {
00400 
00401     Limits::check(c,"Int::linear");
00402 
00403     double d = c;
00404 
00405     eliminate(t,n,d);
00406 
00407     Term<IntView> *t_p, *t_n;
00408     int n_p, n_n;
00409     bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n);
00410 
00411     rewrite(r,d,t_p,n_p,t_n,n_n);
00412 
00413     if (n == 0) {
00414       bool fail = false;
00415       switch (r) {
00416       case IRT_EQ: fail = (d != 0.0); break;
00417       case IRT_NQ: fail = (d == 0.0); break;
00418       case IRT_LQ: fail = (0.0 > d); break;
00419       default: GECODE_NEVER;
00420       }
00421       if ((fail ? b.zero(home) : b.one(home)) == ME_INT_FAILED)
00422         home.fail();
00423       return;
00424     }
00425 
00426     bool is_ip = precision(t_p,n_p,t_n,n_n,d);
00427 
00428     if (is_unit && is_ip) {
00429       c = static_cast<int>(d);
00430       if (n == 1) {
00431         switch (r) {
00432         case IRT_EQ:
00433           if (n_p == 1) {
00434             GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,BoolView>::post
00435                                  (home,t_p[0].x,c,b)));
00436           } else {
00437             GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,BoolView>::post
00438                                  (home,t_n[0].x,-c,b)));
00439           }
00440           break;
00441         case IRT_NQ:
00442           {
00443             NegBoolView nb(b);
00444             if (n_p == 1) {
00445               GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,NegBoolView>::post
00446                                    (home,t_p[0].x,c,nb)));
00447             } else {
00448               GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,NegBoolView>::post
00449                                    (home,t_n[0].x,-c,nb)));
00450             }
00451           }
00452           break;
00453         case IRT_LQ:
00454           if (n_p == 1) {
00455             GECODE_ES_FAIL((Rel::ReLqInt<IntView,BoolView>::post
00456                                  (home,t_p[0].x,c,b)));
00457           } else {
00458             NegBoolView nb(b);
00459             GECODE_ES_FAIL((Rel::ReLqInt<IntView,NegBoolView>::post
00460                                  (home,t_n[0].x,-c-1,nb)));
00461           }
00462           break;
00463         default: GECODE_NEVER;
00464         }
00465       } else if (n == 2) {
00466         switch (r) {
00467         case IRT_EQ:
00468           switch (n_p) {
00469           case 2:
00470             GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView>::post
00471                                  (home,t_p[0].x,t_p[1].x,c,b)));
00472             break;
00473           case 1:
00474             GECODE_ES_FAIL((ReEqBin<int,IntView,MinusView,BoolView>::post
00475                                  (home,t_p[0].x,MinusView(t_n[0].x),c,b)));
00476             break;
00477           case 0:
00478             GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView>::post
00479                                  (home,t_n[0].x,t_n[1].x,-c,b)));
00480             break;
00481           default: GECODE_NEVER;
00482           }
00483           break;
00484         case IRT_NQ:
00485           {
00486             NegBoolView nb(b);
00487             switch (n_p) {
00488             case 2:
00489               GECODE_ES_FAIL(
00490                              (ReEqBin<int,IntView,IntView,NegBoolView>::post
00491                               (home,t_p[0].x,t_p[1].x,c,nb)));
00492               break;
00493             case 1:
00494               GECODE_ES_FAIL(
00495                              (ReEqBin<int,IntView,MinusView,NegBoolView>::post
00496                               (home,t_p[0].x,MinusView(t_n[0].x),c,
00497                                NegBoolView(b))));
00498               break;
00499             case 0:
00500               GECODE_ES_FAIL(
00501                              (ReEqBin<int,IntView,IntView,NegBoolView>::post
00502                               (home,t_p[0].x,t_p[1].x,-c,NegBoolView(b))));
00503               break;
00504             default: GECODE_NEVER;
00505             }
00506           }
00507           break;
00508         case IRT_LQ:
00509           switch (n_p) {
00510           case 2:
00511             GECODE_ES_FAIL((ReLqBin<int,IntView,IntView>::post
00512                                  (home,t_p[0].x,t_p[1].x,c,b)));
00513             break;
00514           case 1:
00515             GECODE_ES_FAIL((ReLqBin<int,IntView,MinusView>::post
00516                                  (home,t_p[0].x,MinusView(t_n[0].x),c,b)));
00517             break;
00518           case 0:
00519             GECODE_ES_FAIL((ReLqBin<int,MinusView,MinusView>::post
00520                                  (home,MinusView(t_n[0].x),
00521                                   MinusView(t_n[1].x),c,b)));
00522             break;
00523           default: GECODE_NEVER;
00524           }
00525           break;
00526         default: GECODE_NEVER;
00527         }
00528       } else {
00529         ViewArray<IntView> x(home,n_p);
00530         for (int i = n_p; i--; )
00531           x[i] = t_p[i].x;
00532         ViewArray<IntView> y(home,n_n);
00533         for (int i = n_n; i--; )
00534           y[i] = t_n[i].x;
00535         post_nary<int,IntView>(home,x,y,r,c,b);
00536       }
00537     } else if (is_ip) {
00538       // Arbitrary coefficients with integer precision
00539       c = static_cast<int>(d);
00540       ViewArray<IntScaleView> x(home,n_p);
00541       for (int i = n_p; i--; )
00542         x[i] = IntScaleView(t_p[i].a,t_p[i].x);
00543       ViewArray<IntScaleView> y(home,n_n);
00544       for (int i = n_n; i--; )
00545         y[i] = IntScaleView(t_n[i].a,t_n[i].x);
00546       post_nary<int,IntScaleView>(home,x,y,r,c,b);
00547     } else {
00548       // Arbitrary coefficients with double precision
00549       ViewArray<DoubleScaleView> x(home,n_p);
00550       for (int i = n_p; i--; )
00551         x[i] = DoubleScaleView(t_p[i].a,t_p[i].x);
00552       ViewArray<DoubleScaleView> y(home,n_n);
00553       for (int i = n_n; i--; )
00554         y[i] = DoubleScaleView(t_n[i].a,t_n[i].x);
00555       post_nary<double,DoubleScaleView>(home,x,y,r,d,b);
00556     }
00557   }
00558 
00559 }}}
00560 
00561 // STATISTICS: int-post