PPL  1.2
Public Member Functions | Static Public Member Functions | Related Functions | List of all members
Parma_Polyhedra_Library::Linear_Form< C > Class Template Reference
C++ Language Interface

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

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 FP_Interval_Type >
void discard_occurrences (std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Variable var)
 
template<typename FP_Interval_Type >
void affine_form_image (std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Variable var, const Linear_Form< FP_Interval_Type > &lf)
 
template<typename FP_Interval_Type >
void upper_bound_assign (std::map< dimension_type, Linear_Form< FP_Interval_Type > > &ls1, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &ls2)
 
template<typename C >
void swap (Linear_Form< C > &x, Linear_Form< C > &y)
 Swaps x with y. More...
 
template<typename C >
Linear_Form< C > operator+ (const Linear_Form< C > &f1, const Linear_Form< C > &f2)
 Returns the linear form f1 + f2. More...
 
template<typename C >
Linear_Form< C > operator+ (Variable v, const Linear_Form< C > &f)
 Returns the linear form v + f. More...
 
template<typename C >
Linear_Form< C > operator+ (const Linear_Form< C > &f, Variable v)
 Returns the linear form f + v. More...
 
template<typename C >
Linear_Form< C > operator+ (const C &n, const Linear_Form< C > &f)
 Returns the linear form n + f. More...
 
template<typename C >
Linear_Form< C > operator+ (const Linear_Form< C > &f, const C &n)
 Returns the linear form f + n. More...
 
template<typename C >
Linear_Form< C > operator+ (const Linear_Form< C > &f)
 Returns the linear form f. More...
 
template<typename C >
Linear_Form< C > operator- (const Linear_Form< C > &f)
 Returns the linear form - f. More...
 
template<typename C >
Linear_Form< C > operator- (const Linear_Form< C > &f1, const Linear_Form< C > &f2)
 Returns the linear form f1 - f2. More...
 
template<typename C >
Linear_Form< C > operator- (Variable v, const Linear_Form< C > &f)
 Returns the linear form v - f. More...
 
template<typename C >
Linear_Form< C > operator- (const Linear_Form< C > &f, Variable v)
 Returns the linear form f - v. More...
 
template<typename C >
Linear_Form< C > operator- (const C &n, const Linear_Form< C > &f)
 Returns the linear form n - f. More...
 
template<typename C >
Linear_Form< C > operator- (const Linear_Form< C > &f, const C &n)
 Returns the linear form f - n. More...
 
template<typename C >
Linear_Form< C > operator* (const C &n, const Linear_Form< C > &f)
 Returns the linear form n * f. More...
 
template<typename C >
Linear_Form< C > operator* (const Linear_Form< C > &f, const C &n)
 Returns the linear form f * n. More...
 
template<typename C >
Linear_Form< C > & operator+= (Linear_Form< C > &f1, const Linear_Form< C > &f2)
 Returns the linear form f1 + f2 and assigns it to e1. More...
 
template<typename C >
Linear_Form< C > & operator+= (Linear_Form< C > &f, Variable v)
 Returns the linear form f + v and assigns it to f. More...
 
template<typename C >
Linear_Form< C > & operator+= (Linear_Form< C > &f, const C &n)
 Returns the linear form f + n and assigns it to f. More...
 
template<typename C >
Linear_Form< C > & operator-= (Linear_Form< C > &f1, const Linear_Form< C > &f2)
 Returns the linear form f1 - f2 and assigns it to f1. More...
 
template<typename C >
Linear_Form< C > & operator-= (Linear_Form< C > &f, Variable v)
 Returns the linear form f - v and assigns it to f. More...
 
template<typename C >
Linear_Form< C > & operator-= (Linear_Form< C > &f, const C &n)
 Returns the linear form f - n and assigns it to f. More...
 
template<typename C >
Linear_Form< C > & operator*= (Linear_Form< C > &f, const C &n)
 Returns the linear form n * f and assigns it to f. More...
 
template<typename C >
Linear_Form< C > & operator/= (Linear_Form< C > &f, const C &n)
 Returns the linear form f / n and assigns it to f. More...
 
