A generic Division Floating Point Expression. More...

#include <Division_Floating_Point_Expression_defs.hh>

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

Collaboration diagram for Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >:

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

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

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

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

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

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

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

typedef FP_Interval_Type::info_type	info_type
	The interval policy used by `FP_Interval_Type`. More...

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 (Division_Floating_Point_Expression< FP_Interval_Type, FP_Format > &y)
	Swaps `*this` with `y`. More...

Constructors and Destructor
	Division_Floating_Point_Expression (Floating_Point_Expression< FP_Interval_Type, FP_Format > const num, Floating_Point_Expression< FP_Interval_Type, FP_Format > const den)
	Constructor with two parameters: builds the division floating point expression corresponding to `num` $\oslash$ `den`. More...

	~Division_Floating_Point_Expression ()
	Destructor. More...

Public Member Functions inherited from Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >
virtual	~Floating_Point_Expression ()
	Destructor. More...

Private Member Functions
	Division_Floating_Point_Expression (const Division_Floating_Point_Expression< FP_Interval_Type, FP_Format > &e)
	Copy constructor: temporary inhibited. More...

Division_Floating_Point_Expression< FP_Interval_Type, FP_Format > &	operator= (const Division_Floating_Point_Expression< FP_Interval_Type, FP_Format > &e)
	Assignment operator: temporary inhibited. More...

Private Attributes
Floating_Point_Expression< FP_Interval_Type, FP_Format > *	first_operand
	Pointer to the first operand. More...

Floating_Point_Expression< FP_Interval_Type, FP_Format > *	second_operand
	Pointer to the second operand. More...

Related Functions
(Note that these are not member functions.)
template<typename FP_Interval_Type , typename FP_Format >
void	swap (Division_Floating_Point_Expression< FP_Interval_Type, FP_Format > &x, Division_Floating_Point_Expression< FP_Interval_Type, FP_Format > &y)
	Swaps `x` with `y`. More...

