Sollya

Sollya is a tool environment for safe floating-point code development. It is particularily targeted to the automatized implementation of mathematical floating-point libraries (libm). Amongst other features, it offers a certified infinity (supremum) norm and a fast Remez algorithm.

Sollya is developped by Arénaire, Caramel, PEQUAN and APICS. It is written by Christoph Lauter, Sylvain Chevillard, M. Joldeș and N. Jourdan.

Sollya provides you:

• a certified infinity (supremum) norm for computing safe approximation error bounds,
• an automatized implementer for approximation polynomials in CRlibm-style C-code with the corresponding Gappa proof,
• a fast implementation of Remez algorithm for computing minimax polynomials,
• a full-featured programming language adapted to analysis of numerical programs like in a Computer-Algebra-System,
• a faithful-rounding, multi-precision evaluator of composed functional expressions extending MPFR,
• a highly accurate and fast floating-point infinity (supremum) norm,
• support for floating-point rounding operators and expansions in common precisions,
• a special floating-point minimax procedure,
• basic MathML input and output support,
• interfaces for extending Sollya with your own code and much more...

Download Sollya:

• Sollya 3.0 has been released and can be downloaded here.
• A weekly build (last compiled on 01/22/2012) of the SVN sources is available as a tar.gz, as a tar.bz2 and as a zip file.
• The latest development version is available through anonymous SVN checkout as indicated here.

Documentation:

• Sollya comes with an integrated help environment. Just type help; on the Sollya prompt.
• A complete documentation in one document is available for download here.
• An online documentation is available:
  • A complete introduction to the basic ideas of Sollya, together with a small tutorial is available here.
  • The documentation of all commands available within Sollya can be found here as a single page or here with each command on a different page (faster to load).

Sollya is based on the following softwares and software libraries:

• A C compiler such as gcc,
• a C++ compiler such as g++,
• the GNU MP Bignum Library,
• the MPFR library version 2.2.0 or later,
• the MPFI library,
• the fplll software,
• the XML C parser and toolkit of Gnome (libxml2),
• the Bison GNU parser generator version 2.3 or later,
• Flex version 2.5.33 or later,
• gnuplot.

Remark that Bison and Flex are only needed if Sollya is to be built from a SVN checkout or if the Sollya lexer and parser files are modified.

The gnuplot software is needed neither for building nor for executing Sollya. Sollya is just able to call the gnuplot executable with a data set representing the graph of a function.

Sollya is already used by the following projects:

• the Metalibm project,
• the FloPoCo project
• and perhaps some others...

License

The Sollya tool and the material of this website is Copyright © 2006-2011 by
Laboratoire de l'Informatique du Parallélisme - UMR CNRS - ENS Lyon - UCB Lyon 1 - INRIA 5668, Lyon, France, LORIA (CNRS, INPL, INRIA, UHP, U-Nancy 2) Nancy, France, Laboratoire d'Informatique de Paris 6, Équipe PEQUAN, UPMC Université Paris 06 - CNRS - UMR 7606 - LIP6, Paris, France, and by INRIA Sophia-Antipolis Méditerranée, APICS Team, Sophia-Antipolis, France. All rights reserved.

The Sollya tool is open software. It is distributed and can be used, modified and redistributed under the terms of the CeCILL-C licence available at http://www.cecill.info/ and reproduced in the COPYING file of the distribution. The distribution contains parts of other libraries as a support for but not integral part of Sollya. These libraries are reigned by the GNU Lesser General Public License that is available at http://www.gnu.org/licenses/ and reproduced in the COPYING file of the distribution.

This software, the Sollya tool, is distributed WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

Last update: 08/01/2011