template<typename C >
bool operator== (const Linear_Form< C > &x, const Linear_Form< C > &y)
 Returns true if and only if x and y are equal. More...
 
template<typename C >
bool operator!= (const Linear_Form< C > &x, const Linear_Form< C > &y)
 Returns true if and only if x and y are different. More...
 
template<typename C >
std::ostream & operator<< (std::ostream &s, const Linear_Form< C > &f)
 Output operator. More...
 
template<typename C >
Linear_Form< C > operator+ (const Linear_Form< C > &f)
 
template<typename C >
Linear_Form< C > operator+ (const Linear_Form< C > &f, const C &n)
 
template<typename C >
Linear_Form< C > operator+ (const Linear_Form< C > &f, const Variable v)
 
template<typename C >
Linear_Form< C > operator- (const Linear_Form< C > &f, const C &n)
 
template<typename C >
Linear_Form< C > operator- (const Variable v, const Variable w)
 
template<typename C >
Linear_Form< C > operator* (const Linear_Form< C > &f, const C &n)
 
template<typename C >
Linear_Form< C > & operator+= (Linear_Form< C > &f, const C &n)
 
template<typename C >
Linear_Form< C > & operator-= (Linear_Form< C > &f, const C &n)
 
template<typename C >
bool operator!= (const Linear_Form< C > &x, const Linear_Form< C > &y)
 
template<typename C >
void swap (Linear_Form< C > &x, Linear_Form< C > &y)
 
template<typename C >
Linear_Form< C > operator+ (const Linear_Form< C > &f1, const Linear_Form< C > &f2)
 
template<typename C >
Linear_Form< C > operator+ (const Variable v, const Linear_Form< C > &f)
 
template<typename C >
Linear_Form< C > operator+ (const C &n, const Linear_Form< C > &f)
 
template<typename C >
Linear_Form< C > operator- (const Linear_Form< C > &f)
 
template<typename C >
Linear_Form< C > operator- (const Linear_Form< C > &f1, const Linear_Form< C > &f2)
 
template<typename C >
Linear_Form< C > operator- (const Variable v, const Linear_Form< C > &f)
 
template<typename C >
Linear_Form< C > operator- (const Linear_Form< C > &f, const Variable v)
 
template<typename C >
Linear_Form< C > operator- (const C &n, const Linear_Form< C > &f)
 
template<typename C >
Linear_Form< C > operator* (const C &n, const Linear_Form< C > &f)
 
template<typename C >
Linear_Form< C > & operator+= (Linear_Form< C > &f1, const Linear_Form< C > &f2)
 
template<typename C >
Linear_Form< C > & operator+= (Linear_Form< C > &f, const Variable v)
 
template<typename C >
Linear_Form< C > & operator-= (Linear_Form< C > &f1, const Linear_Form< C > &f2)
 
template<typename C >
Linear_Form< C > & operator-= (Linear_Form< C > &f, const Variable v)
 
template<typename C >
Linear_Form< C > & operator*= (Linear_Form< C > &f, const C &n)
 
template<typename C >
Linear_Form< C > & operator/= (Linear_Form< C > &f, const C &n)
 
template<typename C >
bool operator== (const Linear_Form< C > &x, const Linear_Form< C > &y)
 
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 $x_i$ is given by $i + 1$.
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 $lf = x_5 - x_2 + 1$ 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 >
Parma_Polyhedra_Library::Linear_Form< C >::Linear_Form ( Variable  v)

Builds the linear form corresponding to the variable v.

Exceptions
std::length_errorThrown if the space dimension of v exceeds Linear_Form::max_space_dimension().

Member Function Documentation

template<typename C >
bool Parma_Polyhedra_Library::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 Parma_Polyhedra_Library::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_formatThe floating point format used by the analyzed program.
resultBecomes 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 Parma_Polyhedra_Library::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
oracleThe FP_Oracle to be queried.
resultThe 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 FP_Interval_Type >
void discard_occurrences ( std::map< dimension_type, Linear_Form< FP_Interval_Type > > &  lf_store,
Variable  var 
)
related

Discards all linear forms containing variable var from the linear form abstract store lf_store.

