PPL  0.12.1
Parma_Polyhedra_Library::Implementation Namespace Reference

Implementation related data and functions. More...

Namespaces

namespace  BD_Shapes
namespace  Boxes
namespace  Octagonal_Shapes
namespace  Pointset_Powersets
namespace  Termination
namespace  Watchdog

Classes

class  Ptr_Iterator
 A class to define STL const and non-const iterators from pointer types. More...
struct  Wrap_Dim_Translations

Typedefs

typedef std::vector
< Wrap_Dim_Translations
Wrap_Translations

Functions

unsigned int first_one (unsigned int u)
 Assuming u is nonzero, returns the index of the first set bit in u.
unsigned int first_one (unsigned long ul)
 Assuming ul is nonzero, returns the index of the first set bit in ul.
unsigned int first_one (unsigned long long ull)
 Assuming ull is nonzero, returns the index of the first set bit in ull.
unsigned int last_one (unsigned int u)
 Assuming u is nonzero, returns the index of the last set bit in u.
unsigned int last_one (unsigned long ul)
 Assuming ul is nonzero, returns the index of the last set bit in ul.
unsigned int last_one (unsigned long long ull)
 Assuming ull is nonzero, returns the index of the last set bit in ull.
dimension_type num_constraints (const Constraint_System &cs)
 Helper returning number of constraints in system.
template<typename P , typename Q >
bool operator== (const Ptr_Iterator< P > &x, const Ptr_Iterator< Q > &y)
template<typename P , typename Q >
bool operator!= (const Ptr_Iterator< P > &x, const Ptr_Iterator< Q > &y)
template<typename P , typename Q >
bool operator< (const Ptr_Iterator< P > &x, const Ptr_Iterator< Q > &y)
template<typename P , typename Q >
bool operator<= (const Ptr_Iterator< P > &x, const Ptr_Iterator< Q > &y)
template<typename P , typename Q >
bool operator> (const Ptr_Iterator< P > &x, const Ptr_Iterator< Q > &y)
template<typename P , typename Q >
bool operator>= (const Ptr_Iterator< P > &x, const Ptr_Iterator< Q > &y)
template<typename P , typename Q >
Ptr_Iterator< P >::difference_type operator- (const Ptr_Iterator< P > &x, const Ptr_Iterator< Q > &y)
template<typename P >
Ptr_Iterator< P > operator+ (typename Ptr_Iterator< P >::difference_type m, const Ptr_Iterator< P > &y)
template<typename Value_Type , typename Compare >
const Value_Type & median (const Value_Type &x, const Value_Type &y, const Value_Type &z, Compare comp)
template<typename Iter , typename Value_Type , typename Compare >
Iter swapping_partition (Iter first, Iter last, const Value_Type &pivot, Compare comp)
template<typename Iter , typename Compare >
void swapping_insertion_sort (Iter first, Iter last, Compare comp)
template<typename Iter , typename Compare >
void swapping_quicksort_loop (Iter first, Iter last, Compare comp)
template<typename Iter , typename Compare >
void swapping_sort (Iter first, Iter last, Compare comp)
template<typename Iter >
Iter swapping_unique (Iter first, Iter last)
template<typename PSET >
void wrap_assign_ind (PSET &pointset, Variables_Set &vars, Wrap_Translations::const_iterator first, Wrap_Translations::const_iterator end, Bounded_Integer_Type_Width w, Coefficient_traits::const_reference min_value, Coefficient_traits::const_reference max_value, const Constraint_System &cs, Coefficient &tmp1, Coefficient &tmp2)
template<typename PSET >
void wrap_assign_col (PSET &dest, const PSET &src, const Variables_Set &vars, Wrap_Translations::const_iterator first, Wrap_Translations::const_iterator end, Bounded_Integer_Type_Width w, Coefficient_traits::const_reference min_value, Coefficient_traits::const_reference max_value, const Constraint_System *cs_p, Coefficient &tmp)
template<typename PSET >
void wrap_assign (PSET &pointset, const Variables_Set &vars, const Bounded_Integer_Type_Width w, const Bounded_Integer_Type_Representation r, const Bounded_Integer_Type_Overflow o, const Constraint_System *cs_p, const unsigned complexity_threshold, const bool wrap_individually, const char *class_name)

Variables

