Module: ppl/ppl Branch: floating_point Commit: 0d9faf95e4bc2c1f7f52936c4db0291a57686d3d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0d9faf95e4bc2...

Author: Fabio Bossi bossi@cs.unipr.it Date: Tue Sep 22 11:50:35 2009 +0200

Written Polyhedron::refine_fp_interval_abstract_store. Various other corrections.

---

src/Octagonal_Shape.defs.hh | 3 +- src/Octagonal_Shape.templates.hh | 2 +- src/Polyhedron.defs.hh | 10 +++++++ src/Polyhedron.templates.hh | 51 ++++++++++++++++++++++++++++++++++++- 4 files changed, 62 insertions(+), 4 deletions(-)

diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 61aebe7..a893fb7 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -1746,7 +1746,8 @@ public: */ template <typename Interval_Info> void refine_fp_interval_abstract_store( - std::map< dimension_type, Interval<T, Interval_Info> >& store); + std::map< dimension_type, Interval<T, Interval_Info> >& store) + const;

//@} // Member Functions that May Modify the Dimension of the Vector Space

diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index f09d910..4b491bf 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -5426,7 +5426,7 @@ template <typename Interval_Info> void Octagonal_Shape<T>:: refine_fp_interval_abstract_store( - std::map< dimension_type, Interval<T, Interval_Info> >& store) { + std::map< dimension_type, Interval<T, Interval_Info> >& store) const {

// Check that T is a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 7ecc2cf..87ece79 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -1011,6 +1011,16 @@ public: const Linear_Form< Interval<FP_Format, Interval_Info> >& right, const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store);

+ //! Refines \p store with the constraints defining \p *this. + /*! + \param store + The interval floating point abstract store to refine. + */ + template <typename FP_Format, typename Interval_Info> + void refine_fp_interval_abstract_store( + std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) + const; + /*! \brief Computes the \ref Cylindrification "cylindrification" of \p *this with respect to space dimension \p var, assigning the result to \p *this. diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 7adf015..8f9be84 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -441,7 +441,6 @@ Polyhedron::convert_to_integer_expression( result = Linear_Expression();

typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; - typedef typename FP_Interval_Type::boundary_type FP_Coeff_Type; std::vector<Coefficient> numerators(lf_dimension+1); std::vector<Coefficient> denominators(lf_dimension+1);

@@ -488,7 +487,6 @@ Polyhedron::convert_to_integer_expressions( res = Linear_Expression();

typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; - typedef typename FP_Interval_Type::boundary_type FP_Coeff_Type; std::vector<Coefficient> numerators(lf_dimension+2); std::vector<Coefficient> denominators(lf_dimension+2);

@@ -541,6 +539,55 @@ Polyhedron::convert_to_integer_expressions( res_hi_coeff = Coefficient(0); }

+template <typename FP_Format, typename Interval_Info> +void +Polyhedron:: +refine_fp_interval_abstract_store( + std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) + const { + + // Check that FP_Format is indeed a floating point type. + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact, + "Polyhedron::refine_fp_interval_abstract_store:" + " T not a floating point type."); + + typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; + typedef typename std::map<dimension_type, FP_Interval_Type>::iterator + Map_Iterator; + + // FIXME: there could be restrictions on Interval_Info. + Box<FP_Interval_Type> limits(*this); + PPL_DIRTY_TEMP_COEFFICIENT(numerator); + PPL_DIRTY_TEMP_COEFFICIENT(denominator); + Map_Iterator store_end = store.end(); + for (Map_Iterator ite = store.begin(); ite != store_end; ++ite) { + dimension_type curr_var = ite->first; + PPL_ASSERT(curr_var < space_dim); + Variable var(curr_var); + Linear_Expression var_exp(var); + bool dummy; + FP_Interval_Type& curr_int = ite->second; + FP_Format& lb = curr_int.lower(); + FP_Format& ub = curr_int.upper(); + FP_Format comparison_term; + mpq_class tmp_rational; + if (limits.minimize(var_exp, numerator, denominator, dummy)) { + assign_r(tmp_rational.get_num(), numerator, ROUND_NOT_NEEDED); + assign_r(tmp_rational.get_den(), denominator, ROUND_NOT_NEEDED); + assign_r(comparison_term, tmp_rational, ROUND_DOWN); + if (comparison_term > lb) + lb = comparison_term; + } + if (limits.maximize(var_exp, numerator, denominator, dummy)) { + assign_r(tmp_rational.get_num(), numerator, ROUND_NOT_NEEDED); + assign_r(tmp_rational.get_den(), denominator, ROUND_NOT_NEEDED); + assign_r(comparison_term, tmp_rational, ROUND_UP); + if (comparison_term < ub) + ub = comparison_term; + } + } +} + template <typename C> void Polyhedron::throw_dimension_incompatible(const char* method,