gecode » int » linear
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: 2009-11-04 17:06:58 +0100 (Wed, 04 Nov 2009) $ by $Author: tack $
00011  *     $Revision: 10046 $
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   const double double_max = 9007199254740991.0;
00049   const double double_min = -9007199254740991.0;
00050 
00052   inline void
00053   eliminate(Term<IntView>* t, int &n, double& d) {
00054     for (int i=n; i--; )
00055       if (t[i].x.assigned()) {
00056         d -= t[i].a * static_cast<double>(t[i].x.val());
00057         t[i]=t[--n];
00058       }
00059     if ((d < double_min) || (d > double_max))
00060       throw OutOfLimits("Int::linear");
00061   }
00062 
00064   inline void
00065   rewrite(IntRelType &r, double &d,
00066           Term<IntView>* &t_p, int &n_p,
00067           Term<IntView>* &t_n, int &n_n) {
00068     switch (r) {
00069     case IRT_EQ: case IRT_NQ: case IRT_LQ:
00070       break;
00071     case IRT_LE:
00072       d--; r = IRT_LQ; break;
00073     case IRT_GR:
00074       d++; /* fall through */
00075     case IRT_GQ:
00076       r = IRT_LQ;
00077       std::swap(n_p,n_n); std::swap(t_p,t_n); d = -d;
00078       break;
00079     default:
00080       throw UnknownRelation("Int::linear");
00081     }
00082   }
00083 
00085   inline bool
00086   precision(Term<IntView>* t_p, int n_p,
00087             Term<IntView>* t_n, int n_n,
00088             double d) {
00089     double sl = 0.0;
00090     double su = 0.0;
00091 
00092     for (int i = n_p; i--; ) {
00093       sl += t_p[i].a * static_cast<double>(t_p[i].x.min());
00094       su += t_p[i].a * static_cast<double>(t_p[i].x.max());
00095     }
00096     for (int i = n_n; i--; ) {
00097       sl -= t_n[i].a * static_cast<double>(t_n[i].x.max());
00098       su -= t_n[i].a * static_cast<double>(t_n[i].x.min());
00099     }
00100     sl -= d;
00101     su -= d;
00102 
00103     if ((sl < double_min) || (su > double_max))
00104       throw OutOfLimits("Int::linear");
00105 
00106     bool is_ip = (sl >= Limits::min) && (su <= Limits::max);
00107 
00108     for (int i = n_p; i--; ) {
00109       if (sl - t_p[i].a * static_cast<double>(t_p[i].x.min()) < double_min)
00110         throw OutOfLimits("Int::linear");
00111       if (sl - t_p[i].a * static_cast<double>(t_p[i].x.min()) < Limits::min)
00112         is_ip = false;
00113       if (su - t_p[i].a * static_cast<double>(t_p[i].x.max()) > double_max)
00114         throw OutOfLimits("Int::linear");
00115       if (su - t_p[i].a * static_cast<double>(t_p[i].x.max()) > Limits::max)
00116         is_ip = false;
00117     }
00118     for (int i = n_n; i--; ) {
00119       if (sl + t_n[i].a * static_cast<double>(t_n[i].x.min()) < double_min)
00120         throw OutOfLimits("Int::linear");
00121       if (sl + t_n[i].a * static_cast<double>(t_n[i].x.min()) < Limits::min)
00122         is_ip = false;
00123       if (su + t_n[i].a * static_cast<double>(t_n[i].x.max()) > double_max)
00124         throw OutOfLimits("Int::linear");
00125       if (su + t_n[i].a * static_cast<double>(t_n[i].x.max()) > Limits::max)
00126         is_ip = false;
00127     }
00128     return is_ip;
00129   }
00130 
00135   template<class Val, class View>
00136   forceinline void
00137   post_nary(Home home,
00138             ViewArray<View>& x, ViewArray<View>& y, IntRelType r, Val c) {
00139     switch (r) {
00140     case IRT_EQ:
00141       GECODE_ES_FAIL(home,(Eq<Val,View,View >::post(home,x,y,c)));
00142       break;
00143     case IRT_NQ:
00144       GECODE_ES_FAIL(home,(Nq<Val,View,View >::post(home,x,y,c)));
00145       break;
00146     case IRT_LQ:
00147       GECODE_ES_FAIL(home,(Lq<Val,View,View >::post(home,x,y,c)));
00148       break;
00149     default: GECODE_NEVER;
00150     }
00151   }
00152 
00153 
00155 #define GECODE_INT_PL_BIN(CLASS)                                             \
00156   switch (n_p) {                                                             \
00157   case 2:                                                                    \
00158     GECODE_ES_FAIL(home,(CLASS<int,IntView,IntView>::post                    \
00159                          (home,t_p[0].x,t_p[1].x,c)));                       \
00160     break;                                                                   \
00161   case 1:                                                                    \
00162     GECODE_ES_FAIL(home,(CLASS<int,IntView,MinusView>::post                  \
00163                          (home,t_p[0].x,MinusView(t_n[0].x),c)));            \
00164     break;                                                                   \
00165   case 0:                                                                    \
00166     GECODE_ES_FAIL(home,(CLASS<int,MinusView,MinusView>::post                \
00167                          (home,MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
00168     break;                                                                   \
00169   default: GECODE_NEVER;                                                     \
00170   }
00171 
00173 #define GECODE_INT_PL_TER(CLASS)                                        \
00174   switch (n_p) {                                                        \
00175   case 3:                                                               \
00176     GECODE_ES_FAIL(home,(CLASS<int,IntView,IntView,IntView>::post       \
00177                          (home,t_p[0].x,t_p[1].x,t_p[2].x,c)));         \
00178     break;                                                              \
00179   case 2:                                                               \
00180     GECODE_ES_FAIL(home,(CLASS<int,IntView,IntView,MinusView>::post     \
00181                          (home,t_p[0].x,t_p[1].x,                       \
00182                           MinusView(t_n[0].x),c)));                     \
00183     break;                                                              \
00184   case 1:                                                               \
00185     GECODE_ES_FAIL(home,(CLASS<int,IntView,MinusView,MinusView>::post   \
00186                          (home,t_p[0].x,                                \
00187                           MinusView(t_n[0].x),MinusView(t_n[1].x),c))); \
00188     break;                                                              \
00189   case 0:                                                               \
00190     GECODE_ES_FAIL(home,(CLASS<int,MinusView,MinusView,MinusView>::post \
00191                          (home,MinusView(t_n[0].x),                     \
00192                           MinusView(t_n[1].x),MinusView(t_n[2].x),c))); \
00193     break;                                                              \
00194   default: GECODE_NEVER;                                                \
00195   }
00196 
00197   void
00198   post(Home home, Term<IntView>* t, int n, IntRelType r, int c,
00199        IntConLevel icl) {
00200 
00201     Limits::check(c,"Int::linear");
00202 
00203     double d = c;
00204 
00205     eliminate(t,n,d);
00206 
00207     Term<IntView> *t_p, *t_n;
00208     int n_p, n_n;
00209     bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n);
00210 
00211     rewrite(r,d,t_p,n_p,t_n,n_n);
00212 
00213     if (n == 0) {
00214       switch (r) {
00215       case IRT_EQ: if (d != 0.0) home.fail(); break;
00216       case IRT_NQ: if (d == 0.0) home.fail(); break;
00217       case IRT_LQ: if (d < 0.0)  home.fail(); break;
00218       default: GECODE_NEVER;
00219       }
00220       return;
00221     }
00222 
00223     if (n == 1) {
00224       if (n_p == 1) {
00225         DoubleScaleView y(t_p[0].a,t_p[0].x);
00226         switch (r) {
00227         case IRT_EQ: GECODE_ME_FAIL(home,y.eq(home,d)); break;
00228         case IRT_NQ: GECODE_ME_FAIL(home,y.nq(home,d)); break;
00229         case IRT_LQ: GECODE_ME_FAIL(home,y.lq(home,d)); break;
00230         default: GECODE_NEVER;
00231         }
00232       } else {
00233         DoubleScaleView y(t_n[0].a,t_n[0].x);
00234         switch (r) {
00235         case IRT_EQ: GECODE_ME_FAIL(home,y.eq(home,-d)); break;
00236         case IRT_NQ: GECODE_ME_FAIL(home,y.nq(home,-d)); break;
00237         case IRT_LQ: GECODE_ME_FAIL(home,y.gq(home,-d)); break;
00238         default: GECODE_NEVER;
00239         }
00240       }
00241       return;
00242     }
00243 
00244     bool is_ip = precision(t_p,n_p,t_n,n_n,d);
00245 
00246     if (is_unit && is_ip && (icl != ICL_DOM)) {
00247       // Unit coefficients with integer precision
00248       c = static_cast<int>(d);
00249       if (n == 2) {
00250         switch (r) {
00251         case IRT_EQ: GECODE_INT_PL_BIN(EqBin); break;
00252         case IRT_NQ: GECODE_INT_PL_BIN(NqBin); break;
00253         case IRT_LQ: GECODE_INT_PL_BIN(LqBin); break;
00254         default: GECODE_NEVER;
00255         }
00256       } else if (n == 3) {
00257         switch (r) {
00258         case IRT_EQ: GECODE_INT_PL_TER(EqTer); break;
00259         case IRT_NQ: GECODE_INT_PL_TER(NqTer); break;
00260         case IRT_LQ: GECODE_INT_PL_TER(LqTer); break;
00261         default: GECODE_NEVER;
00262         }
00263       } else {
00264         ViewArray<IntView> x(home,n_p);
00265         for (int i = n_p; i--; )
00266           x[i] = t_p[i].x;
00267         ViewArray<IntView> y(home,n_n);
00268         for (int i = n_n; i--; )
00269           y[i] = t_n[i].x;
00270         post_nary<int,IntView>(home,x,y,r,c);
00271       }
00272     } else if (is_ip) {
00273       // Arbitrary coefficients with integer precision
00274       c = static_cast<int>(d);
00275       ViewArray<IntScaleView> x(home,n_p);
00276       for (int i = n_p; i--; )
00277         x[i].init(t_p[i].a,t_p[i].x);
00278       ViewArray<IntScaleView> y(home,n_n);
00279       for (int i = n_n; i--; )
00280         y[i].init(t_n[i].a,t_n[i].x);
00281       if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00282         GECODE_ES_FAIL(home,(DomEq<int,IntScaleView>::post(home,x,y,c)));
00283       } else {
00284         post_nary<int,IntScaleView>(home,x,y,r,c);
00285       }
00286     } else {
00287       // Arbitrary coefficients with double precision
00288       ViewArray<DoubleScaleView> x(home,n_p);
00289       for (int i = n_p; i--; )
00290         x[i].init(t_p[i].a,t_p[i].x);
00291       ViewArray<DoubleScaleView> y(home,n_n);
00292       for (int i = n_n; i--; )
00293         y[i].init(t_n[i].a,t_n[i].x);
00294       if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00295         GECODE_ES_FAIL(home,(DomEq<double,DoubleScaleView>::post(home,x,y,d)));
00296       } else {
00297         post_nary<double,DoubleScaleView>(home,x,y,r,d);
00298       }
00299     }
00300   }
00301 
00302 #undef GECODE_INT_PL_BIN
00303 #undef GECODE_INT_PL_TER
00304 
00305 
00310   template<class Val, class View>
00311   forceinline void
00312   post_nary(Home home,
00313             ViewArray<View>& x, ViewArray<View>& y,
00314             IntRelType r, Val c, BoolView b) {
00315     switch (r) {
00316     case IRT_EQ:
00317       GECODE_ES_FAIL(home,(ReEq<Val,View,View,BoolView>::post(home,x,y,c,b)));
00318       break;
00319     case IRT_NQ:
00320       {
00321         NegBoolView n(b);
00322         GECODE_ES_FAIL(home,(ReEq<Val,View,View,NegBoolView>::post
00323                              (home,x,y,c,n)));
00324       }
00325       break;
00326     case IRT_LQ:
00327       GECODE_ES_FAIL(home,(ReLq<Val,View,View>::post(home,x,y,c,b)));
00328       break;
00329     default: GECODE_NEVER;
00330     }
00331   }
00332 
00333   void
00334   post(Home home,
00335        Term<IntView>* t, int n, IntRelType r, int c, BoolView b,
00336        IntConLevel) {
00337 
00338     Limits::check(c,"Int::linear");
00339 
00340     double d = c;
00341 
00342     eliminate(t,n,d);
00343 
00344     Term<IntView> *t_p, *t_n;
00345     int n_p, n_n;
00346     bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n);
00347 
00348     rewrite(r,d,t_p,n_p,t_n,n_n);
00349 
00350     if (n == 0) {
00351       bool fail = false;
00352       switch (r) {
00353       case IRT_EQ: fail = (d != 0.0); break;
00354       case IRT_NQ: fail = (d == 0.0); break;
00355       case IRT_LQ: fail = (0.0 > d); break;
00356       default: GECODE_NEVER;
00357       }
00358       if ((fail ? b.zero(home) : b.one(home)) == ME_INT_FAILED)
00359         home.fail();
00360       return;
00361     }
00362 
00363     bool is_ip = precision(t_p,n_p,t_n,n_n,d);
00364 
00365     if (is_unit && is_ip) {
00366       c = static_cast<int>(d);
00367       if (n == 1) {
00368         switch (r) {
00369         case IRT_EQ:
00370           if (n_p == 1) {
00371             GECODE_ES_FAIL(home,(Rel::ReEqBndInt<IntView,BoolView>::post
00372                                  (home,t_p[0].x,c,b)));
00373           } else {
00374             GECODE_ES_FAIL(home,(Rel::ReEqBndInt<IntView,BoolView>::post
00375                                  (home,t_n[0].x,-c,b)));
00376           }
00377           break;
00378         case IRT_NQ:
00379           {
00380             NegBoolView nb(b);
00381             if (n_p == 1) {
00382               GECODE_ES_FAIL(home,(Rel::ReEqBndInt<IntView,NegBoolView>::post
00383                                    (home,t_p[0].x,c,nb)));
00384             } else {
00385               GECODE_ES_FAIL(home,(Rel::ReEqBndInt<IntView,NegBoolView>::post
00386                                    (home,t_n[0].x,-c,nb)));
00387             }
00388           }
00389           break;
00390         case IRT_LQ:
00391           if (n_p == 1) {
00392             GECODE_ES_FAIL(home,(Rel::ReLqInt<IntView,BoolView>::post
00393                                  (home,t_p[0].x,c,b)));
00394           } else {
00395             NegBoolView nb(b);
00396             GECODE_ES_FAIL(home,(Rel::ReLqInt<IntView,NegBoolView>::post
00397                                  (home,t_n[0].x,-c-1,nb)));
00398           }
00399           break;
00400         default: GECODE_NEVER;
00401         }
00402       } else if (n == 2) {
00403         switch (r) {
00404         case IRT_EQ:
00405           switch (n_p) {
00406           case 2:
00407             GECODE_ES_FAIL(home,(ReEqBin<int,IntView,IntView,BoolView>::post
00408                                  (home,t_p[0].x,t_p[1].x,c,b)));
00409             break;
00410           case 1:
00411             GECODE_ES_FAIL(home,(ReEqBin<int,IntView,MinusView,BoolView>::post
00412                                  (home,t_p[0].x,MinusView(t_n[0].x),c,b)));
00413             break;
00414           case 0:
00415             GECODE_ES_FAIL(home,(ReEqBin<int,IntView,IntView,BoolView>::post
00416                                  (home,t_n[0].x,t_n[1].x,-c,b)));
00417             break;
00418           default: GECODE_NEVER;
00419           }
00420           break;
00421         case IRT_NQ:
00422           {
00423             NegBoolView nb(b);
00424             switch (n_p) {
00425             case 2:
00426               GECODE_ES_FAIL(home,
00427                              (ReEqBin<int,IntView,IntView,NegBoolView>::post
00428                               (home,t_p[0].x,t_p[1].x,c,nb)));
00429               break;
00430             case 1:
00431               GECODE_ES_FAIL(home,
00432                              (ReEqBin<int,IntView,MinusView,NegBoolView>::post
00433                               (home,t_p[0].x,MinusView(t_n[0].x),c,
00434                                NegBoolView(b))));
00435               break;
00436             case 0:
00437               GECODE_ES_FAIL(home,
00438                              (ReEqBin<int,IntView,IntView,NegBoolView>::post
00439                               (home,t_p[0].x,t_p[1].x,-c,NegBoolView(b))));
00440               break;
00441             default: GECODE_NEVER;
00442             }
00443           }
00444           break;
00445         case IRT_LQ:
00446           switch (n_p) {
00447           case 2:
00448             GECODE_ES_FAIL(home,(ReLqBin<int,IntView,IntView>::post
00449                                  (home,t_p[0].x,t_p[1].x,c,b)));
00450             break;
00451           case 1:
00452             GECODE_ES_FAIL(home,(ReLqBin<int,IntView,MinusView>::post
00453                                  (home,t_p[0].x,MinusView(t_n[0].x),c,b)));
00454             break;
00455           case 0:
00456             GECODE_ES_FAIL(home,(ReLqBin<int,MinusView,MinusView>::post
00457                                  (home,MinusView(t_n[0].x),
00458                                   MinusView(t_n[1].x),c,b)));
00459             break;
00460           default: GECODE_NEVER;
00461           }
00462           break;
00463         default: GECODE_NEVER;
00464         }
00465       } else {
00466         ViewArray<IntView> x(home,n_p);
00467         for (int i = n_p; i--; )
00468           x[i] = t_p[i].x;
00469         ViewArray<IntView> y(home,n_n);
00470         for (int i = n_n; i--; )
00471           y[i] = t_n[i].x;
00472         post_nary<int,IntView>(home,x,y,r,c,b);
00473       }
00474     } else if (is_ip) {
00475       // Arbitrary coefficients with integer precision
00476       c = static_cast<int>(d);
00477       ViewArray<IntScaleView> x(home,n_p);
00478       for (int i = n_p; i--; )
00479         x[i].init(t_p[i].a,t_p[i].x);
00480       ViewArray<IntScaleView> y(home,n_n);
00481       for (int i = n_n; i--; )
00482         y[i].init(t_n[i].a,t_n[i].x);
00483       post_nary<int,IntScaleView>(home,x,y,r,c,b);
00484     } else {
00485       // Arbitrary coefficients with double precision
00486       ViewArray<DoubleScaleView> x(home,n_p);
00487       for (int i = n_p; i--; )
00488         x[i].init(t_p[i].a,t_p[i].x);
00489       ViewArray<DoubleScaleView> y(home,n_n);
00490       for (int i = n_n; i--; )
00491         y[i].init(t_n[i].a,t_n[i].x);
00492       post_nary<double,DoubleScaleView>(home,x,y,r,d,b);
00493     }
00494   }
00495 
00496 }}}
00497 
00498 // STATISTICS: int-post