unsigned int in_assert = 0
 Non zero during evaluation of PPL_ASSERT expression.

Detailed Description

Implementation related data and functions.


Typedef Documentation


Function Documentation

unsigned int Parma_Polyhedra_Library::Implementation::first_one ( unsigned int  u)
inline

Assuming u is nonzero, returns the index of the first set bit in u.

Definition at line 168 of file Bit_Row.inlines.hh.

References Parma_Polyhedra_Library::ctz().

Referenced by Parma_Polyhedra_Library::Bit_Row::first(), and Parma_Polyhedra_Library::Bit_Row::next().

                          {
  return ctz(u);
}
unsigned int Parma_Polyhedra_Library::Implementation::first_one ( unsigned long  ul)
inline

Assuming ul is nonzero, returns the index of the first set bit in ul.

Definition at line 177 of file Bit_Row.inlines.hh.

References Parma_Polyhedra_Library::ctz().

                            {
  return ctz(ul);
}
unsigned int Parma_Polyhedra_Library::Implementation::first_one ( unsigned long long  ull)
inline

Assuming ull is nonzero, returns the index of the first set bit in ull.

Definition at line 186 of file Bit_Row.inlines.hh.

References Parma_Polyhedra_Library::ctz().

                                  {
  return ctz(ull);
}
unsigned int Parma_Polyhedra_Library::Implementation::last_one ( unsigned int  u)
inline

Assuming u is nonzero, returns the index of the last set bit in u.

Definition at line 194 of file Bit_Row.inlines.hh.

References Parma_Polyhedra_Library::clz(), and sizeof_to_bits.

Referenced by Parma_Polyhedra_Library::Bit_Row::last(), and Parma_Polyhedra_Library::Bit_Row::prev().

                         {
  return static_cast<unsigned int>(sizeof_to_bits(sizeof(u)))
    - 1U - clz(u);
}
unsigned int Parma_Polyhedra_Library::Implementation::last_one ( unsigned long  ul)
inline

Assuming ul is nonzero, returns the index of the last set bit in ul.

Definition at line 204 of file Bit_Row.inlines.hh.

References Parma_Polyhedra_Library::clz(), and sizeof_to_bits.

                           {
  return static_cast<unsigned int>(sizeof_to_bits(sizeof(ul)))
    - 1U - clz(ul);
}
unsigned int Parma_Polyhedra_Library::Implementation::last_one ( unsigned long long  ull)
inline

Assuming ull is nonzero, returns the index of the last set bit in ull.

Definition at line 214 of file Bit_Row.inlines.hh.

References Parma_Polyhedra_Library::clz(), and sizeof_to_bits.

                                 {
  return static_cast<unsigned int>(sizeof_to_bits(sizeof(ull)))
    - 1U - clz(ull);
}
template<typename Value_Type , typename Compare >
const Value_Type& Parma_Polyhedra_Library::Implementation::median ( const Value_Type &  x,
const Value_Type &  y,
const Value_Type &  z,
Compare  comp 
)
inline

Definition at line 49 of file swapping_sort.templates.hh.

Referenced by swapping_quicksort_loop().

                     {
  return comp(x, y)
    ? (comp(y, z) ? y : (comp(x, z) ? z : x))
    : (comp(x, z) ? x : (comp(y, z) ? z : y));
}
template<typename P , typename Q >
bool Parma_Polyhedra_Library::Implementation::operator!= ( const Ptr_Iterator< P > &  x,
const Ptr_Iterator< Q > &  y 
)
inline

Definition at line 144 of file Ptr_Iterator.inlines.hh.

References Parma_Polyhedra_Library::Implementation::Ptr_Iterator< P >::base().

                                                               {
  return x.base() != y.base();
}
template<typename P >
Ptr_Iterator< P > Parma_Polyhedra_Library::Implementation::operator+ ( typename Ptr_Iterator< P >::difference_type  m,
const Ptr_Iterator< P > &  y 
)
inline

Definition at line 180 of file Ptr_Iterator.inlines.hh.

References Parma_Polyhedra_Library::Implementation::Ptr_Iterator< P >::base().

                                    {
  return Ptr_Iterator<P>(m + y.base());
}
template<typename P , typename Q >
Ptr_Iterator< P >::difference_type Parma_Polyhedra_Library::Implementation::operator- ( const Ptr_Iterator< P > &  x,
const Ptr_Iterator< Q > &  y 
)
inline

