A generic Variable Floating Point Expression. More...

#include <ppl.hh>

Inheritance diagram for Parma_Polyhedra_Library::Variable_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.

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

void	linear_form_assign (const FP_Linear_Form &lf, FP_Linear_Form_Abstract_Store &lf_store) const
	Assigns a linear form to the variable with the same index of `*this` in a given linear form abstract store. More...

void	m_swap (Variable_Floating_Point_Expression &y)
	Swaps `*this` with `y`.

Constructors and Destructor
	Variable_Floating_Point_Expression (const dimension_type v_index)
	Constructor with a parameter: builds the variable floating point expression corresponding to the variable having `v_index` as its index.

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

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

A generic Variable 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 floating-point variable expressions

Given a variable expression $v$ and a composite abstract store $\left \llbracket \rho^{\#}, \rho^{\#}_l \right \rrbracket$ , we construct the interval linear form $\linexprenv{v}{\rho^{\#}}{\rho^{\#}_l}$ as $\rho^{\#}_l(v)$ if it is defined; otherwise we construct it as $[-1, 1]v$ .

Member Function Documentation

template<typename FP_Interval_Type , typename FP_Format >

bool Parma_Polyhedra_Library::Variable_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

inlinevirtual

Linearizes the expression in a given abstract 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 the variable in the expression 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 >.

template<typename FP_Interval_Type , typename FP_Format >

void Parma_Polyhedra_Library::Variable_Floating_Point_Expression< FP_Interval_Type, FP_Format >::linear_form_assign	(	const FP_Linear_Form &	lf,
		FP_Linear_Form_Abstract_Store &	lf_store
	)		const

inline

Assigns a linear form to the variable with the same index of *this in a given linear form abstract store.

Parameters

lf	The linear form assigned to the variable.
lf_store	The linear form abstract store.

Note that once lf is assigned to a variable, all the other entries of lf_store which contain that variable are discarded.

Friends And Related Function Documentation

template<typename FP_Interval_Type , typename FP_Format >

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

template<typename FP_Interval_Type , typename FP_Format >

void swap	(	Variable_Floating_Point_Expression< FP_Interval_Type, FP_Format > &	x,
		Variable_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::Variable_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::Variable_Floating_Point_Expression< FP_Interval_Type, FP_Format >