00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #include <config.h>
00024
00025 #include "Saturation_Row.defs.hh"
00026 #include <cassert>
00027 #include <climits>
00028
00029 namespace PPL = Parma_Polyhedra_Library;
00030
00031 #define BITS_PER_GMP_LIMB (SIZEOF_MP_LIMB_T*CHAR_BIT)
00032
00033 #if !HAVE_DECL_FFS || SIZEOF_MP_LIMB_T != SIZEOF_INT
00034 unsigned int
00035 PPL::Saturation_Row::first_one(mp_limb_t w) {
00036 unsigned int r = 0;
00037 w = w & -w;
00038 #if SIZEOF_MP_LIMB_T == 8
00039 if ((w & 0xffffffff) == 0) {
00040 w >>= 32;
00041 r += 32;
00042 }
00043 #elif SIZEOF_MP_LIMB_T != 4
00044 #error "Size of mp_limb_t not supported by Saturation_Row::first_one(mp_limb_t w)."
00045 #endif
00046 if ((w & 0xffff) == 0) {
00047 w >>= 16;
00048 r += 16;
00049 }
00050 if ((w & 0xff) == 0) {
00051 w >>= 8;
00052 r += 8;
00053 }
00054 if (w & 0xf0)
00055 r += 4;
00056 if (w & 0xcc)
00057 r += 2;
00058 if (w & 0xaa)
00059 r += 1;
00060 return r;
00061 }
00062 #endif // !HAVE_DECL_FFS || SIZEOF_MP_LIMB_T != SIZEOF_INT
00063
00064 unsigned int
00065 PPL::Saturation_Row::last_one(mp_limb_t w) {
00066 unsigned int r = 0;
00067 #if SIZEOF_MP_LIMB_T == 8
00068 if (w & 0xffffffff00000000) {
00069 w >>= 32;
00070 r += 32;
00071 }
00072 #elif SIZEOF_MP_LIMB_T != 4
00073 #error "Size of mp_limb_t not supported by Saturation_Row::last_one(mp_limb_t w)."
00074 #endif
00075 if (w & 0xffff0000) {
00076 w >>= 16;
00077 r += 16;
00078 }
00079 if (w & 0xff00) {
00080 w >>= 8;
00081 r += 8;
00082 }
00083 if (w & 0xf0) {
00084 w >>= 4;
00085 r += 4;
00086 }
00087 if (w & 0xc) {
00088 w >>= 2;
00089 r += 2;
00090 }
00091 if (w & 0x2)
00092 r += 1;
00093 return r;
00094 }
00095
00096 unsigned long
00097 PPL::Saturation_Row::first() const {
00098 const mp_size_t vec_size = vec->_mp_size;
00099 assert(vec_size >= 0);
00100 mp_size_t li = 0;
00101 mp_srcptr p = vec->_mp_d;
00102 for (; li < vec_size; ++li, ++p) {
00103 const mp_limb_t limb = *p;
00104 if (limb != 0)
00105 return li*BITS_PER_GMP_LIMB + first_one(limb);
00106 }
00107 return ULONG_MAX;
00108 }
00109
00110 unsigned long
00111 PPL::Saturation_Row::next(unsigned long position) const {
00112 ++position;
00113
00114
00115
00116
00117
00118
00119
00120
00121 mp_size_t li = position / BITS_PER_GMP_LIMB;
00122 const mp_size_t vec_size = vec->_mp_size;
00123 assert(vec_size >= 0);
00124 if (li >= vec_size)
00125 return ULONG_MAX;
00126
00127
00128 mp_srcptr p = vec->_mp_d + li;
00129
00130
00131 mp_limb_t limb = *p & (~(mp_limb_t) 0) << (position % BITS_PER_GMP_LIMB);
00132
00133 while (true) {
00134 if (limb != 0)
00135 return li*BITS_PER_GMP_LIMB + first_one(limb);
00136 ++li;
00137 if (li == vec_size)
00138 break;
00139 ++p;
00140 limb = *p;
00141 }
00142 return ULONG_MAX;
00143 }
00144
00145 unsigned long
00146 PPL::Saturation_Row::last() const {
00147 mp_size_t li = vec->_mp_size;
00148 assert(li >= 0);
00149 if (li == 0)
00150 return ULONG_MAX;
00151 --li;
00152 const mp_srcptr p = vec->_mp_d + li;
00153 const mp_limb_t limb = *p;
00154 assert(limb != 0);
00155 return li*BITS_PER_GMP_LIMB + last_one(limb);
00156 }
00157
00158 unsigned long
00159 PPL::Saturation_Row::prev(unsigned long position) const {
00160 if (position == 0)
00161 return ULONG_MAX;
00162
00163 --position;
00164
00165 const mp_size_t vec_size = vec->_mp_size;
00166 assert(vec_size > 0);
00167 mp_size_t li = position / BITS_PER_GMP_LIMB;
00168
00169 mp_limb_t limb;
00170 mp_srcptr p = vec->_mp_d;
00171
00172
00173 if (li >= vec_size) {
00174 li = vec_size - 1;
00175 p += li;
00176 limb = *p;
00177 }
00178 else {
00179 const mp_limb_t mask
00180 = (~(mp_limb_t) 0)
00181 >> (BITS_PER_GMP_LIMB - 1 - position % BITS_PER_GMP_LIMB);
00182 p += li;
00183 limb = *p & mask;
00184 }
00185
00186 while (true) {
00187 if (limb != 0)
00188 return li*BITS_PER_GMP_LIMB + last_one(limb);
00189 if (li == 0)
00190 break;
00191 --li;
00192 --p;
00193 limb = *p;
00194 }
00195 return ULONG_MAX;
00196 }
00197
00198 bool
00199 PPL::Saturation_Row::operator[](const unsigned long k) const {
00200 const mp_size_t vec_size = vec->_mp_size;
00201 assert(vec_size >= 0);
00202
00203 unsigned long i = k / GMP_NUMB_BITS;
00204 if (i >= static_cast<unsigned long>(vec_size))
00205 return false;
00206
00207 mp_limb_t limb = *(vec->_mp_d + i);
00208 return (limb >> (k % GMP_NUMB_BITS)) & 1;
00209 }
00210
00212 int
00213 PPL::compare(const Saturation_Row& x, const Saturation_Row& y) {
00214 const mp_size_t x_size = x.vec->_mp_size;
00215 assert(x_size >= 0);
00216 const mp_size_t y_size = y.vec->_mp_size;
00217 assert(y_size >= 0);
00218 mp_size_t size = (x_size > y_size ? y_size : x_size);
00219 mp_srcptr xp = x.vec->_mp_d;
00220 mp_srcptr yp = y.vec->_mp_d;
00221 while (size > 0) {
00222 const mp_limb_t xl = *xp;
00223 const mp_limb_t yl = *yp;
00224 if (xl != yl) {
00225
00226 const mp_limb_t diff = xl ^ yl;
00227
00228 const mp_limb_t mask = diff & ~(diff-1);
00229 return (xl & mask) ? 1 : -1;
00230 }
00231 ++xp;
00232 ++yp;
00233 --size;
00234 }
00235 return x_size == y_size ? 0 : (x_size > y_size ? 1 : -1);
00236 }
00237
00239 bool
00240 PPL::subset_or_equal(const Saturation_Row& x, const Saturation_Row& y) {
00241 mp_size_t x_size = x.vec->_mp_size;
00242 assert(x_size >= 0);
00243 mp_size_t y_size = y.vec->_mp_size;
00244 assert(y_size >= 0);
00245 if (x_size > y_size)
00246 return false;
00247 mp_srcptr xp = x.vec->_mp_d;
00248 mp_srcptr yp = y.vec->_mp_d;
00249 while (x_size > 0) {
00250 if (*xp & ~*yp)
00251 return false;
00252 ++xp;
00253 ++yp;
00254 --x_size;
00255 }
00256 return true;
00257 }
00258
00260 bool
00261 PPL::subset_or_equal(const Saturation_Row& x, const Saturation_Row& y,
00262 bool& strict_subset) {
00263 mp_size_t x_size = x.vec->_mp_size;
00264 assert(x_size >= 0);
00265 mp_size_t y_size = y.vec->_mp_size;
00266 assert(y_size >= 0);
00267 if (x_size > y_size)
00268 return false;
00269 strict_subset = (x_size < y_size);
00270 mp_srcptr xp = x.vec->_mp_d;
00271 mp_srcptr yp = y.vec->_mp_d;
00272 while (x_size > 0) {
00273 const mp_limb_t xl = *xp;
00274 const mp_limb_t yl = *yp;
00275 if (xl & ~yl)
00276 return false;
00277 if (!strict_subset && xl != yl)
00278 strict_subset = true;
00279 ++xp;
00280 ++yp;
00281 --x_size;
00282 }
00283 return true;
00284 }
00285
00287 bool
00288 PPL::strict_subset(const Saturation_Row& x, const Saturation_Row& y) {
00289 mp_size_t x_size = x.vec->_mp_size;
00290 assert(x_size >= 0);
00291 mp_size_t y_size = y.vec->_mp_size;
00292 assert(y_size >= 0);
00293 if (x_size > y_size)
00294 return false;
00295 bool different = (x_size < y_size);
00296 mp_srcptr xp = x.vec->_mp_d;
00297 mp_srcptr yp = y.vec->_mp_d;
00298 while (x_size > 0) {
00299 const mp_limb_t xl = *xp;
00300 const mp_limb_t yl = *yp;
00301 if (xl & ~yl)
00302 return false;
00303 if (!different && xl != yl)
00304 different = true;
00305 ++xp;
00306 ++yp;
00307 --x_size;
00308 }
00309 return different;
00310 }
00311
00313 bool
00314 PPL::operator==(const Saturation_Row& x, const Saturation_Row& y) {
00315 const mp_size_t x_vec_size = x.vec->_mp_size;
00316 assert(x_vec_size >= 0);
00317 const mp_size_t y_vec_size = y.vec->_mp_size;
00318 assert(y_vec_size >= 0);
00319
00320 if (x_vec_size != y_vec_size)
00321 return false;
00322
00323 return mpn_cmp(x.vec->_mp_d, y.vec->_mp_d, x_vec_size) == 0;
00324 }
00325
00327 bool
00328 PPL::operator!=(const Saturation_Row& x, const Saturation_Row& y) {
00329 const mp_size_t x_vec_size = x.vec->_mp_size;
00330 assert(x_vec_size >= 0);
00331 const mp_size_t y_vec_size = y.vec->_mp_size;
00332 assert(y_vec_size >= 0);
00333
00334 if (x_vec_size != y_vec_size)
00335 return true;
00336
00337 return mpn_cmp(x.vec->_mp_d, y.vec->_mp_d, x_vec_size) != 0;
00338 }
00339
00340 bool
00341 PPL::Saturation_Row::OK() const {
00342 const mp_size_t vec_size = vec->_mp_size;
00343 const mp_size_t vec_alloc = vec->_mp_alloc;
00344 return vec_size >= 0
00345 && vec_alloc >= vec_size
00346 && (vec_size == 0 || mpz_getlimbn(vec, vec_size-1) != 0);
00347 }