This is a draft documentation for the VPL library.
The VPL is an implementation of the abstract domain of polyhedra
which provides correctness certificates of its results.
A certificate checker comes with the library
whose correctness has been proved using the Coq proof assistant.
Interaction between the library and the checker occurs through the
{! Glue} module, which performs the necessary representation translation.
Please note that the interfaces described here are subject to change.
VPL stands for Verimag Polyhedra Libray.

Module {! VPL} provides a simple user interface to the library.
It is meant to be customized to suit the user particular use-case.

The following modules describe the main data structures used by the library.
{ul
	{li {! Var}: a representation of program variables}
	{li {! Nb}: rational numbers and operations on them}
	{li {! Vec}: vectors of rational numbers and operations on them}
	{li {! Cstr}: linear constraints and operations on them}
	{li {! Pol}: polyhedra and operations on them}
	{li {! Cert}: certificates and operations on them}
}

The following modules are internal representations of the library.
{ul
	{li {! Rtree}: association table with key type {! Var.t}}
	{li {! IneqSet}: inequality set used in {! Pol.t}}
	{li {! EqSet}: equality set used in {! Pol.t}}
	{li {! Cons}: extended representation of linear constraints}
	{li {! Glue}: representation conversion to the certified checker}
	{li {! Splx}: satisfiability-only simplex algorithm implementation}
}
