4. Various existing implementations:

For the bounded from above or from below status, we have seen the equivalent notions only in PPL. Besides the emptiness test int ppl_Polyhedron_is_empty(ppl_const_Polyhedron_t ph), we have functions that are not available in $C^3$, such as int ppl_Polyhedron_is_bounded
(ppl_const_Polyhedron_t ph), int ppl_Polyhedron_bounds_from_above(ppl_const_Polyhedron_t ph), or int ppl_Polyhedron_bounds_from_below(ppl_const_Polyhedron_t ph) .

PPL uses the notation get_relation_with_, which permits specifying many relations such as inclusion, equality, disjoint, strictly or not, etc. This notation is not used in the other libraries. In New POLKA, the notation _versus_ is used. This notation is however in our opinion not intuitive enough.