bool-post.cc

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-06-11 11:39:04 +0200 (Wed, 11 Jun 2008) $ by $Author: tack $
00011  *     $Revision: 7094 $
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 "gecode/int/linear.hh"
00039 
00040 namespace Gecode { namespace Int { namespace Linear {
00041 
00042   void
00043   post_pos_unit(Space* home, 
00044                 Term<BoolView>* t_p, int n_p,
00045                 IntRelType r, IntView y, int c,
00046                 PropKind) {
00047     switch (r) {
00048     case IRT_EQ:
00049       {
00050         ViewArray<BoolView> x(home,n_p);
00051         for (int i=n_p; i--; )
00052           x[i]=t_p[i].x;
00053         GECODE_ES_FAIL(home,(EqBoolView<BoolView,IntView>
00054                              ::post(home,x,y,c)));
00055       }
00056       break;
00057     case IRT_NQ:
00058       {
00059         ViewArray<BoolView> x(home,n_p);
00060         for (int i=n_p; i--; )
00061           x[i]=t_p[i].x;
00062         GECODE_ES_FAIL(home,(NqBoolView<BoolView,IntView>
00063                              ::post(home,x,y,c)));
00064       }
00065       break;
00066     case IRT_GQ:
00067       {
00068         ViewArray<BoolView> x(home,n_p);
00069         for (int i=n_p; i--; )
00070           x[i]=t_p[i].x;
00071         GECODE_ES_FAIL(home,(GqBoolView<BoolView,IntView>
00072                              ::post(home,x,y,c)));
00073       }
00074       break;
00075     case IRT_LQ:
00076       {
00077         ViewArray<NegBoolView> x(home,n_p);
00078         for (int i=n_p; i--; )
00079           x[i]=t_p[i].x;
00080         MinusView z(y);
00081         GECODE_ES_FAIL(home,(GqBoolView<NegBoolView,MinusView>
00082                              ::post(home,x,z,n_p-c)));
00083       }
00084       break;
00085     default: GECODE_NEVER;
00086     }
00087   }
00088   
00089   void
00090   post_pos_unit(Space* home, 
00091                 Term<BoolView>* t_p, int n_p,
00092                 IntRelType r, ZeroIntView, int c, 
00093                 PropKind pk) {
00094     switch (r) {
00095     case IRT_EQ:
00096       {
00097         ViewArray<BoolView> x(home,n_p);
00098         for (int i=n_p; i--; )
00099           x[i]=t_p[i].x;
00100         GECODE_ES_FAIL(home,(EqBoolInt<BoolView>::post(home,x,c,pk)));
00101       }
00102       break;
00103     case IRT_NQ:
00104       {
00105         ViewArray<BoolView> x(home,n_p);
00106         for (int i=n_p; i--; )
00107           x[i]=t_p[i].x;
00108         GECODE_ES_FAIL(home,(NqBoolInt<BoolView>::post(home,x,c)));
00109       }
00110       break;
00111     case IRT_GQ:
00112       {
00113         ViewArray<BoolView> x(home,n_p);
00114         for (int i=n_p; i--; )
00115           x[i]=t_p[i].x;
00116         GECODE_ES_FAIL(home,(GqBoolInt<BoolView>::post(home,x,c,pk)));
00117       }
00118       break;
00119     case IRT_LQ:
00120       {
00121         ViewArray<NegBoolView> x(home,n_p);
00122         for (int i=n_p; i--; )
00123           x[i]=t_p[i].x;
00124         GECODE_ES_FAIL(home,(GqBoolInt<NegBoolView>::post(home,x,n_p-c,pk)));
00125       }
00126       break;
00127     default: GECODE_NEVER;
00128     }
00129   }
00130   
00131   void
00132   post_neg_unit(Space* home, 
00133                 Term<BoolView>* t_n, int n_n,
00134                 IntRelType r, IntView y, int c,
00135                 PropKind) {
00136     switch (r) {
00137     case IRT_EQ:
00138       {
00139         ViewArray<BoolView> x(home,n_n);
00140         for (int i=n_n; i--; )
00141           x[i]=t_n[i].x;
00142         MinusView z(y);
00143         GECODE_ES_FAIL(home,(EqBoolView<BoolView,MinusView>
00144                              ::post(home,x,z,-c)));
00145       }
00146       break;
00147     case IRT_NQ:
00148       {
00149         ViewArray<BoolView> x(home,n_n);
00150         for (int i=n_n; i--; )
00151           x[i]=t_n[i].x;
00152         MinusView z(y);
00153         GECODE_ES_FAIL(home,(NqBoolView<BoolView,MinusView>
00154                              ::post(home,x,z,-c)));
00155       }
00156       break;
00157     case IRT_GQ:
00158       {
00159         ViewArray<NegBoolView> x(home,n_n);
00160         for (int i=n_n; i--; )
00161           x[i]=t_n[i].x;
00162         GECODE_ES_FAIL(home,(GqBoolView<NegBoolView,IntView>
00163                              ::post(home,x,y,n_n+c)));
00164       }
00165       break;
00166     case IRT_LQ:
00167       {
00168         ViewArray<BoolView> x(home,n_n);
00169         for (int i=n_n; i--; )
00170           x[i]=t_n[i].x;
00171         MinusView z(y);
00172         GECODE_ES_FAIL(home,(GqBoolView<BoolView,MinusView>
00173                              ::post(home,x,z,-c)));
00174       }
00175       break;
00176     default: GECODE_NEVER;
00177     }
00178   }
00179   
00180   void
00181   post_neg_unit(Space* home, 
00182                 Term<BoolView>* t_n, int n_n,
00183                 IntRelType r, ZeroIntView, int c, 
00184                 PropKind pk) {
00185     switch (r) {
00186     case IRT_EQ:
00187       {
00188         ViewArray<BoolView> x(home,n_n);
00189         for (int i=n_n; i--; )
00190           x[i]=t_n[i].x;
00191         GECODE_ES_FAIL(home,(EqBoolInt<BoolView>::post(home,x,-c,pk)));
00192       }
00193       break;
00194     case IRT_NQ:
00195       {
00196         ViewArray<BoolView> x(home,n_n);
00197         for (int i=n_n; i--; )
00198           x[i]=t_n[i].x;
00199         GECODE_ES_FAIL(home,(NqBoolInt<BoolView>::post(home,x,-c)));
00200       }
00201       break;
00202     case IRT_GQ:
00203       {
00204         ViewArray<NegBoolView> x(home,n_n);
00205         for (int i=n_n; i--; )
00206           x[i]=t_n[i].x;
00207         GECODE_ES_FAIL(home,(GqBoolInt<NegBoolView>::post(home,x,n_n+c,pk)));
00208       }
00209       break;
00210     case IRT_LQ:
00211       {
00212         ViewArray<BoolView> x(home,n_n);
00213         for (int i=n_n; i--; )
00214           x[i]=t_n[i].x;
00215         GECODE_ES_FAIL(home,(GqBoolInt<BoolView>::post(home,x,-c,pk)));
00216       }
00217       break;
00218     default: GECODE_NEVER;
00219     }
00220   }
00221 
00222 
00223   void
00224   post_mixed(Space* home,
00225              Term<BoolView>* t_p, int n_p,
00226              Term<BoolView>* t_n, int n_n,
00227              IntRelType r, IntView y, int c) {
00228     ScaleBoolArray b_p(home,n_p);
00229     {
00230       ScaleBool* f=b_p.fst();
00231       for (int i=n_p; i--; ) {
00232         f[i].x=t_p[i].x; f[i].a=t_p[i].a;
00233       }
00234     }
00235     ScaleBoolArray b_n(home,n_n);
00236     {
00237       ScaleBool* f=b_n.fst();
00238       for (int i=n_n; i--; ) {
00239         f[i].x=t_n[i].x; f[i].a=t_n[i].a;
00240       }
00241     }
00242     switch (r) {
00243     case IRT_EQ:
00244       GECODE_ES_FAIL(home,
00245                      (EqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView>
00246                       ::post(home,b_p,b_n,y,c)));
00247       break;
00248     case IRT_NQ:
00249       GECODE_ES_FAIL(home,
00250                      (NqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView>
00251                       ::post(home,b_p,b_n,y,c)));
00252       break;
00253     case IRT_LQ:
00254       GECODE_ES_FAIL(home,
00255                      (LqBoolScale<ScaleBoolArray,ScaleBoolArray,IntView>
00256                       ::post(home,b_p,b_n,y,c)));
00257       break;
00258     case IRT_GQ:
00259       {
00260         MinusView m(y);
00261         GECODE_ES_FAIL(home,
00262                        (LqBoolScale<ScaleBoolArray,ScaleBoolArray,MinusView>
00263                         ::post(home,b_n,b_p,m,-c)));
00264       }
00265       break;
00266     default:
00267       GECODE_NEVER;
00268     }
00269   }
00270   
00271 
00272   void
00273   post_mixed(Space* home, 
00274              Term<BoolView>* t_p, int n_p,
00275              Term<BoolView>* t_n, int n_n,
00276              IntRelType r, ZeroIntView y, int c) {
00277     ScaleBoolArray b_p(home,n_p);
00278     {
00279       ScaleBool* f=b_p.fst();
00280       for (int i=n_p; i--; ) {
00281         f[i].x=t_p[i].x; f[i].a=t_p[i].a;
00282       }
00283     }
00284     ScaleBoolArray b_n(home,n_n);
00285     {
00286       ScaleBool* f=b_n.fst();
00287       for (int i=n_n; i--; ) {
00288         f[i].x=t_n[i].x; f[i].a=t_n[i].a;
00289       }
00290     }
00291     switch (r) {
00292     case IRT_EQ:
00293       GECODE_ES_FAIL(home,
00294                      (EqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
00295                       ::post(home,b_p,b_n,y,c)));
00296       break;
00297     case IRT_NQ:
00298       GECODE_ES_FAIL(home,
00299                      (NqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
00300                       ::post(home,b_p,b_n,y,c)));
00301       break;
00302     case IRT_LQ:
00303       GECODE_ES_FAIL(home,
00304                      (LqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
00305                       ::post(home,b_p,b_n,y,c)));
00306       break;
00307     case IRT_GQ:
00308       GECODE_ES_FAIL(home,
00309                      (LqBoolScale<ScaleBoolArray,ScaleBoolArray,ZeroIntView>
00310                       ::post(home,b_n,b_p,y,-c)));
00311       break;
00312     default:
00313       GECODE_NEVER;
00314     }
00315   }
00316   
00317   template <class View>
00318   forceinline void
00319   post_all(Space* home, 
00320            Term<BoolView>* t, int n,
00321            IntRelType r, View x, int c, PropKind pk) {
00322 
00323     Limits::check(c,"Int::linear");
00324 
00325     {
00326       double d = c;
00327 
00328       // Eliminate non-strict relations
00329       switch (r) {
00330       case IRT_EQ: case IRT_NQ: case IRT_LQ: case IRT_GQ:
00331         break;
00332       case IRT_LE:
00333         d--; r = IRT_LQ; break;
00334       case IRT_GR:
00335         d++; r = IRT_GQ; break;
00336       default:
00337         throw UnknownRelation("Int::linear");
00338       }
00339 
00340       // Eliminate assigned views
00341       for (int i=n; i--; )
00342         if (t[i].x.one()) {
00343           d -= t[i].a; t[i]=t[--n];
00344         } else if (t[i].x.zero()) {
00345           t[i]=t[--n];
00346         }
00347 
00348       Limits::check(d,"Int::linear");
00349       
00350       c = static_cast<int>(d);
00351     }
00352     
00353     Term<BoolView> *t_p, *t_n;
00354     int n_p, n_n;
00355     bool unit = normalize<BoolView>(t,n,t_p,n_p,t_n,n_n);
00356 
00357     if (n == 0) {
00358       switch (r) {
00359       case IRT_EQ: GECODE_ME_FAIL(home,x.eq(home,-c)); break;
00360       case IRT_NQ: GECODE_ME_FAIL(home,x.nq(home,-c)); break;
00361       case IRT_GQ: GECODE_ME_FAIL(home,x.lq(home,-c)); break;
00362       case IRT_LQ: GECODE_ME_FAIL(home,x.gq(home,-c)); break;
00363       default: GECODE_NEVER;
00364       }
00365       return;
00366     }
00367     
00368     // Check for overflow
00369     {
00370       double sl = x.max()+c;
00371       double su = x.min()+c;
00372       for (int i=n_p; i--; )
00373         su -= t_p[i].a;
00374       for (int i=n_n; i--; )
00375         sl += t_n[i].a;
00376       Limits::check(sl,"Int::linear");
00377       Limits::check(su,"Int::linear");
00378     }
00379     
00380     if (unit && (n_n == 0)) {
00382       post_pos_unit(home,t_p,n_p,r,x,c,pk);
00383     } else if (unit && (n_p == 0)) {
00384       // All coefficients are -1
00385       post_neg_unit(home,t_n,n_n,r,x,c,pk);
00386     } else {
00387       // Mixed coefficients
00388       post_mixed(home,t_p,n_p,t_n,n_n,r,x,c);
00389     }
00390   }
00391   
00392 
00393   void
00394   post(Space* home, 
00395        Term<BoolView>* t, int n, IntRelType r, IntView x, int c, 
00396        IntConLevel, PropKind pk) {
00397     post_all(home,t,n,r,x,c,pk);
00398   }
00399   
00400   void
00401   post(Space* home, 
00402        Term<BoolView>* t, int n, IntRelType r, int c, 
00403        IntConLevel, PropKind pk) {
00404     ZeroIntView x;
00405     post_all(home,t,n,r,x,c,pk);
00406   }
00407 
00408   void
00409   post(Space* home, 
00410        Term<BoolView>* t, int n, IntRelType r, IntView x, BoolView b,
00411        IntConLevel icl, PropKind pk) {
00412     int l, u;
00413     estimate(t,n,0,l,u);
00414     IntVar z(home,l,u); IntView zv(z);
00415     post_all(home,t,n,IRT_EQ,zv,0,pk);
00416     rel(home,z,r,x,b,icl,pk);    
00417   }
00418   
00419   void
00420   post(Space* home, 
00421        Term<BoolView>* t, int n, IntRelType r, int c, BoolView b,
00422        IntConLevel icl, PropKind pk) {
00423     int l, u;
00424     estimate(t,n,0,l,u);
00425     IntVar z(home,l,u); IntView zv(z);
00426     post_all(home,t,n,IRT_EQ,zv,0,pk);
00427     rel(home,z,r,c,b,icl,pk);
00428   }
00429 
00430 }}}
00431 
00432 // STATISTICS: int-post
00433