Generated on Sat Feb 12 2011 17:40:56 for Gecode by doxygen 1.7.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-08-02 14:34:35 +0200 (Mon, 02 Aug 2010) $ by $Author: tack $
00011  *     $Revision: 11321 $
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       if (n==2 && is_unit && icl == ICL_DOM && r == IRT_EQ) {
00273         // Binary domain-consistent equality
00274         c = static_cast<int>(d);
00275         if (c==0) {
00276           switch (n_p) {
00277           case 2: {
00278             IntView x(t_p[0].x);
00279             MinusView y(t_p[1].x);
00280             GECODE_ES_FAIL(
00281               (Rel::EqDom<IntView,MinusView>::post(home,x,y)));
00282             break;
00283           }
00284           case 1: {
00285             IntView x(t_p[0].x);
00286             IntView y(t_n[0].x);
00287             GECODE_ES_FAIL(
00288               (Rel::EqDom<IntView,IntView>::post(home,x,y)));
00289             break;
00290           }
00291           case 0: {
00292             IntView x(t_n[0].x);
00293             MinusView y(t_n[1].x);
00294             GECODE_ES_FAIL(
00295               (Rel::EqDom<IntView,MinusView>::post(home,x,y)));
00296             break;
00297           }
00298           default:
00299             GECODE_NEVER;
00300           }
00301         } else {
00302           switch (n_p) {
00303           case 2: {
00304             MinusView x(t_p[0].x);
00305             OffsetView y(t_p[1].x, -c);
00306             GECODE_ES_FAIL(
00307               (Rel::EqDom<MinusView,OffsetView>::post(home,x,y)));
00308             break;
00309           }
00310           case 1: {
00311             IntView x(t_p[0].x);
00312             OffsetView y(t_n[0].x, c);
00313             GECODE_ES_FAIL(
00314               (Rel::EqDom<IntView,OffsetView>::post(home,x,y)));
00315             break;
00316           }
00317           case 0: {
00318             MinusView x(t_n[0].x);
00319             OffsetView y(t_n[1].x, c);
00320             GECODE_ES_FAIL(
00321               (Rel::EqDom<MinusView,OffsetView>::post(home,x,y)));
00322             break;
00323           }
00324           default:
00325             GECODE_NEVER;
00326           }          
00327         }
00328       } else {
00329         // Arbitrary coefficients with integer precision
00330         c = static_cast<int>(d);
00331         ViewArray<IntScaleView> x(home,n_p);
00332         for (int i = n_p; i--; )
00333           x[i] = IntScaleView(t_p[i].a,t_p[i].x);
00334         ViewArray<IntScaleView> y(home,n_n);
00335         for (int i = n_n; i--; )
00336           y[i] = IntScaleView(t_n[i].a,t_n[i].x);
00337         if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00338           GECODE_ES_FAIL((DomEq<int,IntScaleView>::post(home,x,y,c)));
00339         } else {
00340           post_nary<int,IntScaleView>(home,x,y,r,c);
00341         }
00342       }
00343     } else {
00344       // Arbitrary coefficients with double precision
00345       ViewArray<DoubleScaleView> x(home,n_p);
00346       for (int i = n_p; i--; )
00347         x[i] = DoubleScaleView(t_p[i].a,t_p[i].x);
00348       ViewArray<DoubleScaleView> y(home,n_n);
00349       for (int i = n_n; i--; )
00350         y[i] = DoubleScaleView(t_n[i].a,t_n[i].x);
00351       if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00352         GECODE_ES_FAIL((DomEq<double,DoubleScaleView>::post(home,x,y,d)));
00353       } else {
00354         post_nary<double,DoubleScaleView>(home,x,y,r,d);
00355       }
00356     }
00357   }
00358 
00359 #undef GECODE_INT_PL_BIN
00360 #undef GECODE_INT_PL_TER
00361 
00362 
00367   template<class Val, class View>
00368   forceinline void
00369   post_nary(Home home,
00370             ViewArray<View>& x, ViewArray<View>& y,
00371             IntRelType r, Val c, BoolView b) {
00372     switch (r) {
00373     case IRT_EQ:
00374       GECODE_ES_FAIL((ReEq<Val,View,View,BoolView>::post(home,x,y,c,b)));
00375       break;
00376     case IRT_NQ:
00377       {
00378         NegBoolView n(b);
00379         GECODE_ES_FAIL((ReEq<Val,View,View,NegBoolView>::post
00380                              (home,x,y,c,n)));
00381       }
00382       break;
00383     case IRT_LQ:
00384       GECODE_ES_FAIL((ReLq<Val,View,View>::post(home,x,y,c,b)));
00385       break;
00386     default: GECODE_NEVER;
00387     }
00388   }
00389 
00390   void
00391   post(Home home,
00392        Term<IntView>* t, int n, IntRelType r, int c, BoolView b,
00393        IntConLevel) {
00394 
00395     Limits::check(c,"Int::linear");
00396 
00397     double d = c;
00398 
00399     eliminate(t,n,d);
00400 
00401     Term<IntView> *t_p, *t_n;
00402     int n_p, n_n;
00403     bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n);
00404 
00405     rewrite(r,d,t_p,n_p,t_n,n_n);
00406 
00407     if (n == 0) {
00408       bool fail = false;
00409       switch (r) {
00410       case IRT_EQ: fail = (d != 0.0); break;
00411       case IRT_NQ: fail = (d == 0.0); break;
00412       case IRT_LQ: fail = (0.0 > d); break;
00413       default: GECODE_NEVER;
00414       }
00415       if ((fail ? b.zero(home) : b.one(home)) == ME_INT_FAILED)
00416         home.fail();
00417       return;
00418     }
00419 
00420     bool is_ip = precision(t_p,n_p,t_n,n_n,d);
00421 
00422     if (is_unit && is_ip) {
00423       c = static_cast<int>(d);
00424       if (n == 1) {
00425         switch (r) {
00426         case IRT_EQ:
00427           if (n_p == 1) {
00428             GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,BoolView>::post
00429                                  (home,t_p[0].x,c,b)));
00430           } else {
00431             GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,BoolView>::post
00432                                  (home,t_n[0].x,-c,b)));
00433           }
00434           break;
00435         case IRT_NQ:
00436           {
00437             NegBoolView nb(b);
00438             if (n_p == 1) {
00439               GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,NegBoolView>::post
00440                                    (home,t_p[0].x,c,nb)));
00441             } else {
00442               GECODE_ES_FAIL((Rel::ReEqBndInt<IntView,NegBoolView>::post
00443                                    (home,t_n[0].x,-c,nb)));
00444             }
00445           }
00446           break;
00447         case IRT_LQ:
00448           if (n_p == 1) {
00449             GECODE_ES_FAIL((Rel::ReLqInt<IntView,BoolView>::post
00450                                  (home,t_p[0].x,c,b)));
00451           } else {
00452             NegBoolView nb(b);
00453             GECODE_ES_FAIL((Rel::ReLqInt<IntView,NegBoolView>::post
00454                                  (home,t_n[0].x,-c-1,nb)));
00455           }
00456           break;
00457         default: GECODE_NEVER;
00458         }
00459       } else if (n == 2) {
00460         switch (r) {
00461         case IRT_EQ:
00462           switch (n_p) {
00463           case 2:
00464             GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView>::post
00465                                  (home,t_p[0].x,t_p[1].x,c,b)));
00466             break;
00467           case 1:
00468             GECODE_ES_FAIL((ReEqBin<int,IntView,MinusView,BoolView>::post
00469                                  (home,t_p[0].x,MinusView(t_n[0].x),c,b)));
00470             break;
00471           case 0:
00472             GECODE_ES_FAIL((ReEqBin<int,IntView,IntView,BoolView>::post
00473                                  (home,t_n[0].x,t_n[1].x,-c,b)));
00474             break;
00475           default: GECODE_NEVER;
00476           }
00477           break;
00478         case IRT_NQ:
00479           {
00480             NegBoolView nb(b);
00481             switch (n_p) {
00482             case 2:
00483               GECODE_ES_FAIL(
00484                              (ReEqBin<int,IntView,IntView,NegBoolView>::post
00485                               (home,t_p[0].x,t_p[1].x,c,nb)));
00486               break;
00487             case 1:
00488               GECODE_ES_FAIL(
00489                              (ReEqBin<int,IntView,MinusView,NegBoolView>::post
00490                               (home,t_p[0].x,MinusView(t_n[0].x),c,
00491                                NegBoolView(b))));
00492               break;
00493             case 0:
00494               GECODE_ES_FAIL(
00495                              (ReEqBin<int,IntView,IntView,NegBoolView>::post
00496                               (home,t_p[0].x,t_p[1].x,-c,NegBoolView(b))));
00497               break;
00498             default: GECODE_NEVER;
00499             }
00500           }
00501           break;
00502         case IRT_LQ:
00503           switch (n_p) {
00504           case 2:
00505             GECODE_ES_FAIL((ReLqBin<int,IntView,IntView>::post
00506                                  (home,t_p[0].x,t_p[1].x,c,b)));
00507             break;
00508           case 1:
00509             GECODE_ES_FAIL((ReLqBin<int,IntView,MinusView>::post
00510                                  (home,t_p[0].x,MinusView(t_n[0].x),c,b)));
00511             break;
00512           case 0:
00513             GECODE_ES_FAIL((ReLqBin<int,MinusView,MinusView>::post
00514                                  (home,MinusView(t_n[0].x),
00515                                   MinusView(t_n[1].x),c,b)));
00516             break;
00517           default: GECODE_NEVER;
00518           }
00519           break;
00520         default: GECODE_NEVER;
00521         }
00522       } else {
00523         ViewArray<IntView> x(home,n_p);
00524         for (int i = n_p; i--; )
00525           x[i] = t_p[i].x;
00526         ViewArray<IntView> y(home,n_n);
00527         for (int i = n_n; i--; )
00528           y[i] = t_n[i].x;
00529         post_nary<int,IntView>(home,x,y,r,c,b);
00530       }
00531     } else if (is_ip) {
00532       // Arbitrary coefficients with integer precision
00533       c = static_cast<int>(d);
00534       ViewArray<IntScaleView> x(home,n_p);
00535       for (int i = n_p; i--; )
00536         x[i] = IntScaleView(t_p[i].a,t_p[i].x);
00537       ViewArray<IntScaleView> y(home,n_n);
00538       for (int i = n_n; i--; )
00539         y[i] = IntScaleView(t_n[i].a,t_n[i].x);
00540       post_nary<int,IntScaleView>(home,x,y,r,c,b);
00541     } else {
00542       // Arbitrary coefficients with double precision
00543       ViewArray<DoubleScaleView> x(home,n_p);
00544       for (int i = n_p; i--; )
00545         x[i] = DoubleScaleView(t_p[i].a,t_p[i].x);
00546       ViewArray<DoubleScaleView> y(home,n_n);
00547       for (int i = n_n; i--; )
00548         y[i] = DoubleScaleView(t_n[i].a,t_n[i].x);
00549       post_nary<double,DoubleScaleView>(home,x,y,r,d,b);
00550     }
00551   }
00552 
00553 }}}
00554 
00555 // STATISTICS: int-post