Talence Presburger Arithmetic Suite¶
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.
- GENEPI, a generic API that can be used as a Presburger formula solver.
- a set of plugins for the GENEPI solver.
- 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 FASTer tool uses the GENEPI solver.
Installing TaPAS¶
Each tool/library is distributed in separate packages downloadable from the Download Area or from each page of tools.
However the nightly build components of TaPAS are also distributed in a single archive file tapas-current.tar.gz.
- First extract files from the TaPAS archive:
$ gzip -dc tapas-current.tar.gz | tar xvf - tapas/ tapas/packages.txt ...
- Move to the TaPAS source directory and launch the installation script (note that my_install_dir is an absolute path):
$ cd tapas $ ./tapas-install.sh --prefix=my_install_dir installing package ccl-current. all operations are logged into ccl-current.log. ...
- Add the installation directory to your PATH environment variable if you are interested by using [[tools:tapas:distiller|Distiller]].
$ PATH=$PATH:my_install_dir/bin $ echo "2*nat || 2*nat + 1;" | distiller -s { x0 | x0 in nat }; // Automata size : #SA=1 #EA=1 #S=1 #D=0 #Refs=11 #to0=0/2 // Formula size : 8 nodes