[PPL-devel] [GIT] ppl/ppl(floating_point): Use Box to represent an interval abstract store.
Fabio Bossi
bossi at cs.unipr.it
Tue Sep 22 15:52:06 CEST 2009
Module: ppl/ppl
Branch: floating_point
Commit: 79572e84de987a3e979f8629b3f468659dee2d84
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=79572e84de987a3e979f8629b3f468659dee2d84
Author: Fabio Bossi <bossi at 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>
More information about the PPL-devel
mailing list