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

A generic Difference Floating Point Expression. More...

#include <ppl.hh>

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

List of all members.

Public Types

typedef
Floating_Point_Expression
< FP_Interval_Type, FP_Format >
::FP_Linear_Form 
FP_Linear_Form
 Alias for the Linear_Form<FP_Interval_Type> from Floating_Point_Expression.
typedef
Floating_Point_Expression
< FP_Interval_Type, FP_Format >
::FP_Interval_Abstract_Store 
FP_Interval_Abstract_Store
 Alias for the Box<FP_Interval_Type> from Floating_Point_Expression.
typedef
Floating_Point_Expression
< FP_Interval_Type, FP_Format >
::FP_Linear_Form_Abstract_Store 
FP_Linear_Form_Abstract_Store
 Alias for the std::map<dimension_type, FP_Linear_Form> from Floating_Point_Expression.
typedef
Floating_Point_Expression
< FP_Interval_Type, FP_Format >
::boundary_type 
boundary_type
 Alias for the FP_Interval_Type::boundary_type from Floating_Point_Expression.
typedef
Floating_Point_Expression
< FP_Interval_Type, FP_Format >
::info_type 
info_type
 Alias for the FP_Interval_Type::info_type from Floating_Point_Expression.
- Public Types inherited from Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >

Public Member Functions

bool linearize (const FP_Interval_Abstract_Store &int_store, const FP_Linear_Form_Abstract_Store &lf_store, FP_Linear_Form &result) const
 Linearizes the expression in a given astract store.
void m_swap (Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format > &y)
 Swaps *this with y.
Constructors and Destructor
 Difference_Floating_Point_Expression (Floating_Point_Expression< FP_Interval_Type, FP_Format > *const x, Floating_Point_Expression< FP_Interval_Type, FP_Format > *const y)
 Constructor with two parameters: builds the difference floating point expression corresponding to x $\ominus$ y.
 ~Difference_Floating_Point_Expression ()
 Destructor.
- Public Member Functions inherited from Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >
virtual ~Floating_Point_Expression ()
 Destructor.

Related Functions

(Note that these are not member functions.)

template<typename FP_Interval_Type , typename FP_Format >
void swap (Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format > &x, Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format > &y)
 Swaps x with y.
template<typename FP_Interval_Type , typename FP_Format >
void swap (Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format > &x, Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format > &y)

Additional Inherited Members

- Static Public Member Functions inherited from Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >
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 inherited from Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >
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::Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format >

A generic Difference Floating Point Expression.

Template type parameters
  • The class template type parameter FP_Interval_Type represents the type of the intervals used in the abstract domain.
  • The class template type parameter FP_Format represents the floating point format used in the concrete domain.
Linearization of difference floating-point expressions

Let $i + \sum_{v \in \cV}i_{v}v $ and $i' + \sum_{v \in \cV}i'_{v}v $ be two linear forms, $\aslf$ and $\adlf$ two sound abstract operators on linear form such that:

\[ \left(i + \sum_{v \in \cV}i_{v}v\right) \aslf \left(i' + \sum_{v \in \cV}i'_{v}v\right) = \left(i \asifp i'\right) + \sum_{v \in \cV}\left(i_{v} \asifp i'_{v}\right)v, \]

\[ \left(i + \sum_{v \in \cV}i_{v}v\right) \adlf \left(i' + \sum_{v \in \cV}i'_{v}v\right) = \left(i \adifp i'\right) + \sum_{v \in \cV}\left(i_{v} \adifp i'_{v}\right)v. \]

Given an expression $e_{1} \ominus e_{2}$ and a composite abstract store $\left \llbracket \rho^{\#}, \rho^{\#}_l \right \rrbracket$, we construct the interval linear form $\linexprenv{e_{1} \ominus e_{2}}{\rho^{\#}}{\rho^{\#}_l}$ on $\cV$ as follows:

\[ \linexprenv{e_{1} \ominus e_{2}}{\rho^{\#}}{\rho^{\#}_l} = \linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l} \adlf \linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l} \aslf \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l} \right) \aslf \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l} \right) \aslf mf_{\mathbf{f}}[-1, 1] \]

where $\varepsilon_{\mathbf{f}}(l)$ is the linear form computed by calling method Floating_Point_Expression::relative_error on $l$ and $mf_{\mathbf{f}}$ is a rounding error defined in Floating_Point_Expression::absolute_error.


Member Function Documentation

template<typename FP_Interval_Type , typename FP_Format >
bool Parma_Polyhedra_Library::Difference_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
virtual

Linearizes the expression in a given astract store.

Makes result become the linearization of *this in the given composite abstract store.

Parameters:
int_storeThe interval abstract store.
lf_storeThe linear form abstract store.
resultThe modified linear form.
Returns:
true if the linearization succeeded, false otherwise.

Note that all variables occuring in the expressions represented by first_operand and second_operand MUST have an associated value in int_store. If this precondition is not met, calling the method causes an undefined behavior.

See the class description for a detailed explanation of how result is computed.

Implements Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >.


Friends And Related Function Documentation

template<typename FP_Interval_Type , typename FP_Format >
void swap ( Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format > &  x,
Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format > &  y 
)
related

Swaps x with y.

template<typename FP_Interval_Type , typename FP_Format >
void swap ( Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format > &  x,
Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format > &  y 
)
related

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