The convergence certificate for the BHRZ03 widening operator. More...

#include <ppl.hh>

Classes
struct	Compare
	A total ordering on BHRZ03 certificates. More...

Public Member Functions
	BHRZ03_Certificate ()
	Default constructor.

	BHRZ03_Certificate (const Polyhedron &ph)
	Constructor: computes the certificate for `ph`.

	BHRZ03_Certificate (const BHRZ03_Certificate &y)
	Copy constructor.

	~BHRZ03_Certificate ()
	Destructor.

int	compare (const BHRZ03_Certificate &y) const
	The comparison function for certificates. More...

int	compare (const Polyhedron &ph) const
	Compares `*this` with the certificate for polyhedron `ph`.

Detailed Description

The convergence certificate for the BHRZ03 widening operator.

Convergence certificates are used to instantiate the BHZ03 framework so as to define widening operators for the finite powerset domain.

Note: Each convergence certificate has to be used together with a compatible widening operator. In particular, BHRZ03_Certificate can certify the convergence of both the BHRZ03 and the H79 widenings.

Member Function Documentation

int Parma_Polyhedra_Library::BHRZ03_Certificate::compare ( const BHRZ03_Certificate & y ) const

The comparison function for certificates.

Returns: , or depending on whether *this is smaller than, equal to, or greater than y, respectively.

Compares *this with y, using a total ordering which is a refinement of the limited growth ordering relation for the BHRZ03 widening.

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