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.

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.
  • 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.

To install packages into the directory /my/install/dir (it must be an absolute path), simply enter the following commands at your prompt:
  • 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
    

tapas-archi.png (68.5 kB) Gérald Point, 03/17/2010 10:19 am

tapas-archi-tn.png (40.4 kB) Gérald Point, 03/17/2010 10:19 am