5. Clarity of terminology in use:

We also have other examples about the clarity of terminology in use. It is not clear how to define and use minimization, normalization, simplification in existing implementations. Similarly, the closure operator in the octagon library does not make much sense in the polyhedral domain. For more explanation, one is referred to [APRa], where the term canonicalization is also introduced.

In Octagon, we have bool oct_is_empty(oct_t* m), tbool oct_is_empty_lazy(oct_t* m), that test the emptiness of the octagon in question. bool oct_is_universe(oct_t* m) tests whether the octagon is the constant universe or not. bool oct_is_closed(oct_t* m), is a low level function that tests if the octagon is closed or not, meanwhile all the polyhedra are closed (see the author's thesis for the octagonal domain).

In New POLKA, we have bool poly_is_empty (const poly_t* po) and tbool poly_is_empty_lazy (const poly_t* po) that test the emptiness of the polyhedron, bool poly_is_universe (const poly_t* po) that tests if the polyhedron is the constant universe.

Here, bool is the standard boolean type with two values, true and false, whereas tbool stands for the triple true, false and top. The top element serves for exceptional cases, i.e. do not know.