#include <Saturation_Row.defs.hh>
Public Member Functions | |
Saturation_Row () | |
Default constructor. | |
Saturation_Row (const Saturation_Row &y) | |
Copy-constructor. | |
~Saturation_Row () | |
Destructor. | |
Saturation_Row & | operator= (const Saturation_Row &y) |
Assignment operator. | |
void | swap (Saturation_Row &y) |
Swaps *this with y . | |
bool | operator[] (unsigned long k) const |
Returns the truth value corresponding to the bit in position k . | |
void | set (unsigned long k) |
Sets the bit in position k . | |
void | clear (unsigned long k) |
Clears the bit in position k . | |
void | clear_from (unsigned long k) |
Clears bits from position k (included) onward. | |
void | clear () |
Clears all the bits of the row. | |
unsigned long | first () const |
Returns the index of the first set bit or ULONG_MAX if no bit is set. | |
unsigned long | next (unsigned long position) const |
Returns the index of the first set bit after position or ULONG_MAX if no bit after position is set. | |
unsigned long | last () const |
Returns the index of the last set bit or ULONG_MAX if no bit is set. | |
unsigned long | prev (unsigned long position) const |
Returns the index of the first set bit before position or ULONG_MAX if no bits before position is set. | |
unsigned long | count_ones () const |
Returns the number of set bits in the row. | |
bool | empty () const |
Returns true if no bit is set in the row. | |
memory_size_type | total_memory_in_bytes () const |
Returns the total size in bytes of the memory occupied by *this . | |
memory_size_type | external_memory_in_bytes () const |
Returns the size in bytes of the memory managed by *this . | |
bool | OK () const |
Checks if all the invariants are satisfied. | |
Static Private Member Functions | |
static unsigned int | first_one (mp_limb_t w) |
Assuming w is nonzero, returns the index of the first set bit in w . | |
static unsigned int | last_one (mp_limb_t w) |
Assuming w is nonzero, returns the index of the last set bit in w . | |
Private Attributes | |
mpz_t | vec |
Bit-vector representing the row. | |
Friends | |
int | compare (const Saturation_Row &x, const Saturation_Row &y) |
The basic comparison function. | |
bool | operator== (const Saturation_Row &x, const Saturation_Row &y) |
Returns true if and only if x and y are equal. | |
bool | operator!= (const Saturation_Row &x, const Saturation_Row &y) |
Returns true if and only if x and y are not equal. | |
bool | subset_or_equal (const Saturation_Row &x, const Saturation_Row &y) |
Set-theoretic inclusion test. | |
bool | subset_or_equal (const Saturation_Row &x, const Saturation_Row &y, bool &strict_subset) |
Set-theoretic inclusion test: sets strict_subset to a boolean indicating whether the inclusion is strict or not. | |
bool | strict_subset (const Saturation_Row &x, const Saturation_Row &y) |
Set-theoretic strict inclusion test. | |
void | set_union (const Saturation_Row &x, const Saturation_Row &y, Saturation_Row &z) |
Set-theoretic union. | |
Related Functions | |
(Note that these are not member functions.) | |
void | swap (Parma_Polyhedra_Library::Saturation_Row &x, Parma_Polyhedra_Library::Saturation_Row &y) |
Specializes std::swap . | |
void | iter_swap (std::vector< Parma_Polyhedra_Library::Saturation_Row >::iterator x, std::vector< Parma_Polyhedra_Library::Saturation_Row >::iterator y) |
Specializes std::iter_swap . |
An object of this class represents a single row of a saturation matrix. The saturation row corresponds to a constraint and a system of generators (resp., a generator and a system of constraints) and records whether or not the constraint is saturated by each one of the generators (resp., the generator saturates each one of the constraints).
The saturation relation is encoded by using a bitset, so that the constraint is saturated by the -th generator in the system (resp., the generator saturates the
-th constraint in the system) if and only if the
-th bit is not set.
Definition at line 112 of file Saturation_Row.defs.hh.
Parma_Polyhedra_Library::Saturation_Row::Saturation_Row | ( | ) | [inline] |
Default constructor.
Definition at line 33 of file Saturation_Row.inlines.hh.
References vec.
00033 { 00034 mpz_init(vec); 00035 }
Parma_Polyhedra_Library::Saturation_Row::Saturation_Row | ( | const Saturation_Row & | y | ) | [inline] |
Copy-constructor.
Definition at line 38 of file Saturation_Row.inlines.hh.
References vec.
00038 { 00039 mpz_init_set(vec, y.vec); 00040 }
Parma_Polyhedra_Library::Saturation_Row::~Saturation_Row | ( | ) | [inline] |
Destructor.
Definition at line 43 of file Saturation_Row.inlines.hh.
References vec.
00043 { 00044 mpz_clear(vec); 00045 }
Saturation_Row & Parma_Polyhedra_Library::Saturation_Row::operator= | ( | const Saturation_Row & | y | ) | [inline] |
Assignment operator.
Definition at line 48 of file Saturation_Row.inlines.hh.
References vec.
00048 { 00049 mpz_set(vec, y.vec); 00050 return *this; 00051 }
void Parma_Polyhedra_Library::Saturation_Row::swap | ( | Saturation_Row & | y | ) | [inline] |
Swaps *this
with y
.
Definition at line 80 of file Saturation_Row.inlines.hh.
References vec.
Referenced by Parma_Polyhedra_Library::Saturation_Matrix::add_row(), iter_swap(), and swap().
00080 { 00081 mpz_swap(vec, y.vec); 00082 }
bool Parma_Polyhedra_Library::Saturation_Row::operator[] | ( | unsigned long | k | ) | const |
Returns the truth value corresponding to the bit in position k
.
Definition at line 199 of file Saturation_Row.cc.
00199 { 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 }
void Parma_Polyhedra_Library::Saturation_Row::set | ( | unsigned long | k | ) | [inline] |
Sets the bit in position k
.
Definition at line 54 of file Saturation_Row.inlines.hh.
References vec.
Referenced by Parma_Polyhedra_Library::Polyhedron::conversion(), Parma_Polyhedra_Library::Polyhedron::select_H79_constraints(), Parma_Polyhedra_Library::Polyhedron::strongly_minimize_constraints(), and Parma_Polyhedra_Library::Polyhedron::strongly_minimize_generators().
00054 { 00055 mpz_setbit(vec, k); 00056 }
void Parma_Polyhedra_Library::Saturation_Row::clear | ( | unsigned long | k | ) | [inline] |
Clears the bit in position k
.
Definition at line 59 of file Saturation_Row.inlines.hh.
References vec.
Referenced by Parma_Polyhedra_Library::Polyhedron::select_H79_constraints(), and Parma_Polyhedra_Library::Polyhedron::strongly_minimize_constraints().
00059 { 00060 mpz_clrbit(vec, k); 00061 }
void Parma_Polyhedra_Library::Saturation_Row::clear_from | ( | unsigned long | k | ) | [inline] |
Clears bits from position k
(included) onward.
Definition at line 64 of file Saturation_Row.inlines.hh.
References vec.
void Parma_Polyhedra_Library::Saturation_Row::clear | ( | ) | [inline] |
Clears all the bits of the row.
Definition at line 85 of file Saturation_Row.inlines.hh.
References vec.
00085 { 00086 mpz_set_ui(vec, 0UL); 00087 }
unsigned long Parma_Polyhedra_Library::Saturation_Row::first | ( | ) | const |
Returns the index of the first set bit or ULONG_MAX if no bit is set.
Definition at line 97 of file Saturation_Row.cc.
References BITS_PER_GMP_LIMB, first_one(), vec, and vec_size.
00097 { 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 }
unsigned long Parma_Polyhedra_Library::Saturation_Row::next | ( | unsigned long | position | ) | const |
Returns the index of the first set bit after position
or ULONG_MAX if no bit after position
is set.
Definition at line 111 of file Saturation_Row.cc.
References BITS_PER_GMP_LIMB, first_one(), vec, and vec_size.
00111 { 00112 ++position; 00113 00114 // The alternative implementation using the mpz_scan1() function 00115 // of GMP was measured to be slower that ours. Here it is, in 00116 // case mpz_scan1() is improved. 00117 // 00118 // unsigned long r = mpz_scan1(vec, position); 00119 // return (r == ULONG_MAX) ? -1 : r; 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 // Get the first limb. 00128 mp_srcptr p = vec->_mp_d + li; 00129 00130 // Mask off any bits before `position' in the first limb. 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 }
unsigned long Parma_Polyhedra_Library::Saturation_Row::last | ( | ) | const |
Returns the index of the last set bit or ULONG_MAX if no bit is set.
Definition at line 146 of file Saturation_Row.cc.
References BITS_PER_GMP_LIMB, last_one(), and vec.
Referenced by Parma_Polyhedra_Library::Saturation_Matrix::OK().
00146 { 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 }
unsigned long Parma_Polyhedra_Library::Saturation_Row::prev | ( | unsigned long | position | ) | const |
Returns the index of the first set bit before position
or ULONG_MAX if no bits before position
is set.
Definition at line 159 of file Saturation_Row.cc.
References BITS_PER_GMP_LIMB, last_one(), vec, and vec_size.
00159 { 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 // Get the first limb. 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 }
unsigned long Parma_Polyhedra_Library::Saturation_Row::count_ones | ( | ) | const [inline] |
Returns the number of set bits in the row.
Definition at line 69 of file Saturation_Row.inlines.hh.
References vec.
Referenced by Parma_Polyhedra_Library::Polyhedron::conversion().
00069 { 00070 assert(vec->_mp_size >= 0); 00071 return mpn_popcount(vec->_mp_d, vec->_mp_size); 00072 }
bool Parma_Polyhedra_Library::Saturation_Row::empty | ( | ) | const [inline] |
Returns true
if no bit is set in the row.
Definition at line 75 of file Saturation_Row.inlines.hh.
References vec.
00075 { 00076 return mpz_sgn(vec) == 0; 00077 }
memory_size_type Parma_Polyhedra_Library::Saturation_Row::total_memory_in_bytes | ( | ) | const [inline] |
Returns the total size in bytes of the memory occupied by *this
.
Definition at line 95 of file Saturation_Row.inlines.hh.
References external_memory_in_bytes().
00095 { 00096 return sizeof(*this) + external_memory_in_bytes(); 00097 }
memory_size_type Parma_Polyhedra_Library::Saturation_Row::external_memory_in_bytes | ( | ) | const [inline] |
Returns the size in bytes of the memory managed by *this
.
Definition at line 90 of file Saturation_Row.inlines.hh.
References vec.
Referenced by total_memory_in_bytes().
00090 { 00091 return vec[0]._mp_alloc * SIZEOF_MP_LIMB_T; 00092 }
bool Parma_Polyhedra_Library::Saturation_Row::OK | ( | ) | const |
Checks if all the invariants are satisfied.
Definition at line 341 of file Saturation_Row.cc.
Referenced by Parma_Polyhedra_Library::Saturation_Matrix::OK().
00341 { 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 }
unsigned int Parma_Polyhedra_Library::Saturation_Row::first_one | ( | mp_limb_t | w | ) | [static, private] |
Assuming w
is nonzero, returns the index of the first set bit in w
.
Definition at line 35 of file Saturation_Row.cc.
Referenced by first(), and next().
00035 { 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 }
unsigned int Parma_Polyhedra_Library::Saturation_Row::last_one | ( | mp_limb_t | w | ) | [static, private] |
Assuming w
is nonzero, returns the index of the last set bit in w
.
Definition at line 65 of file Saturation_Row.cc.
Referenced by last(), and prev().
00065 { 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 }
int compare | ( | const Saturation_Row & | x, | |
const Saturation_Row & | y | |||
) | [friend] |
The basic comparison function.
Compares x
with y
starting from the least significant bits. The ordering is total and has the following property: if x
and y
are two rows seen as sets of naturals, if x
is a strict subset of y
, then x
comes before y
.
Returns
x
comes before y
in the ordering;x
and y
are equal;x
comes after y
in the ordering.Definition at line 213 of file Saturation_Row.cc.
00213 { 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 // Get the one's where they are different. 00226 const mp_limb_t diff = xl ^ yl; 00227 // First bit that is different. 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 }
bool operator== | ( | const Saturation_Row & | x, | |
const Saturation_Row & | y | |||
) | [friend] |
Returns true
if and only if x
and y
are equal.
Definition at line 314 of file Saturation_Row.cc.
00314 { 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 }
bool operator!= | ( | const Saturation_Row & | x, | |
const Saturation_Row & | y | |||
) | [friend] |
Returns true
if and only if x
and y
are not equal.
Definition at line 328 of file Saturation_Row.cc.
00328 { 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 }
bool subset_or_equal | ( | const Saturation_Row & | x, | |
const Saturation_Row & | y | |||
) | [friend] |
Set-theoretic inclusion test.
Definition at line 240 of file Saturation_Row.cc.
00240 { 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 }
bool subset_or_equal | ( | const Saturation_Row & | x, | |
const Saturation_Row & | y, | |||
bool & | strict_subset | |||
) | [friend] |
Set-theoretic inclusion test: sets strict_subset
to a boolean indicating whether the inclusion is strict or not.
Definition at line 261 of file Saturation_Row.cc.
00262 { 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 }
bool strict_subset | ( | const Saturation_Row & | x, | |
const Saturation_Row & | y | |||
) | [friend] |
Set-theoretic strict inclusion test.
Definition at line 288 of file Saturation_Row.cc.
00288 { 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 }
void set_union | ( | const Saturation_Row & | x, | |
const Saturation_Row & | y, | |||
Saturation_Row & | z | |||
) | [friend] |
void swap | ( | Parma_Polyhedra_Library::Saturation_Row & | x, | |
Parma_Polyhedra_Library::Saturation_Row & | y | |||
) | [related] |
Specializes std::swap
.
Definition at line 122 of file Saturation_Row.inlines.hh.
References swap().
00123 { 00124 x.swap(y); 00125 }
void iter_swap | ( | std::vector< Parma_Polyhedra_Library::Saturation_Row >::iterator | x, | |
std::vector< Parma_Polyhedra_Library::Saturation_Row >::iterator | y | |||
) | [related] |
Specializes std::iter_swap
.
Definition at line 129 of file Saturation_Row.inlines.hh.
References swap().
00130 { 00131 swap(*x, *y); 00132 }
mpz_t Parma_Polyhedra_Library::Saturation_Row::vec [private] |
Bit-vector representing the row.
Definition at line 209 of file Saturation_Row.defs.hh.
Referenced by clear(), clear_from(), count_ones(), empty(), external_memory_in_bytes(), first(), last(), next(), OK(), operator=(), operator[](), prev(), Saturation_Row(), set(), swap(), and ~Saturation_Row().