Definition at line 174 of file Ptr_Iterator.inlines.hh.

References Parma_Polyhedra_Library::Implementation::Ptr_Iterator< P >::base().

                                                              {
  return x.base() - y.base();
}
template<typename P , typename Q >
bool Parma_Polyhedra_Library::Implementation::operator< ( const Ptr_Iterator< P > &  x,
const Ptr_Iterator< Q > &  y 
)
inline

Definition at line 150 of file Ptr_Iterator.inlines.hh.

References Parma_Polyhedra_Library::Implementation::Ptr_Iterator< P >::base().

                                                              {
  return x.base() < y.base();
}
template<typename P , typename Q >
bool Parma_Polyhedra_Library::Implementation::operator<= ( const Ptr_Iterator< P > &  x,
const Ptr_Iterator< Q > &  y 
)
inline

Definition at line 156 of file Ptr_Iterator.inlines.hh.

References Parma_Polyhedra_Library::Implementation::Ptr_Iterator< P >::base().

                                                               {
  return x.base() <= y.base();
}
template<typename P , typename Q >
bool Parma_Polyhedra_Library::Implementation::operator== ( const Ptr_Iterator< P > &  x,
const Ptr_Iterator< Q > &  y 
)
inline

Definition at line 138 of file Ptr_Iterator.inlines.hh.

References Parma_Polyhedra_Library::Implementation::Ptr_Iterator< P >::base().

                                                               {
  return x.base() == y.base();
}
template<typename P , typename Q >
bool Parma_Polyhedra_Library::Implementation::operator> ( const Ptr_Iterator< P > &  x,
const Ptr_Iterator< Q > &  y 
)
inline

Definition at line 162 of file Ptr_Iterator.inlines.hh.

References Parma_Polyhedra_Library::Implementation::Ptr_Iterator< P >::base().

                                                              {
  return x.base() > y.base();
}
template<typename P , typename Q >
bool Parma_Polyhedra_Library::Implementation::operator>= ( const Ptr_Iterator< P > &  x,
const Ptr_Iterator< Q > &  y 
)
inline

Definition at line 168 of file Ptr_Iterator.inlines.hh.

References Parma_Polyhedra_Library::Implementation::Ptr_Iterator< P >::base().

                                                               {
  return x.base() >= y.base();
}
template<typename Iter , typename Compare >
void Parma_Polyhedra_Library::Implementation::swapping_insertion_sort ( Iter  first,
Iter  last,
Compare  comp 
)

Definition at line 78 of file swapping_sort.templates.hh.

Referenced by swapping_sort().

                                                             {
  if (first == last)
    return;
  for (Iter i = first + 1; i != last; ++i) {
    using std::iter_swap;
    Iter current = i;
    if (comp(*current, *first)) {
      Iter next = current + 1;
      while (current != first)
        iter_swap(--current, --next);
    }
    else {
      Iter previous = current - 1;
      while (comp(*current, *previous))
        iter_swap(current--, previous--);
    }
  }
}
template<typename Iter , typename Value_Type , typename Compare >
Iter Parma_Polyhedra_Library::Implementation::swapping_partition ( Iter  first,
Iter  last,
const Value_Type &  pivot,
Compare  comp 
)

Definition at line 58 of file swapping_sort.templates.hh.

Referenced by swapping_quicksort_loop().

                                 {
  for ( ; ; ) {
    while (comp(*first, pivot))
      ++first;
    --last;
    while (comp(pivot, *last))
      --last;
    if (first < last) {
      using std::iter_swap;
      iter_swap(first, last);
      ++first;
    }
    else
      return first;
  }
}
template<typename Iter , typename Compare >
void Parma_Polyhedra_Library::Implementation::swapping_quicksort_loop ( Iter  first,
Iter  last,
Compare  comp 
)

Definition at line 99 of file swapping_sort.templates.hh.

References median(), and swapping_partition().

