New Polka is a library to handle convex polyhedra, whose constraints and generators have rational coefficients. It is programmed in ANSI C, so you can use it in any C or C++ programs. An interface to the OCaml language is also provided. This library is currently used in my verification tool NBac and by others research teams working on static analysis and abstract interpretation.
It is mainly based on the old IRISA PolyLib and the old library used in the Polka tool inside the synchronous team of the Verimag laboratory.
The main motivation to develop a new library at that time (1998) was the need for multi-precision integers. The interface and memory management have also been improved (according to the author !), and saturation matrices can be kept in memory, thus saving computation time. There is also an option to handle strict constraints like x>y.
Implemented operations include creation of polyhedra from constraints or generators, intersection, convex hull, image and preimage by linear transformations, widening operator and inspection of saturation matrices.
The C interface is simple but also quite rough. The OCaml interface offers however pretty input and output of constraints, matrices and polyhedra, and gives you a polyhedra desk calculator thanks to the OCaml toplevel.
NEWPOLKA is now integrated in the Apron library, which offers access to several abstract domains, and also a higher-level interface. This documentation is kept only for users who do not want to switch to the new interface and/or have reasons to use this one.(15 november 2006)