Generated on Thu Jul 6 07:06:45 2006 for Gecode by doxygen 1.4.7

post.cc

Go to the documentation of this file.
00001 /*
00002  *  Main authors:
00003  *     Christian Schulte <schulte@gecode.org>
00004  *
00005  *  Copyright:
00006  *     Christian Schulte, 2002
00007  *
00008  *  Last modified:
00009  *     $Date: 2006-04-11 15:58:37 +0200 (Tue, 11 Apr 2006) $ by $Author: tack $
00010  *     $Revision: 3188 $
00011  *
00012  *  This file is part of Gecode, the generic constraint
00013  *  development environment:
00014  *     http://www.gecode.org
00015  *
00016  *  See the file "LICENSE" for information on usage and
00017  *  redistribution of this file, and for a
00018  *     DISCLAIMER OF ALL WARRANTIES.
00019  *
00020  */
00021 
00022 #include "gecode/int/rel.hh"
00023 #include "gecode/int/linear.hh"
00024 
00025 #include "gecode/support/sort.hh"
00026 
00027 #include <climits>
00028 #include <algorithm>
00029 
00030 namespace Gecode { namespace Int { namespace Linear {
00031 
00033   class TermLess {
00034   public:
00035     forceinline bool
00036     operator()(const Term& a, const Term& b) {
00037       return before(a.x,b.x);
00038     }
00039   };
00040 
00041   bool
00042   preprocess(Term e[], int& n, IntRelType& r, int& c, int& n_p, int& n_n) {
00043     if ((c < Limits::Int::int_min) || (c > Limits::Int::int_max))
00044       throw NumericalOverflow("Int::linear");
00045     /*
00046      * Join coefficients for aliased variables:
00047      */
00048     {
00049       // Group same variables
00050       TermLess el;
00051       Support::quicksort<Term,TermLess>(e,n,el);
00052 
00053       // Join adjacent variables
00054       int i = 0;
00055       int j = 0;
00056       while (i < n) {
00057         int     a = e[i].a;
00058         if ((a < Limits::Int::int_min) || (a > Limits::Int::int_max))
00059           throw NumericalOverflow("Int::linear");
00060         IntView x = e[i].x;
00061         while ((++i < n) && same(e[i].x,x)) {
00062           a += e[i].a;
00063           if ((a < Limits::Int::int_min) || (a > Limits::Int::int_max))
00064             throw NumericalOverflow("Int::linear");
00065         }
00066         if (a != 0) {
00067           e[j].a = a; e[j].x = x; j++;
00068         }
00069       }
00070       n = j;
00071     }
00072     /*
00073      * All inequations in terms of <=
00074      */
00075     switch (r) {
00076     case IRT_EQ: case IRT_NQ: case IRT_LQ:
00077       break;
00078     case IRT_LE:
00079       c--; r = IRT_LQ; break;
00080     case IRT_GR:
00081       c++; /* fall through */
00082     case IRT_GQ:
00083       r = IRT_LQ;
00084       for (int i = n; i--; )
00085         e[i].a = -e[i].a;
00086       c = -c;
00087       break;
00088     default:
00089       throw UnknownRelation("Int::linear");
00090     }
00091     /*
00092      * Partition into positive/negative coefficents
00093      */
00094     {
00095       int i = 0;
00096       int j = n-1;
00097       while (true) {
00098         while ((e[j].a < 0) && (--j >= 0)) ;
00099         while ((e[i].a > 0) && (++i <  n)) ;
00100         if (j <= i) break;
00101         std::swap(e[i],e[j]);
00102       }
00103       n_p = i;
00104       n_n = n-n_p;
00105     }
00106     for (int i = n; i--; )
00107       if ((e[i].a != 1) && (e[i].a != -1))
00108         return false;
00109     return true;
00110   }
00111 
00112   bool
00113   int_precision(Term e[], int n, int c) {
00114     // Decide the required precision
00115     double sn = 0.0; double sp = 0.0;
00116 
00117     for (int i = n; i--; ) {
00118       const double l = e[i].a * static_cast<double>(e[i].x.min());
00119       if (l < 0.0) sn += l; else sp += l;
00120       const double u = e[i].a * static_cast<double>(e[i].x.max());
00121       if (u < 0.0) sn += u; else sp += u;
00122     }
00123     double cp = (c<0) ? -c : c;
00124     if ((sn-cp < Limits::Int::double_min) || 
00125         (sp+cp > Limits::Int::double_max))
00126       throw NumericalOverflow("Int::linear");
00127 
00128     return ((sn >= Limits::Int::int_min) && (sn <= Limits::Int::int_max) &&
00129             (sp >= Limits::Int::int_min) && (sp <= Limits::Int::int_max) &&
00130             (sn-c >= Limits::Int::int_min) && (sn-c <= Limits::Int::int_max) &&
00131             (sp-c >= Limits::Int::int_min) && (sp-c <= Limits::Int::int_max));
00132   }
00133 
00134   /*
00135    * Posting plain propagators
00136    *
00137    */
00138 
00139   template <class Val, class View>
00140   forceinline void
00141   post_nary(Space* home,
00142             ViewArray<View>& x, ViewArray<View>& y, IntRelType r, Val c) {
00143     switch (r) {
00144     case IRT_LQ:
00145       if (Lq<Val,View,View >::post(home,x,y,c) == ES_FAILED)
00146         home->fail();
00147       break;
00148     case IRT_EQ:
00149       if (Eq<Val,View,View >::post(home,x,y,c) == ES_FAILED)
00150         home->fail();
00151       break;
00152     case IRT_NQ:
00153       if (Nq<Val,View,View >::post(home,x,y,c) == ES_FAILED)
00154         home->fail();
00155       break;
00156     default:
00157       assert(0);
00158     }
00159   }
00160 
00161   void
00162   post(Space* home, Term e[], int n, IntRelType r, int c,
00163        IntConLevel icl) {
00164     int n_p, n_n;
00165     bool is_unit = preprocess(e,n,r,c,n_p,n_n);
00166     if (n == 0) {
00167       switch (r) {
00168       case IRT_EQ: if (c != 0) home->fail(); break;
00169       case IRT_NQ: if (c == 0) home->fail(); break;
00170       case IRT_LQ: if (0 > c)  home->fail(); break;
00171       default: assert(0);
00172       }
00173       return;
00174     }
00175     if (n == 1) {
00176       if (e[0].a > 0) {
00177         DoubleScaleView y(e[0].a,e[0].x);
00178         switch (r) {
00179         case IRT_EQ: GECODE_ME_FAIL(home,y.eq(home,c)); break;
00180         case IRT_NQ: GECODE_ME_FAIL(home,y.nq(home,c)); break;
00181         case IRT_LQ: GECODE_ME_FAIL(home,y.lq(home,c)); break;
00182         default: assert(0);
00183         }
00184       } else {
00185         DoubleScaleView y(-e[0].a,e[0].x);
00186         switch (r) {
00187         case IRT_EQ: GECODE_ME_FAIL(home,y.eq(home,-c)); break;
00188         case IRT_NQ: GECODE_ME_FAIL(home,y.nq(home,-c)); break;
00189         case IRT_LQ: GECODE_ME_FAIL(home,y.gq(home,-c)); break;
00190         default: assert(0);
00191         }
00192       }
00193       return;
00194     }
00195     bool is_ip = int_precision(e,n,c);
00196     if (is_unit && is_ip && (icl != ICL_DOM)) {
00197       if (n == 2) {
00198         switch (r) {
00199         case IRT_LQ:
00200           switch (n_p) {
00201           case 2:
00202             if (LqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,c)
00203                 == ES_FAILED) home->fail();
00204             break;
00205           case 1:
00206             if (LqBin<int,IntView,MinusView>::post(home,e[0].x,e[1].x,c)
00207                 == ES_FAILED) home->fail();
00208             break;
00209           case 0:
00210             if (LqBin<int,MinusView,MinusView>::post(home,e[0].x,e[1].x,c)
00211                 == ES_FAILED) home->fail();
00212             break;
00213           default:
00214             assert(0);
00215           }
00216           break;
00217         case IRT_EQ:
00218           switch (n_p) {
00219           case 2:
00220             if (EqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,c)
00221                 == ES_FAILED) home->fail();
00222             break;
00223           case 1:
00224             if (EqBin<int,IntView,MinusView>::post(home,e[0].x,e[1].x,c)
00225                 == ES_FAILED) home->fail();
00226             break;
00227           case 0:
00228             if (EqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,-c)
00229                 == ES_FAILED) home->fail();
00230             break;
00231           default:
00232             assert(0);
00233           }
00234           break;
00235         case IRT_NQ:
00236           switch (n_p) {
00237           case 2:
00238             if (NqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,c)
00239                 == ES_FAILED) home->fail();
00240             break;
00241           case 1:
00242             if (NqBin<int,IntView,MinusView>::post(home,e[0].x,e[1].x,c)
00243                 == ES_FAILED) home->fail();
00244             break;
00245           case 0:
00246             if (NqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,-c)
00247                 == ES_FAILED) home->fail();
00248             break;
00249           default:
00250             assert(0);
00251           }
00252           break;
00253         default:
00254           assert(0);
00255         }
00256       } else if (n == 3) {
00257         switch (r) {                                            
00258         case IRT_LQ:
00259           switch (n_p) {
00260           case 3:
00261             if (LqTer<int,IntView,IntView,IntView>::post
00262                 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00263             break;
00264           case 2:
00265             if (LqTer<int,IntView,IntView,MinusView>::post
00266                 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00267             break;
00268           case 1:
00269             if (LqTer<int,IntView,MinusView,MinusView>::post
00270                 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00271             break;
00272           case 0:
00273             if (LqTer<int,MinusView,MinusView,MinusView>::post
00274                 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00275             break;
00276           default:
00277             assert(0);
00278           }
00279           break;
00280         case IRT_EQ:
00281           switch (n_p) {
00282           case 3:
00283             if (EqTer<int,IntView,IntView,IntView>::post
00284                 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00285             break;
00286           case 2:
00287             if (EqTer<int,IntView,IntView,MinusView>::post
00288                 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00289             break;
00290           case 1:
00291             if (EqTer<int,IntView,IntView,MinusView>::post
00292                 (home,e[1].x,e[2].x,e[0].x,-c) == ES_FAILED) home->fail();
00293             break;
00294           case 0:
00295             if (EqTer<int,IntView,IntView,IntView>::post
00296                 (home,e[0].x,e[1].x,e[2].x,-c) == ES_FAILED) home->fail();
00297             break;
00298           default:
00299             assert(0);
00300           }
00301           break;
00302         case IRT_NQ:
00303           switch (n_p) {
00304           case 3:
00305             if (NqTer<int,IntView,IntView,IntView>::post
00306               (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00307             break;
00308           case 2:
00309             if (NqTer<int,IntView,IntView,MinusView>::post
00310               (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00311             break;
00312           case 1:
00313             if (NqTer<int,IntView,IntView,MinusView>::post
00314               (home,e[1].x,e[2].x,e[0].x,-c) == ES_FAILED) home->fail();
00315             break;
00316           case 0:
00317             if (NqTer<int,IntView,IntView,IntView>::post
00318               (home,e[0].x,e[1].x,e[2].x,-c) == ES_FAILED) home->fail();
00319             break;
00320           default:
00321             assert(0);
00322           }
00323           break;
00324         default:
00325           assert(0);
00326         }
00327       } else {
00328         ViewArray<IntView> x(home,n_p);
00329         for (int i = n_p; i--; ) x[i] = e[i].x;
00330         ViewArray<IntView> y(home,n_n);
00331         for (int i = n_n; i--; ) y[i] = e[i+n_p].x;
00332         post_nary<int,IntView>(home,x,y,r,c);
00333       }
00334     } else {
00335       if (is_ip) {
00336         ViewArray<IntScaleView> x(home,n_p);
00337         for (int i = n_p; i--; )
00338           x[i].init(e[i].a,e[i].x);
00339         ViewArray<IntScaleView> y(home,n_n);
00340         for (int i = n_n; i--; )
00341           y[i].init(-e[i+n_p].a,e[i+n_p].x);
00342         if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00343           if (DomEq<int,IntScaleView>::post(home,x,y,c) == ES_FAILED)
00344             home->fail();
00345         } else {
00346           post_nary<int,IntScaleView>(home,x,y,r,c);
00347         }
00348       } else {
00349         ViewArray<DoubleScaleView> x(home,n_p);
00350         for (int i = n_p; i--; )
00351           x[i].init(e[i].a,e[i].x);
00352         ViewArray<DoubleScaleView> y(home,n_n);
00353         for (int i = n_n; i--; )
00354           y[i].init(-e[i+n_p].a,e[i+n_p].x);
00355         if ((icl == ICL_DOM) && (r == IRT_EQ)) {
00356           if (DomEq<double,DoubleScaleView>::post(home,x,y,c) == ES_FAILED)
00357             home->fail();
00358         } else {
00359           post_nary<double,DoubleScaleView>(home,x,y,r,c);
00360         }
00361       }
00362     }
00363   }
00364 
00365 
00366 
00367   /*
00368    * Posting reified propagators
00369    *
00370    */
00371 
00372   template <class Val, class View>
00373   forceinline void
00374   post_nary(Space* home,
00375             ViewArray<View>& x, ViewArray<View>& y, IntRelType r, Val c, BoolView b) {
00376     switch (r) {
00377     case IRT_LQ:
00378       if (ReLq<Val,View,View>::post(home,x,y,c,b) == ES_FAILED)
00379         home->fail();
00380       break;
00381     case IRT_EQ:
00382       if (ReEq<Val,View,View,BoolView>::post(home,x,y,c,b) == ES_FAILED)
00383         home->fail();
00384       break;
00385     case IRT_NQ: 
00386       {
00387         NegBoolView n(b);
00388         if (ReEq<Val,View,View,NegBoolView>::post(home,x,y,c,n) == ES_FAILED)
00389           home->fail();
00390       }
00391       break;
00392     default:
00393       assert(0);
00394     }
00395   }
00396 
00397   void
00398   post(Space* home,
00399        Term e[], int n, IntRelType r, int c, BoolView b) {
00400     int n_p, n_n;
00401     bool is_unit = preprocess(e,n,r,c,n_p,n_n);
00402     if (n == 0) {
00403       bool fail = false;
00404       switch (r) {
00405       case IRT_EQ: fail = (c != 0); break;
00406       case IRT_NQ: fail = (c == 0); break;
00407       case IRT_LQ: fail = (0 > c);  break;
00408       default: assert(0);
00409       }
00410       if ((fail ? b.t_zero(home) : b.t_one(home)) == ME_INT_FAILED)
00411         home->fail();
00412       return;
00413     }
00414     bool is_ip  = int_precision(e,n,c);
00415     if (is_unit && is_ip) {
00416       if (n == 1) {
00417         switch (r) {
00418         case IRT_EQ: 
00419           if (e[0].a == 1) {
00420             if (Rel::ReEqBndInt<IntView,BoolView>::post(home,e[0].x,c,b)
00421                 == ES_FAILED)
00422               home->fail();
00423           } else {
00424             if (Rel::ReEqBndInt<IntView,BoolView>::post(home,e[0].x,-c,b)
00425                 == ES_FAILED)
00426               home->fail();
00427           }
00428           break;
00429         case IRT_NQ:
00430           {
00431             NegBoolView n(b);
00432             if (e[0].a == 1) {
00433               if (Rel::ReEqBndInt<IntView,NegBoolView>::post(home,e[0].x,c,n)
00434                   == ES_FAILED)
00435                 home->fail();
00436             } else {
00437               if (Rel::ReEqBndInt<IntView,NegBoolView>::post(home,e[0].x,-c,n)
00438                   == ES_FAILED)
00439                 home->fail();
00440             }
00441           }
00442           break;
00443         case IRT_LQ:
00444           if (e[0].a == 1) {
00445             if (Rel::ReLqInt<IntView,BoolView>::post(home,e[0].x,c,b) 
00446                 == ES_FAILED)
00447               home->fail();
00448           } else {
00449             NegBoolView n(b);
00450             if (Rel::ReLqInt<IntView,NegBoolView>::post(home,e[0].x,-c-1,n)
00451                 == ES_FAILED)
00452               home->fail();
00453           }
00454           break;
00455         default: 
00456           assert(false);
00457         }
00458       } else if (n == 2) {
00459         switch (r) {
00460         case IRT_LQ:
00461           switch (n_p) {
00462           case 2:
00463             if (ReLqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,c,b)
00464                 == ES_FAILED) home->fail();
00465             break;
00466           case 1:
00467             if (ReLqBin<int,IntView,MinusView>::post(home,e[0].x,e[1].x,c,b)
00468                 == ES_FAILED) home->fail();
00469             break;
00470           case 0:
00471             if (ReLqBin<int,MinusView,MinusView>::post(home,e[0].x,e[1].x,c,b)
00472                 == ES_FAILED) home->fail();
00473             break;
00474           default:
00475             assert(0);
00476           }
00477           break;
00478         case IRT_EQ:
00479           switch (n_p) {
00480           case 2:
00481             if (ReEqBin<int,IntView,IntView,BoolView>::post
00482                 (home,e[0].x,e[1].x,c,b)
00483                 == ES_FAILED) home->fail();
00484             break;
00485           case 1:
00486             if (ReEqBin<int,IntView,MinusView,BoolView>::post
00487                 (home,e[0].x,e[1].x,c,b)
00488                 == ES_FAILED) home->fail();
00489             break;
00490           case 0:
00491             if (ReEqBin<int,IntView,IntView,BoolView>::post
00492                 (home,e[0].x,e[1].x,-c,b)
00493                 == ES_FAILED) home->fail();
00494             break;
00495           default:
00496             assert(0);
00497           }
00498           break;
00499         case IRT_NQ:
00500           {
00501             NegBoolView n(b);
00502             switch (n_p) {
00503             case 2:
00504               if (ReEqBin<int,IntView,IntView,NegBoolView>::post
00505                   (home,e[0].x,e[1].x,c,n)
00506                   == ES_FAILED) home->fail();
00507               break;
00508             case 1:
00509               if (ReEqBin<int,IntView,MinusView,NegBoolView>::post
00510                   (home,e[0].x,e[1].x,c,b)
00511                   == ES_FAILED) home->fail();
00512               break;
00513             case 0:
00514               if (ReEqBin<int,IntView,IntView,NegBoolView>::post
00515                   (home,e[0].x,e[1].x,-c,b)
00516                   == ES_FAILED) home->fail();
00517               break;
00518             default:
00519               assert(0);
00520             }
00521           }
00522           break;
00523         default:
00524           assert(0);
00525         }
00526       } else {
00527         ViewArray<IntView> x(home,n_p);
00528         for (int i = n_p; i--; ) x[i] = e[i].x;
00529         ViewArray<IntView> y(home,n_n);
00530         for (int i = n_n; i--; ) y[i] = e[i+n_p].x;
00531         post_nary<int,IntView>(home,x,y,r,c,b);
00532       }
00533     } else {
00534       if (is_ip) {
00535         ViewArray<IntScaleView> x(home,n_p);
00536         for (int i = n_p; i--; )
00537           x[i].init(e[i].a,e[i].x);
00538         ViewArray<IntScaleView> y(home,n_n);
00539         for (int i = n_n; i--; )
00540           y[i].init(-e[i+n_p].a,e[i+n_p].x);
00541         post_nary<int,IntScaleView>(home,x,y,r,c,b);
00542       } else {
00543         ViewArray<DoubleScaleView> x(home,n_p);
00544         for (int i = n_p; i--; )
00545           x[i].init(e[i].a,e[i].x);
00546         ViewArray<DoubleScaleView> y(home,n_n);
00547         for (int i = n_n; i--; )
00548           y[i].init(-e[i+n_p].a,e[i+n_p].x);
00549         post_nary<double,DoubleScaleView>(home,x,y,r,c,b);
00550       }
00551     }
00552   }
00553 
00554 }}}
00555 
00556 // STATISTICS: int-post
00557