template<typename FP_Interval_Type , typename FP_Format >
void	swap (Division_Floating_Point_Expression< FP_Interval_Type, FP_Format > &x, Division_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::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >

A generic Division 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.

Linearizationd of division 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 $\adivlf$ two sound abstract operator 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,$

$\left(i + \sum_{v \in \cV}i_{v}v\right) \adivlf i' = \left(i \adivifp i'\right) + \sum_{v \in \cV}\left(i_{v} \adivifp i'\right)v.$

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

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

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

$\linexprenv{e_{1} \oslash e_{2}}{\rho^{\#}}{\rho^{\#}_l} = \linexprenv{e_{1} \oslash \iota\left( \linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l} \right)\rho^{\#}}{\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.

Definition at line 118 of file Division_Floating_Point_Expression_defs.hh.

Member Typedef Documentation

template<typename FP_Interval_Type, typename FP_Format>

typedef Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::boundary_type

Alias for the FP_Interval_Type::boundary_type from Floating_Point_Expression.

Definition at line 153 of file Division_Floating_Point_Expression_defs.hh.

template<typename FP_Interval_Type, typename FP_Format>

typedef Floating_Point_Expression<FP_Interval_Type, FP_Format>::FP_Interval_Abstract_Store Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Interval_Abstract_Store

Alias for the Box<FP_Interval_Type> from Floating_Point_Expression.

Definition at line 137 of file Division_Floating_Point_Expression_defs.hh.

template<typename FP_Interval_Type, typename FP_Format>

typedef Floating_Point_Expression<FP_Interval_Type, FP_Format>::FP_Linear_Form Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Linear_Form

Alias for the Linear_Form<FP_Interval_Type> from Floating_Point_Expression.

Definition at line 129 of file Division_Floating_Point_Expression_defs.hh.

template<typename FP_Interval_Type, typename FP_Format>

typedef Floating_Point_Expression<FP_Interval_Type, FP_Format>:: FP_Linear_Form_Abstract_Store Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Linear_Form_Abstract_Store

Alias for the std::map<dimension_type, FP_Linear_Form> from Floating_Point_Expression.

Definition at line 145 of file Division_Floating_Point_Expression_defs.hh.

template<typename FP_Interval_Type, typename FP_Format>

typedef Floating_Point_Expression<FP_Interval_Type, FP_Format>::info_type Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::info_type

Alias for the FP_Interval_Type::info_type from Floating_Point_Expression.

Definition at line 159 of file Division_Floating_Point_Expression_defs.hh.

Constructor & Destructor Documentation

template<typename FP_Interval_Type , typename FP_Format >

Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::Division_Floating_Point_Expression	(	Floating_Point_Expression< FP_Interval_Type, FP_Format > *const	num,
		Floating_Point_Expression< FP_Interval_Type, FP_Format > *const	den
	)

inline

Constructor with two parameters: builds the division floating point expression corresponding to num $\oslash$ den.

Definition at line 34 of file Division_Floating_Point_Expression_inlines.hh.

   : first_operand(num), second_operand(den) {
   assert(num != 0);
   assert(den != 0);
 }

template<typename FP_Interval_Type , typename FP_Format >

Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::~Division_Floating_Point_Expression ( )

inline

Destructor.

Definition at line 45 of file Division_Floating_Point_Expression_inlines.hh.

                                       {
   delete first_operand;
   delete second_operand;
 }

template<typename FP_Interval_Type, typename FP_Format>

Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::Division_Floating_Point_Expression ( const Division_Floating_Point_Expression< FP_Interval_Type, FP_Format > & e )

private

Copy constructor: temporary inhibited.

Member Function Documentation

template<typename FP_Interval_Type , typename FP_Format >

bool Parma_Polyhedra_Library::Division_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 >.

Definition at line 32 of file Division_Floating_Point_Expression_templates.hh.

                                           {
   FP_Linear_Form linearized_second_operand;
   if (!second_operand->linearize(int_store, lf_store,
                                 linearized_second_operand)) {
     return false;
   }
   FP_Interval_Type intervalized_second_operand;
   this->intervalize(linearized_second_operand, int_store,
                     intervalized_second_operand);
 
   // Check if we may divide by zero.
   if (intervalized_second_operand.lower() <= 0
       && intervalized_second_operand.upper() >= 0) {
     return false;
   }
 
   if (!first_operand->linearize(int_store, lf_store, result)) {
     return false;
   }
   FP_Linear_Form rel_error;
   relative_error(result, rel_error);
   result /= intervalized_second_operand;
   rel_error /= intervalized_second_operand;
   result += rel_error;
   result += this->absolute_error;
   return !this->overflows(result);
 }

template<typename FP_Interval_Type , typename FP_Format >

void Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::m_swap ( Division_Floating_Point_Expression< FP_Interval_Type, FP_Format > & y )

inline

Swaps *this with y.

Definition at line 53 of file Division_Floating_Point_Expression_inlines.hh.

References Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::first_operand, Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::second_operand, and Parma_Polyhedra_Library::swap().

Referenced by Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::swap().

                                                                            {
   using std::swap;
   swap(first_operand, y.first_operand);
   swap(second_operand, y.second_operand);
 }

template<typename FP_Interval_Type, typename FP_Format>

Division_Floating_Point_Expression<FP_Interval_Type, FP_Format>& Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::operator= ( const Division_Floating_Point_Expression< FP_Interval_Type, FP_Format > & e )

private

Assignment operator: temporary inhibited.

Friends And Related Function Documentation

template<typename FP_Interval_Type , typename FP_Format >

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

template<typename FP_Interval_Type , typename FP_Format >

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

References Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::m_swap().

                                                                          {
   x.m_swap(y);
 }

Member Data Documentation

template<typename FP_Interval_Type, typename FP_Format>

Floating_Point_Expression<FP_Interval_Type, FP_Format>* Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::first_operand

private

Pointer to the first operand.

Definition at line 208 of file Division_Floating_Point_Expression_defs.hh.

Referenced by Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::m_swap().

template<typename FP_Interval_Type, typename FP_Format>

Floating_Point_Expression<FP_Interval_Type, FP_Format>* Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::second_operand

private

Pointer to the second operand.

Definition at line 210 of file Division_Floating_Point_Expression_defs.hh.

Referenced by Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >::m_swap().

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

Public Types

Public Member Functions

Private Member Functions

Private Attributes

Related Functions

Additional Inherited Members

Detailed Description

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

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation

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