Referenced by swapping_sort().

                                                             {
  const typename std::iterator_traits<Iter>::difference_type threshold = 16;
  while (last - first > threshold) {
    // The construction of this temporary object is
    // required for the correctness of the algorithm.
    Iter middle = first + (last - first) / 2;
    typename std::iterator_traits<Iter>::value_type
      pivot = median(*first, *middle, *(last - 1), comp);
    Iter part_point = swapping_partition(first, last, pivot, comp);
    swapping_quicksort_loop(part_point, last, comp);
    last = part_point;
  }
}
template<typename Iter , typename Compare >
void Parma_Polyhedra_Library::Implementation::swapping_sort ( Iter  first,
Iter  last,
Compare  comp 
)
inline
template<typename Iter >
Iter Parma_Polyhedra_Library::Implementation::swapping_unique ( Iter  first,
Iter  last 
)

Definition at line 124 of file swapping_sort.templates.hh.

Referenced by Parma_Polyhedra_Library::Linear_System::sort_and_remove_with_sat(), Parma_Polyhedra_Library::Bit_Matrix::sort_rows(), and Parma_Polyhedra_Library::Linear_System::sort_rows().

                                       {
  if (first == last)
    return last;
  Iter current = first;
  Iter next = current;
  ++next;
  while(next != last && *current != *next) {
    current = next;
    ++next;
  }
  if (next == last)
    return last;
  ++next;
  while (next != last) {
    if (*current != *next) {
      using std::iter_swap;
      iter_swap(++current, next);
    }
    ++next;
  }
  return ++current;
}
template<typename PSET >
void Parma_Polyhedra_Library::Implementation::wrap_assign ( PSET &  pointset,
const Variables_Set &  vars,
const Bounded_Integer_Type_Width  w,
const Bounded_Integer_Type_Representation  r,
const Bounded_Integer_Type_Overflow  o,
const Constraint_System *  cs_p,
const unsigned  complexity_threshold,
const bool  wrap_individually,
const char *  class_name 
)

Definition at line 158 of file wrap_assign.hh.

