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

A generic Multiplication Floating Point Expression. More...

#include <Multiplication_Floating_Point_Expression.defs.hh>

Inheritance diagram for Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >:
Inheritance graph
[legend]
Collaboration diagram for Parma_Polyhedra_Library::Multiplication_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.
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 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 (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.

Private Member Functions

 Multiplication_Floating_Point_Expression (const Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &e)
 Inhibited copy constructor.
Multiplication_Floating_Point_Expression
< FP_Interval_Type, FP_Format > & 		operator= (const Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &e)
 Inhibited assignment operator.

Private Attributes

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

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

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.

Definition at line 131 of file Multiplication_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::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::boundary_type

Alias for the FP_Interval_Type::boundary_type from Floating_Point_Expression.

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

Definition at line 166 of file Multiplication_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::Multiplication_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 150 of file Multiplication_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::Multiplication_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 142 of file Multiplication_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::Multiplication_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 158 of file Multiplication_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::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::info_type

Alias for the FP_Interval_Type::info_type from Floating_Point_Expression.

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

Definition at line 172 of file Multiplication_Floating_Point_Expression.defs.hh.

Constructor & Destructor Documentation

template<typename FP_Interval_Type , typename FP_Format >
Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::Multiplication_Floating_Point_Expression ( Floating_Point_Expression< FP_Interval_Type, FP_Format > *const  x,
Floating_Point_Expression< FP_Interval_Type, FP_Format > *const  y 
)
inline

Constructor with two parameters: builds the multiplication floating point expression corresponding to x $\otimes$ y.

Definition at line 35 of file Multiplication_Floating_Point_Expression.inlines.hh.

  : first_operand(x), second_operand(y) {
  assert(x != 0);
  assert(y != 0);
}
template<typename FP_Interval_Type , typename FP_Format >
Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::~Multiplication_Floating_Point_Expression ( )
inline

Destructor.

Definition at line 46 of file Multiplication_Floating_Point_Expression.inlines.hh.

                                            {
  delete first_operand;
  delete second_operand;
}
template<typename FP_Interval_Type, typename FP_Format>
Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::Multiplication_Floating_Point_Expression ( const Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &  e)
private

Inhibited copy constructor.

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_storeThe interval abstract store.
lf_storeThe linear form abstract store.
resultThe 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 Multiplication_Floating_Point_Expression.templates.hh.

                                          {
  /*
    FIXME: We currently adopt the "Interval-Size Local" strategy in order to
    decide which of the two linear forms must be intervalized, as described
    in Section 6.2.4 ("Multiplication Strategies") of Antoine Mine's Ph.D.
    thesis "Weakly Relational Numerical Abstract Domains".
    In this Section are also described other multiplication strategies, such
    as All-Cases, Relative-Size Local, Simplification-Driven Global and
    Homogeneity Global.
  */

  // Here we choose which of the two linear forms must be intervalized.

  // true if we intervalize the first form, false if we intervalize the second.
  bool intervalize_first;
  FP_Linear_Form linearized_first_operand;
  if (!first_operand->linearize(int_store, lf_store,
                               linearized_first_operand))
    return false;
  FP_Interval_Type intervalized_first_operand;
  this->intervalize(linearized_first_operand, int_store,
                    intervalized_first_operand);
  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);

  // FIXME: we are not sure that what we do here is policy-proof.
  if (intervalized_first_operand.is_bounded()) {
    if (intervalized_second_operand.is_bounded()) {
      boundary_type first_interval_size
        = intervalized_first_operand.upper()
        - intervalized_first_operand.lower();
      boundary_type second_interval_size
        = intervalized_second_operand.upper()
        - intervalized_second_operand.lower();
      if (first_interval_size <= second_interval_size)
        intervalize_first = true;
      else
        intervalize_first = false;
    }
    else
      intervalize_first = true;
  }
  else {
    if (intervalized_second_operand.is_bounded())
      intervalize_first = false;
    else
      return false;
  }

  // Here we do the actual computation.
  // For optimizing, we store the relative error directly into result.
  if (intervalize_first) {
    relative_error(linearized_second_operand, result);
    linearized_second_operand *= intervalized_first_operand;
    result *= intervalized_first_operand;
    result += linearized_second_operand;
  }
  else {
    relative_error(linearized_first_operand, result);
    linearized_first_operand *= intervalized_second_operand;
    result *= intervalized_second_operand;
    result += linearized_first_operand;
  }

  result += this->absolute_error;
  return !this->overflows(result);
}
template<typename FP_Interval_Type , typename FP_Format >
void Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::m_swap ( Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &  y)
inline

Swaps *this with y.

Definition at line 54 of file Multiplication_Floating_Point_Expression.inlines.hh.

References Parma_Polyhedra_Library::swap().

Referenced by Parma_Polyhedra_Library::Multiplication_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>
Multiplication_Floating_Point_Expression<FP_Interval_Type, FP_Format>& Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::operator= ( const Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &  e)
private

Inhibited assignment operator.

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 
)
related

Swaps x with 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 
)
related

Definition at line 64 of file Multiplication_Floating_Point_Expression.inlines.hh.

References Parma_Polyhedra_Library::Multiplication_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::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::first_operand
private

Pointer to the first operand.

Definition at line 221 of file Multiplication_Floating_Point_Expression.defs.hh.

template<typename FP_Interval_Type, typename FP_Format>
Floating_Point_Expression<FP_Interval_Type, FP_Format>* Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::second_operand
private

Pointer to the second operand.

Definition at line 223 of file Multiplication_Floating_Point_Expression.defs.hh.

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