template<typename FP_Interval_Type >
void affine_form_image ( std::map< dimension_type, Linear_Form< FP_Interval_Type > > &  lf_store,
Variable  var,
const Linear_Form< FP_Interval_Type > &  lf 
)
related

Assigns the linear form lf to var in the linear form abstract store lf_store, then discards all occurrences of var from it.

template<typename FP_Interval_Type >
void upper_bound_assign ( std::map< dimension_type, Linear_Form< FP_Interval_Type > > &  ls1,
const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &  ls2 
)
related

Discards from ls1 all linear forms but those that are associated to the same variable in ls2.

template<typename C >
void swap ( Linear_Form< C > &  x,
Linear_Form< C > &  y 
)
related

Swaps x with y.

template<typename C >
Linear_Form< C > operator+ ( const Linear_Form< C > &  f1,
const Linear_Form< C > &  f2 
)
related

Returns the linear form f1 + f2.

template<typename C >
Linear_Form< C > operator+ ( Variable  v,
const Linear_Form< C > &  f 
)
related

Returns the linear form v + f.

template<typename C >
Linear_Form< C > operator+ ( const Linear_Form< C > &  f,
Variable  v 
)
related

Returns the linear form f + v.

template<typename C >
Linear_Form< C > operator+ ( const C &  n,
const Linear_Form< C > &  f 
)
related

Returns the linear form n + f.

template<typename C >
Linear_Form< C > operator+ ( const Linear_Form< C > &  f,
const C &  n 
)
related

Returns the linear form f + n.

template<typename C >
Linear_Form< C > operator+ ( const Linear_Form< C > &  f)
related

Returns the linear form f.

template<typename C >
Linear_Form< C > operator- ( const Linear_Form< C > &  f)
related

Returns the linear form - f.

template<typename C >
Linear_Form< C > operator- ( const Linear_Form< C > &  f1,
const Linear_Form< C > &  f2 
)
related

Returns the linear form f1 - f2.

template<typename C >
Linear_Form< C > operator- ( Variable  v,
const Linear_Form< C > &  f 
)
related

Returns the linear form v - f.

template<typename C >
Linear_Form< C > operator- ( const Linear_Form< C > &  f,
Variable  v 
)
related

Returns the linear form f - v.

template<typename C >
Linear_Form< C > operator- ( const C &  n,
const Linear_Form< C > &  f 
)
related

Returns the linear form n - f.

template<typename C >
Linear_Form< C > operator- ( const Linear_Form< C > &  f,
const C &  n 
)
related

Returns the linear form f - n.

template<typename C >
Linear_Form< C > operator* ( const C &  n,
const Linear_Form< C > &  f 
)
related

Returns the linear form n * f.

template<typename C >
Linear_Form< C > operator* ( const Linear_Form< C > &  f,
const C &  n 
)
related

Returns the linear form f * n.

template<typename C >
Linear_Form< C > & operator+= ( Linear_Form< C > &  f1,
const Linear_Form< C > &  f2 
)
related

Returns the linear form f1 + f2 and assigns it to e1.

template<typename C >
Linear_Form< C > & operator+= ( Linear_Form< C > &  f,
Variable  v 
)
related

Returns the linear form f + v and assigns it to f.

Exceptions
std::length_errorThrown if the space dimension of v exceeds Linear_Form::max_space_dimension().
template<typename C >
Linear_Form< C > & operator+= ( Linear_Form< C > &  f,
const C &  n 
)
related

Returns the linear form f + n and assigns it to f.

template<typename C >
Linear_Form< C > & operator-= ( Linear_Form< C > &  f1,
const Linear_Form< C > &  f2 
)
related

Returns the linear form f1 - f2 and assigns it to f1.

template<typename C >
Linear_Form< C > & operator-= ( Linear_Form< C > &  f,
Variable  v 
)
related

Returns the linear form f - v and assigns it to f.

Exceptions
std::length_errorThrown if the space dimension of v exceeds Linear_Form::max_space_dimension().
template<typename C >
Linear_Form< C > & operator-= ( Linear_Form< C > &  f,
const C &  n 
)
related

Returns the linear form f - n and assigns it to f.