References Parma_Polyhedra_Library::assign_r(), Parma_Polyhedra_Library::Constraint_System::begin(), c, Parma_Polyhedra_Library::Constraint::coefficient(), Parma_Polyhedra_Library::Coefficient_one(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Variables_Set::insert(), Parma_Polyhedra_Library::Constraint_System::insert(), Parma_Polyhedra_Library::mul_2exp_assign(), Parma_Polyhedra_Library::neg_assign(), Parma_Polyhedra_Library::OVERFLOW_IMPOSSIBLE, Parma_Polyhedra_Library::OVERFLOW_UNDEFINED, PPL_ASSERT, PPL_DIRTY_TEMP_COEFFICIENT, PPL_UNINITIALIZED, Parma_Polyhedra_Library::result_overflow(), Parma_Polyhedra_Library::ROUND_DOWN, Parma_Polyhedra_Library::ROUND_IGNORE, Parma_Polyhedra_Library::SIGNED_2_COMPLEMENT, Parma_Polyhedra_Library::Variables_Set::space_dimension(), Parma_Polyhedra_Library::Constraint_System::space_dimension(), Parma_Polyhedra_Library::UNSIGNED, wrap_assign_col(), and wrap_assign_ind().

Referenced by Parma_Polyhedra_Library::Box< ITV >::wrap_assign(), Parma_Polyhedra_Library::Octagonal_Shape< T >::wrap_assign(), Parma_Polyhedra_Library::BD_Shape< T >::wrap_assign(), and Parma_Polyhedra_Library::Polyhedron::wrap_assign().

                                    {
  // We must have cs_p->space_dimension() <= vars.space_dimension()
  //         and  vars.space_dimension() <= pointset.space_dimension().

  // Dimension-compatibility check of `*cs_p', if any.
  if (cs_p != 0) {
    const dimension_type vars_space_dim = vars.space_dimension();
    if (cs_p->space_dimension() > vars_space_dim) {
      std::ostringstream s;
      s << "PPL::" << class_name << "::wrap_assign(..., cs_p, ...):"
        << std::endl
        << "vars.space_dimension() == " << vars_space_dim
        << ", cs_p->space_dimension() == " << cs_p->space_dimension() << ".";
      throw std::invalid_argument(s.str());
    }

#ifndef NDEBUG
    // Check that all variables upon which `*cs_p' depends are in `vars'.
    // An assertion is violated otherwise.
    const Constraint_System cs = *cs_p;
    const dimension_type cs_space_dim = cs.space_dimension();
    Variables_Set::const_iterator vars_end = vars.end();
    for (Constraint_System::const_iterator i = cs.begin(),
           cs_end = cs.end(); i != cs_end; ++i) {
      const Constraint& c = *i;
      for (dimension_type d = cs_space_dim; d-- > 0; ) {
        PPL_ASSERT(c.coefficient(Variable(d)) == 0
                   || vars.find(d) != vars_end);
      }
    }
#endif
  }

  // Wrapping no variable only requires refining with *cs_p, if any.
  if (vars.empty()) {
    if (cs_p != 0)
      pointset.refine_with_constraints(*cs_p);
    return;
  }

  // Dimension-compatibility check of `vars'.
  const dimension_type space_dim = pointset.space_dimension();
  if (vars.space_dimension() > space_dim) {
    std::ostringstream s;
    s << "PPL::" << class_name << "::wrap_assign(vs, ...):" << std::endl
      << "this->space_dimension() == " << space_dim
      << ", required space dimension == " << vars.space_dimension() << ".";
    throw std::invalid_argument(s.str());
  }

  // Wrapping an empty polyhedron is a no-op.
  if (pointset.is_empty())
    return;

  // Set `min_value' and `max_value' to the minimum and maximum values
  // a variable of width `w' and signedness `s' can take.
  PPL_DIRTY_TEMP_COEFFICIENT(min_value);
  PPL_DIRTY_TEMP_COEFFICIENT(max_value);
  if (r == UNSIGNED) {
    min_value = 0;
    mul_2exp_assign(max_value, Coefficient_one(), w);
    --max_value;
  }
  else {
    PPL_ASSERT(r == SIGNED_2_COMPLEMENT);
    mul_2exp_assign(max_value, Coefficient_one(), w-1);
    neg_assign(min_value, max_value);
    --max_value;
  }

  // If we are wrapping variables collectively, the ranges for the
  // required translations are saved in `translations' instead of being
  // immediately applied.
  Wrap_Translations translations;

  // Dimensions subject to translation are added to this set if we are
  // wrapping collectively or if `cs_p' is non null.
  Variables_Set dimensions_to_be_translated;

  // This will contain a lower bound to the number of abstractions
  // to be joined in order to obtain the collective wrapping result.
  // As soon as this exceeds `complexity_threshold', counting will be
  // interrupted and the full range will be the result of wrapping
  // any dimension that is not fully contained in quadrant 0.
  unsigned collective_wrap_complexity = 1;

  // This flag signals that the maximum complexity for collective
  // wrapping as been exceeded.
  bool collective_wrap_too_complex = false;

  if (!wrap_individually) {
    translations.reserve(space_dim);
  }

  // We use `full_range_bounds' to delay conversions whenever
  // this delay does not negatively affect precision.
  Constraint_System full_range_bounds;

  PPL_DIRTY_TEMP_COEFFICIENT(l_n);
  PPL_DIRTY_TEMP_COEFFICIENT(l_d);
  PPL_DIRTY_TEMP_COEFFICIENT(u_n);
  PPL_DIRTY_TEMP_COEFFICIENT(u_d);

  for (Variables_Set::const_iterator i = vars.begin(),
         vars_end = vars.end(); i != vars_end; ++i) {

    const Variable x(*i);

    bool extremum;

    if (!pointset.minimize(x, l_n, l_d, extremum)) {
    set_full_range:
      pointset.unconstrain(x);
      full_range_bounds.insert(min_value <= x);
      full_range_bounds.insert(x <= max_value);
      continue;
    }

    if (!pointset.maximize(x, u_n, u_d, extremum))
      goto set_full_range;

    div_assign_r(l_n, l_n, l_d, ROUND_DOWN);
    div_assign_r(u_n, u_n, u_d, ROUND_DOWN);
    l_n -= min_value;
    u_n -= min_value;
    div_2exp_assign_r(l_n, l_n, w, ROUND_DOWN);
    div_2exp_assign_r(u_n, u_n, w, ROUND_DOWN);
    Coefficient& first_quadrant = l_n;
    Coefficient& last_quadrant = u_n;

    // Special case: this variable does not need wrapping.
    if (first_quadrant == 0 && last_quadrant == 0)
      continue;

    // If overflow is impossible, try not to add useless constraints.
    if (o == OVERFLOW_IMPOSSIBLE) {
      if (first_quadrant < 0)
        full_range_bounds.insert(min_value <= x);
      if (last_quadrant > 0)
        full_range_bounds.insert(x <= max_value);
      continue;
    }

    if (o == OVERFLOW_UNDEFINED || collective_wrap_too_complex)
      goto set_full_range;

    Coefficient& quadrants = u_d;
    quadrants = last_quadrant - first_quadrant + 1;

    PPL_UNINITIALIZED(unsigned, extension);
    Result res = assign_r(extension, quadrants, ROUND_IGNORE);
    if (result_overflow(res) != 0 || extension > complexity_threshold)
      goto set_full_range;

    if (!wrap_individually && !collective_wrap_too_complex) {
      res = mul_assign_r(collective_wrap_complexity,
                         collective_wrap_complexity, extension, ROUND_IGNORE);
      if (result_overflow(res) != 0
          || collective_wrap_complexity > complexity_threshold)
        collective_wrap_too_complex = true;
      if (collective_wrap_too_complex) {
        // Set all the dimensions in `translations' to full range.
        for (Wrap_Translations::const_iterator j = translations.begin(),
               translations_end = translations.end();
             j != translations_end;
             ++j) {
          const Variable y(j->var);
          pointset.unconstrain(y);
          full_range_bounds.insert(min_value <= y);
          full_range_bounds.insert(y <= max_value);
        }
      }
    }

    if (wrap_individually && cs_p == 0) {
      Coefficient& quadrant = first_quadrant;
      // Temporary variable holding the shifts to be applied in order
      // to implement the translations.
      Coefficient& shift = l_d;
      PSET hull(space_dim, EMPTY);
      for ( ; quadrant <= last_quadrant; ++quadrant) {
        PSET p(pointset);
        if (quadrant != 0) {
          mul_2exp_assign(shift, quadrant, w);
          p.affine_image(x, x - shift, 1);
        }
        p.refine_with_constraint(min_value <= x);
        p.refine_with_constraint(x <= max_value);
        hull.upper_bound_assign(p);
      }
      pointset.m_swap(hull);
    }
    else if (wrap_individually || !collective_wrap_too_complex) {
      PPL_ASSERT(!wrap_individually || cs_p != 0);
      dimensions_to_be_translated.insert(x);
      translations
        .push_back(Wrap_Dim_Translations(x, first_quadrant, last_quadrant));
    }
  }

  if (!translations.empty()) {
    if (wrap_individually) {
      PPL_ASSERT(cs_p != 0);
      wrap_assign_ind(pointset, dimensions_to_be_translated,
                      translations.begin(), translations.end(),
                      w, min_value, max_value, *cs_p, l_n, l_d);
    }
    else {
      PSET hull(space_dim, EMPTY);
      wrap_assign_col(hull, pointset, dimensions_to_be_translated,
                      translations.begin(), translations.end(),
                      w, min_value, max_value, cs_p, l_n);
      pointset.m_swap(hull);
    }
  }

  if (cs_p != 0)
    pointset.refine_with_constraints(*cs_p);
  pointset.refine_with_constraints(full_range_bounds);
}
template<typename PSET >
void Parma_Polyhedra_Library::Implementation::wrap_assign_col ( PSET &  dest,
const PSET &  src,
const Variables_Set &  vars,
Wrap_Translations::const_iterator  first,
Wrap_Translations::const_iterator  end,
Bounded_Integer_Type_Width  w,
Coefficient_traits::const_reference  min_value,
Coefficient_traits::const_reference  max_value,
const Constraint_System *  cs_p,
Coefficient &  tmp 
)

Definition at line 112 of file wrap_assign.hh.

References Parma_Polyhedra_Library::Implementation::Wrap_Dim_Translations::first_quadrant, Parma_Polyhedra_Library::Implementation::Wrap_Dim_Translations::last_quadrant, Parma_Polyhedra_Library::mul_2exp_assign(), PPL_DIRTY_TEMP_COEFFICIENT, and Parma_Polyhedra_Library::Implementation::Wrap_Dim_Translations::var.

Referenced by wrap_assign().

                                  {
  if (first == end) {
    PSET p(src);
    if (cs_p != 0)
      p.refine_with_constraints(*cs_p);
    for (Variables_Set::const_iterator i = vars.begin(),
           vars_end = vars.end(); i != vars_end; ++i) {
      const Variable x(*i);
      p.refine_with_constraint(min_value <= x);
      p.refine_with_constraint(x <= max_value);
    }
    dest.upper_bound_assign(p);
  }
  else {
    const Wrap_Dim_Translations& wrap_dim_translations = *first;
    const Variable x(wrap_dim_translations.var);
    const Coefficient& first_quadrant = wrap_dim_translations.first_quadrant;
    const Coefficient& last_quadrant = wrap_dim_translations.last_quadrant;
    Coefficient& shift = tmp;
    PPL_DIRTY_TEMP_COEFFICIENT(quadrant);
    for (quadrant = first_quadrant; quadrant <= last_quadrant; ++quadrant) {
      if (quadrant != 0) {
        mul_2exp_assign(shift, quadrant, w);
        PSET p(src);
        p.affine_image(x, x - shift, 1);
        wrap_assign_col(dest, p, vars, first+1, end, w, min_value, max_value,
                        cs_p, tmp);
      }
      else
        wrap_assign_col(dest, src, vars, first+1, end, w, min_value, max_value,
                        cs_p, tmp);
    }
  }
}
template<typename PSET >
void Parma_Polyhedra_Library::Implementation::wrap_assign_ind ( PSET &  pointset,
Variables_Set &  vars,
Wrap_Translations::const_iterator  first,
Wrap_Translations::const_iterator  end,
Bounded_Integer_Type_Width  w,
Coefficient_traits::const_reference  min_value,
Coefficient_traits::const_reference  max_value,
const Constraint_System &  cs,
Coefficient &  tmp1,
Coefficient &  tmp2 
)

Definition at line 52 of file wrap_assign.hh.

References Parma_Polyhedra_Library::Constraint_System::begin(), c, Parma_Polyhedra_Library::Constraint::coefficient(), Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::Constraint_System::end(), Parma_Polyhedra_Library::Implementation::Wrap_Dim_Translations::first_quadrant, Parma_Polyhedra_Library::Variable::id(), Parma_Polyhedra_Library::Implementation::Wrap_Dim_Translations::last_quadrant, Parma_Polyhedra_Library::mul_2exp_assign(), Parma_Polyhedra_Library::Constraint_System::space_dimension(), and Parma_Polyhedra_Library::Implementation::Wrap_Dim_Translations::var.

Referenced by wrap_assign().

                                   {
  const dimension_type space_dim = pointset.space_dimension();
  const dimension_type cs_space_dim = cs.space_dimension();
  for (Wrap_Translations::const_iterator i = first; i != end; ++i) {
    const Wrap_Dim_Translations& wrap_dim_translations = *i;
    const Variable x(wrap_dim_translations.var);
    const Coefficient& first_quadrant = wrap_dim_translations.first_quadrant;
    const Coefficient& last_quadrant = wrap_dim_translations.last_quadrant;
    Coefficient& quadrant = tmp1;
    Coefficient& shift = tmp2;
    PSET hull(space_dim, EMPTY);
    for (quadrant = first_quadrant; quadrant <= last_quadrant; ++quadrant) {
      PSET p(pointset);
      if (quadrant != 0) {
        mul_2exp_assign(shift, quadrant, w);
        p.affine_image(x, x - shift, 1);
      }
      // `x' has just been wrapped.
      vars.erase(x.id());

      // Refine `p' with all the constraints in `cs' not depending
      // on variables in `vars'.
      if (vars.empty())
        p.refine_with_constraints(cs);
      else {
        Variables_Set::const_iterator vars_end = vars.end();
        for (Constraint_System::const_iterator j = cs.begin(),
               cs_end = cs.end(); j != cs_end; ++j) {
          const Constraint& c = *j;
          for (dimension_type d = cs_space_dim; d-- > 0; ) {
            if (c.coefficient(Variable(d)) != 0 && vars.find(d) != vars_end)
              goto skip;
          }
          // If we are here it means `c' does not depend on variables
          // in `vars'.
          p.refine_with_constraint(c);

        skip:
          continue;
        }
      }
      p.refine_with_constraint(min_value <= x);
      p.refine_with_constraint(x <= max_value);
      hull.upper_bound_assign(p);
    }
    pointset.m_swap(hull);
  }
}

Variable Documentation

Non zero during evaluation of PPL_ASSERT expression.

Definition at line 40 of file globals.cc.

Referenced by Parma_Polyhedra_Library::maybe_abandon().