Module: ppl/ppl Branch: floating_point Commit: 79572e84de987a3e979f8629b3f468659dee2d84 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=79572e84de987... Author: Fabio Bossi <bossi@cs.unipr.it> Date: Tue Sep 22 15:46:05 2009 +0200 Use Box to represent an interval abstract store. --- src/Floating_Point_Expression.defs.hh | 10 +++++-- src/Floating_Point_Expression.inlines.hh | 1 + src/Floating_Point_Expression.templates.hh | 9 +++--- src/Octagonal_Shape.defs.hh | 3 +- src/Octagonal_Shape.templates.hh | 32 ++-------------------- src/Polyhedron.defs.hh | 2 +- src/Polyhedron.templates.hh | 39 ++------------------------- 7 files changed, 21 insertions(+), 75 deletions(-) diff --git a/src/Floating_Point_Expression.defs.hh b/src/Floating_Point_Expression.defs.hh index 6d6b336..f0cd9c5 100644 --- a/src/Floating_Point_Expression.defs.hh +++ b/src/Floating_Point_Expression.defs.hh @@ -25,7 +25,8 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "globals.defs.hh" #include "Floating_Point_Expression.types.hh" -#include "Linear_Form.defs.hh" +#include "Linear_Form.types.hh" +#include "Box.types.hh" #include <cmath> #include <map> @@ -62,11 +63,14 @@ public: typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; //! Alias for a map that associates a variable index to an interval. - /*! + /*! \brief + Alias for a Box storing lower and upper bounds for floating point + variables. + The type a linear form abstract store associating each variable with an interval that correctly approximates its value. */ - typedef std::map<dimension_type, FP_Interval_Type> FP_Interval_Abstract_Store; + typedef Box<FP_Interval_Type> FP_Interval_Abstract_Store; //! Alias for a map that associates a variable index to a linear form. /*! diff --git a/src/Floating_Point_Expression.inlines.hh b/src/Floating_Point_Expression.inlines.hh index 3e38dd2..f55488e 100644 --- a/src/Floating_Point_Expression.inlines.hh +++ b/src/Floating_Point_Expression.inlines.hh @@ -24,6 +24,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #define PPL_Floating_Point_Expression_inlines_hh 1 #include "globals.defs.hh" +#include "Linear_Form.defs.hh" namespace Parma_Polyhedra_Library { diff --git a/src/Floating_Point_Expression.templates.hh b/src/Floating_Point_Expression.templates.hh index 557cddc..17e796d 100644 --- a/src/Floating_Point_Expression.templates.hh +++ b/src/Floating_Point_Expression.templates.hh @@ -24,6 +24,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #ifndef PPL_Floating_Point_Expression_templates_hh #define PPL_Floating_Point_Expression_templates_hh 1 +#include "Linear_Form.defs.hh" #include <cmath> namespace Parma_Polyhedra_Library { @@ -70,12 +71,12 @@ Floating_Point_Expression<FP_Interval_Type, FP_Format> FP_Interval_Type& result) { result = FP_Interval_Type(lf.inhomogeneous_term()); dimension_type dimension = lf.space_dimension(); + assert(dimension <= store.space_dimension()); for (dimension_type i = 0; i < dimension; ++i) { - typename FP_Interval_Abstract_Store::const_iterator - next_variable_value = store.find(i); - assert(next_variable_value != store.end()); FP_Interval_Type current_addend = lf.coefficient(Variable(i)); - current_addend *= next_variable_value->second; + const FP_Interval_Type& curr_int = store.get_interval(Variable(i)); + assert(curr_int.is_bounded()); + current_addend *= curr_int; result += current_addend; } diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 6f910d2..81ddf92 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -1746,8 +1746,7 @@ public: */ template <typename Interval_Info> void refine_fp_interval_abstract_store( - std::map< dimension_type, Interval<T, Interval_Info> >& store) - const; + Box< 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 e3ae567..04906d6 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -30,6 +30,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Interval.defs.hh" #include "Linear_Form.defs.hh" #include "meta_programming.hh" +#include "Box.defs.hh" #include "assert.hh" #include <vector> #include <map> @@ -5426,43 +5427,16 @@ template <typename Interval_Info> void Octagonal_Shape<T>:: refine_fp_interval_abstract_store( - std::map< dimension_type, Interval<T, Interval_Info> >& store) const { + Box< Interval<T, Interval_Info> >& store) const { // Check that T is a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, "Octagonal_Shape<T>::refine_fp_interval_abstract_store:" " T not a floating point type."); - strong_closure_assign(); - typedef Interval<T, Interval_Info> FP_Interval_Type; - typedef typename std::map<dimension_type, FP_Interval_Type>::iterator - Map_Iterator; - - PPL_DIRTY_TEMP(N, upper_bound); - 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); - dimension_type n_curr_var = curr_var * 2; - FP_Interval_Type& curr_int = ite->second; - T& lb = curr_int.lower(); - T& ub = curr_int.upper(); - // Now get the upper bound for curr_var in the octagon. - assign_r(upper_bound, matrix[n_curr_var+1][n_curr_var], ROUND_NOT_NEEDED); - div_2exp_assign_r(upper_bound, upper_bound, 1, ROUND_UP); - - if (upper_bound < ub) - ub = upper_bound.raw_value(); - - // Now get the lower bound for curr_var in the octagon. - neg_assign_r(upper_bound, matrix[n_curr_var][n_curr_var+1], - ROUND_NOT_NEEDED); - div_2exp_assign_r(upper_bound, upper_bound, 1, ROUND_DOWN); + store.intersection_assign(Box<FP_Interval_Type>(*this)); - if (upper_bound > lb) - lb = upper_bound.raw_value(); - } } template <typename T> diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 7f17172..55d7c44 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -1018,7 +1018,7 @@ public: */ template <typename FP_Format, typename Interval_Info> void refine_fp_interval_abstract_store( - std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) + Box< Interval<FP_Format, Interval_Info> >& store) const; /*! \brief diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 8ad8b01..c312028 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -543,8 +543,7 @@ 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 { + Box< 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, @@ -552,40 +551,8 @@ 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; - } - } + store.intersection_assign(Box<FP_Interval_Type>(*this)); + } template <typename C>