TaPAS is a set of ANSI C libraries related to Presburger Arithmetic and a small solver program. The architecture of the TaPAS development framework is depicted on the figure below.
This suite is composed of:
- GENEPI, a generic API that can be used as a Presburger formula solver.
- a set of plugins for the GENEPI solver. Among them PresTAF is the only one that permit to synthesis Presburger formulas from sets encoded by binary automata.
- a language Armoise to describe sets over integer or real numbers.
- a compiler Alambic that transforms Armoise specifications into Presburger formulas and solve them using GENEPI.
- an Armoise formula synthesizer integrated into the PresTAF plugin.
- a solver program called distiller (distributed with the Alambic packages) that exemplifies how to use all these libraries.