A generic Opposite Floating Point Expression. More...

#include <Opposite_Floating_Point_Expression.defs.hh>

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

Collaboration diagram for Parma_Polyhedra_Library::Opposite_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 a linear form with template argument `FP_Interval_Type`.
typedef Floating_Point_Expression < FP_Interval_Type, FP_Format > ::FP_Interval_Abstract_Store	FP_Interval_Abstract_Store
	Alias for a map that associates a variable index to an interval.
typedef Floating_Point_Expression < FP_Interval_Type, FP_Format > ::FP_Linear_Form_Abstract_Store	FP_Linear_Form_Abstract_Store
	Alias for a map that associates a variable index to a linear form.
typedef Floating_Point_Expression < FP_Interval_Type, FP_Format > ::boundary_type	boundary_type
	The floating point format used by the analyzer.
typedef Floating_Point_Expression < FP_Interval_Type, FP_Format > ::info_type	info_type
	The interval policy used by `FP_Interval_Type`.
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 (Opposite_Floating_Point_Expression &y)
	Swaps `*this` with `y`.
Constructors and Destructor
	Opposite_Floating_Point_Expression (Floating_Point_Expression< FP_Interval_Type, FP_Format > *const op)
	Constructor with one parameter: builds the opposite floating point expression $\ominus$ `op`.
	~Opposite_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.

Private Member Functions
	Opposite_Floating_Point_Expression (const Opposite_Floating_Point_Expression &y)
	Inhibited copy constructor.
Opposite_Floating_Point_Expression &	operator= (const Opposite_Floating_Point_Expression &y)
	Inhibited assignment operator.

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

Related Functions
(Note that these are not member functions.)
template<typename FP_Interval_Type , typename FP_Format >
void	swap (Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format > &x, Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format > &y)
	Swaps `x` with `y`.
template<typename FP_Interval_Type , typename FP_Format >
void	swap (Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format > &x, Opposite_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::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >

A generic Opposite 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 opposite floating-point expressions

Let $i + \sum_{v \in \cV}i_{v}v$ be an interval linear form and let $\adlf$ be a sound unary operator on linear forms such that:

$\adlf \left(i + \sum_{v \in \cV}i_{v}v\right) = \left(\adifp i\right) + \sum_{v \in \cV}\left(\adifp i_{v} \right)v,$

Given a floating point expression $\ominus e$ and a composite abstract store $\left \llbracket \rho^{\#}, \rho^{\#}_l \right \rrbracket$ , we construct the interval linear form $\linexprenv{\ominus e}{\rho^{\#}}{\rho^{\#}_l}$ as follows:

$\linexprenv{\ominus e}{\rho^{\#}}{\rho^{\#}_l} = \adlf \left( \linexprenv{e}{\rho^{\#}}{\rho^{\#}_l} \right).$

Definition at line 81 of file Opposite_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::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >::boundary_type

The floating point format used by the analyzer.

Reimplemented from Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >.

Definition at line 116 of file Opposite_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::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Interval_Abstract_Store

Alias for a map that associates a variable index to an interval.

Alias for a Box storing lower and upper bounds for floating point variables.

The type a linear form abstract store associating each variable with an interval that correctly approximates its value.

Reimplemented from Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >.

Definition at line 100 of file Opposite_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::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Linear_Form

Alias for a linear form with template argument FP_Interval_Type.

Reimplemented from Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >.

Definition at line 92 of file Opposite_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::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Linear_Form_Abstract_Store

Alias for a map that associates a variable index to a linear form.

The type a linear form abstract store associating each variable with a linear form that correctly approximates its value.

Reimplemented from Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >.

Definition at line 108 of file Opposite_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::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >::info_type

The interval policy used by FP_Interval_Type.

Reimplemented from Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >.

Definition at line 122 of file Opposite_Floating_Point_Expression.defs.hh.

Constructor & Destructor Documentation

template<typename FP_Interval_Type , typename FP_Format >

Parma_Polyhedra_Library::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >::Opposite_Floating_Point_Expression ( Floating_Point_Expression< FP_Interval_Type, FP_Format > *const op )

inlineexplicit

Constructor with one parameter: builds the opposite floating point expression $\ominus$ op.

Definition at line 34 of file Opposite_Floating_Point_Expression.inlines.hh.

  : operand(op)
{
  assert(op != 0);
}

template<typename FP_Interval_Type , typename FP_Format >

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

inline

Destructor.

Definition at line 44 of file Opposite_Floating_Point_Expression.inlines.hh.

                                      {
  delete operand;
}

template<typename FP_Interval_Type, typename FP_Format>

Parma_Polyhedra_Library::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >::Opposite_Floating_Point_Expression ( const Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format > & y )

private

Inhibited copy constructor.

Member Function Documentation

template<typename FP_Interval_Type , typename FP_Format >

bool Parma_Polyhedra_Library::Opposite_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 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 expression represented by 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 59 of file Opposite_Floating_Point_Expression.inlines.hh.

References Parma_Polyhedra_Library::Linear_Form< C >::negate().

                                          {
  if (!operand->linearize(int_store, lf_store, result))
    return false;
  result.negate();
  return true;
}

template<typename FP_Interval_Type , typename FP_Format >

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

inline

Swaps *this with y.

Definition at line 51 of file Opposite_Floating_Point_Expression.inlines.hh.

References Parma_Polyhedra_Library::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >::operand, and Parma_Polyhedra_Library::swap().

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

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

template<typename FP_Interval_Type, typename FP_Format>

Opposite_Floating_Point_Expression& Parma_Polyhedra_Library::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >::operator= ( const Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format > & y )

private

Inhibited assignment operator.

Friends And Related Function Documentation

template<typename FP_Interval_Type , typename FP_Format >

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

template<typename FP_Interval_Type , typename FP_Format >

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

References Parma_Polyhedra_Library::Opposite_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::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >::operand

private

Pointer to the operand.

Definition at line 185 of file Opposite_Floating_Point_Expression.defs.hh.

Referenced by Parma_Polyhedra_Library::Opposite_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::Opposite_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::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >