PPL  1.0
Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format > Class Template Reference

A floating point expression on a given format. More...

#include <ppl.hh>

Inheritance diagram for Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >:

List of all members.

Public Types

typedef Linear_Form
< FP_Interval_Type > 
FP_Linear_Form
 Alias for a linear form with template argument FP_Interval_Type.
typedef Box< FP_Interval_Type > FP_Interval_Abstract_Store
 Alias for a map that associates a variable index to an interval.
typedef std::map
< dimension_type,
FP_Linear_Form
FP_Linear_Form_Abstract_Store
 Alias for a map that associates a variable index to a linear form.
typedef
FP_Interval_Type::boundary_type 
boundary_type
 The floating point format used by the analyzer.
typedef FP_Interval_Type::info_type info_type
 The interval policy used by FP_Interval_Type.

Public Member Functions

virtual ~Floating_Point_Expression ()
 Destructor.
virtual bool linearize (const FP_Interval_Abstract_Store &int_store, const FP_Linear_Form_Abstract_Store &lf_store, FP_Linear_Form &result) const =0
 Linearizes a floating point expression.

Static Public Member Functions

static bool overflows (const FP_Linear_Form &lf)
 Verifies if a given linear form overflows.
static void relative_error (const FP_Linear_Form &lf, FP_Linear_Form &result)
 Computes the relative error of a given linear form.
static void intervalize (const FP_Linear_Form &lf, const FP_Interval_Abstract_Store &store, FP_Interval_Type &result)
 Makes result become an interval that overapproximates all the possible values of lf in the interval abstract store store.

Static Public Attributes

static FP_Interval_Type absolute_error = compute_absolute_error()
 Absolute error.

Detailed Description

template<typename FP_Interval_Type, typename FP_Format>
class Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >

A floating point expression on a given format.

This class represents a concrete floating point expression. This includes constants, floating point variables, binary and unary arithmetic operators.

Template type parameters
  • The class template type parameter FP_Interval_Type represents the type of the intervals used in the abstract domain. The interval bounds should have a floating point type.
  • The class template type parameter FP_Format represents the floating point format used in the concrete domain. This parameter must be a struct similar to the ones defined in file Float.defs.hh, even though it is sufficient to define the three fields BASE, MANTISSA_BITS and EXPONENT_BIAS.

Member Typedef Documentation


Member Function Documentation

template<typename FP_Interval_Type , typename FP_Format >
virtual bool Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >::linearize ( const FP_Interval_Abstract_Store int_store,
const FP_Linear_Form_Abstract_Store lf_store,
FP_Linear_Form result 
) const
pure virtual

Linearizes a floating point expression.

Makes result become a linear form that correctly approximates the value of the floating point expression in the given composite abstract store.

Parameters:
int_storeThe interval abstract store.
lf_storeThe linear form abstract store.
resultBecomes the linearized expression.
Returns:
true if the linearization succeeded, false otherwise.

Formally, if *this represents the expression $e$, int_store represents the interval abstract store $\rho^{\#}$ and lf_store represents the linear form abstract store $\rho^{\#}_l$, then result will become $\linexprenv{e}{\rho^{\#}}{\rho^{\#}_l}$ if the linearization succeeds.

All variables occurring in the floating point expression MUST have an associated interval in int_store. If this precondition is not met, calling the method causes an undefined behavior.

Implemented in Parma_Polyhedra_Library::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Sum_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Variable_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Constant_Floating_Point_Expression< FP_Interval_Type, FP_Format >, and Parma_Polyhedra_Library::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format >.

template<typename FP_Interval_Type , typename FP_Format >
bool Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >::overflows ( const FP_Linear_Form lf)
inlinestatic

Verifies if a given linear form overflows.

Parameters:
lfThe linear form to verify.
Returns:
Returns false if all coefficients in lf are bounded, true otherwise.
template<typename FP_Interval_Type , typename FP_Format >
void Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >::relative_error ( const FP_Linear_Form lf,
FP_Linear_Form result 
)
static

Computes the relative error of a given linear form.

Static helper method that is used by linearize to account for the relative errors on lf.

Parameters:
lfThe linear form used to compute the relative error.
resultBecomes the linear form corresponding to a relative error committed on lf.

This method makes result become a linear form obtained by evaluating the function $\varepsilon_{\mathbf{f}}(l)$ on the linear form lf. This function is defined such as:

\[ \varepsilon_{\mathbf{f}}\left([a, b]+\sum_{v \in \cV}[a_{v}, b_{v}]v\right) \defeq (\textrm{max}(|a|, |b|) \amifp [-\beta^{-\textrm{p}}, \beta^{-\textrm{p}}]) + \sum_{v \in \cV}(\textrm{max}(|a_{v}|,|b_{v}|) \amifp [-\beta^{-\textrm{p}}, \beta^{-\textrm{p}}])v \]

where p is the fraction size in bits for the format $\mathbf{f}$ and $\beta$ the base.

template<typename FP_Interval_Type , typename FP_Format >
void Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >::intervalize ( const FP_Linear_Form lf,
const FP_Interval_Abstract_Store store,
FP_Interval_Type &  result 
)
static

Makes result become an interval that overapproximates all the possible values of lf in the interval abstract store store.

Parameters:
lfThe linear form to aproximate.
storeThe abstract store.
resultThe linear form that will be modified.

This method makes result become $\iota(lf)\rho^{\#}$, that is an interval defined as:

\[ \iota\left(i + \sum_{v \in \cV}i_{v}v\right)\rho^{\#} \defeq i \asifp \left(\bigoplus_{v \in \cV}{}^{\#}i_{v} \amifp \rho^{\#}(v)\right) \]


Member Data Documentation

template<typename FP_Interval_Type , typename FP_Format >
FP_Interval_Type Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >::absolute_error = compute_absolute_error()
static

Absolute error.

Represents the interval $[-\omega, \omega]$ where $\omega$ is the smallest non-zero positive number in the less precise floating point format between the analyzer format and the analyzed format.


The documentation for this class was generated from the following file: