Looking for TaPAS ?

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.

The well-known FASTer tool uses the GENEPI solver.