GENEric Presburger programming Interface

The GENEPI library gathers a set of routines that can be used in place of Presburger solver. GENEPI is not an real solver but rather an abstraction layer of a solver. The decision procedures are not implemented into the GENEPI library; the necessary functions are imported from dynamically loaded plugins. Each plugin must furnish a set of functions specified by the plugin API.

GENEPI is useful at both sides of the programming interface:
  • On one side, applications that require the resolution of Presburger formulas can take advantage of the abstraction that allows to use dynamically loaded solvers and thus, to postpone the choice of the actually used solver at run-time.
  • On the other side, solver developers can use any GENEPI-based application to benchmark their solver and compare it to other solvers.

The API documentation is available here.

Plugins

Several implementations of the GENEPI Plugin API have been developed. Each one is a simple encapsulation of an existing solver library.
  • Plugins over natural numbers
    • The automaton data-structure (DFA library) of MONA is used to encode binary automata.
    • The Shared Automata data-structure is used to implement the plugin PresTAF.
  • Plugins over integers
    • The LASH is used to implement a solver over integers; the NDD are used to implement it.
    • One of the plugins not based on binary automata uses the Omega library (formula transformations).
  • Plugins over real numbers
    • The PPL plugin is another plugin not based on the automaton representation.
  • Plugins mixing real and integer variables
    • The LIRA plugin is based on weak deterministic Büchi automata.
    • The LASH is also used to implement a solver over reals and integers; the RVA library is used to implement it.

Downloads

GENEPI package and plugins are freely available from the Download area (or from links directly below).

Packages

Package Name Nightly built packages Last stable package
GENEPI genepi-current.tar.gz genepi-3.1.tar.gz
LASH/RVA genepi-lash-plugin-current.tar.gz lash-plugin-1.2.tar.gz
LIRA genepi-lira-plugin-current.tar.gz lira-plugin-1.2.tar.gz
MONA genepi-mona-plugin-current.tar.gz mona-plugin-1.3.tar.gz
OMEGA genepi-omega-plugin-current.tar.gz omega-plugin-1.2.tar.gz
PPL genepi-ppl-plugin-current.tar.gz ppl-plugin-1.2.tar.gz
PresTAF prestaf-current.tar.gz prestaf-1.6.tar.gz

GIT Repositories

You can also remain up-do-date using our GIT repository:

  1. Using the HTTP protocol, sources are freely available for read only access:
     git clone http://altarica.labri.fr/git/genepi.git
    git clone http://altarica.labri.fr/git/genepi-plugins.git
  2. Using a SSH authorized access, the repository is accessible for read and write synchronizations:
      git clone git@altarica.labri.fr:genepi.git
    git clone git@altarica.labri.fr:genepi-plugins.git