Widening operators on polyhedra lattice
These two operations are parametrized by the widening mode, see
- Function: poly_t* poly_widening (const poly_t* pa, const poly_t* pb)
- This function implements the standard widening operator defined in
cousot78. Minimal form is required for the two polyhedra.
The returned polyhedron is defined by those constraints which are
satisfied by both parameter polyhedra.
- Function: poly_t* poly_limited_widening (const poly_t* pa, const poly_t* pb, matrix_t* mat)
- This function implements the version of the widening operator
parametrized by a set of constraints. It adds to the polyhedron
obtained by the standard widening the constraints of the matrix
which are satisfied by both parameter polyhedra
polka:fmsd:97. The parameter matrix may be sorted.
This document was generated
on October, 27 2006