Module: ppl/ppl Branch: master Commit: 07abce21d65f995dc378d84c3c8ad65728f23fb7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=07abce21d65f9...

Author: Enea Zaffanella zaffanella@cs.unipr.it Date: Wed Mar 31 21:23:41 2010 +0200

Drafted drop_some_non_integer_points() for weakly relational shapes.

---

src/BD_Shape.defs.hh | 2 + src/BD_Shape.inlines.hh | 10 ++++++++ src/BD_Shape.templates.hh | 47 +++++++++++++++++++++++++++++++++---- src/Octagonal_Shape.defs.hh | 2 + src/Octagonal_Shape.inlines.hh | 13 ++++++++++ src/Octagonal_Shape.templates.hh | 44 +++++++++++++++++++++++++++++++---- 6 files changed, 108 insertions(+), 10 deletions(-)

diff --git a/src/BD_Shape.defs.hh b/src/BD_Shape.defs.hh index 74cbc52..3f019eb 100644 --- a/src/BD_Shape.defs.hh +++ b/src/BD_Shape.defs.hh @@ -2244,6 +2244,8 @@ private: */ void compute_leaders(std::vector<dimension_type>& leaders) const;

+ void drop_some_non_integer_points_helper(N& elem); + friend std::ostream& Parma_Polyhedra_Library::IO_Operators ::operator<<<>(std::ostream& s, const BD_Shape<T>& c); diff --git a/src/BD_Shape.inlines.hh b/src/BD_Shape.inlines.hh index 62f4c85..275b0df 100644 --- a/src/BD_Shape.inlines.hh +++ b/src/BD_Shape.inlines.hh @@ -852,6 +852,16 @@ BD_Shape<T>::refine_fp_interval_abstract_store(

}

+template <typename T> +inline void +BD_Shape<T>::drop_some_non_integer_points_helper(N& elem) { + if (!is_integer(elem)) { + Result r = floor_assign_r(elem, elem, ROUND_DOWN); + used(r); + PPL_ASSERT(r == V_EQ); + reset_shortest_path_closed(); + } +}

} // namespace Parma_Polyhedra_Library

diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index e580ec8..02eec79 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -836,7 +836,7 @@ BD_Shape<T>::frequency(const Linear_Expression& expr, // Check the bounded differences with the other dimensions that // have non-zero coefficient in `le'. else { - assert(!constant_v); + PPL_ASSERT(!constant_v); for (dimension_type j = i; j-- > 1; ) { const Variable vj(j-1); if (le.coefficient(vj) == 0) @@ -6348,7 +6348,18 @@ BD_Shape<T>::drop_some_non_integer_points(Complexity_Class) { if (std::numeric_limits<T>::is_integer) return;

- // FIXME(0.11): complete. + const dimension_type space_dim = space_dimension(); + shortest_path_closure_assign(); + if (space_dim == 0 || marked_empty()) + return; + + for (dimension_type i = space_dim + 1; i-- > 0; ) { + DB_Row<N>& dbm_i = dbm[i]; + for (dimension_type j = space_dim + 1; j-- > 0; ) + if (i != j) + drop_some_non_integer_points_helper(dbm_i[j]); + } + PPL_ASSERT(OK()); }

template <typename T> @@ -6356,15 +6367,41 @@ void BD_Shape<T>::drop_some_non_integer_points(const Variables_Set& vars, Complexity_Class) { // Dimension-compatibility check. + const dimension_type space_dim = space_dimension(); const dimension_type min_space_dim = vars.space_dimension(); - if (space_dimension() < min_space_dim) + if (space_dim < min_space_dim) throw_dimension_incompatible("drop_some_non_integer_points(vs, cmpl)", min_space_dim);

- if (std::numeric_limits<T>::is_integer) + if (std::numeric_limits<T>::is_integer || min_space_dim == 0) return;

- // FIXME(0.11): complete. + shortest_path_closure_assign(); + if (marked_empty()) + return; + + const Variables_Set::const_iterator v_begin = vars.begin(); + const Variables_Set::const_iterator v_end = vars.end(); + PPL_ASSERT(v_begin != v_end); + // Unary constraints on a variable occurring in `vars'. + DB_Row<N>& dbm_0 = dbm[0]; + for (Variables_Set::const_iterator v_i = v_begin; v_i != v_end; ++v_i) { + const dimension_type i = *v_i + 1; + drop_some_non_integer_points_helper(dbm_0[i]); + drop_some_non_integer_points_helper(dbm[i][0]); + } + + // Binary constraints where both variables occur in `vars'. + for (Variables_Set::const_iterator v_i = v_begin; v_i != v_end; ++v_i) { + const dimension_type i = *v_i + 1; + DB_Row<N>& dbm_i = dbm[i]; + for (Variables_Set::const_iterator v_j = v_begin; v_j != v_end; ++v_j) { + const dimension_type j = *v_j + 1; + if (i != j) + drop_some_non_integer_points_helper(dbm_i[j]); + } + } + PPL_ASSERT(OK()); }

/*! \relates Parma_Polyhedra_Library::BD_Shape */ diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 4f28fe1..9fe32c1 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -2231,6 +2231,8 @@ private: Coefficient& ext_n, Coefficient& ext_d, bool& included, Generator& g) const;

+ void drop_some_non_integer_points_helper(N& elem); + friend std::ostream& Parma_Polyhedra_Library::IO_Operators ::operator<<<>(std::ostream& s, const Octagonal_Shape<T>& c); diff --git a/src/Octagonal_Shape.inlines.hh b/src/Octagonal_Shape.inlines.hh index b496fdf..c79c7b8 100644 --- a/src/Octagonal_Shape.inlines.hh +++ b/src/Octagonal_Shape.inlines.hh @@ -864,6 +864,19 @@ Octagonal_Shape<T>::hash_code() const { return space_dimension() & 0x7fffffff; }

+template <typename T> +inline void +Octagonal_Shape<T>::drop_some_non_integer_points_helper(N& elem) { + if (!is_integer(elem)) { +#ifndef NDEBUG + Result r = +#endif + floor_assign_r(elem, elem, ROUND_DOWN); + PPL_ASSERT(r == V_EQ); + reset_strongly_closed(); + } +} + } // namespace Parma_Polyhedra_Library

namespace std { diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 94dab08..fb123c4 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -7559,12 +7559,20 @@ Octagonal_Shape<T>

template <typename T> void -Octagonal_Shape<T> -::drop_some_non_integer_points(Complexity_Class) { +Octagonal_Shape<T>::drop_some_non_integer_points(Complexity_Class) { if (std::numeric_limits<T>::is_integer) return;

- // FIXME(0.11): complete. + const dimension_type space_dim = space_dimension(); + strong_closure_assign(); + if (space_dim == 0 || marked_empty()) + return; + + for (typename OR_Matrix<N>::element_iterator i = matrix.element_begin(), + i_end = matrix.element_end(); i != i_end; ++i) + drop_some_non_integer_points_helper(*i); + + PPL_ASSERT(OK()); }

template <typename T> @@ -7578,10 +7586,36 @@ Octagonal_Shape<T> throw_dimension_incompatible("drop_some_non_integer_points(vs, cmpl)", min_space_dim);

- if (std::numeric_limits<T>::is_integer) + if (std::numeric_limits<T>::is_integer || min_space_dim == 0) + return; + + strong_closure_assign(); + if (marked_empty()) return;

- // FIXME(0.11): complete. + const Variables_Set::const_iterator v_begin = vars.begin(); + const Variables_Set::const_iterator v_end = vars.end(); + PPL_ASSERT(v_begin != v_end); + typedef typename OR_Matrix<N>::row_reference_type Row_Reference; + for (Variables_Set::const_iterator v_i = v_begin; v_i != v_end; ++v_i) { + const dimension_type i = *v_i; + Row_Reference m_i = matrix[i]; + const dimension_type ci = i + 1; + Row_Reference m_ci = matrix[ci]; + // Unary constaints. + drop_some_non_integer_points_helper(m_i[ci]); + drop_some_non_integer_points_helper(m_ci[i]); + // Binary constraint (note: only consider j < i). + for (Variables_Set::const_iterator v_j = v_begin; v_j != v_i; ++v_j) { + const dimension_type j = *v_j; + const dimension_type cj = j + 1; + drop_some_non_integer_points_helper(m_i[j]); + drop_some_non_integer_points_helper(m_i[cj]); + drop_some_non_integer_points_helper(m_ci[j]); + drop_some_non_integer_points_helper(m_ci[cj]); + } + } + PPL_ASSERT(OK()); }

/*! \relates Parma_Polyhedra_Library::Octagonal_Shape */