Generated on Mon Aug 25 11:35:38 2008 for Gecode by doxygen 1.5.6
gecode » int » linear

int-post.cc

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: 2008-07-11 09:31:51 +0200 (Fri, 11 Jul 2008) $ by $Author: tack $
00011  *     $Revision: 7288 $
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(Space* 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,t_n[0].x,c)));          \
00164     break;                                                      \
00165   case 0:                                                       \
00166     GECODE_ES_FAIL(home,(CLASS<int,MinusView,MinusView>::post   \
00167                          (home,t_n[0].x,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,t_n[0].x,c)));         \
00182     break;                                                              \
00183   case 1:                                                               \
00184     GECODE_ES_FAIL(home,(CLASS<int,IntView,MinusView,MinusView>::post   \
00185                          (home,t_p[0].x,t_n[0].x,t_n[1].x,c)));         \
00186     break;                                                              \
00187   case 0:                                                               \
00188     GECODE_ES_FAIL(home,(CLASS<int,MinusView,MinusView,MinusView>::post \
00189                          (home,t_n[0].x,t_n[1].x,t_n[2].x,c)));         \
00190     break;                                                              \
00191   default: GECODE_NEVER;                                                \
00192   }
00193 
00194   void
00195   post(Space* home, Term<IntView>* t, int n, IntRelType r, int c,
00196        IntConLevel icl, PropKind) {
00197 
00198     Limits::check(c,"Int::linear");
00199 
00200     double d = c;
00201     
00202     eliminate(t,n,d);
00203 
00204     Term<IntView> *t_p, *t_n;
00205     int n_p, n_n;
00206     bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n);
00207 
00208     rewrite(r,d,t_p,n_p,t_n,n_n);
00209 
00210     if (n == 0) {
00211       switch (r) {
00212       case IRT_EQ: if (d != 0.0) home->fail(); break;
00213       case IRT_NQ: if (d == 0.0) home->fail(); break;
00214       case IRT_LQ: if (d < 0.0)  home->fail(); break;
00215       default: GECODE_NEVER;
00216       }
00217       return;
00218     }
00219 
00220     if (n == 1) {
00221       if (n_p == 1) {
00222         DoubleScaleView y(t_p[0].a,t_p[0].x);
00223         switch (r) {
00224         case IRT_EQ: GECODE_ME_FAIL(home,y.eq(home,d)); break;
00225         case IRT_NQ: GECODE_ME_FAIL(home,y.nq(home,d)); break;
00226         case IRT_LQ: GECODE_ME_FAIL(home,y.lq(home,d)); break;
00227         default: GECODE_NEVER;
00228         }
00229       } else {
00230         DoubleScaleView y(t_n[0].a,t_n[0].x);
00231         switch (r) {
00232         case IRT_EQ: GECODE_ME_FAIL(home,y.eq(home,-d)); break;
00233         case IRT_NQ: GECODE_ME_FAIL(home,y.nq(home,-d)); break;
00234         case IRT_LQ: GECODE_ME_FAIL(home,y.gq(home,-d)); break;
00235         default: GECODE_NEVER;
00236         }
00237       }
00238       return;
00239     }
00240 
00241     bool is_ip = precision(t_p,n_p,t_n,n_n,d);
00242 
00243     if (is_unit && is_ip && (icl != ICL_DOM)) {
00244       // Unit coefficients with integer precision
00245       c = static_cast<int>(d);
00246       if (n == 2) {
00247         switch (r) {
00248         case IRT_EQ: GECODE_INT_PL_BIN(EqBin); break;
00249         case IRT_NQ: GECODE_INT_PL_BIN(NqBin); break;
00250         case IRT_LQ: GECODE_INT_PL_BIN(LqBin); break;
00251         default: GECODE_NEVER;
00252         }
00253       } else if (n == 3) {
00254         switch (r) {                                                
00255         case IRT_EQ: GECODE_INT_PL_TER(EqTer); break;
00256         case IRT_NQ: GECODE_INT_PL_TER(NqTer); break;
00257         case IRT_LQ: GECODE_INT_PL_TER(LqTer); break;
00258         default: GECODE_NEVER;
00259         }
00260       } else {
00261         ViewArray<IntView> x(home,n_p);
00262         for (int i = n_p; i--; ) 
00263           x[i] = t_p[i].x;
00264         ViewArray<IntView> y(home,n_n);
00265         for (int i = n_n; i--; ) 
00266           y[i] = t_n[i].x;
00267         post_nary<int,IntView>(home,x,y,r,c);
00268       }
00269     } else if (is_ip) {
00270       // Arbitrary coefficients with integer precision
00271       c = static_cast<int>(d);
00272       ViewArray<IntScaleView> x(home,n_p);
00273       for (int i = n_p; i--; )
00274         x[i].init(t_p[i].a,t_p[i].x);
00275       ViewArray<IntScaleView> y(home,n_n);
00276       for (int i = n_n; i--; )
00277         y[i].init(t_n[i].a,t_n[i].x);
00278       if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00279         GECODE_ES_FAIL(home,(DomEq<int,IntScaleView>::post(home,x,y,c)));
00280       } else {
00281         post_nary<int,IntScaleView>(home,x,y,r,c);
00282       }
00283     } else {
00284       // Arbitrary coefficients with double precision
00285       ViewArray<DoubleScaleView> x(home,n_p);
00286       for (int i = n_p; i--; )
00287         x[i].init(t_p[i].a,t_p[i].x);
00288       ViewArray<DoubleScaleView> y(home,n_n);
00289       for (int i = n_n; i--; )
00290         y[i].init(t_n[i].a,t_n[i].x);
00291       if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00292         GECODE_ES_FAIL(home,(DomEq<double,DoubleScaleView>::post(home,x,y,d)));
00293       } else {
00294         post_nary<double,DoubleScaleView>(home,x,y,r,d);
00295       }
00296     }
00297   }
00298 
00299 #undef GECODE_INT_PL_BIN
00300 #undef GECODE_INT_PL_TER
00301 
00302 
00307   template <class Val, class View>
00308   forceinline void
00309   post_nary(Space* home,
00310             ViewArray<View>& x, ViewArray<View>& y, 
00311             IntRelType r, Val c, BoolView b) {
00312     switch (r) {
00313     case IRT_EQ:
00314       GECODE_ES_FAIL(home,(ReEq<Val,View,View,BoolView>::post(home,x,y,c,b)));
00315       break;
00316     case IRT_NQ:
00317       {
00318         NegBoolView n(b);
00319         GECODE_ES_FAIL(home,(ReEq<Val,View,View,NegBoolView>::post
00320                              (home,x,y,c,n)));
00321       }
00322       break;
00323     case IRT_LQ:
00324       GECODE_ES_FAIL(home,(ReLq<Val,View,View>::post(home,x,y,c,b)));
00325       break;
00326     default: GECODE_NEVER;
00327     }
00328   }
00329 
00330   void
00331   post(Space* home,
00332        Term<IntView>* t, int n, IntRelType r, int c, BoolView b,
00333        IntConLevel,PropKind) {
00334 
00335     Limits::check(c,"Int::linear");
00336 
00337     double d = c;
00338     
00339     eliminate(t,n,d);
00340 
00341     Term<IntView> *t_p, *t_n;
00342     int n_p, n_n;
00343     bool is_unit = normalize<IntView>(t,n,t_p,n_p,t_n,n_n);
00344 
00345     rewrite(r,d,t_p,n_p,t_n,n_n);
00346 
00347     if (n == 0) {
00348       bool fail = false;
00349       switch (r) {
00350       case IRT_EQ: fail = (d != 0.0); break;
00351       case IRT_NQ: fail = (d == 0.0); break;
00352       case IRT_LQ: fail = (0.0 > d); break;
00353       default: GECODE_NEVER;
00354       }
00355       if ((fail ? b.zero(home) : b.one(home)) == ME_INT_FAILED)
00356         home->fail();
00357       return;
00358     }
00359 
00360     bool is_ip = precision(t_p,n_p,t_n,n_n,d);
00361 
00362     if (is_unit && is_ip) {
00363       c = static_cast<int>(d);
00364       if (n == 1) {
00365         switch (r) {
00366         case IRT_EQ:
00367           if (n_p == 1) {
00368             GECODE_ES_FAIL(home,(Rel::ReEqBndInt<IntView,BoolView>::post
00369                                  (home,t_p[0].x,c,b)));
00370           } else {
00371             GECODE_ES_FAIL(home,(Rel::ReEqBndInt<IntView,BoolView>::post
00372                                  (home,t_n[0].x,-c,b)));
00373           }
00374           break;
00375         case IRT_NQ:
00376           {
00377             NegBoolView nb(b);
00378             if (n_p == 1) {
00379               GECODE_ES_FAIL(home,(Rel::ReEqBndInt<IntView,NegBoolView>::post
00380                                    (home,t_p[0].x,c,nb)));
00381             } else {
00382               GECODE_ES_FAIL(home,(Rel::ReEqBndInt<IntView,NegBoolView>::post
00383                                    (home,t_n[0].x,-c,nb)));
00384             }
00385           }
00386           break;
00387         case IRT_LQ:
00388           if (n_p == 1) {
00389             GECODE_ES_FAIL(home,(Rel::ReLqInt<IntView,BoolView>::post
00390                                  (home,t_p[0].x,c,b)));
00391           } else {
00392             NegBoolView nb(b);
00393             GECODE_ES_FAIL(home,(Rel::ReLqInt<IntView,NegBoolView>::post
00394                                  (home,t_n[0].x,-c-1,nb)));
00395           }
00396           break;
00397         default: GECODE_NEVER;
00398         }
00399       } else if (n == 2) {
00400         switch (r) {
00401         case IRT_EQ:
00402           switch (n_p) {
00403           case 2:
00404             GECODE_ES_FAIL(home,(ReEqBin<int,IntView,IntView,BoolView>::post
00405                                  (home,t_p[0].x,t_p[1].x,c,b)));
00406             break;
00407           case 1:
00408             GECODE_ES_FAIL(home,(ReEqBin<int,IntView,MinusView,BoolView>::post
00409                                  (home,t_p[0].x,t_n[0].x,c,b)));
00410             break;
00411           case 0:
00412             GECODE_ES_FAIL(home,(ReEqBin<int,IntView,IntView,BoolView>::post
00413                                  (home,t_n[0].x,t_n[1].x,-c,b)));
00414             break;
00415           default: GECODE_NEVER;
00416           }
00417           break;
00418         case IRT_NQ:
00419           {
00420             NegBoolView nb(b);
00421             switch (n_p) {
00422             case 2:
00423               GECODE_ES_FAIL(home,
00424                              (ReEqBin<int,IntView,IntView,NegBoolView>::post
00425                               (home,t_p[0].x,t_p[1].x,c,nb)));
00426               break;
00427             case 1:
00428               GECODE_ES_FAIL(home,
00429                              (ReEqBin<int,IntView,MinusView,NegBoolView>::post
00430                               (home,t_p[0].x,t_n[0].x,c,b)));
00431               break;
00432             case 0:
00433               GECODE_ES_FAIL(home,
00434                              (ReEqBin<int,IntView,IntView,NegBoolView>::post
00435                               (home,t_p[0].x,t_p[1].x,-c,b)));
00436               break;
00437             default: GECODE_NEVER;
00438             }
00439           }
00440           break;
00441         case IRT_LQ:
00442           switch (n_p) {
00443           case 2:
00444             GECODE_ES_FAIL(home,(ReLqBin<int,IntView,IntView>::post
00445                                  (home,t_p[0].x,t_p[1].x,c,b)));
00446             break;
00447           case 1:
00448             GECODE_ES_FAIL(home,(ReLqBin<int,IntView,MinusView>::post
00449                                  (home,t_p[0].x,t_n[0].x,c,b)));
00450             break;
00451           case 0:
00452             GECODE_ES_FAIL(home,(ReLqBin<int,MinusView,MinusView>::post
00453                                  (home,t_n[0].x,t_n[1].x,c,b)));
00454             break;
00455           default: GECODE_NEVER;
00456           }
00457           break;
00458         default: GECODE_NEVER;
00459         }
00460       } else {
00461         ViewArray<IntView> x(home,n_p);
00462         for (int i = n_p; i--; ) 
00463           x[i] = t_p[i].x;
00464         ViewArray<IntView> y(home,n_n);
00465         for (int i = n_n; i--; )
00466           y[i] = t_n[i].x;
00467         post_nary<int,IntView>(home,x,y,r,c,b);
00468       }
00469     } else if (is_ip) {
00470       // Arbitrary coefficients with integer precision
00471       c = static_cast<int>(d); 
00472       ViewArray<IntScaleView> x(home,n_p);
00473       for (int i = n_p; i--; )
00474         x[i].init(t_p[i].a,t_p[i].x);
00475       ViewArray<IntScaleView> y(home,n_n);
00476       for (int i = n_n; i--; )
00477         y[i].init(t_n[i].a,t_n[i].x);
00478       post_nary<int,IntScaleView>(home,x,y,r,c,b);
00479     } else {
00480       // Arbitrary coefficients with double precision
00481       ViewArray<DoubleScaleView> x(home,n_p);
00482       for (int i = n_p; i--; )
00483         x[i].init(t_p[i].a,t_p[i].x);
00484       ViewArray<DoubleScaleView> y(home,n_n);
00485       for (int i = n_n; i--; )
00486         y[i].init(t_n[i].a,t_n[i].x);
00487       post_nary<double,DoubleScaleView>(home,x,y,r,d,b);
00488     }
00489   }
00490 
00491 }}}
00492 
00493 // STATISTICS: int-post