Widening operators on polyhedra lattice

These two operations are parametrized by the widening mode, see Widening mode.

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.