Generated on Wed Jan 4 17:49:11 2006 for Gecode by doxygen 1.4.6

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: 2005-11-01 16:35:02 +0100 (Tue, 01 Nov 2005) $ by $Author: schulte $
00010  *     $Revision: 2467 $
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 "int/rel.hh"
00023 #include "int/linear.hh"
00024 
00025 #include "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     int n_p, n_n;
00164     bool is_unit = preprocess(e,n,r,c,n_p,n_n);
00165     if (n == 0) {
00166       switch (r) {
00167       case IRT_EQ: if (c != 0) home->fail(); break;
00168       case IRT_NQ: if (c == 0) home->fail(); break;
00169       case IRT_LQ: if (0 > c)  home->fail(); break;
00170       default: assert(0);
00171       }
00172       return;
00173     }
00174     if (n == 1) {
00175       if (e[0].a > 0) {
00176         DoubleScaleView y(e[0].a,e[0].x);
00177         switch (r) {
00178         case IRT_EQ: GECODE_ME_FAIL(home,y.eq(home,c)); break;
00179         case IRT_NQ: GECODE_ME_FAIL(home,y.nq(home,c)); break;
00180         case IRT_LQ: GECODE_ME_FAIL(home,y.lq(home,c)); break;
00181         default: assert(0);
00182         }
00183       } else {
00184         DoubleScaleView y(-e[0].a,e[0].x);
00185         switch (r) {
00186         case IRT_EQ: GECODE_ME_FAIL(home,y.eq(home,-c)); break;
00187         case IRT_NQ: GECODE_ME_FAIL(home,y.nq(home,-c)); break;
00188         case IRT_LQ: GECODE_ME_FAIL(home,y.gq(home,-c)); break;
00189         default: assert(0);
00190         }
00191       }
00192       return;
00193     }
00194     bool is_ip = int_precision(e,n,c);
00195     if (is_unit && is_ip) {
00196       if (n == 2) {
00197         switch (r) {
00198         case IRT_LQ:
00199           switch (n_p) {
00200           case 2:
00201             if (LqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,c)
00202                 == ES_FAILED) home->fail();
00203             break;
00204           case 1:
00205             if (LqBin<int,IntView,MinusView>::post(home,e[0].x,e[1].x,c)
00206                 == ES_FAILED) home->fail();
00207             break;
00208           case 0:
00209             if (LqBin<int,MinusView,MinusView>::post(home,e[0].x,e[1].x,c)
00210                 == ES_FAILED) home->fail();
00211             break;
00212           default:
00213             assert(0);
00214           }
00215           break;
00216         case IRT_EQ:
00217           switch (n_p) {
00218           case 2:
00219             if (EqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,c)
00220                 == ES_FAILED) home->fail();
00221             break;
00222           case 1:
00223             if (EqBin<int,IntView,MinusView>::post(home,e[0].x,e[1].x,c)
00224                 == ES_FAILED) home->fail();
00225             break;
00226           case 0:
00227             if (EqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,-c)
00228                 == ES_FAILED) home->fail();
00229             break;
00230           default:
00231             assert(0);
00232           }
00233           break;
00234         case IRT_NQ:
00235           switch (n_p) {
00236           case 2:
00237             if (NqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,c)
00238                 == ES_FAILED) home->fail();
00239             break;
00240           case 1:
00241             if (NqBin<int,IntView,MinusView>::post(home,e[0].x,e[1].x,c)
00242                 == ES_FAILED) home->fail();
00243             break;
00244           case 0:
00245             if (NqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,-c)
00246                 == ES_FAILED) home->fail();
00247             break;
00248           default:
00249             assert(0);
00250           }
00251           break;
00252         default:
00253           assert(0);
00254         }
00255       } else if (n == 3) {
00256         switch (r) {                                            
00257         case IRT_LQ:
00258           switch (n_p) {
00259           case 3:
00260             if (LqTer<int,IntView,IntView,IntView>::post
00261                 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00262             break;
00263           case 2:
00264             if (LqTer<int,IntView,IntView,MinusView>::post
00265                 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00266             break;
00267           case 1:
00268             if (LqTer<int,IntView,MinusView,MinusView>::post
00269                 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00270             break;
00271           case 0:
00272             if (LqTer<int,MinusView,MinusView,MinusView>::post
00273                 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00274             break;
00275           default:
00276             assert(0);
00277           }
00278           break;
00279         case IRT_EQ:
00280           switch (n_p) {
00281           case 3:
00282             if (EqTer<int,IntView,IntView,IntView>::post
00283                 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00284             break;
00285           case 2:
00286             if (EqTer<int,IntView,IntView,MinusView>::post
00287                 (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00288             break;
00289           case 1:
00290             if (EqTer<int,IntView,IntView,MinusView>::post
00291                 (home,e[1].x,e[2].x,e[0].x,-c) == ES_FAILED) home->fail();
00292             break;
00293           case 0:
00294             if (EqTer<int,IntView,IntView,IntView>::post
00295                 (home,e[0].x,e[1].x,e[2].x,-c) == ES_FAILED) home->fail();
00296             break;
00297           default:
00298             assert(0);
00299           }
00300           break;
00301         case IRT_NQ:
00302           switch (n_p) {
00303           case 3:
00304             if (NqTer<int,IntView,IntView,IntView>::post
00305               (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00306             break;
00307           case 2:
00308             if (NqTer<int,IntView,IntView,MinusView>::post
00309               (home,e[0].x,e[1].x,e[2].x,c) == ES_FAILED) home->fail();
00310             break;
00311           case 1:
00312             if (NqTer<int,IntView,IntView,MinusView>::post
00313               (home,e[1].x,e[2].x,e[0].x,-c) == ES_FAILED) home->fail();
00314             break;
00315           case 0:
00316             if (NqTer<int,IntView,IntView,IntView>::post
00317               (home,e[0].x,e[1].x,e[2].x,-c) == ES_FAILED) home->fail();
00318             break;
00319           default:
00320             assert(0);
00321           }
00322           break;
00323         default:
00324           assert(0);
00325         }
00326       } else {
00327         ViewArray<IntView> x(home,n_p);
00328         for (int i = n_p; i--; ) x[i] = e[i].x;
00329         ViewArray<IntView> y(home,n_n);
00330         for (int i = n_n; i--; ) y[i] = e[i+n_p].x;
00331         post_nary<int,IntView>(home,x,y,r,c);
00332       }
00333     } else {
00334       if (is_ip) {
00335         ViewArray<IntScaleView> x(home,n_p);
00336         for (int i = n_p; i--; )
00337           x[i].init(e[i].a,e[i].x);
00338         ViewArray<IntScaleView> y(home,n_n);
00339         for (int i = n_n; i--; )
00340           y[i].init(-e[i+n_p].a,e[i+n_p].x);
00341         post_nary<int,IntScaleView>(home,x,y,r,c);
00342       } else {
00343         ViewArray<DoubleScaleView> x(home,n_p);
00344         for (int i = n_p; i--; )
00345           x[i].init(e[i].a,e[i].x);
00346         ViewArray<DoubleScaleView> y(home,n_n);
00347         for (int i = n_n; i--; )
00348           y[i].init(-e[i+n_p].a,e[i+n_p].x);
00349         post_nary<double,DoubleScaleView>(home,x,y,r,c);
00350       }
00351     }
00352   }
00353 
00354 
00355 
00356   /*
00357    * Posting reified propagators
00358    *
00359    */
00360 
00361   template <class Val, class View>
00362   forceinline void
00363   post_nary(Space* home,
00364             ViewArray<View>& x, ViewArray<View>& y, IntRelType r, Val c, BoolView b) {
00365     switch (r) {
00366     case IRT_LQ:
00367       if (ReLq<Val,View,View>::post(home,x,y,c,b) == ES_FAILED)
00368         home->fail();
00369       break;
00370     case IRT_EQ:
00371       if (ReEq<Val,View,View,BoolView>::post(home,x,y,c,b) == ES_FAILED)
00372         home->fail();
00373       break;
00374     case IRT_NQ: 
00375       {
00376         NegBoolView n(b);
00377         if (ReEq<Val,View,View,NegBoolView>::post(home,x,y,c,n) == ES_FAILED)
00378           home->fail();
00379       }
00380       break;
00381     default:
00382       assert(0);
00383     }
00384   }
00385 
00386   void
00387   post(Space* home,
00388        Term e[], int n, IntRelType r, int c, BoolView b) {
00389     int n_p, n_n;
00390     bool is_unit = preprocess(e,n,r,c,n_p,n_n);
00391     if (n == 0) {
00392       bool fail = false;
00393       switch (r) {
00394       case IRT_EQ: fail = (c != 0); break;
00395       case IRT_NQ: fail = (c == 0); break;
00396       case IRT_LQ: fail = (0 > c);  break;
00397       default: assert(0);
00398       }
00399       if ((fail ? b.t_zero(home) : b.t_one(home)) == ME_INT_FAILED)
00400         home->fail();
00401       return;
00402     }
00403     bool is_ip  = int_precision(e,n,c);
00404     if (is_unit && is_ip) {
00405       if (n == 1) {
00406         switch (r) {
00407         case IRT_EQ: 
00408           if (e[0].a == 1) {
00409             if (Rel::ReEqBndInt<IntView,BoolView>::post(home,e[0].x,c,b)
00410                 == ES_FAILED)
00411               home->fail();
00412           } else {
00413             if (Rel::ReEqBndInt<IntView,BoolView>::post(home,e[0].x,-c,b)
00414                 == ES_FAILED)
00415               home->fail();
00416           }
00417           break;
00418         case IRT_NQ:
00419           {
00420             NegBoolView n(b);
00421             if (e[0].a == 1) {
00422               if (Rel::ReEqBndInt<IntView,NegBoolView>::post(home,e[0].x,c,n)
00423                   == ES_FAILED)
00424                 home->fail();
00425             } else {
00426               if (Rel::ReEqBndInt<IntView,NegBoolView>::post(home,e[0].x,-c,n)
00427                   == ES_FAILED)
00428                 home->fail();
00429             }
00430           }
00431           break;
00432         case IRT_LQ:
00433           if (e[0].a == 1) {
00434             if (Rel::ReLqInt<IntView,BoolView>::post(home,e[0].x,c,b) 
00435                 == ES_FAILED)
00436               home->fail();
00437           } else {
00438             NegBoolView n(b);
00439             if (Rel::ReLqInt<IntView,NegBoolView>::post(home,e[0].x,-c-1,n)
00440                 == ES_FAILED)
00441               home->fail();
00442           }
00443           break;
00444         default: 
00445           assert(false);
00446         }
00447       } else if (n == 2) {
00448         switch (r) {
00449         case IRT_LQ:
00450           switch (n_p) {
00451           case 2:
00452             if (ReLqBin<int,IntView,IntView>::post(home,e[0].x,e[1].x,c,b)
00453                 == ES_FAILED) home->fail();
00454             break;
00455           case 1:
00456             if (ReLqBin<int,IntView,MinusView>::post(home,e[0].x,e[1].x,c,b)
00457                 == ES_FAILED) home->fail();
00458             break;
00459           case 0:
00460             if (ReLqBin<int,MinusView,MinusView>::post(home,e[0].x,e[1].x,c,b)
00461                 == ES_FAILED) home->fail();
00462             break;
00463           default:
00464             assert(0);
00465           }
00466           break;
00467         case IRT_EQ:
00468           switch (n_p) {
00469           case 2:
00470             if (ReEqBin<int,IntView,IntView,BoolView>::post
00471                 (home,e[0].x,e[1].x,c,b)
00472                 == ES_FAILED) home->fail();
00473             break;
00474           case 1:
00475             if (ReEqBin<int,IntView,MinusView,BoolView>::post
00476                 (home,e[0].x,e[1].x,c,b)
00477                 == ES_FAILED) home->fail();
00478             break;
00479           case 0:
00480             if (ReEqBin<int,IntView,IntView,BoolView>::post
00481                 (home,e[0].x,e[1].x,-c,b)
00482                 == ES_FAILED) home->fail();
00483             break;
00484           default:
00485             assert(0);
00486           }
00487           break;
00488         case IRT_NQ:
00489           {
00490             NegBoolView n(b);
00491             switch (n_p) {
00492             case 2:
00493               if (ReEqBin<int,IntView,IntView,NegBoolView>::post
00494                   (home,e[0].x,e[1].x,c,n)
00495                   == ES_FAILED) home->fail();
00496               break;
00497             case 1:
00498               if (ReEqBin<int,IntView,MinusView,NegBoolView>::post
00499                   (home,e[0].x,e[1].x,c,b)
00500                   == ES_FAILED) home->fail();
00501               break;
00502             case 0:
00503               if (ReEqBin<int,IntView,IntView,NegBoolView>::post
00504                   (home,e[0].x,e[1].x,-c,b)
00505                   == ES_FAILED) home->fail();
00506               break;
00507             default:
00508               assert(0);
00509             }
00510           }
00511           break;
00512         default:
00513           assert(0);
00514         }
00515       } else {
00516         ViewArray<IntView> x(home,n_p);
00517         for (int i = n_p; i--; ) x[i] = e[i].x;
00518         ViewArray<IntView> y(home,n_n);
00519         for (int i = n_n; i--; ) y[i] = e[i+n_p].x;
00520         post_nary<int,IntView>(home,x,y,r,c,b);
00521       }
00522     } else {
00523       if (is_ip) {
00524         ViewArray<IntScaleView> x(home,n_p);
00525         for (int i = n_p; i--; )
00526           x[i].init(e[i].a,e[i].x);
00527         ViewArray<IntScaleView> y(home,n_n);
00528         for (int i = n_n; i--; )
00529           y[i].init(-e[i+n_p].a,e[i+n_p].x);
00530         post_nary<int,IntScaleView>(home,x,y,r,c,b);
00531       } else {
00532         ViewArray<DoubleScaleView> x(home,n_p);
00533         for (int i = n_p; i--; )
00534           x[i].init(e[i].a,e[i].x);
00535         ViewArray<DoubleScaleView> y(home,n_n);
00536         for (int i = n_n; i--; )
00537           y[i].init(-e[i+n_p].a,e[i+n_p].x);
00538         post_nary<double,DoubleScaleView>(home,x,y,r,c,b);
00539       }
00540     }
00541   }
00542 
00543 }}}
00544 
00545 // STATISTICS: int-post
00546