A linear form with interval coefficients. More...

#include <ppl.hh>

Public Member Functions
	Linear_Form ()
	Default constructor: returns a copy of Linear_Form::zero().

	Linear_Form (const Linear_Form &f)
	Ordinary copy constructor.

	~Linear_Form ()
	Destructor.

	Linear_Form (const C &n)
	Builds the linear form corresponding to the inhomogeneous term `n`.

	Linear_Form (Variable v)
	Builds the linear form corresponding to the variable `v`.

	Linear_Form (const Linear_Expression &e)
	Builds a linear form approximating the linear expression `e`.

dimension_type	space_dimension () const
	Returns the dimension of the vector space enclosing `*this`.

const C &	coefficient (Variable v) const
	Returns the coefficient of `v` in `*this`.

const C &	inhomogeneous_term () const
	Returns the inhomogeneous term of `*this`.

void	negate ()
	Negates all the coefficients of `*this`.

memory_size_type	total_memory_in_bytes () const
	Returns a lower bound to the total size in bytes of the memory occupied by `*this`.

memory_size_type	external_memory_in_bytes () const
	Returns the size in bytes of the memory managed by `*this`.

void	ascii_dump () const
	Writes to `std::cerr` an ASCII representation of `*this`.

void	ascii_dump (std::ostream &s) const
	Writes to `s` an ASCII representation of `*this`.

void	print () const
	Prints `*this` to `std::cerr` using `operator<<`.

bool	ascii_load (std::istream &s)
	Loads from `s` an ASCII representation (as produced by ascii_dump(std::ostream&) const) and sets `*this` accordingly. Returns `true` if successful, `false` otherwise.

bool	OK () const
	Checks if all the invariants are satisfied.

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

bool	overflows () const
	Verifies if the linear form overflows.

void	relative_error (Floating_Point_Format analyzed_format, Linear_Form &result) const
	Computes the relative error associated to floating point computations that operate on a quantity that is overapproximated by `*this`.

template<typename Target >
bool	intervalize (const FP_Oracle< Target, C > &oracle, C &result) const
	Makes `result` become an interval that overapproximates all the possible values of `*this`.

Static Public Member Functions
static dimension_type	max_space_dimension ()
	Returns the maximum space dimension a Linear_Form can handle.

Related Functions
(Note that these are not member functions.)
template<typename C >
std::ostream &	operator<< (std::ostream &s, const Linear_Form< C > &f)
	Output operator.

template<typename C >
std::ostream &	operator<< (std::ostream &s, const Linear_Form< C > &f)

Detailed Description

template<typename C>
class Parma_Polyhedra_Library::Linear_Form< C >

A linear form with interval coefficients.

An object of the class Linear_Form represents the interval linear form

$\sum_{i=0}^{n-1} a_i x_i + b$

where $n$ is the dimension of the vector space, each $a_i$ is the coefficient of the $i$ -th variable $x_i$ and $b$ is the inhomogeneous term. The coefficients and the inhomogeneous term of the linear form have the template parameter C as their type. C must be the type of an Interval.

How to build a linear form.: A full set of functions is defined in order to provide a convenient interface for building complex linear forms starting from simpler ones and from objects of the classes Variable and C. Available operators include binary addition and subtraction, as well as multiplication and division by a coefficient. The space dimension of a linear form is defined as the highest variable dimension among variables that have a nonzero coefficient in the linear form, or zero if no such variable exists. The space dimension for each variable is given by .

Example: Given the type T of an Interval with floating point coefficients (though any integral type may also be used), the following code builds the interval linear form with space dimension 6:
Variable x5(5);

Variable x2(2);

T x5_coefficient;

x5_coefficient.lower() = 2.0;

x5_coefficient.upper() = 3.0;

T inhomogeneous_term;

inhomogeneous_term.lower() = 4.0;

inhomogeneous_term.upper() = 8.0;

Linear_Form<T> lf(x2);

lf = -lf;

lf += Linear_Form<T>(x2);

Linear_Form<T> lf_x5(x5);

lf_x5 *= x5_coefficient;

lf += lf_x5;

Note that lf_x5 is created with space dimension 6, while lf is created with space dimension 0 and then extended first to space dimension 2 when x2 is subtracted and finally to space dimension 6 when lf_x5 is added.

Constructor & Destructor Documentation

template<typename C >

Linear_Form< C >::Linear_Form ( Variable v )

Builds the linear form corresponding to the variable v.

Exceptions

std::length_error Thrown if the space dimension of v exceeds Linear_Form::max_space_dimension().

Member Function Documentation

template<typename C >

bool Linear_Form< C >::overflows ( ) const

inline

Verifies if the linear form overflows.

Returns: Returns false if all coefficients in lf are bounded, true otherwise.

T must be the type of possibly unbounded quantities.

template<typename C >

void Linear_Form< C >::relative_error	(	Floating_Point_Format	analyzed_format,
		Linear_Form< C > &	result
	)		const

Computes the relative error associated to floating point computations that operate on a quantity that is overapproximated by *this.

Parameters

analyzed_format	The floating point format used by the analyzed program.
result	Becomes the linear form corresponding to the relative error committed.

This method makes result become a linear form obtained by evaluating the function $\varepsilon_{\mathbf{f}}(l)$ on the linear form. This function is defined as:

$\varepsilon_{\mathbf{f}}\left([a, b]+\sum_{v \in \cV}[a_{v}, b_{v}]v\right) \defeq (\textrm{max}(|a|, |b|) \amifp [-\beta^{-\textrm{p}}, \beta^{-\textrm{p}}]) + \sum_{v \in \cV}(\textrm{max}(|a_{v}|,|b_{v}|) \amifp [-\beta^{-\textrm{p}}, \beta^{-\textrm{p}}])v$

where p is the fraction size in bits for the format $\mathbf{f}$ and $\beta$ the base.

The result is undefined if T is not the type of an interval with floating point boundaries.

template<typename C >

template<typename Target >

bool Linear_Form< C >::intervalize	(	const FP_Oracle< Target, C > &	oracle,
		C &	result
	)		const

Makes result become an interval that overapproximates all the possible values of *this.

Parameters

oracle	The FP_Oracle to be queried.
result	The linear form that will store the result.

Returns: true if the operation was successful, false otherwise (the possibility of failure depends on the oracle's implementation).

Template type parameters

The class template parameter Target specifies the implementation of Concrete_Expression to be used.

This method makes result become $\iota(lf)\rho^{\#}$ , that is an interval defined as:

$\iota\left(i + \sum_{v \in \cV}i_{v}v\right)\rho^{\#} \defeq i \asifp \left(\bigoplus_{v \in \cV}{}^{\#}i_{v} \amifp \rho^{\#}(v)\right)$

where $\rho^{\#}(v)$ is an interval (provided by the oracle) that correctly approximates the value of $v$ .

The result is undefined if C is not the type of an interval with floating point boundaries.

Friends And Related Function Documentation

template<typename C >

std::ostream & operator<<	(	std::ostream &	s,
		const Linear_Form< C > &	f
	)

template<typename C >

std::ostream & operator<<	(	std::ostream &	s,
		const Linear_Form< C > &	f
	)

ppl.hh

Public Member Functions

Static Public Member Functions

Related Functions

Detailed Description

template<typename C> class Parma_Polyhedra_Library::Linear_Form< C >

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

template<typename C>
class Parma_Polyhedra_Library::Linear_Form< C >