A generic Multiplication Floating Point Expression. More...

#include <ppl.hh>

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

[legend]

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 >
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. More...

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. More...

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
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. More...

void	m_swap (Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &y)
	Swaps `*this` with `y`.

Constructors and Destructor
	Multiplication_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 multiplication floating point expression corresponding to `x` $\otimes$ `y`.

	~Multiplication_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 (Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &x, Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &y)
	Swaps `x` with `y`. More...

template<typename FP_Interval_Type , typename FP_Format >
void	swap (Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &x, Multiplication_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. More...

static void	relative_error (const FP_Linear_Form &lf, FP_Linear_Form &result)
	Computes the relative error of a given linear form. More...

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`. More...

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. More...

Detailed Description

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

A generic Multiplication 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 multiplication 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 $\amlf$ two sound abstract operators on linear forms 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,$

$i \amlf \left(i' + \sum_{v \in \cV}i'_{v}v\right) = \left(i \amifp i'\right) + \sum_{v \in \cV}\left(i \amifp i'_{v}\right)v.$

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

$\linexprenv{[a, b] \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l} = \left([a, b] \amlf \linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}\right) \aslf \left([a, b] \amlf \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l} \right)\right) \aslf mf_{\mathbf{f}}[-1, 1].$

.

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

$\linexprenv{e_{1} \otimes [a, b]}{\rho^{\#}}{\rho^{\#}_l} = \linexprenv{[a, b] \otimes e_{1}}{\rho^{\#}}{\rho^{\#}_l}.$

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

$\linexprenv{e_{1} \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l} = \linexprenv{\iota\left(\linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l} \right)\rho^{\#} \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l},$

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

Even though we intervalize the first operand in the above example, the actual implementation utilizes an heuristics for choosing which of the two operands must be intervalized in order to obtain the most precise result.

Member Function Documentation

template<typename FP_Interval_Type , typename FP_Format >

bool Parma_Polyhedra_Library::Multiplication_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_store	The interval abstract store.
lf_store	The linear form abstract store.
result	The 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	(	Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &	x,
		Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &	y
	)

template<typename FP_Interval_Type , typename FP_Format >

void swap	(	Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &	x,
		Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &	y
	)

ppl.hh

Public Types

Public Member Functions

Related Functions

Additional Inherited Members

Detailed Description

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

Member Function Documentation

Friends And Related Function Documentation

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