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 and written by Christoph Lauter, Sylvain Chevillard, M. Joldes 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 1.1 has been released and can be downloaded here.
• A weekly build (last compiled on 01/31/2010) 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.

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: Sollya is governed by the CeCILL-C license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the software under the terms of the CeCILL-C license as circulated by CEA, CNRS, and INRIA at the following URL http://www.cecill.info/.

Last update: 01/07/2010