Parma_Polyhedra_Library::Saturation_Row Class Reference
[C++ Language Interface]

A row of a saturation matrix. More...

#include <Saturation_Row.defs.hh>

List of all members.

Public Member Functions

 Saturation_Row ()
 Default constructor.
 Saturation_Row (const Saturation_Row &y)
 Copy-constructor.
 ~Saturation_Row ()
 Destructor.
Saturation_Rowoperator= (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.


Detailed Description

A row of a saturation matrix.

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 $i$-th generator in the system (resp., the generator saturates the $i$-th constraint in the system) if and only if the $i$-th bit is not set.

Definition at line 112 of file Saturation_Row.defs.hh.


Constructor & Destructor Documentation

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 }


Member Function Documentation

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.

References vec, and vec_size.

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]

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.

00064                                                 {
00065   mpz_tdiv_r_2exp(vec, vec, k);
00066 }

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.

References vec, and vec_size.

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 }


Friends And Related Function Documentation

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

  • -1 if x comes before y in the ordering;
  • 0 if x and y are equal;
  • 1 if 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]

Set-theoretic union.

Definition at line 110 of file Saturation_Row.inlines.hh.

00111                              {
00112   mpz_ior(z.vec, x.vec, y.vec);
00113 }

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 }


Member Data Documentation


The documentation for this class was generated from the following files:

Generated on Wed Jul 16 22:55:46 2008 for PPL by  doxygen 1.5.6