1. Description:

The emptiness test, also known as feasibility or satisfiability test in case of polyhedra, verifies if a HQSet represents an empty set or not. A HQSet over $D^n$ is said to be not empty when it contains at least one element in $D^n$, or empty if it contains no element.

The emptiness test of a rational polyhedron by means of its generating system is equal to the satisfiability test of its constraint system, since we have the duality of the two representations . A constraint system is said to be satisfiable or feasible, if all its constraints are simultaneously satisfied or feasible; on the contrary, if we detect a contradiction among its constraints, it is said to be not satisfiable or infeasible.

Sometime this operator can be referred as, although it is not much in use yet, is_bottom test of an element. This is due to the fact that when we consider the lattice of the abstract domain, we call the empty HQSet the bottom element of the lattice, and the HQSet that spans all the space, the top element.

The emptiness test for a HQSet normally returns a boolean answer, whereas its semantics is different for integer and rational elements. The complexity of available algorithms is usually exponential. Indeed, it returns the answer not practically calculable when an exception is raised, due to computing complexity. In this case we cannot prove whether the HQSet is empty or not.

The emptiness test has only one integer implementation, JANUS [SOG], adapted by the author to be used in $C^3$. Therefore, existing implementations for rational and integer problem are:

• Only rational operators: New POLKA, PPL;
• Integer when possible, otherwise use rational operator: $C^3$.

About exception handlers, existing solutions using C language, with magnitude overflow and out-of-memory space are:

• CATCH/THROW mechanism: $C^3$;
• Integer returned codes which indicate exceptions: PPL;
• No exception handlers: New POLKA.

In the next section, we present our prototype signature for the emptiness test, which in fact can be used for status-related queries.