template<typename C >
Linear_Form< C > & operator*= ( Linear_Form< C > &  f,
const C &  n 
)
related

Returns the linear form n * f and assigns it to f.

template<typename C >
Linear_Form< C > & operator/= ( Linear_Form< C > &  f,
const C &  n 
)
related

Returns the linear form f / n and assigns it to f.

Performs the division of a linear form by a scalar. It is up to the user to ensure that division by 0 is not performed.

template<typename C >
bool operator== ( const Linear_Form< C > &  x,
const Linear_Form< C > &  y 
)
related

Returns true if and only if x and y are equal.

template<typename C >
bool operator!= ( const Linear_Form< C > &  x,
const Linear_Form< C > &  y 
)
related

Returns true if and only if x and y are different.

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

Output operator.

template<typename C >
Linear_Form< C > operator+ ( const Linear_Form< C > &  f)
related
template<typename C >
Linear_Form< C > operator+ ( const Linear_Form< C > &  f,
const C &  n 
)
related
template<typename C >
Linear_Form< C > operator+ ( const Linear_Form< C > &  f,
const Variable  v 
)
related
template<typename C >
Linear_Form< C > operator- ( const Linear_Form< C > &  f,
const C &  n 
)
related
template<typename C >
Linear_Form< C > operator- ( const Variable  v,
const Variable  w 
)
related
template<typename C >
Linear_Form< C > operator* ( const Linear_Form< C > &  f,
const C &  n 
)
related
template<typename C >
Linear_Form< C > & operator+= ( Linear_Form< C > &  f,
const C &  n 
)
related
template<typename C >
Linear_Form< C > & operator-= ( Linear_Form< C > &  f,
const C &  n 
)
related
template<typename C >
bool operator!= ( const Linear_Form< C > &  x,
const Linear_Form< C > &  y 
)
related
template<typename C >
void swap ( Linear_Form< C > &  x,
Linear_Form< C > &  y 
)
related
template<typename C >
Linear_Form< C > operator+ ( const Linear_Form< C > &  f1,
const Linear_Form< C > &  f2 
)
related
template<typename C >
Linear_Form< C > operator+ ( const Variable  v,
const Linear_Form< C > &  f 
)
related
template<typename C >
Linear_Form< C > operator+ ( const C &  n,
const Linear_Form< C > &  f 
)
related
template<typename C >
Linear_Form< C > operator- ( const Linear_Form< C > &  f)
related
template<typename C >
Linear_Form< C > operator- ( const Linear_Form< C > &  f1,
const Linear_Form< C > &  f2 
)
related
template<typename C >
Linear_Form< C > operator- ( const Variable  v,
const Linear_Form< C > &  f 
)
related
template<typename C >
Linear_Form< C > operator- ( const Linear_Form< C > &  f,
const Variable  v 
)
related
template<typename C >
Linear_Form< C > operator- ( const C &  n,
const Linear_Form< C > &  f 
)
related
template<typename C >
Linear_Form< C > operator* ( const C &  n,
const Linear_Form< C > &  f 
)
related
template<typename C >
Linear_Form< C > & operator+= ( Linear_Form< C > &  f1,
const Linear_Form< C > &  f2 
)
related
template<typename C >
Linear_Form< C > & operator+= ( Linear_Form< C > &  f,
const Variable  v 
)
related
template<typename C >
Linear_Form< C > & operator-= ( Linear_Form< C > &  f1,
const Linear_Form< C > &  f2 
)
related
template<typename C >
Linear_Form< C > & operator-= ( Linear_Form< C > &  f,
const Variable  v 
)
related
template<typename C >
Linear_Form< C > & operator*= ( Linear_Form< C > &  f,
const C &  n 
)
related
template<typename C >
Linear_Form< C > & operator/= ( Linear_Form< C > &  f,
const C &  n 
)
related
template<typename C >
bool operator== ( const Linear_Form< C > &  x,
const Linear_Form< C > &  y 
)
related
template<typename C >
std::ostream & operator<< ( std::ostream &  s,
const Linear_Form< C > &  f 
)
related
The documentation for this class was generated from the following file: