Generated on Fri Oct 19 11:25:07 2018 for Gecode by doxygen 1.6.3

bool-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  *     Tias Guns <tias.guns@cs.kuleuven.be>
00006  *
00007  *  Copyright:
00008  *     Christian Schulte, 2002
00009  *     Tias Guns, 2009
00010  *
00011  *  This file is part of Gecode, the generic constraint
00012  *  development environment:
00013  *     http://www.gecode.org
00014  *
00015  *  Permission is hereby granted, free of charge, to any person obtaining
00016  *  a copy of this software and associated documentation files (the
00017  *  "Software"), to deal in the Software without restriction, including
00018  *  without limitation the rights to use, copy, modify, merge, publish,
00019  *  distribute, sublicense, and/or sell copies of the Software, and to
00020  *  permit persons to whom the Software is furnished to do so, subject to
00021  *  the following conditions:
00022  *
00023  *  The above copyright notice and this permission notice shall be
00024  *  included in all copies or substantial portions of the Software.
00025  *
00026  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00027  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00028  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00029  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00030  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00031  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00032  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00033  *
00034  */
00035 
00036 #include <gecode/int/linear.hh>
00037 #include <gecode/int/div.hh>
00038 
00039 namespace Gecode { namespace Int { namespace Linear {
00040 
00042   forceinline void
00043   eliminate(Term<BoolView>* t, int &n, long long int& d) {
00044     for (int i=n; i--; )
00045       if (t[i].x.one()) {
00046         d -= t[i].a; t[i]=t[--n];
00047       } else if (t[i].x.zero()) {
00048         t[i]=t[--n];
00049       }
00050     Limits::check(d,"Int::linear");
00051   }
00052 
00054   forceinline void
00055   rewrite(IntRelType &r, long long int &d) {
00056       switch (r) {
00057       case IRT_EQ: case IRT_NQ: case IRT_LQ: case IRT_GQ:
00058         break;
00059       case IRT_LE:
00060         d--; r = IRT_LQ; break;
00061       case IRT_GR:
00062         d++; r = IRT_GQ; break;
00063       default:
00064         throw UnknownRelation("Int::linear");
00065       }
00066   }
00067 
00068   forceinline void
00069   post_pos_unit(Home home,
00070                 Term<BoolView>* t_p, int n_p,
00071                 IntRelType irt, IntView y, int c) {
00072     switch (irt) {
00073     case IRT_EQ:
00074       {
00075         ViewArray<BoolView> x(home,n_p);
00076         for (int i=0; i<n_p; i++)
00077           x[i]=t_p[i].x;
00078         GECODE_ES_FAIL((EqBoolView<BoolView,IntView>
00079                              ::post(home,x,y,c)));
00080       }
00081       break;
00082     case IRT_NQ:
00083       {
00084         ViewArray<BoolView> x(home,n_p);
00085         for (int i=0; i<n_p; i++)
00086           x[i]=t_p[i].x;
00087         GECODE_ES_FAIL((NqBoolView<BoolView,IntView>
00088                              ::post(home,x,y,c)));
00089       }
00090       break;
00091     case IRT_GQ:
00092       {
00093         ViewArray<BoolView> x(home,n_p);
00094         for (int i=0; i<n_p; i++)
00095           x[i]=t_p[i].x;
00096         GECODE_ES_FAIL((GqBoolView<BoolView,IntView>
00097                              ::post(home,x,y,c)));
00098       }
00099       break;
00100     case IRT_LQ:
00101       {
00102         ViewArray<NegBoolView> x(home,n_p);
00103         for (int i=0; i<n_p; i++)
00104           x[i]=NegBoolView(t_p[i].x);
00105         MinusView z(y);
00106         GECODE_ES_FAIL((GqBoolView<NegBoolView,MinusView>
00107                              ::post(home,x,z,n_p-c)));
00108       }
00109       break;
00110     default: GECODE_NEVER;
00111     }
00112   }
00113 
00114   forceinline void
00115   post_pos_unit(Home home,
00116                 Term<BoolView>* t_p, int n_p,
00117                 IntRelType irt, ZeroIntView, int c) {
00118     switch (irt) {
00119     case IRT_EQ:
00120       {
00121         ViewArray<BoolView> x(home,n_p);
00122         for (int i=0; i<n_p; i++)
00123           x[i]=t_p[i].x;
00124         GECODE_ES_FAIL((EqBoolInt<BoolView>::post(home,x,c)));
00125       }
00126       break;
00127     case IRT_NQ:
00128       {
00129         ViewArray<BoolView> x(home,n_p);
00130         for (int i=0; i<n_p; i++)
00131           x[i]=t_p[i].x;
00132         GECODE_ES_FAIL((NqBoolInt<BoolView>::post(home,x,c)));
00133       }
00134       break;
00135     case IRT_GQ:
00136       {
00137         ViewArray<BoolView> x(home,n_p);
00138         for (int i=0; i<n_p; i++)
00139           x[i]=t_p[i].x;
00140         GECODE_ES_FAIL((GqBoolInt<BoolView>::post(home,x,c)));
00141       }
00142       break;
00143     case IRT_LQ:
00144       {
00145         ViewArray<NegBoolView> x(home,n_p);
00146         for (int i=0; i<n_p; i++)
00147           x[i]=NegBoolView(t_p[i].x);
00148         GECODE_ES_FAIL((GqBoolInt<NegBoolView>::post(home,x,n_p-c)));
00149       }
00150       break;
00151     default: GECODE_NEVER;
00152     }
00153   }
00154 
00155   forceinline void
00156   post_pos_unit(Home home,
00157                 Term<BoolView>* t_p, int n_p,
00158                 IntRelType irt, int c, Reify r,
00159                 IntPropLevel) {
00160     switch (irt) {
00161     case IRT_EQ:
00162       {
00163         ViewArray<BoolView> x(home,n_p);
00164         for (int i=0; i<n_p; i++)
00165           x[i]=t_p[i].x;
00166         switch (r.mode()) {
00167         case RM_EQV:
00168           GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView,RM_EQV>::
00169                           post(home,x,c,r.var())));
00170           break;
00171         case RM_IMP:
00172           GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView,RM_IMP>::
00173                           post(home,x,c,r.var())));
00174           break;
00175         case RM_PMI:
00176           GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView,RM_PMI>::
00177                           post(home,x,c,r.var())));
00178           break;
00179         default: GECODE_NEVER;
00180         }
00181       }
00182       break;
00183     case IRT_NQ:
00184       {
00185         ViewArray<BoolView> x(home,n_p);
00186         for (int i=0; i<n_p; i++)
00187           x[i]=t_p[i].x;
00188         NegBoolView nb(r.var());
00189         switch (r.mode()) {
00190         case RM_EQV:
00191           GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView,RM_EQV>::
00192                           post(home,x,c,nb)));
00193           break;
00194         case RM_IMP:
00195           GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView,RM_PMI>::
00196                           post(home,x,c,nb)));
00197           break;
00198         case RM_PMI:
00199           GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView,RM_IMP>::
00200                           post(home,x,c,nb)));
00201           break;
00202         default: GECODE_NEVER;
00203         }
00204       }
00205       break;
00206     case IRT_GQ:
00207       {
00208         ViewArray<BoolView> x(home,n_p);
00209         for (int i=0; i<n_p; i++)
00210           x[i]=t_p[i].x;
00211         switch (r.mode()) {
00212         case RM_EQV:
00213           GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView,RM_EQV>::
00214                           post(home,x,c,r.var())));
00215           break;
00216         case RM_IMP:
00217           GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView,RM_IMP>::
00218                           post(home,x,c,r.var())));
00219           break;
00220         case RM_PMI:
00221           GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView,RM_PMI>::
00222                           post(home,x,c,r.var())));
00223           break;
00224         default: GECODE_NEVER;
00225         }
00226       }
00227       break;
00228     case IRT_LQ:
00229       {
00230         ViewArray<NegBoolView> x(home,n_p);
00231         for (int i=0; i<n_p; i++)
00232           x[i]=NegBoolView(t_p[i].x);
00233         switch (r.mode()) {
00234         case RM_EQV:
00235           GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView,RM_EQV>::
00236                           post(home,x,n_p-c,r.var())));
00237           break;
00238         case RM_IMP:
00239           GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView,RM_IMP>::
00240                           post(home,x,n_p-c,r.var())));
00241           break;
00242         case RM_PMI:
00243           GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView,RM_PMI>::
00244                           post(home,x,n_p-c,r.var())));
00245           break;
00246         default: GECODE_NEVER;
00247         }
00248       }
00249       break;
00250     default: GECODE_NEVER;
00251     }
00252   }
00253 
00254   forceinline void
00255   post_neg_unit(Home home,
00256                 Term<BoolView>* t_n, int n_n,
00257                 IntRelType irt, IntView y, int c) {
00258     switch (irt) {
00259     case IRT_EQ:
00260       {
00261         ViewArray<BoolView> x(home,n_n);
00262         for (int i=0; i<n_n; i++)
00263           x[i]=t_n[i].x;
00264         MinusView z(y);
00265         GECODE_ES_FAIL((EqBoolView<BoolView,MinusView>
00266                         ::post(home,x,z,-c)));
00267       }
00268       break;
00269     case IRT_NQ:
00270       {
00271         ViewArray<BoolView> x(home,n_n);
00272         for (int i=0; i<n_n; i++)
00273           x[i]=t_n[i].x;
00274         MinusView z(y);
00275         GECODE_ES_FAIL((NqBoolView<BoolView,MinusView>
00276                         ::post(home,x,z,-c)));
00277       }
00278       break;
00279     case IRT_GQ:
00280       {
00281         ViewArray<NegBoolView> x(home,n_n);
00282         for (int i=0; i<n_n; i++)
00283           x[i]=NegBoolView(t_n[i].x);
00284         GECODE_ES_FAIL((GqBoolView<NegBoolView,IntView>
00285                         ::post(home,x,y,n_n+c)));
00286       }
00287       break;
00288     case IRT_LQ:
00289       {
00290         ViewArray<BoolView> x(home,n_n);
00291         for (int i=0; i<n_n; i++)
00292           x[i]=t_n[i].x;
00293         MinusView z(y);
00294         GECODE_ES_FAIL((GqBoolView<BoolView,MinusView>
00295                         ::post(home,x,z,-c)));
00296       }
00297       break;
00298     default: GECODE_NEVER;
00299     }
00300   }
00301 
00302   forceinline void
00303   post_neg_unit(Home home,
00304                 Term<BoolView>* t_n, int n_n,
00305                 IntRelType irt, ZeroIntView, int c) {
00306     switch (irt) {
00307     case IRT_EQ:
00308       {
00309         ViewArray<BoolView> x(home,n_n);
00310         for (int i=0; i<n_n; i++)
00311           x[i]=t_n[i].x;
00312         GECODE_ES_FAIL((EqBoolInt<BoolView>::post(home,x,-c)));
00313       }
00314       break;
00315     case IRT_NQ:
00316       {
00317         ViewArray<BoolView> x(home,n_n);
00318         for (int i=0; i<n_n; i++)
00319           x[i]=t_n[i].x;
00320         GECODE_ES_FAIL((NqBoolInt<BoolView>::post(home,x,-c)));
00321       }
00322       break;
00323     case IRT_GQ:
00324       {
00325         ViewArray<NegBoolView> x(home,n_n);
00326         for (int i=0; i<n_n; i++)
00327           x[i]=NegBoolView(t_n[i].x);
00328         GECODE_ES_FAIL((GqBoolInt<NegBoolView>::post(home,x,n_n+c)));
00329       }
00330       break;
00331     case IRT_LQ:
00332       {
00333         ViewArray<BoolView> x(home,n_n);
00334         for (int i=0; i<n_n; i++)
00335           x[i]=t_n[i].x;
00336         GECODE_ES_FAIL((GqBoolInt<BoolView>::post(home,x,-c)));
00337       }
00338       break;
00339     default: GECODE_NEVER;
00340     }
00341   }
00342 
00343   forceinline void
00344   post_neg_unit(Home home,
00345                 Term<BoolView>* t_n, int n_n,
00346                 IntRelType irt, int c, Reify r,
00347                 IntPropLevel) {
00348     switch (irt) {
00349     case IRT_EQ:
00350       {
00351         ViewArray<BoolView> x(home,n_n);
00352         for (int i=0; i<n_n; i++)
00353           x[i]=t_n[i].x;
00354         switch (r.mode()) {
00355         case RM_EQV:
00356           GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView,RM_EQV>::
00357                           post(home,x,-c,r.var())));
00358           break;
00359         case RM_IMP:
00360           GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView,RM_IMP>::
00361                           post(home,x,-c,r.var())));
00362           break;
00363         case RM_PMI:
00364           GECODE_ES_FAIL((ReEqBoolInt<BoolView,BoolView,RM_PMI>::
00365                           post(home,x,-c,r.var())));
00366           break;
00367         default: GECODE_NEVER;
00368         }
00369       }
00370       break;
00371     case IRT_NQ:
00372       {
00373         ViewArray<BoolView> x(home,n_n);
00374         for (int i=0; i<n_n; i++)
00375           x[i]=t_n[i].x;
00376         NegBoolView nb(r.var());
00377         switch (r.mode()) {
00378         case RM_EQV:
00379           GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView,RM_EQV>::
00380                           post(home,x,-c,nb)));
00381           break;
00382         case RM_IMP:
00383           GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView,RM_PMI>::
00384                           post(home,x,-c,nb)));
00385           break;
00386         case RM_PMI:
00387           GECODE_ES_FAIL((ReEqBoolInt<BoolView,NegBoolView,RM_IMP>::
00388                           post(home,x,-c,nb)));
00389           break;
00390         default: GECODE_NEVER;
00391         }
00392       }
00393       break;
00394     case IRT_GQ:
00395       {
00396         ViewArray<NegBoolView> x(home,n_n);
00397         for (int i=0; i<n_n; i++)
00398           x[i]=NegBoolView(t_n[i].x);
00399         switch (r.mode()) {
00400         case RM_EQV:
00401           GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView,RM_EQV>::
00402                           post(home,x,n_n+c,r.var())));
00403           break;
00404         case RM_IMP:
00405           GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView,RM_IMP>::
00406                           post(home,x,n_n+c,r.var())));
00407           break;
00408         case RM_PMI:
00409           GECODE_ES_FAIL((ReGqBoolInt<NegBoolView,BoolView,RM_PMI>::
00410                           post(home,x,n_n+c,r.var())));
00411           break;
00412         default: GECODE_NEVER;
00413         }
00414       }
00415       break;
00416     case IRT_LQ:
00417       {
00418         ViewArray<BoolView> x(home,n_n);
00419         for (int i=0; i<n_n; i++)
00420           x[i]=t_n[i].x;
00421         switch (r.mode()) {
00422         case RM_EQV:
00423           GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView,RM_EQV>::
00424                           post(home,x,-c,r.var())));
00425           break;
00426         case RM_IMP:
00427           GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView,RM_IMP>::
00428                           post(home,x,-c,r.var())));
00429           break;
00430         case RM_PMI:
00431           GECODE_ES_FAIL((ReGqBoolInt<BoolView,BoolView,RM_PMI>::
00432                           post(home,x,-c,r.var())));
00433           break;
00434         default: GECODE_NEVER;
00435         }
00436       }
00437       break;
00438     default: GECODE_NEVER;
00439     }
00440   }
00441 
00442   forceinline void
00443   post_mixed(Home home,
00444              Term<BoolView>* t_p, int n_p,
00445              Term<BoolView>* t_n, int n_n,
00446              IntRelType irt, IntView y, int c) {
00447     ScaleBoolArray b_p(home,n_p);
00448     {
00449       ScaleBool* f=b_p.fst();
00450       for (int i=0; i<n_p; i++) {
00451         f[i].x=t_p[i].x; f[i].a=t_p[i].a;
00452       }
00453     }
00454     ScaleBoolArray b_n(home,n_n);
00455     {
00456       ScaleBool* f=b_n.fst();
00457       for (int i=0; i<n_n; i++) {
00458         f[i].x=t_n[i].x; f[i].a=t_n[i].a;
00459       }
00460     }
00461     switch (irt) {
00462     case IRT_EQ:
00463       GECODE_ES_FAIL((EqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView>
00464                       ::post(home,b_p,b_n,y,c)));
00465       break;
00466     case IRT_NQ:
00467       GECODE_ES_FAIL((NqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView>
00468                       ::post(home,b_p,b_n,y,c)));
00469       break;
00470     case IRT_LQ:
00471       GECODE_ES_FAIL((LqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView>
00472                       ::post(home,b_p,b_n,y,c)));
00473       break;
00474     case IRT_GQ:
00475       {
00476         MinusView m(y);
00477         GECODE_ES_FAIL((LqBoolScale<ScaleBoolArray,ScaleBoolArray,MinusView>
00478                         ::post(home,b_n,b_p,m,-c)));
00479       }
00480       break;
00481     default:
00482       GECODE_NEVER;
00483     }
00484   }
00485 
00486 
00487   forceinline void
00488   post_mixed(Home home,
00489              Term<BoolView>* t_p, int n_p,
00490              Term<BoolView>* t_n, int n_n,
00491              IntRelType irt, ZeroIntView y, int c) {
00492     ScaleBoolArray b_p(home,n_p);
00493     {
00494       ScaleBool* f=b_p.fst();
00495       for (int i=0; i<n_p; i++) {
00496         f[i].x=t_p[i].x; f[i].a=t_p[i].a;
00497       }
00498     }
00499     ScaleBoolArray b_n(home,n_n);
00500     {
00501       ScaleBool* f=b_n.fst();
00502       for (int i=0; i<n_n; i++) {
00503         f[i].x=t_n[i].x; f[i].a=t_n[i].a;
00504       }
00505     }
00506     switch (irt) {
00507     case IRT_EQ:
00508       GECODE_ES_FAIL(
00509                      (EqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
00510                       ::post(home,b_p,b_n,y,c)));
00511       break;
00512     case IRT_NQ:
00513       GECODE_ES_FAIL(
00514                      (NqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
00515                       ::post(home,b_p,b_n,y,c)));
00516       break;
00517     case IRT_LQ:
00518       GECODE_ES_FAIL(
00519                      (LqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
00520                       ::post(home,b_p,b_n,y,c)));
00521       break;
00522     case IRT_GQ:
00523       GECODE_ES_FAIL(
00524                      (LqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
00525                       ::post(home,b_n,b_p,y,-c)));
00526       break;
00527     default:
00528       GECODE_NEVER;
00529     }
00530   }
00531 
00532   template<class View>
00533   forceinline void
00534   post_all(Home home,
00535            Term<BoolView>* t, int n,
00536            IntRelType irt, View x, int c) {
00537 
00538     Limits::check(c,"Int::linear");
00539 
00540     long long int d = c;
00541 
00542     eliminate(t,n,d);
00543 
00544     Term<BoolView> *t_p, *t_n;
00545     int n_p, n_n, gcd=0;
00546     bool unit = normalize<BoolView>(t,n,t_p,n_p,t_n,n_n,gcd);
00547 
00548     rewrite(irt,d);
00549 
00550     c = static_cast<int>(d);
00551 
00552     if (n == 0) {
00553       switch (irt) {
00554       case IRT_EQ: GECODE_ME_FAIL(x.eq(home,-c)); break;
00555       case IRT_NQ: GECODE_ME_FAIL(x.nq(home,-c)); break;
00556       case IRT_GQ: GECODE_ME_FAIL(x.lq(home,-c)); break;
00557       case IRT_LQ: GECODE_ME_FAIL(x.gq(home,-c)); break;
00558       default: GECODE_NEVER;
00559       }
00560       return;
00561     }
00562 
00563     // Check for overflow
00564     {
00565       long long int sl = static_cast<long long int>(x.max())+c;
00566       long long int su = static_cast<long long int>(x.min())+c;
00567       for (int i=0; i<n_p; i++)
00568         su -= t_p[i].a;
00569       for (int i=0; i<n_n; i++)
00570         sl += t_n[i].a;
00571       Limits::check(sl,"Int::linear");
00572       Limits::check(su,"Int::linear");
00573     }
00574 
00575     if (unit && (n_n == 0)) {
00577       post_pos_unit(home,t_p,n_p,irt,x,c);
00578     } else if (unit && (n_p == 0)) {
00579       // All coefficients are -1
00580       post_neg_unit(home,t_n,n_n,irt,x,c);
00581     } else {
00582       // Mixed coefficients
00583       post_mixed(home,t_p,n_p,t_n,n_n,irt,x,c);
00584     }
00585   }
00586 
00587 
00588   void
00589   post(Home home,
00590        Term<BoolView>* t, int n, IntRelType irt, IntView x, int c,
00591        IntPropLevel) {
00592     post_all(home,t,n,irt,x,c);
00593   }
00594 
00595   void
00596   post(Home home,
00597        Term<BoolView>* t, int n, IntRelType irt, int c,
00598        IntPropLevel) {
00599     ZeroIntView x;
00600     post_all(home,t,n,irt,x,c);
00601   }
00602 
00603   void
00604   post(Home home,
00605        Term<BoolView>* t, int n, IntRelType irt, IntView x, Reify r,
00606        IntPropLevel ipl) {
00607     int l, u;
00608     estimate(t,n,0,l,u);
00609     IntVar z(home,l,u); IntView zv(z);
00610     post_all(home,t,n,IRT_EQ,zv,0);
00611     rel(home,z,irt,x,r,ipl);
00612   }
00613 
00614   void
00615   post(Home home,
00616        Term<BoolView>* t, int n, IntRelType irt, int c, Reify r,
00617        IntPropLevel ipl) {
00618 
00619     if (r.var().one()) {
00620       if (r.mode() != RM_PMI)
00621         post(home,t,n,irt,c,ipl);
00622       return;
00623     }
00624     if (r.var().zero()) {
00625       if (r.mode() != RM_IMP)
00626         post(home,t,n,neg(irt),c,ipl);
00627       return;
00628     }
00629 
00630     Limits::check(c,"Int::linear");
00631 
00632     long long int d = c;
00633 
00634     eliminate(t,n,d);
00635 
00636     Term<BoolView> *t_p, *t_n;
00637     int n_p, n_n, gcd=1;
00638     bool unit = normalize<BoolView>(t,n,t_p,n_p,t_n,n_n,gcd);
00639 
00640     rewrite(irt,d);
00641 
00642     // Divide by gcd
00643     if (gcd > 1) {
00644       switch (irt) {
00645       case IRT_EQ:
00646         if ((d % gcd) != 0) {
00647           if (r.mode() != RM_PMI)
00648             GECODE_ME_FAIL(BoolView(r.var()).zero(home));
00649           return;
00650         }
00651         d /= gcd;
00652         break;
00653       case IRT_NQ:
00654         if ((d % gcd) == 0) {
00655           if (r.mode() != RM_IMP)
00656             GECODE_ME_FAIL(BoolView(r.var()).one(home));
00657           return;
00658         }
00659         d /= gcd;
00660         break;
00661       case IRT_LQ:
00662         d = floor_div_xp(d,static_cast<long long int>(gcd));
00663         break;
00664       case IRT_GQ:
00665         d = ceil_div_xp(d,static_cast<long long int>(gcd));
00666         break;
00667       default: GECODE_NEVER;
00668       }
00669     }
00670 
00671     c = static_cast<int>(d);
00672 
00673     if (n == 0) {
00674       bool fail = false;
00675       switch (irt) {
00676       case IRT_EQ: fail = (0 != c); break;
00677       case IRT_NQ: fail = (0 == c); break;
00678       case IRT_GQ: fail = (0 < c); break;
00679       case IRT_LQ: fail = (0 > c); break;
00680       default: GECODE_NEVER;
00681       }
00682       if (fail) {
00683         if (r.mode() != RM_PMI)
00684           GECODE_ME_FAIL(BoolView(r.var()).zero(home));
00685       } else {
00686         if (r.mode() != RM_IMP)
00687           GECODE_ME_FAIL(BoolView(r.var()).one(home));
00688       }
00689       return;
00690     }
00691 
00692     // Check for overflow
00693     {
00694       long long int sl = c;
00695       long long int su = c;
00696       for (int i=0; i<n_p; i++)
00697         su -= t_p[i].a;
00698       for (int i=0; i<n_n; i++)
00699         sl += t_n[i].a;
00700       Limits::check(sl,"Int::linear");
00701       Limits::check(su,"Int::linear");
00702     }
00703 
00704     if (unit && (n_n == 0)) {
00706       post_pos_unit(home,t_p,n_p,irt,c,r,ipl);
00707     } else if (unit && (n_p == 0)) {
00708       // All coefficients are -1
00709       post_neg_unit(home,t_n,n_n,irt,c,r,ipl);
00710     } else {
00711       // Mixed coefficients
00712       /*
00713        * Denormalize: Make all t_n coefficients negative again
00714        * (t_p and t_n are shared in t)
00715        */
00716       for (int i=0; i<n_n; i++)
00717         t_n[i].a = -t_n[i].a;
00718 
00719       // Note: still slow implementation
00720       int l, u;
00721       estimate(t,n,0,l,u);
00722       IntVar z(home,l,u); IntView zv(z);
00723       post_all(home,t,n,IRT_EQ,zv,0);
00724       rel(home,z,irt,c,r,ipl);
00725     }
00726   }
00727 
00728 }}}
00729 
00730 // STATISTICS: int-post
00731