PPL  0.12.1
Public Types | Public Member Functions | Private Member Functions | Private Attributes | Related Functions
Parma_Polyhedra_Library::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format > Class Template Reference
C++ Language Interface

A generic Cast Floating Point Expression. More...

#include <Cast_Floating_Point_Expression.defs.hh>

Inheritance diagram for Parma_Polyhedra_Library::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format >:
Inheritance graph
[legend]
Collaboration diagram for Parma_Polyhedra_Library::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format >:
Collaboration graph
[legend]

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.

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 (Cast_Floating_Point_Expression &y)
 Swaps *this with y.
Constructors and Destructor
 Cast_Floating_Point_Expression (Floating_Point_Expression< FP_Interval_Type, FP_Format > *const expr)
 Builds a cast floating point expression with the value expressed by expr.
 ~Cast_Floating_Point_Expression ()
 Destructor.

Private Member Functions

 Cast_Floating_Point_Expression (const Cast_Floating_Point_Expression &y)
 Inhibited copy constructor.
Cast_Floating_Point_Expression & operator= (const Cast_Floating_Point_Expression &y)
 Inhibited assignment operator.

Private Attributes

Floating_Point_Expression
< FP_Interval_Type, FP_Format > * 		expr
 Pointer to the casted expression.

Related Functions

(Note that these are not member functions.)

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

Detailed Description

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

A generic Cast 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 cast expressions

Let $i + \sum_{v \in \cV}i_{v}v $ and $i' + \sum_{v \in \cV}i'_{v}v $ be two linear forms and $\aslf$ a 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. \]

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

\[ \linexprenv{cast(e)}{\rho^{\#}}{\rho^{\#}_l} = \linexprenv{e}{\rho^{\#}}{\rho^{\#}_l} \aslf \varepsilon_{\mathbf{f}}\left(\linexprenv{e}{\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.

Definition at line 90 of file Cast_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>:: FP_Interval_Abstract_Store Parma_Polyhedra_Library::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Interval_Abstract_Store

Alias for the Box<FP_Interval_Type> from Floating_Point_Expression.

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

Definition at line 109 of file Cast_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::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Linear_Form

Alias for the Linear_Form<FP_Interval_Type> from Floating_Point_Expression.

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

Definition at line 101 of file Cast_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::Cast_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.

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

Definition at line 117 of file Cast_Floating_Point_Expression.defs.hh.

Constructor & Destructor Documentation

template<typename FP_Interval_Type , typename FP_Format >
Parma_Polyhedra_Library::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format >::Cast_Floating_Point_Expression ( Floating_Point_Expression< FP_Interval_Type, FP_Format > *const  expr)
inline

Builds a cast floating point expression with the value expressed by expr.

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

  : expr(e) {
  assert(e != 0);
}
template<typename FP_Interval_Type , typename FP_Format >
Parma_Polyhedra_Library::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format >::~Cast_Floating_Point_Expression ( )
inline

Destructor.

Definition at line 43 of file Cast_Floating_Point_Expression.inlines.hh.

                                  {
  delete expr;
}
template<typename FP_Interval_Type, typename FP_Format>
Parma_Polyhedra_Library::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format >::Cast_Floating_Point_Expression ( const Cast_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::Cast_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.

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

Implements Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >.

Definition at line 32 of file Cast_Floating_Point_Expression.templates.hh.

                                          {
  if (!expr->linearize(int_store, lf_store, result))
    return false;
  FP_Linear_Form rel_error;
  relative_error(result, rel_error);
  result += rel_error;
  result += this->absolute_error;
  return !this->overflows(result);
}
template<typename FP_Interval_Type , typename FP_Format >
void Parma_Polyhedra_Library::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format >::m_swap ( Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format > &  y)
inline

Swaps *this with y.

Definition at line 50 of file Cast_Floating_Point_Expression.inlines.hh.

References Parma_Polyhedra_Library::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format >::expr, and Parma_Polyhedra_Library::swap().

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

                                          {
  swap(expr, y.expr);
}
template<typename FP_Interval_Type, typename FP_Format>
Cast_Floating_Point_Expression& Parma_Polyhedra_Library::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format >::operator= ( const Cast_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 ( Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format > &  x,
Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format > &  y 
)
related

Swaps x with y.

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

Definition at line 57 of file Cast_Floating_Point_Expression.inlines.hh.

References Parma_Polyhedra_Library::Cast_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::Cast_Floating_Point_Expression< FP_Interval_Type, FP_Format >::expr
private

Pointer to the casted expression.

Definition at line 158 of file Cast_Floating_Point_Expression.defs.hh.

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

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