Users' manual for the Sollya tool - weekly-08-20-2017

Sylvain Chevillard (sylvain.chevillard@ens-lyon.org),
Christoph Lauter (christoph.lauter@ens-lyon.org)
and Mioara Joldeș (joldes@laas.fr)

License

The Sollya tool is Copyright © 2006-2016 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 Sorbonne Universités UPMC Univ Paris 06 UMR 7606, LIP6 Boîte Courrier 169 4, place Jussieu F-75252 Paris Cedex 05 France,
CNRS, LIP6, UPMC Sorbonne Universités, UPMC Univ Paris 06 CNRS, LIP6 UMR 7606, 4 place Jussieu 75005 Paris,
and by

INRIA Sophia-Antipolis Méditerranée, APICS Team, Sophia-Antipolis, France.
All rights reserved.

This software 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.

As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only with a limited warranty and the software's author, the holder of the economic rights, and the successive licensors have only limited liability.

In this respect, the user's attention is drawn to the risks associated with loading, using, modifying and/or developing or reproducing the software by the user in light of its specific status of free software, that may mean that it is complicated to manipulate, and that also therefore means that it is reserved for developers and experienced professionals having in-depth computer knowledge. Users are therefore encouraged to load and test the software's suitability as regards their requirements in conditions enabling the security of their systems and/or data to be ensured and, more generally, to use and operate it in the same conditions as regards security.

The fact that you are presently reading this means that you have had knowledge of the CeCILL-C license and that you accept its terms.

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

Direct access to the list of available commands

1 - Compilation and installation of Sollya

Sollya comes in two flavors:

The installation of the tool and the library follow the same steps, desribed below. The present documentation focuses more on the interactive tool. As a matter of fact, the library works exactly the same way as the tool, so it is necessary to know a little about the tool in order to correctly use the library. The reader who is only interested in the library should at least read the following Sections Introduction, General Principles and Data Types. A documentation specifically describing the library usage is available in Appendix the Sollya library at the end of the present documentation.

1.1 - Compilation dependencies

The Sollya distribution can be compiled and installed using the usual ./configure, make, make install procedure. Besides a C and a C++ compiler, Sollya needs the following software libraries and tools to be installed. The ./configure script checks for the installation of the libraries. However Sollya will build without error if some of its external tools are not installed. In this case an error will be displayed at runtime.

The use of the external tool rlwrap is highly recommended but not required to use the Sollya interactive tool. Use the -A option of rlwrap for correctly displayed ANSI X3.64/ ISO/IEC 6429 colored prompts (see below).

1.2 - Sollya command line options

Sollya can read input on standard input or in a file whose name is given as an argument when Sollya is invoked. The tool will always produce its output on standard output, unless specificly instructed by a particular Sollya command that writes to a file. The following lines are valid invocations of Sollya, assuming that bash is used as a shell:

 /% sollya
...
 /% sollya myfile.sollya
...
 /% sollya < myfile.sollya

If a file given as an input does not exist, an error message is displayed.

All configurations of the internal state of the tool are done by commands given on the Sollya prompt or in Sollya scripts. Nevertheless, some command line options are supported; they work at a very basic I/O-level and can therefore not be implemented as commands.

The following options are supported when calling Sollya:

2 - Introduction

Sollya is an interactive tool for handling numerical functions and working with arbitrary precision. It can evaluate functions accurately, compute polynomial approximations of functions, automatically implement polynomials for use in math libraries, plot functions, compute infinity norms, etc. Sollya is also a full-featured script programming language with support for procedures etc.

Let us begin this manual with an example. Sollya does not allow command line edition; since this may quickly become uncomfortable, we highly suggest to use the rlwrap tool with Sollya:

 /% rlwrap -A sollya
   >

Sollya manipulates only functions in one variable. The first time that an unbound variable is used, this name is fixed. It will be used to refer to the free variable. For instance, try

   > f = sin(x)/x;
   > g = cos(y)-1;
   Warning: the identifier "y" is neither assigned to, nor bound to a library function nor external procedure, nor equal to the current free variable.
   Will interpret "y" as "x".
   > g;
   cos(x) - 1

Now, the name 'x' can only be used to refer to the free variable:

   > x = 3;
   Warning: the identifier "x" is already bound to the free variable, to a library function, library constant or to an external procedure.
   The command will have no effect.
   Warning: the last assignment will have no effect.

If you really want to unbind 'x', you can use the rename command and change the name of the free variable:

   > rename(x,y);
   Information: the free variable has been renamed from "x" to "y".
   > g;
   cos(y) - 1
   > x=3;
   > x;
   3

Sollya has a reserved keyword that can always be used to refer to the free variable. This keyword is _x_. This is particularly useful in contexts when the name of the variable is not known: typically when refering to the free variable in a pattern matching or inside a procedure.

   > f == sin(_x_)/_x_;
   true

As you have seen, you can name functions and easily work with them. The basic thing to do with a function is to evaluate it at some point:

   > f(-2);
   Warning: rounding has happened. The value displayed is a faithful rounding to 165 bits of the true result.
   0.45464871341284084769800993295587242135112748572394
   > evaluate(f,-2);
   0.45464871341284084769800993295587242135112748572394

The printed value is generally a faithful rounding of the exact value at the working precision (i.e., one of the two floating-point numbers enclosing the exact value). Internally Sollya represents numbers as floating-point numbers in arbitrary precision with radix 2: the fact that a faithful rounding is performed in binary does not imply much on the exactness of the digits displayed in decimal. The working precision is controlled by the global variable prec:

   > prec;
   165
   > prec=200;
   The precision has been set to 200 bits.
   > prec;
   200
   > f(-2);
   Warning: rounding has happened. The value displayed is a faithful rounding to 200 bits of the true result.
   0.4546487134128408476980099329558724213511274857239451341894865

Sometimes a faithful rounding cannot easily be computed. In such a case, a value is printed that was obtained using floating-point approximations without control on the final accuracy:

   > log2(5)/log2(17) - log(5)/log(17);
   Warning: rounding may have happened.
   If there is rounding, the displayed value is *NOT* guaranteed to be a faithful rounding of the true result.
   0

The philosophy of Sollya is: Whenever something is not exact, print a warning. This explains the warnings in the previous examples. If the result can be shown to be exact, there is no warning:

   > sin(0);
   0

Let us finish this Section with a small complete example that shows a bit of what can be done with Sollya:

   > restart;
   The tool has been restarted.
   > prec=50;
   The precision has been set to 50 bits.
   > f=cos(2*exp(x));
   > d=[-1/8;1/8];
   > p=remez(f,2,d);
   > derivativeZeros = dirtyfindzeros(diff(p-f),d);
   > derivativeZeros = inf(d).:derivativeZeros:.sup(d);
   > maximum=0;
   > for t in derivativeZeros do {
        r = evaluate(abs(p-f), t);
        if r > maximum then { maximum=r; argmaximum=t; };
     };
   > print("The infinity norm of", p-f, "is", maximum, "and is reached at", argmaximum);
   The infinity norm of -3.89710727796949e-2 * x^2 + -1.79806720921853 * x + (-0.4162655728752966) - cos(2 * exp(x)) is 8.6306594443227e-4 and is reached at 6.66355088071379e-2

In this example, we define a function f, an interval d and we compute the best degree-2 polynomial approximation of f on d with respect to the infinity norm. In other words, max {|p(x)-f(x)|, x in d} is minimal amongst polynomials with degree not greater than 2. Then, we compute the list of the zeros of the derivative of p-f and add the bounds of d to this list. Finally, we evaluate |p-f| for each point in the list and store the maximum and the point where it is reached. We conclude by printing the result in a formatted way.

Let us mention as a sidenote that you do not really need to use such a script for computing an infinity norm; as we will see, the command dirtyinfnorm does this for you.

3 - General principles

The first purpose of Sollya is to help people using numerical functions and numerical algorithms in a safe way. It is first designed to be used interactively but it can also be used in scripts (remark: some of the behaviors of Sollya slightly change when it is used in scripts. For example, no prompt is printed).

One of the particularities of Sollya is to work with multi-precision arithmetic (it uses the MPFR library). For safety purposes, Sollya knows how to use interval arithmetic. It uses interval arithmetic to produce tight and safe results with the precision required by the user.

The general philosophy of Sollya is: When you can perform a computation exactly and sufficiently quickly, do it; when you cannot, do not, unless you have been explicitly asked for.

The precision of the tool is set by the global variable prec. In general, the variable prec determines the precision of the outputs of commands: more precisely, the command will internally determine how much precision should be used during the computations in order to ensure that the output is a faithfully rounded result with prec bits.

For decidability and efficiency reasons, this general principle cannot be applied every time, so be careful. Moreover certain commands are known to be unsafe: they give in general excellent results and give almost prec correct bits in output for everyday examples. However they are merely based on heuristics and should not be used when the result must be safe. See the documentation of each command to know precisely how confident you can be with their result.

A second principle (that comes together with the first one) is the following one: When a computation leads to inexact results, inform the user with a warning. This can be quite irritating in some circumstances: in particular if you are using Sollya within other scripts. The global variable verbosity lets you change the level of verbosity of Sollya. When the variable is set to 0, Sollya becomes completely silent on standard output and prints only very important messages on standard error. Increase verbosity if you want more information about what Sollya is doing. Please keep in mind that when you affect a value to a global variable, a message is always printed even if verbosity is set to 0. In order to silently affect a global variable, use !:

   > prec=30;
   The precision has been set to 30 bits.
   > prec=30!;
   >

For conviviality reasons, values are displayed in decimal by default. This lets a normal human being understand the numbers they manipulate. But since constants are internally represented in binary, this causes permanent conversions that are sources of roundings. Thus you are loosing in accuracy and Sollya is always complaining about inexact results. If you just want to store or communicate your results (to another tools for instance) you can use bit-exact representations available in Sollya. The global variable display defines the way constants are displayed. Here is an example of the five available modes:

   > prec=30!;
   > a = 17.25;
   > display=decimal;
   Display mode is decimal numbers.
   > a;
   17.25
   > display=binary;
   Display mode is binary numbers.
   > a;
   1.000101_2 * 2^(4)
   > display=powers;
   Display mode is dyadic numbers in integer-power-of-2 notation.
   > a;
   69 * 2^(-2)
   > display=dyadic;
   Display mode is dyadic numbers.
   > a;
   69b-2
   > display=hexadecimal;
   Display mode is hexadecimal numbers.
   > a;
   0x1.14p4

Please keep in mind that it is possible to maintain the general verbosity level at some higher setting while deactivating all warnings on roundings. This feature is controlled using the roundingwarnings global variable. It may be set to on or off. By default, the warnings are activated (roundingwarnings = on) when Sollya is connected on standard input to a pseudo-file that represents a terminal. They are deactivated when Sollya is connected on standard input to a real file. See roundingwarnings for further details; the behavior is illustrated with examples there.

As always, the symbol e means (* 10^x). The same way the symbol b means (* 2^x). The symbol p means (* 16^x) and is used only with the 0x prefix. The prefix 0x indicates that the digits of the following number until a symbol p or white-space are hexadecimal. The suffix _2 indicates to Sollya that the previous number has been written in binary. Sollya can parse these notations even if you are not in the corresponding display mode, so you can always use them.

You can also use memory-dump hexadecimal notation frequently used to represent IEEE 754 double and single precision numbers. Since this notation does not allow for exactly representing numbers with arbitrary precision, there is no corresponding display mode. However, the commands printdouble respectively printsingle round the value to the nearest double respectively single. The number is then printed in hexadecimal as the integer number corresponding to the memory representation of the IEEE 754 double or single number:

   > printdouble(a);
   0x4031400000000000
   > printsingle(a);
   0x418a0000

Sollya can parse these memory-dump hexadecimal notation back in any display mode. The difference of this memory-dump notation with the hexadecimal notation (as defined above) is made by the presence or absence of a p indicator.

4 - Variables

As already explained, Sollya can manipulate variate functional expressions in one variable. These expressions contain a unique free variable the name of which is fixed by its first usage in an expression that is not a left-hand-side of an assignment. This global and unique free variable is a variable in the mathematical sense of the term.

Sollya also provides variables in the sense programming languages give to the term. These variables, which must be different in their name from the global free variable, may be global or declared and attached to a block of statements, i.e., a begin-end-block. These programming language variables may hold any object of the Sollya language, as for example functional expressions, strings, intervals, constant values, procedures, external functions and procedures, etc.

Global variables need not to be declared. They start existing, i.e., can be correctly used in expressions that are not left-hand-sides of assignments, when they are assigned a value in an assignment. Since they are global, this kind of variables is recommended only for small Sollya scripts. Larger scripts with code reuse should use declared variables in order to avoid name clashes for example in loop variables.

Declared variables are attached to a begin-end-block. The block structure builds scopes for declared variables. Declared variables in inner scopes shadow (global and declared) variables of outer scopes. The global free variable, i.e., the mathematical variable for variate functional expressions in one variable, cannot be shadowed. Variables are declared using the var keyword. See Section var for details on its usage and semantic.

The following code examples illustrate the use of variables.

   > f = exp(x);
   > f;
   exp(x)
   > a = "Hello world";
   > a;
   Hello world
   > b = 5;
   > f(b);
   Warning: rounding has happened. The value displayed is a faithful rounding to 165 bits of the true result.
   148.41315910257660342111558004055227962348766759388
   > {var b; b = 4; f(b); };
   Warning: rounding has happened. The value displayed is a faithful rounding to 165 bits of the true result.
   54.598150033144239078110261202860878402790737038614
   > {var x; x = 3; };
   Warning: the identifier "x" is already bound to the current free variable.
   It cannot be declared as a local variable. The declaration of "x" will have no effect.
   Warning: the identifier "x" is already bound to the free variable, to a library function, library constant or to an external procedure.
   The command will have no effect.
   Warning: the last assignment will have no effect.
   > {var a, b; a=5; b=3; {var a; var b; b = true; a = 1; a; b;}; a; b; };
   1
   true
   5
   3
   > a;
   Hello world

Let us state that a variable identifier, just as every identifier in Sollya, contains at least one character, starts with a ASCII letter and continues with ASCII letters or numerical digits.

Two predefined variables exist when Sollya is started:

Even though these variables exist upon Sollya startup with predefined values, they behave like any other variable: the predefined value can be overwritten by assigning any new value to the variables, the variables can be shadowed by declared, local variables of the same name and so on.

5 - Data types

Sollya has a (very) basic system of types. If you try to perform an illicit operation (such as adding a number and a string, for instance), you will get a typing error. Let us see the available data types.

5.1 - Booleans

There are two special values true and false. Boolean expressions can be constructed using the boolean connectors && (and), || (or), ! (not), and cosmparisons.

The comparison operators <, <=, > and >= can only be used between two numbers or constant expressions.

The comparison operators == and != are polymorphic. You can use them to compare any two objects, like two strings, two intervals, etc. As a matter of fact, polymorphism is allowed on both sides: it is possible to compare objects of different type. Such objects of different type, as they can never be syntactically equal, will always compare unequal (see exception for error, Section error) and never equal. It is important to remember that testing the equality between two functions will return true if and only if the expression trees representing the two functions are exactly the same or automatic simplification is activated and both functions are polynomials that are equal. See error for an exception concerning the special object error. Example:

   > 1+x==1+x;
   true

5.2 - Numbers

Sollya represents numbers as binary multi-precision floating-point values. For integer values and values in dyadic, binary, hexadecimal or memory dump notation, it automatically uses a precision needed for representing the value exactly (unless this behaviour is overridden using the syntax given below). Additionally, automatic precision adaption takes place for all integer values (even in decimal notation) written without the exponent sign e or with the exponent sign e and an exponent sufficiently small that they are less than 10^999. Otherwise the values are represented with the current precision prec. When a number must be rounded, it is rounded to the precision prec before the expression get evaluated:

   > prec=12!;
   > 4097.1;
   Warning: Rounding occurred when converting the constant "4097.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   4098
   > 4098.1;
   Warning: Rounding occurred when converting the constant "4098.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   4098
   > 4097.1+1;
   Warning: Rounding occurred when converting the constant "4097.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   4099

As a matter of fact, each variable has its own precision that corresponds to its intrinsic precision or, if it cannot be represented, to the value of prec when the variable was set. Thus you can work with variables having a precision higher than the current precision.

The same way, if you define a function that refers to some constant, this constant is stored in the function with the current precision and will keep this value in the future, even if prec becomes smaller.

If you define a function that refers to some variable, the precision of the variable is kept, independently of the current precision:

   > prec = 50!;
   > a = 4097.1;
   Warning: Rounding occurred when converting the constant "4097.1" to floating-point with 50 bits.
   If safe computation is needed, try to increase the precision.
   > prec = 12!;
   > f = x + a;
   > g = x + 4097.1;
   Warning: Rounding occurred when converting the constant "4097.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   > prec = 120;
   The precision has been set to 120 bits.
   > f;
   4097.099999999998544808477163314819336 + x
   > g;
   4098 + x

In some rare cases, it is necessary to read in decimal constants with a particular precision being used in the conversion to the binary floating-point format, which Sollya uses. Setting prec to that precision may prove to be an insufficient means for doing so, for example when several different precisions have to be used in one expression. For these rare cases, Sollya provides the following syntax: decimal constants may be written %precision%constant, where precision is a constant integer, written in decimal, and constant is the decimal constant. Sollya will convert the constant constant with precision precision, regardless of the global variable prec and regardless if constant is an integer or would otherwise be representable.

   > prec = 24;
   The precision has been set to 24 bits.
   > a = 0.1;
   Warning: Rounding occurred when converting the constant "0.1" to floating-point with 24 bits.
   If safe computation is needed, try to increase the precision.
   > b = 33554433;
   > prec = 64;
   The precision has been set to 64 bits.
   > display = binary;
   Display mode is binary numbers.
   > a;
   1.10011001100110011001101_2 * 2^(-4)
   > 0.1;
   Warning: Rounding occurred when converting the constant "0.1" to floating-point with 64 bits.
   If safe computation is needed, try to increase the precision.
   1.100110011001100110011001100110011001100110011001100110011001101_2 * 2^(-4)
   > %24%0.1;
   Warning: Rounding occurred when converting the constant "0.1" to floating-point with 24 bits.
   If safe computation is needed, try to increase the precision.
   1.10011001100110011001101_2 * 2^(-4)
   > c = 33554433;
   > b;
   1.0000000000000000000000001_2 * 2^(25)
   > c;
   1.0000000000000000000000001_2 * 2^(25)
   > %24%33554433;
   Warning: Rounding occurred when converting the constant "33554433" to floating-point with 24 bits.
   If safe computation is needed, try to increase the precision.
   1_2 * 2^(25)
   >
   >

Sollya is an environment that uses floating-point arithmetic. The IEEE 754-2008 standard on floating-point arithmetic does not only define floating-point numbers that represent real numbers but also floating-point data representing infinities and Not-a-Numbers (NaNs). Sollya also supports infinities and NaNs in the spirit of the IEEE 754-2008 standard without taking the standard's choices literally.

The evaluation of an expression involving a NaN or the evaluation of a function at a point being NaN always results in a NaN.

Infinities are considered to be the limits of expressions tending to infinity. They are supported as bounds of intervals in some cases. However, particular commands might prohibit their use even though there might be a mathematical meaning attached to such expressions. For example, while Sollya will evaluate expressions such as the limit of e^x when x goes to -infinity, expressed e.g., through evaluate(exp(x),[-infty;0]), it will not accept to compute the (finite) value of the integral of e^x between -infinity and 0.

The following examples give an idea of what can be done with Sollya infinities and NaNs. Here is what can be done with infinities:

   > f = exp(x) + 5;
   > f(-infty);
   5
   > evaluate(f,[-infty;infty]);
   [5;infty]
   > f(infty);
   infty
   > [-infty;5] * [3;4];
   [-infty;20]
   > -infty < 5;
   true
   > log(0);
   -infty
   > [log(0);17];
   Warning: inclusion property is satisfied but the diameter may be greater than the least possible.
   Warning: at least one of the given expressions is not a constant but requires evaluation.
   Evaluation is guaranteed to ensure the inclusion property. The approximate result is at least 165 bit accurate.
   [-infty;17]
   >

And the following example illustrates NaN behavior.

   > 3/0;
   Warning: the given expression is undefined or numerically unstable.
   NaN
   > (-3)/0;
   Warning: the given expression is undefined or numerically unstable.
   NaN
   > infty/infty;
   Warning: the given expression is undefined or numerically unstable.
   NaN
   > infty + infty;
   infty
   > infty - infty;
   Warning: the given expression is undefined or numerically unstable.
   NaN
   > f = exp(x) + 5;
   > f(NaN);
   NaN
   > NaN == 5;
   false
   > NaN == NaN;
   false
   > NaN != NaN;
   false
   > X = "Vive la Republique!";
   > !(X == X);
   false
   > X = 5;
   > !(X == X);
   false
   > X = NaN;
   > !(X == X);
   true
   >

5.3 - Rational numbers and rational arithmetic

The Sollya tool is mainly based on floating-point arithmetic: wherever possible, floating-point algorithms, including algorithms using interval arithmetic, are used to produce approximate but safe results. For some particular cases, floating-point arithmetic is not sufficient: some algorithms just require natural and rational numbers to be handled exactly. More importantly, for these applications, it is required that rational numbers be displayed as such.

Sollya implements a particular mode that offers a lightweight support for rational arithmetic. When needed, it can be enabled by assigning on to the global variable rationalmode. It is disabled by assigning off; the default is off.

When the mode for rational arithmetic is enabled, Sollya's behavior will change as follows:

Even when rationalmode is on, Sollya will not be able to exhibit integer ratios between transcendental quantities. For example, Sollya will not display 1/6 for arcsin(1/2)/pi but 0.16666... Sollya's evaluator for rational arithmetic is only able to simplify rational expressions based on addition, subtraction, multiplication, division, negation, perfect squares (for square root) and integer powers.

The following example illustrates what can and what cannot be done with Sollya's mode for rational arithmetic:

   > 1/3 - 1/7;
   Warning: rounding has happened. The value displayed is a faithful rounding to 165 bits of the true result.
   0.19047619047619047619047619047619047619047619047619
   > rationalmode = on;
   Rational mode has been activated.
   > 1/3 - 1/7;
   4 / 21
   > (2 + 1/7)^2 + (6/7)^2 + 2 * (2 + 1/7) * 6/7;
   9
   > rationalmode = off;
   Rational mode has been deactivated.
   > (2 + 1/7)^2 + (6/7)^2 + 2 * (2 + 1/7) * 6/7;
   Warning: rounding has happened. The value displayed is a faithful rounding to 165 bits of the true result.
   9
   > rationalmode = on;
   Rational mode has been activated.
   > asin(1)/pi;
   Warning: rounding has happened. The value displayed is a faithful rounding to 165 bits of the true result.
   0.5
   > sin(1/6 * pi);
   Warning: rounding has happened. The value displayed is a faithful rounding to 165 bits of the true result.
   0.5
   > exp(1/7 - 3/21) / 7;
   1 / 7
   > rationalmode = off;
   Rational mode has been deactivated.
   > exp(1/7 - 3/21) / 7;
   Warning: rounding has happened. The value displayed is a faithful rounding to 165 bits of the true result.
   0.142857142857142857142857142857142857142857142857145
   > print(1/7 - 3/21);
   1 / 7 - 3 / 21
   > rationalmode = on;
   Rational mode has been activated.
   > print(1/7 - 3/21);
   0

5.4 - Intervals and interval arithmetic

Sollya can manipulate intervals that are closed subsets of the real numbers. Several ways of defining intervals exist in Sollya. There is the most common way where intervals are composed of two numbers or constant expressions representing the lower and the upper bound. These values are separated either by commas or semi-colons. Interval bound evaluation is performed in a way that ensures the inclusion property: all points in the original, unevaluated interval will be contained in the interval with its bounds evaluated to floating-point numbers.

   > d=[1;2];
   > d2=[1,1+1];
   > d==d2;
   true
   > prec=12!;
   > 8095.1;
   Warning: Rounding occurred when converting the constant "8095.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   8096
   > [8095.1; 8096.1];
   Warning: Rounding occurred when converting the constant "8095.1" to floating-point with 12 bits.
   The inclusion property is nevertheless satisfied.
   Warning: Rounding occurred when converting the constant "8096.1" to floating-point with 12 bits.
   The inclusion property is nevertheless satisfied.
   [8094;8098]

Sollya has a mode for printing intervals that are that thin that their bounds have a number of decimal digits in common when printed. That mode is called midpointmode; see below for an introduction and Section midpointmode for details. As Sollya must be able to parse back its own output, a syntax is provided to input intervals in midpoint mode. However, please pay attention to the fact that the notation used in midpoint mode generally increases the width of intervals: hence when an interval is displayed in midpoint mode and read again, the resulting interval may be wider than the original interval.

   > midpointmode = on!;
   > [1.725e4;1.75e4];
   0.17~2/5~e5
   > 0.17~2/5~e5;
   0.17~2/5~e5
   > midpointmode = off!;
   > 0.17~2/5~e5;
   [17200;17500]

In some cases, intervals become infinitely thin in theory, in which case one tends to think of point intervals even if their floating-point representation is not infinitely thin. Sollya provides a very covenient way for input of such point intervals. Instead of writing [a;a], it is possible to just write [a]. Sollya will expand the notation while making sure that the inclusion property is satisfied:

   > [3];
   [3;3]
   > [1/7];
   Warning: at least one of the given expressions is not a constant but requires evaluation.
   Evaluation is guaranteed to ensure the inclusion property. The approximate result is at least 24 bit accurate.
   [0.14285713;0.14285715]
   > [exp(8)];
   Warning: at least one of the given expressions is not a constant but requires evaluation.
   Evaluation is guaranteed to ensure the inclusion property. The approximate result is at least 24 bit accurate.
   [2980.9578;2980.958]

When the mode midpointmode is set to on (see midpointmode), Sollya will display intervals that are provably reduced to one point in this extended interval syntax. It will use midpointmode syntax for intervals that are sufficiently thin but not reduced to one point (see Section midpointmode for details):

   > midpointmode = off;
   Midpoint mode has been deactivated.
   > [17;17];
   [17;17]
   > [exp(pi);exp(pi)];
   Warning: at least one of the given expressions is not a constant but requires evaluation.
   Evaluation is guaranteed to ensure the inclusion property. The approximate result is at least 165 bit accurate.
   [23.1406926327792690057290863679485473802661062426;23.140692632779269005729086367948547380266106242601]
   > midpointmode = on;
   Midpoint mode has been activated.
   > [17;17];
   [17]
   > [exp(pi);exp(pi)];
   Warning: at least one of the given expressions is not a constant but requires evaluation.
   Evaluation is guaranteed to ensure the inclusion property. The approximate result is at least 165 bit accurate.
   0.231406926327792690057290863679485473802661062426~0/1~e2
   >

Sollya intervals are internally represented with floating-point numbers as bounds; rational numbers are not supported here. If bounds are defined by constant expressions, these are evaluated to floating-point numbers using the current precision. Numbers or variables containing numbers keep their precision for the interval bounds.

Constant expressions get evaluated to floating-point values immediately; this includes pi and rational numbers, even when rationalmode is on (see Section Rational numbers and rational arithmetic for this mode).

   > prec = 300!;
   > a = 4097.1;
   Warning: Rounding occurred when converting the constant "4097.1" to floating-point with 300 bits.
   If safe computation is needed, try to increase the precision.
   > prec = 12!;
   > d = [4097.1; a];
   Warning: Rounding occurred when converting the constant "4097.1" to floating-point with 12 bits.
   The inclusion property is nevertheless satisfied.
   > prec = 300!;
   > d;
   [4096;4097.1]
   > prec = 30!;
   > [-pi;pi];
   Warning: at least one of the given expressions is not a constant but requires evaluation.
   Evaluation is guaranteed to ensure the inclusion property. The approximate result is at least 30 bit accurate.
   [-3.141592655;3.141592655]

You can get the upper-bound (respectively the lower-bound) of an interval with the command sup (respectively inf). The middle of the interval can be computed with the command mid. Let us also mention that these commands can also be used on numbers (in that case, the number is interpreted as an interval containing only one single point. In that case the commands inf, mid and sup are just the identity):

   > d=[1;3];
   > inf(d);
   1
   > mid(d);
   2
   > sup(4);
   4

Let us mention that the mid operator never provokes a rounding. It is rewritten as an unevaluated expression in terms of inf and sup.

Sollya permits intervals to also have non-real bounds, such as infinities or NaNs. When evaluating certain expressions, in particular given as interval bounds, Sollya will itself generate intervals containing infinities or NaNs. When evaluation yields an interval with a NaN bound, the given expression is most likely undefined or numerically unstable. Such results should not be trusted; a warning is displayed.

While computations on intervals with bounds being NaN will always fail, Sollya will try to interpret infinities in the common way as limits. However, this is not guaranteed to work, even if it is guaranteed that no unsafe results will be produced. See also section Numbers for more detail on infinities in Sollya. The behavior of interval arithmetic on intervals containing infinities or NaNs is subject to debate; moreover, there is no complete consensus on what should be the result of the evaluation of a function f over an interval I containing points where f is not defined. Sollya has its own philosophy regarding these questions. This philosophy is explained in Appendix interval arithmetic philosophy in Sollya at the end of this document.

   > evaluate(exp(x),[-infty;0]);
   [0;1]
   > dirtyinfnorm(exp(x),[-infty;0]);
   Warning: a bound of the interval is infinite or NaN.
   This command cannot handle such intervals.
   NaN
   >
   > f = log(x);
   > [f(0); f(1)];
   Warning: inclusion property is satisfied but the diameter may be greater than the least possible.
   Warning: at least one of the given expressions is not a constant but requires evaluation.
   Evaluation is guaranteed to ensure the inclusion property. The approximate result is at least 165 bit accurate.
   [-infty;0]
   >

Sollya internally uses interval arithmetic extensively to provide safe answers. In order to provide for algorithms written in the Sollya language being able to use interval arithmetic, Sollya offers native support of interval arithmetic. Intervals can be added, subtracted, multiplied, divided, raised to powers, for short, given in argument to any Sollya function. The tool will apply the rules of interval arithmetic in order to compute output intervals that safely encompass the hull of the image of the function on the given interval:

   > [1;2] + [3;4];
   [4;6]
   > [1;2] * [3;4];
   [3;8]
   > sqrt([9;25]);
   [3;5]
   > exp(sin([10;100]));
   [0.36787942;2.718282]

When such expressions involving intervals are given, Sollya will follow the rules of interval arithmetic in precision prec for immediately evaluating them to interval enclosures. While Sollya's evaluator always guarantees the inclusion property, it also applies some optimisations in some cases in order to make the image interval as thin as possible. For example, Sollya will use a Taylor expansion based evaluation if a composed function, call it f, is applied to an interval. In other words, in this case Sollya will behave as if the evaluate command (see Section evaluate) were implicitly used. In most cases, the result will be different from the one obtained by replacing all occurences of the free variable of a function by the interval the function is to be evaluated on:

   > f = x - sin(x);
   > [-1b-10;1b-10] - sin([-1b-10;1b-10]);
   [-1.95312484477957829894e-3;1.95312484477957829894e-3]
   > f([-1b-10;1b-10]);
   [-1.552204217011176269e-10;1.552204217011176269e-10]
   > evaluate(f,[-1b-10;1b-10]);
   [-1.552204217011176269e-10;1.552204217011176269e-10]

5.5 - Functions

Sollya knows only about functions with one single variable. The first time in a session that an unbound name is used (without being assigned) it determines the name used to refer to the free variable.

The basic functions available in Sollya are the following:

The constant pi is available through the keyword pi as a 0-ary function:

   > display=binary!;
   > prec=12!;
   > a=pi;
   > a;
   Warning: rounding has happened. The value displayed is a faithful rounding to 12 bits of the true result.
   1.10010010001_2 * 2^(1)
   > prec=30!;
   > a;
   Warning: rounding has happened. The value displayed is a faithful rounding to 30 bits of the true result.
   1.10010010000111111011010101001_2 * 2^(1)

The reader may wish to see Sections library and function for ways of dynamically adding other base functions to Sollya.

5.6 - Strings

Anything written between quotes is interpreted as a string. The infix operator @ concatenates two strings. To get the length of a string, use the length function. You can access the i-th character of a string using brackets (see the example below). There is no character type in Sollya: the i-th character of a string is returned as a string itself.

   > s1 = "Hello "; s2 = "World!";
   > s = s1@s2;
   > length(s);
   12
   > s[0];
   H
   > s[11];
   !

Strings may contain the following escape sequences: \\, \“, \?, \', \n, \t, \a, \b, \f, \r, \v, \x[hexadecimal number] and \[octal number]. Refer to the C99 standard for their meaning.

5.7 - Particular values

Sollya knows about some particular values. These values do not really have a type. They can be stored in variables and in lists. A (possibly not exhaustive) list of such values is the following one:

5.8 - Lists

Objects can be grouped into lists. A list can contain elements with different types. As for strings, you can concatenate two lists with @. The function length also gives the length of a list.

You can prepend an element to a list using .: and you can append an element to a list using :.
The following example illustrates some features:

   > L = [| "foo" |];
   > L = L:.1;
   > L = "bar".:L;
   > L;
   [|"bar", "foo", 1|]
   > L[1];
   foo
   > L@L;
   [|"bar", "foo", 1, "bar", "foo", 1|]

Lists can be considered arrays and elements of lists can be referenced using brackets. Possible indices start at 0. The following example illustrates this point:

   > L = [|1,2,3,4,5|];
   > L;
   [|1, 2, 3, 4, 5|]
   > L[3];
   4

Lists may contain ellipses indicated by ,..., between elements that are constant and evaluate to integers that are incrementally ordered. Sollya translates such ellipses to the full list upon evaluation. The use of ellipses between elements that are not constants is not allowed. This feature is provided for ease of programming; remark that the complexity for expanding such lists is high. For illustration, see the following example:

   > [|1,...,5|];
   [|1, 2, 3, 4, 5|]
   > [|-5,...,5|];
   [|-5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5|]
   > [|3,...,1|];
   Warning: at least one of the given expressions or a subexpression is not correctly typed
   or its evaluation has failed because of some error on a side-effect.
   error
   > [|true,...,false|];
   Warning: at least one of the given expressions or a subexpression is not correctly typed
   or its evaluation has failed because of some error on a side-effect.
   error

Lists may be continued to infinity by means of the ... indicator after the last element given. At least one element must explicitly be given. If the last element given is a constant expression that evaluates to an integer, the list is considered as continued to infinity by all integers greater than that last element. If the last element is another object, the list is considered as continued to infinity by re-duplicating this last element. Let us remark that bracket notation is supported for such end-elliptic lists even for implicitly given elements. However, evaluation complexity is high. Combinations of ellipses inside a list and in its end are possible. The usage of lists described here is best illustrated by the following examples:

   > L = [|1,2,true,3...|];
   > L;
   [|1, 2, true, 3...|]
   > L[2];
   true
   > L[3];
   3
   > L[4];
   4
   > L[1200];
   1200
   > L = [|1,...,5,true...|];
   > L;
   [|1, 2, 3, 4, 5, true...|]
   > L[1200];
   true

5.9 - Structures

In a similar way as in lists, Sollya allows data to be grouped in – untyped – structures. A structure forms an object to which other objects can be added as elements and identified by their names. The elements of a structure can be retrieved under their name and used as usual. The following sequence shows that point:

   > s.a = 17;
   > s.b = exp(x);
   > s.a;
   17
   > s.b;
   exp(x)
   > s.b(1);
   Warning: rounding has happened. The value displayed is a faithful rounding to 165 bits of the true result.
   2.7182818284590452353602874713526624977572470937
   > s.d.a = [-1;1];
   > s.d.b = sin(x);
   > inf(s.d.a);
   -1
   > diff(s.d.b);
   cos(x)

Structures can also be defined literally using the syntax illustrated in the next example. They will also be printed in that syntax.

   > a = { .f = exp(x), .dom = [-1;1] };
   > a;
   { .f = exp(x), .dom = [-1;1] }
   > a.f;
   exp(x)
   > a.dom;
   [-1;1]
   > b.f = sin(x);
   > b.dom = [-1b-5;1b-5];
   > b;
   { .dom = [-3.125e-2;3.125e-2], .f = sin(x) }
   > { .f = asin(x), .dom = [-1;1] }.f(1);
   Warning: rounding has happened. The value displayed is a faithful rounding to 165 bits of the true result.
   1.57079632679489661923132169163975144209858469968754

If the variable a is bound to an existing structure, it is possible to use the “dot notation” a.b to assign the value of the field b of the structure a. This works even if b is not yet a field of a: in this case a new field is created inside the structure a.

Besides, the dot notation can be used even when a is unassigned. In this case a new structure is created with a field b, and this structure is bound to a. However, the dot notation cannot be used if a is already bound to something that is not a structure.

These principles apply recursively: for instance, if a is a structure that contains only one field d, the command a.b.c = 3 creates a new field named b inside the structure a; this field itself is a structure containing the field c. The command a.d.c = 3 is allowed if a.d is already a structure, but forbidden otherwise (e.g., if a.d was equal to sin(x)). This is summed up in the following example.

   > restart;
   The tool has been restarted.
   > a.f = exp(x);
   > a.dom = [-1;1];
   > a.info.text = "My akrnoximation problem";
   > a;
   { .info = { .text = "My akrnoximation problem" }, .dom = [-1;1], .f = exp(x) }
   >
   > a.info.text = "My approximation problem";
   > a;
   { .info = { .text = "My approximation problem" }, .dom = [-1;1], .f = exp(x) }
   >
   > b = exp(x);
   > b.a = 5;
   Warning: cannot modify an element of something that is not a structure.
   Warning: the last assignment will have no effect.
   > b;
   exp(x)
   >
   > a.dom.a = -1;
   Warning: cannot modify an element of something that is not a structure.
   Warning: the last assignment will have no effect.
   > a;
   { .info = { .text = "My approximation problem" }, .dom = [-1;1], .f = exp(x) }

When printed, the elements of a structure are not sorted in any manner. They get printed in an arbitrary order that just maintains the order given in the definition of literate structures. That said, when compared, two structures compare equal iff they contain the same number of identifiers, with the same names and iff the elements of corresponding names all compare equal. This means the order does not matter in comparisons and otherwise does only for printing.

The following example illustrates this matter:

   > a = { .f = exp(x), .a = -1, .b = 1 };
   > a;
   { .f = exp(x), .a = -1, .b = 1 }
   > a.info = "My function";
   > a;
   { .info = "My function", .f = exp(x), .a = -1, .b = 1 }
   >
   > b = { .a = -1, .f = exp(x), .info = "My function", .b = 1 };
   > b;
   { .a = -1, .f = exp(x), .info = "My function", .b = 1 }
   >
   > a == b;
   true
   >
   > b.info = "My other function";
   > a == b;
   false
   >
   > b.info = "My function";
   > a == b;
   true
   > b.something = true;
   > a == b;
   false

6 - Iterative language elements: assignments, conditional statements and loops

6.1 - Blocks

Statements in Sollya can be grouped in blocks, so-called begin-end-blocks. This can be done using the key tokens { and }. Blocks declared this way are considered to be one single statement. As already explained in Section Variables, using begin-end-blocks also opens the possibility of declaring variables through the keyword var.

6.2 - Assignments

Sollya has two different assignment operators, = and :=. The assignment operator = assigns its right-hand-object “as is”, i.e., without evaluating functional expressions. For instance, i = i + 1; will dereferentiate the identifier i with some content, notate it y, build up the expression (function) y + 1 and assign this expression back to i. In the example, if i stood for the value 1000, the statement i = i + 1; would assign “1000 + 1” – and not “1001” – to i. The assignment operator := evaluates constant functional expressions before assigning them. On other expressions it behaves like =. Still in the example, the statement i := i + 1; really assigns 1001 to i.

Both Sollya assignment operators support indexing of lists or strings elements using brackets on the left-hand-side of the assignment operator. The indexed element of the list or string gets replaced by the right-hand-side of the assignment operator. When indexing strings this way, that right-hand side must evaluate to a string of length 1. End-elliptic lists are supported with their usual semantic for this kind of assignment. When referencing and assigning a value in the implicit part of the end-elliptic list, the list gets expanded to the corresponding length.

The following examples well illustrate the behavior of assignment statements:

   > autosimplify = off;
   Automatic pure tree simplification has been deactivated.
   > i = 1000;
   > i = i + 1;
   > print(i);
   1000 + 1
   > i := i + 1;
   > print(i);
   1002
   > L = [|1,...,5|];
   > print(L);
   [|1, 2, 3, 4, 5|]
   > L[3] = L[3] + 1;
   > L[4] := L[4] + 1;
   > print(L);
   [|1, 2, 3, 4 + 1, 6|]
   > L[5] = true;
   > L;
   [|1, 2, 3, 5, 6, true|]
   > s = "Hello world";
   > s;
   Hello world
   > s[1] = "a";
   > s;
   Hallo world
   > s[2] = "foo";
   Warning: the string to be assigned is not of length 1.
   This command will have no effect.
   > L = [|true,1,...,5,9...|];
   > L;
   [|true, 1, 2, 3, 4, 5, 9...|]
   > L[13] = "Hello";
   > L;
   [|true, 1, 2, 3, 4, 5, 9, 10, 11, 12, 13, 14, 15, "Hello", 17...|]

The indexing of lists on left-hand sides of assignments is reduced to the first order. Multiple indexing of lists of lists on assignment is not supported for complexity reasons. Multiple indexing is possible in right-hand sides.

   > L = [| 1, 2, [|"a", "b", [|true, false|] |] |];
   > L[2][2][1];
   false
   > L[2][2][1] = true;
   Warning: the first element of the left-hand side is not an identifier.
   This command will have no effect.
   > L[2][2] = "c";
   Warning: the first element of the left-hand side is not an identifier.
   This command will have no effect.
   > L[2] = 3;
   > L;
   [|1, 2, 3|]

6.3 - Conditional statements

Sollya supports conditional statements expressed with the keywords if, then and optionally else. Let us mention that only conditional statements are supported and not conditional expressions.

The following examples illustrate both syntax and semantic of conditional statements in Sollya. Concerning syntax, be aware that there must not be any semicolon before the else keyword.

   > a = 3;
   > b = 4;
   > if (a == b) then print("Hello world");
   > b = 3;
   > if (a == b) then print("Hello world");
   Hello world
   > if (a == b) then print("You are telling the truth") else print("Liar!");
   You are telling the truth

6.4 - Loops

Sollya supports three kinds of loops. General while-condition loops can be expressed using the keywords while and do. One has to be aware of the fact that the condition test is executed always before the loop, there is no do-until-condition loop. Consider the following examples for both syntax and semantic:

   > verbosity = 0!;
   > prec = 30!;
   > i = 5;
   > while (expm1(i) > 0) do { expm1(i); i := i - 1; };
   147.4131591
   53.59815
   19.08553693
   6.3890561
   1.718281828
   > print(i);
   0

The second kind of loops are loops on a variable ranging from a numerical start value and a end value. These kind of loops can be expressed using the keywords for, from, to, do and optionally by. The by statement indicates the width of the steps on the variable from the start value to the end value. Once again, syntax and semantic are best explained with an example:

   > for i from 1 to 5 do print ("Hello world",i);
   Hello world 1
   Hello world 2
   Hello world 3
   Hello world 4
   Hello world 5
   > for i from 2 to 1 by -0.5 do print("Hello world",i);
   Hello world 2
   Hello world 1.5
   Hello world 1

The third kind of loops are loops on a variable ranging on values contained in a list. In order to ensure the termination of the loop, that list must not be end-elliptic. The loop is expressed using the keywords for, in and do as in the following examples:

   > L = [|true, false, 1,...,4, "Hello", exp(x)|];
   > for i in L do i;
   true
   false
   1
   2
   3
   4
   Hello
   exp(x)

For both types of for loops, assigning the loop variable is allowed and possible. When the loop terminates, the loop variable will contain the value that made the loop condition fail. Consider the following examples:

   > for i from 1 to 5 do { if (i == 3) then i = 4 else i; };
   1
   2
   5
   > i;
   6

7 - Functional language elements: procedures and pattern matching

7.1 - Procedures

Sollya has some elements of functional languages. In order to avoid confusion with mathematical functions, the associated programming objects are called procedures in Sollya.

Sollya procedures are common objects that can be, for example, assigned to variables or stored in lists. Procedures are declared by the proc keyword; see Section proc for details. The returned procedure object must then be assigned to a variable. It can hence be applied to arguments with common application syntax. The procedure keyword provides an abbreviation for declaring and assigning a procedure; see Section procedure for details.

Sollya procedures can return objects using the return keyword at the end of the begin-end-block of the procedure. Section return gives details on the usage of return. Procedures further can take any type of object in argument, in particular also other procedures that are then applied to arguments. Procedures can be declared inside other procedures.

Common Sollya procedures are declared with a certain number of formal parameters. When the procedure is applied to actual parameters, a check is performed if the right number of actual parameters is given. Then the actual parameters are applied to the formal parameters. In some cases, it is required that the number of parameters of a procedure be variable. Sollya provides support for the case with procedures with an arbitrary number of actual arguments. When the procedure is called, those actual arguments are gathered in a list which is applied to the only formal list parameter of a procedure with an arbitrary number of arguments. See Section procedure for the exact syntax and details; an example is given just below.

Let us remark that declaring a procedure does not involve any evaluation or other interpretation of the procedure body. In particular, this means that constants are evaluated to floating-point values inside Sollya when the procedure is applied to actual parameters and the global precision valid at this moment.

Sollya procedures are well illustrated with the following examples:

   > succ = proc(n) { return n + 1; };
   > succ(5);
   6
   > 3 + succ(0);
   4
   > succ;
   proc(n)
   {
   nop;
   return (n) + (1);
   }

   > add = proc(m,n) { var res; res := m + n; return res; };
   > add(5,6);
   11
   > hey = proc() { print("Hello world."); };
   > hey();
   Hello world.
   > print(hey());
   Hello world.
   void
   > hey;
   proc()
   {
   print("Hello world.");
   return void;
   }

   > fac = proc(n) { var res; if (n == 0) then res := 1 else res := n * fac(n - 1); return res; };
   > fac(5);
   120
   > fac(11);
   39916800
   > fac;
   proc(n)
   {
   var res;
   if (n) == (0) then
   res := 1
   else
   res := (n) * (fac((n) - (1)));
   return res;
   }

   > sumall = proc(args = ...) { var i, acc; acc = 0; for i in args do acc = acc + i; return acc; };
   > sumall;
   proc(args = ...)
   {
   var i, acc;
   acc = 0;
   for i in args do
   acc = (acc) + (i);
   return acc;
   }
   > sumall();
   0
   > sumall(1);
   1
   > sumall(1,5);
   6
   > sumall(1,5,9);
   15
   > sumall @ [|1,5,9,4,8|];
   27
   >

Let us note that, when writing a procedure, one does not know what will be the name of the free variable at run-time. This is typically the context when one should use the special keyword _x_:

   > ChebPolynomials = proc(n) {
       var i, res;
       if (n<0) then res = [||]
       else if (n==0) then res = [|1|]
       else {
          res = [|1, _x_|];
          for i from 2 to n do res[i] = horner(2*_x_*res[i-1]-res[i-2]);
       };
       return res;
     };
   >
   > f = sin(x);
   > T = ChebPolynomials(4);
   > canonical = on!;
   > for i from 0 to 4 do T[i];
   1
   x
   -1 + 2 * x^2
   -3 * x + 4 * x^3
   1 + -8 * x^2 + 8 * x^4

Sollya also supports external procedures, i.e., procedures written in C (or some other language) and dynamically bound to Sollya identifiers. See externalproc for details.

7.2 - Pattern matching

Starting with version 3.0, Sollya supports matching expressions with expression patterns. This feature is important for an extended functional programming style. Further, and most importantly, it allows expression trees to be recursively decomposed using native constructs of the Sollya language. This means no help from external procedures or other compiled-language mechanisms is needed here anymore.

Basically, pattern matching supports relies on one Sollya construct:

match expr with
pattern1 : (return-expr1)
pattern2 : (return-expr2)
...
patternN : (return-exprN)

That construct has the following semantic: try to match the expression expr with the patterns pattern1 through patternN, proceeding in natural order. If a pattern patternI is found that matches, evaluate the whole match ... with construct to the return expression return-exprI associated with the matching pattern patternI. If no matching pattern is found, display an error warning and return error. Note that the parentheses around the expressions return-exprI are mandatory.

Matching a pattern means the following:

If a pattern patternI with variables is matched in a match ... with construct, the variables in the pattern stay bound during the evaluation of the corresponding return expression return-exprI. This allows subexpressions to be extracted from expressions and/or recursively handled as needed.

The following examples illustrate the basic principles of pattern matching in Sollya. One can remark that it is useful to use the keyword _x_ when one wants to be sure to refer to the free variable in a pattern matching:

   > match exp(x) with
         exp(x)      : (1)
         sin(x)      : (2)
         default     : (3);
   1
   >
   > match sin(x) with
         exp(x)      : (1)
         sin(x)      : (2)
         default     : (3);
   2
   >
   > match exp(sin(x)) with
         exp(x)      : ("Exponential of x")
         exp(sin(x)) : ("Exponential of sine of x")
         default     : ("Something else");
   Exponential of sine of x
   >
   > match exp(sin(x)) with
         exp(x)      : ("Exponential of x")
         exp(a)      : ("Exponential of " @ a)
         default     : ("Something else");
   Exponential of sin(x)
   >
   >
   > procedure differentiate(f) {
         return match f with
             g + h   : (differentiate(g) + differentiate(h))
             g * h   : (differentiate(g) * h + differentiate(h) * g)
             g / h   : ((differentiate(g) * h - differentiate(h) * g) / (h^2))
             exp(_x_)  : (exp(_x_))
             sin(_x_)  : (cos(_x_))
             cos(_x_)  : (-sin(_x_))
             g(h)    : ((differentiate(g))(h) * differentiate(h))
             _x_       : (1)
             h(_x_)    : (NaN)
             c       : (0);
     };
   >
   > rename(x,y);
   Information: the free variable has been renamed from "x" to "y".
   > differentiate(exp(sin(y + y)));
   exp(sin(y * 2)) * cos(y * 2) * 2
   > diff(exp(sin(y + y)));
   exp(sin(y * 2)) * cos(y * 2) * 2
   >

As Sollya is not a purely functional language, the match ... with construct can also be used in a more imperative style, which makes it become closer to constructs like switch in C or Perl. In lieu of a simple return expression, a whole block of imperative statements can be given. The expression to be returned by that block is indicated in the end of the block, using the return keyword. That syntax is illustrated in the next example:

   > match exp(sin(x)) with
         exp(a)  : {
                      write("Exponential of ", a, "\n");
                      return a;
                   }
         sin(x)  : {
                      var foo;
                      foo = 17;
                      write("Sine of x\n");
                      return foo;
                   }
         default : {
                      write("Something else\n");
                      bashexecute("LANG=C date");
                      return true;
                   };
   Exponential of sin(x)
   sin(x)
   >
   > match sin(x) with
         exp(a)  : {
                      write("Exponential of ", a, "\n");
                      return a;
                   }
         sin(x)  : {
                      var foo;
                      foo = 17;
                      write("Sine of x\n");
                      return foo;
                   }
         default : {
                      write("Something else\n");
                      bashexecute("LANG=C date");
                      return true;
                   };
   Sine of x
   17
   >
   > match acos(17 * pi * x) with
         exp(a)  : {
                      write("Exponential of ", a, "\n");
                      return a;
                   }
         sin(x)  : {
                      var foo;
                      foo = 17;
                      write("Sine of x\n");
                      return foo;
                   }
         default : {
                      write("Something else\n");
                      bashexecute("LANG=C date");
                      return true;
                   };
   Something else
   Mon Oct 17 09:47:15 CEST 2016
   true

In the case when no return statement is indicated for a statement-block in a match ... with construct, the construct evaluates to the special value void if that pattern matches.

In order to well understand pattern matching in Sollya, it is important to realize the meaning of variables in patterns. This meaning is different from the one usually found for variables. In a pattern, variables are never evaluated to whatever they might have set before the pattern is executed. In contrast, all variables in patterns are new, free variables that will freshly be bound to subexpressions of the matching expression. If a variable of the same name already exists, it will be shadowed during the evaluation of the statement block and the return expression corresponding to the matching expression. This type of semantic implies that patterns can never be computed at run-time, they must always be hard-coded beforehand. However this is necessary to make pattern matching context-free.

As a matter of course, all variables figuring in the expression expr to be matched are evaluated before pattern matching is attempted. In fact, expr is a usual Sollya expression, not a pattern.

In Sollya, the use of variables in patterns does not need to be linear. This means the same variable might appear twice or more in a pattern. Such a pattern will only match an expression if it contains the same subexpression, associated with the variable, in all places indicated by the variable in the pattern.

The following examples illustrate the use of variables in patterns in detail:

   > a = 5;
   > b = 6;
   > match exp(x + 3) with
           exp(a + b) : {
                           print("Exponential");
                           print("a = ", a);
                           print("b = ", b);
                        }
           sin(x)     : {
                           print("Sine of x");
                        };
   Exponential
   a =  x
   b =  3
   > print("a = ", a, ", b = ", b);
   a =  5 , b =  6
   >
   > a = 5;
   > b = 6;
   > match exp(x + 3) with
           exp(a + b) : {
                           var a, c;
                           a = 17;
                           c = "Hallo";
                           print("Exponential");
                           print("a = ", a);
                           print("b = ", b);
                           print("c = ", c);
                        }
           sin(x)     : {
                           print("Sine of x");
                        };
   Exponential
   a =  17
   b =  3
   c =  Hallo
   > print("a = ", a, ", b = ", b);
   a =  5 , b =  6

   > match exp(sin(x)) + sin(x) with
           exp(a) + a : {
                           print("Winner");
                           print("a = ", a);
                        }
           default    : {
                           print("Loser");
                        };
   Winner
   a =  sin(x)
   >
   > match exp(sin(x)) + sin(3 * x) with
           exp(a) + a : {
                           print("Winner");
                           print("a = ", a);
                        }
           default    : {
                           print("Loser");
                        };
   Loser
   >
   > f = exp(x);
   > match f with
           sin(x) : (1)
           cos(x) : (2)
           exp(x) : (3)
           default : (4);
   3

Pattern matching is meant to be a means to decompose expressions structurally. For this reason and in an analogous way to variables, no evaluation is performed at all on (sub-)expressions that form constant functions. As a consequence, patterns match constant expressions only if they are structurally identical. For example 5+1 only matches 5+1 and not 1+5, 3+3 nor 6.

This general rule on constant expressions admits one exception. Intervals in Sollya can be defined using constant expressions as bounds. These bounds are immediately evaluated to floating-point constants, though. In order to permit pattern matching on intervals, constant expressions given as bounds of intervals that form patterns are evaluated before pattern matching. However, in order not conflict with the rules of no evaluation of variables, these constant expressions as bounds of intervals in patterns must not contain free variables.

   > match 5 + 1 with
         1 + 5 : ("One plus five")
         6     : ("Six")
         5 + 1 : ("Five plus one");
   Five plus one
   >
   > match 6 with
         1 + 5 : ("One plus five")
         6     : ("Six")
         5 + 1 : ("Five plus one");
   Six
   >   
   > match 1 + 5 with
         1 + 5 : ("One plus five")
         6     : ("Six")
         5 + 1 : ("Five plus one");
   One plus five
   >
   > match [1; 5 + 1] with
         [1; 1 + 5] : ("Interval from one to one plus five")
         [1; 6]     : ("Interval from one to six")
         [1; 5 + 1] : ("Interval from one to five plus one");
   Interval from one to one plus five
   >
   > match [1; 6] with
         [1; 1 + 5] : ("Interval from one to one plus five")
         [1; 6]     : ("Interval from one to six")
         [1; 5 + 1] : ("Interval from one to five plus one");
   Interval from one to one plus five
   >

The Sollya keyword default has a special meaning in patterns. It acts like a wild-card, matching any (sub-)expression, as long as the whole expression stays correctly typed. Upon matching with default, no variable gets bound. This feature is illustrated in the next example:

   > match exp(x) with
         sin(x)    : ("Sine of x")
         atan(x^2) : ("Arctangent of square of x")
         default   : ("Something else")
         exp(x)    : ("Exponential of x");
   Something else
   >
   > match atan(x^2) with
         sin(x)          : ("Sine of x")
         atan(default^2) : ("Arctangent of the square of something")
         default         : ("Something else");
   Arctangent of the square of something
   >
   > match atan(exp(x)^2) with
         sin(x)          : ("Sine of x")
         atan(default^2) : ("Arctangent of the square of something")
         default         : ("Something else");
   Arctangent of the square of something
   >
   > match exp("Hello world") with
         exp(default)    : ("A miracle has happened")
         default         : ("Something else");
   Warning: at least one of the given expressions or a subexpression is not correctly typed
   or its evaluation has failed because of some error on a side-effect.
   error

In Sollya, pattern matching is possible on the following Sollya types and operations defined on them:

   > procedure detector(obj) {
         match obj with
             exp(a * x)            : { "Exponential of ", a, " times x"; }
             [ a; 17 ]             : { "An interval from ", a, " to 17"; }
             [| |]                 : { "Empty list"; }
             [| a, b, 2, exp(c) |] : { "A list of ", a, ", ", b, ", 2 and ",
                                       "exponential of ", c; }
             a @ [| 2, 3 |]        : { "Concatenation of the list ", a, " and ",
                                       "the list of 2 and 3"; }
             a .: [| 9 ... |]      : { a, " prepended to all integers >= 9"; }
             "Hello" @ w           : { "Hello concatenated with ", w; }
             { .a = sin(b);
               .b = [c;d] }        : { "A structure containing as .a the ",
                                       "sine of ", b,
                                       " and as .b the range from ", c,
                                       " to ", d; }
             perturb               : { "The special object perturb"; }
             default               : { "Something else"; };
     };
   >
   > detector(exp(5 * x));
   Exponential of 5 times x
   > detector([3.25;17]);
   An interval from 3.25 to 17
   > detector([||]);
   Empty list
   > detector([| sin(x), nearestint(x), 2, exp(5 * atan(x)) |]);
   A list of sin(x), nearestint(x), 2 and exponential of 5 * atan(x)
   > detector([| sin(x), cos(5 * x), "foo", 2, 3 |]);
   Concatenation of the list [|sin(x), cos(x * 5), "foo"|] and the list of 2 and 3
   > detector([| DE, 9... |]);
   doubleextended prepended to all integers >= 9
   > detector("Hello world");
   Hello concatenated with  world
   > detector({ .a = sin(x); .c = "Hello"; .b = [9;10] });
   A structure containing as .a the sine of x and as .b the range from 9 to 10
   > detector(perturb);
   The special object perturb
   > detector([13;19]);
   Something else

Concerning intervals, please pay attention to the fact that expressions involving intervals are immediately evaluated and that structural pattern matching on functions on intervals is not possible. This point is illustrated in the next example:

   > match exp([1;2]) with
           [a;b]              : {
                                   a,", ",b;
                                }
           default            : {
                                   "Something else";
                                };
   2.7182818284590452353602874713526624977572470936999, 7.3890560989306502272304274605750078131803155705519
   >
   > match exp([1;2]) with
           exp([a;b])         : {
                                   a,", ", b;
                                }
           default            : {
                                   "Something else";
                                };
   Warning: at least one of the given expressions or a subexpression is not correctly typed
   or its evaluation has failed because of some error on a side-effect.
   error
   >
   > match exp([1;2]) with
       exp(a)  : {
                   "Exponential of ", a;
                 }
       default : {
                   "Something else";
                 };
   Something else

With respect to pattern matching on lists or character sequences defined using the @ operator, the following is to be mentionned:

These points are illustrated in this example:

   > match [| exp(sin(x)), sin(x), 4, DE(x), 9... |] with
           exp(a) .: (a .: (([||] :. 4) @ (b @ [| 13... |]))) :
                              { "a = ", a, ", b = ", b; };
   a = sin(x), b = [|doubleextended(x), 9, 10, 11, 12|]
   >
   > match [| 1, 2, 3, 4, D... |] with
           a @ [| 4, D...|] : (a);
   [|1, 2, 3|]
   >
   > match [| 1, 2, 3, 4, D... |] with
           a @ [| D...|] : (a);
   [|1, 2, 3, 4|]
   >
   > match [| 1, 2, 3, 4... |] with
           a @ [| 3...|] : (a);
   [|1, 2|]
   >
   > match [| 1, 2, 3, 4... |] with
           a @ [| 4...|] : (a);
   [|1, 2, 3|]
   >
   > match [| 1, 2, 3, 4... |] with
           a @ [| 17...|] : (a);
   [|1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16|]
   >
   > match [| 1, 2, 3, 4... |] with
           a @ [| 17, 18, 19 |] : (a)
           default              : ("Something else");
   Something else

As mentionned above, pattern matching on Sollya structures is possible. Patterns for such a match are given in a literately, i.e., using the syntax { .a = exprA, .b = exprB, ... }. A structure pattern sp will be matched by a structure s iff that structure s contains at least all the elements (like .a, .b etc.) of the structure pattern sp and iff each of the elements of the structure s matches the pattern in the corresponding element of the structure pattern sp. The user should be aware of the fact that the structure to be matched is only supposed to have at least the elements of the pattern but that it may contain more elements is a particular Sollya feature. For instance with pattern matching, it is hence possible to ensure that access to particular elements will be possible in a particular code segment. The following example is meant to clarify this point:

   > structure.f = exp(x);
   > structure.dom = [1;2];
   > structure.formats = [| DD, D, D, D |];
   > match structure with
          { .f = sin(x);
            .dom = [a;b]
          }                    : { "Sine, ",a,", ",b; }
          { .f = exp(c);
            .dom = [a;b];
            .point = default
          }                    : { "Exponential, ",a, ", ", b, ", ", c; }
          { .f = exp(x);
            .dom = [a;b]
          }                    : { "Exponential, ",a, ", ", b; }
          default              : { "Something else"; };
   Exponential, 1, 2
   >
   > structure.f = sin(x);
   > match structure with
          { .f = sin(x);
            .dom = [a;b]
          }                    : { "Sine, ",a,", ",b; }
          { .f = exp(c);
            .dom = [a;b];
            .point = default
          }                    : { "Exponential, ",a, ", ", b, ", ", c; }
          { .f = exp(x);
            .dom = [a;b]
          }                    : { "Exponential, ",a, ", ", b; }
          default              : { "Something else"; };
   Sine, 1, 2
   >
   > structure.f = exp(x + 2);
   > structure.point = 23;
   > match structure with
          { .f = sin(x);
            .dom = [a;b]
          }                    : { "Sine, ",a,", ",b; }
          { .f = exp(c);
            .dom = [a;b];
            .point = default
          }                    : { "Exponential, ",a, ", ", b, ", ", c; }
          { .f = exp(x);
            .dom = [a;b]
          }                    : { "Exponential, ",a, ", ", b; }
          default              : { "Something else"; };
   Exponential, 1, 2, 2 + x

8 - Commands and functions

The list of commands of Sollya is available in two flavours:

9 - Appendix: interval arithmetic philosophy in Sollya

Although it is currently based on the MPFI library, Sollya has its own way of interpreting interval arithmetic when infinities or NaN occur, or when a function is evaluated on an interval containing points out of its domain, etc. This philosophy may differ from the one applied in MPFI. It is also possible that the behavior of Sollya does not correspond to the behavior that one would expect, e.g., as a natural consequence of the IEEE-754 standard.

The topology that we consider is always the usual topology of R bar: R U {-infinity, +infinity}. For any function, if one of its arguments is empty (respectively NaN), we return empty (respectively NaN).

9.1 - Univariate functions

Let f be a univariate basic function and I an interval. We denote by J the result of the interval evaluation of f over I in Sollya. If I is completely included in the domain of f, J will usually be the smallest interval (at the current precision) containing the exact image f(I) However, in some cases, it may happen that J is not as small as possible. It is guaranteed however, that J tends to f(I) when the precision of the tool tends to infinity.

When f is not defined at some point x but is defined on a neighborhood of x, we consider that the “value” of f at x is the convex hull of the limit points of f around x. For instance, consider the evaluation of f= tan on [0, Pi]. It is not defined at Pi/2 (and only at this point). The limit points of f around Pi/2 are -infinity and +infinity, so, we return [-infinity, +infinity]. Another example: f=sin on [+infinity]. The function has no limit at this point, but all points of [-1, 1] are limit points. So, we return [-1,1].

Finally, if I contains a subinterval on which f is not defined, we return [NaN, NaN] (example: sqrt([-1, 2])).

9.2 - Bivariate functions

Let f be a bivariate function and I1 and I2 be intervals. If I1=[x] and I2=[y] are both point-intervals, we return the convex hull of the limit points of f around (x, y) if it exists. In particular, if f is defined at (x, y) we return its value (or a small interval around it, if it is not exactly representable). As an example [1]/[+infinity] returns [0]. Also, [1]/[0] returns [-infinity, +infinity] (note that Sollya does not consider signed zeros). If it is not possible to give a meaning to the expression f(I1, I2), we return NaN: for instance [0]/[0] or [0]*[+infinity].

If one and only one of the intervals is a point-interval (say I1 = [x]), we consider the partial function g: y -> f(x,y) and return the value that would be obtained when evaluating g on I2. For instance, in order to evaluate [0]/I2, we consider the function g defined for every y != 0 by g(y)=0/y=0. Hence, g(I2) = [0] (even if I2 contains 0, by the argument of limit-points). In particular, please note that [0]/[-1, 1] returns [0] even though [0]/[0] returns NaN. This rule even holds when g can only be defined as limit points: for instance, in the case I1/[0] we consider g: x -> x/0. This function cannot be defined stricto sensu, but we can give it a meaning by considering 0 as a limit. Hence g is multivalued and its value is {-infinity, +infinity} for every x. Hence, I1/[0] returns [-infinity, +infinity] when I1 is not a point-interval.

Finally, if neither I1 nor I2 are point-intervals, we try to give a meaning to f(I1, I2) by an argument of limit-points when possible. For instance [1, 2] / [0, 1] returns [1, +infinity].

As a special exception to these rules, [0]^[0] returns [1].

10 - Appendix: the Sollya library

10.1 - Introduction

The header file of the Sollya library is sollya.h. Its inclusion may provoke the inclusion of other header files, such as gmp.h, mpfr.h or mpfi.h.

The library provides a virtual Sollya session that is perfectly similar to an interactive session: global variables such as verbosity, prec, display, midpointmode, etc. are maintained and affect the behavior of the library, warning messages are displayed when something is not exact, etc. Please notice that the Sollya library currently is not re-entrant and can only be opened once. A process using the library must hence not be multi-threaded and is limited to one single virtual Sollya session.

In order to get started with the Sollya library, the first thing to do is hence to initialize this virtual session. This is performed with the sollya_lib_init function. Accordingly, one should close the session at the end of the program (which has the effect of releasing all the memory used by Sollya). Please notice that Sollya uses its own allocation functions and registers them to GMP using the custom allocation functions provided by GMP. Particular precautions should hence be taken when using the Sollya library in a program that also registers its own functions to GMP: in that case sollya_lib_init_with_custom_memory_functions should be used instead of sollya_lib_init for initializing the library. This is discussed in a specific section.

In the usual case when Sollya is used in a program that does not register allocation functions to GMP, a minimal file using the library is hence the following.

#include <sollya.h>

int main(void) {
  sollya_lib_init();

    /* Functions of the library can be called here */

  sollya_lib_close();
  return 0;
}

Suppose that this code is saved in a file called foo.c. The compilation is performed as usual without forgetting to link against libsollya (since the libraries libgmp, libmpfr and libmpfi are dependencies of Sollya, it might also be necessary to explicitly link against them):

  /% cc foo.c -c
  /% cc foo.o -o foo -lsollya -lmpfi -lmpfr -lgmp

10.2 - Sollya object data-type

The library provides a single data type called sollya_obj_t that can contain any Sollya object (a Sollya object is anything that can be stored in a variable within the interactive tool. See Section Data Types of the present documentation for details). Please notice that sollya_obj_t is in fact a pointer type; this has two consequences:

Except for a few functions for which the contrary is explicitly specified, the following conventions are used:

In general, except if the user perfectly knows what they are doing, the following rules should be applied (here a and b are C variables of type sollya_obj_t, and sollya_lib_foo and sollya_lib_bar are functions of the library):

Please notice that sollya_lib_close() clears the memory allocated by the virtual Sollya session but not the objects that have been created and stored in C variables. All the sollya_obj_t created by function calls should be cleared manually.

We can now write a simple Hello World program using the Sollya library:

#include <sollya.h>

int main(void) {
  sollya_obj_t s1, s2, s;
  sollya_lib_init();

  s1 = sollya_lib_string("Hello ");
  s2 = sollya_lib_string("World!");
  s = sollya_lib_concat(s1, s2);
  sollya_lib_clear_obj(s1);
  sollya_lib_clear_obj(s2);

  sollya_lib_printf("%b\n", s);
  sollya_lib_clear_obj(s);
  sollya_lib_close();
  return 0;
}

A universal function allows the user to execute any expression, as if it were given at the prompt of the Sollya tool, and to get a sollya_obj_t containing the result of the evaluation: this function is sollya_lib_parse_string("some expression here"). This is very convenient, and indeed, any script written in the Sollya language, could easily be converted into a C program by intensively using sollya_lib_parse_string. However, this should not be the preferred way if efficiency is targeted because (as its name suggests) this function uses a parser to decompose its argument, then constructs intermediate data structures to store the abstract interpretation of the expression, etc. Low-level functions are provided for efficiently creating Sollya objects; they are detailed in the next Section.

10.3 - Conventions in use in the library

The library follows some conventions that are useful to remember:

10.4 - Displaying Sollya objects and numerical values

Within the interactive tool, the most simple way of displaying the content of a variable or the value of an expression is to write the name of the variable or the expression, followed by the character “;”. As a result, Sollya evaluates the expression or the variable and displays the result. Alternatively, a set of objects can be displayed the same way, separating the objects with commas. In library mode, the same behavior can be reproduced using the function void sollya_lib_autoprint(sollya_obj_t, ...). Please notice that this function has a variable number of arguments: they are all displayed, until an argument equal to NULL is found. The NULL argument is mandatory, even if only one object shall be displayed (the function has no other way to know if other arguments follow or not). So, if only one argument should be displayed, the correct function call is sollya_lib_autoprint(arg, NULL). Accordingly, if two arguments should be displayed, the function call is sollya_lib_autoprint(arg1, arg2, NULL), etc. The function void sollya_lib_v_autoprint(sollya_obj_t, va_list) is the same, but it takes a va_list argument instead of a variable number of arguments.

Further, there is another way of printing formatted strings containing Sollya objects, using a printf-like syntax. Eight functions are provided, namely:

Each one of these functions overloads the usual function (respectively, printf, vprintf, fprintf, vfprintf, sprintf, vsprintf, snprintf and vsnprintf). The full syntax of conversions specifiers supported with the usual functions is handled (please note that the style using '$' – as in %3$ or %*3$ – is not handled though. It is not included in the C99 standard anyway). Additionally, the following conversion specifiers are provided:

When one of the above conversion specifiers is used, the corresponding argument is displayed as it would be within the interactive tool: i.e., the way the argument is displayed depends on Sollya environment variables, such as prec, display, midpointmode, etc. When a precision modifier n is used, the argument is first rounded to a binary precision of roughly log2(10)*n bits (i.e., roughly equivalent to n decimal digits) before being displayed. As with traditional printf, the precision modifier can be replaced with * which causes the precision to be determined by an additional int argument.

Flag characters (e.g., ‘#’, ‘0’, etc.) are allowed but have no effect, except flag character ‘-’ that is supported with its usual meaning of left-aligning the converted value. The full syntax for minimum field width is supported: it can be given directly as an integer in the format string (e.g., %22b) or it can be replaced with *, which causes the field width to be determined by an additional int argument. As usual, a negative field width is taken as a ‘-’ flag followed by a positive width.

As a special (and sometimes convenient) case, %b accepts that its corresponding sollya_obj_t argument be NULL: in this particular case, the string “NULL” is used in the displayed string. Please notice that, except for the particular case of NULL, the behavior of sollya_lib_printf is completely undefined if the argument of %b is not a valid Sollya object.

The sollya_lib_printf functions return an integer with the same meaning as the traditional printf functions. It indicates the number of characters that have been output (excluding the final \0 character). Similarly, the conversion specifier %n can be used, even together with the Sollya conversion specifiers %b, %v, %w, %r and %k. The functions sollya_lib_snprintf and sollya_lib_v_snprintf will never write more characters than indicated by their size argument (including the final \0 character). If the output gets truncated due to this limit, they will return the number of characters (excluding the final \0 character) that would have been output if there had not been any truncation. In case of error, all sollya_lib_printf functions return a negative value.

10.5 Creating Sollya objects

Sollya objects conceptually fall into one of five categories: numerical constants (e.g., 1 or 1.5), functional expressions (they might contain numerical constants, e.g., sin(cos(x+1.5))), other simple objects (intervals, strings, built-in constants such as dyadic, etc.), lists of objects (e.g., [|1, "Hello"|]) and structures (e.g., {.a = 1; .b = "Hello"}).

10.5.1 - Numerical constants

Table Creating numerical constants lists the different functions available to construct numerical constants. A Sollya constant is always created without rounding (whatever the value of global variable prec is at the moment of the function call): a sufficient precision is always allocated so that the constant is stored exactly. All these functions return a constant floating-point number except sollya_lib_constant_from_mpq that may return a constant expression if the value of the rational number given as argument is not exactly representable as a floating-point number at some precision. The returned expression is of the form p/q in this case.

The objects returned by these functions are newly allocated and copies of the argument. For instance, after the instruction a = sollya_lib_constant(b), the user will eventually have to clear a (with sollya_lib_clear(a)) and b (with mpfr_clear(b)).

The function sollya_lib_constant_from_double (or more conveniently its shortcut SOLLYA_CONST) is probably the preferred way for constructing numerical constants. As the name indicates it, its argument is a double; however, due to implicit casting in C, it is perfectly possible to give an int as argument: it will be converted into a double (without rounding if the integer fits on 53 bits) before being passed to SOLLYA_CONST. On the contrary, the user should be aware of the fact that if decimal non-integer constants are given, C rules of rounding (to double) are applied, regardless of the setting of the Sollya precision variable prec.

Creating numerical constants (Creates a fresh sollya_obj_t. Conversion is always exact)
Type of the argument Name of the function Shortcut macro
double sollya_lib_constant_from_double(x) SOLLYA_CONST(x)
uint64_t sollya_lib_constant_from_uint64(x) SOLLYA_CONST_UI64(x)
int64_t sollya_lib_constant_from_int64(x) SOLLYA_CONST_SI64(x)
int sollya_lib_constant_from_int(x) N/A
mpq_t sollya_lib_constant_from_mpq(x) N/A
mpz_t sollya_lib_constant_from_mpz(x) N/A
mpfr_t sollya_lib_constant(x) N/A

10.5.2 - Functional expressions

Functional expressions are built by composition of basic functions with constants and the free mathematical variable. Since it is convenient to build such expressions by chaining function calls, the library provides functions that “eat up” their arguments (actually embedding them in a bigger expression). The convention is that functions that eat up their arguments are prefixed by sollya_lib_build_. For the purpose of building expressions, shortcut macros for the corresponding functions exist. They are all listed in Table Building functional expressions.

It is worth mentioning that, although SOLLYA_X_ and SOLLYA_PI are used without parentheses (as if they denoted constants), they are in fact function calls that create a new object each time they are used. The absence of parentheses is just more convenient for constructing expressions, such as, e.g., SOLLYA_COS(SOLLYA_X_).

Building functional expressions (Eats up arguments, embedding them in the returned object.)
Name in the interactive tool Function to build it Shortcut macro
_x_ sollya_lib_build_function_free_variable() SOLLYA_X_
pi sollya_lib_build_function_pi() SOLLYA_PI
e1 + e2 sollya_lib_build_function_add(e1, e2) SOLLYA_ADD(e1, e2)
e1 - e2 sollya_lib_build_function_sub(e1, e2) SOLLYA_SUB(e1, e2)
e1 * e2 sollya_lib_build_function_mul(e1, e2) SOLLYA_MUL(e1, e2)
e1 / e2 sollya_lib_build_function_div(e1, e2) SOLLYA_DIV(e1, e2)
pow(e1, e2) sollya_lib_build_function_pow(e1, e2) SOLLYA_POW(e1, e2)
-e sollya_lib_build_function_neg(e) SOLLYA_NEG(e)
sqrt(e) sollya_lib_build_function_sqrt(e) SOLLYA_SQRT(e)
abs(e) sollya_lib_build_function_abs(e) SOLLYA_ABS(e)
erf(e) sollya_lib_build_function_erf(e) SOLLYA_ERF(e)
erfc(e) sollya_lib_build_function_erfc(e) SOLLYA_ERFC(e)
exp(e) sollya_lib_build_function_exp(e) SOLLYA_EXP(e)
expm1(e) sollya_lib_build_function_expm1(e) SOLLYA_EXPM1(e)
log(e) sollya_lib_build_function_log(e) SOLLYA_LOG(e)
log2(e) sollya_lib_build_function_log2(e) SOLLYA_LOG2(e)
log10(e) sollya_lib_build_function_log10(e) SOLLYA_LOG10(e)
log1p(e) sollya_lib_build_function_log1p(e) SOLLYA_LOG1P(e)
sin(e) sollya_lib_build_function_sin(e) SOLLYA_SIN(e)
cos(e) sollya_lib_build_function_cos(e) SOLLYA_COS(e)
tan(e) sollya_lib_build_function_tan(e) SOLLYA_TAN(e)
asin(e) sollya_lib_build_function_asin(e) SOLLYA_ASIN(e)
acos(e) sollya_lib_build_function_acos(e) SOLLYA_ACOS(e)
atan(e) sollya_lib_build_function_atan(e) SOLLYA_ATAN(e)
sinh(e) sollya_lib_build_function_sinh(e) SOLLYA_SINH(e)
cosh(e) sollya_lib_build_function_cosh(e) SOLLYA_COSH(e)
tanh(e) sollya_lib_build_function_tanh(e) SOLLYA_TANH(e)
asinh(e) sollya_lib_build_function_asinh(e) SOLLYA_ASINH(e)
acosh(e) sollya_lib_build_function_acosh(e) SOLLYA_ACOSH(e)
atanh(e) sollya_lib_build_function_atanh(e) SOLLYA_ATANH(e)
D(e), double(e) sollya_lib_build_function_double(e) SOLLYA_D(e)
SG(e), single(e) sollya_lib_build_function_single(e) SOLLYA_SG(e)
QD(e), quad(e) sollya_lib_build_function_quad(e) SOLLYA_QD(e)
HP(e), halfprecision(e) sollya_lib_build_function_halfprecision(e) SOLLYA_HP(e)
DD(e), doubledouble(e) sollya_lib_build_function_double_double(e) SOLLYA_DD(e)
TD(e), tripledouble(e) sollya_lib_build_function_triple_double(e) SOLLYA_TD(e)
DE(e), doubleextended(e) sollya_lib_build_function_doubleextended(e) SOLLYA_DE(e)
ceil(e) sollya_lib_build_function_ceil(e) SOLLYA_CEIL(e)
floor(e) sollya_lib_build_function_floor(e) SOLLYA_FLOOR(e)
nearestint(e) sollya_lib_build_function_nearestint(e) SOLLYA_NEARESTINT(e)

For each function of the form sollya_lib_build_function_foo, there exists a function called sollya_lib_foo. There are two differences between them:

Actually, sollya_lib_foo has exactly the same behavior as writing an expression at the prompt within the interactive tool. In particular, it is possible to give a range as an argument to sollya_lib_foo: the returned object will be the result of the evaluation of function foo on that range by interval arithmetic. In contrast, trying to use sollya_lib_build_function_foo on a range would result in a typing error.

Alternatively, one may create functional expressions with the functions
   int sollya_lib_construct_function(sollya_obj_t *res, sollya_base_function_t type, ...)
   int sollya_lib_v_construct_function(sollya_obj_t *, sollya_base_function_t, va_list).
The advantage of these functions with respect to the others presented above lies in the fact that they offer a way to create any functional expression, the basic function that one wants to construct being provided with the argument type. Since these functions are indeed doing the exact contrary of sollya_lib_decompose_function, they are described in details in the corresponding Section Decomposing a functional expression.

10.5.3 - Other simple objects

Other simple objects are created with functions listed in Table Creating Sollya objects from scratch. The functions with a name of the form sollya_lib_something follow the same convention as sollya_lib_constant: they build a new object from a copy of their argument, and the conversion is always exact, whatever the value of prec is.

Please note that in the interactive tool, D either denotes the discrete mathematical function that maps a real number to its closest double number, or is used as a symbolic constant to indicate that the double format must be used (as an argument of round for instance). In the library, they are completely distinct objects, the mathematical function being obtained with sollya_lib_build_function_double and the symbolic constant with sollya_lib_double_obj. The same holds for other formats (DD, SG, etc.)

Creating Sollya objects from scratch (Returns a new sollya_obj_t)
Name in the interactive tool Function to create it
on sollya_lib_on();
off sollya_lib_off();
dyadic sollya_lib_dyadic();
powers sollya_lib_powers();
binary sollya_lib_binary();
hexadecimal sollya_lib_hexadecimal();
file sollya_lib_file();
postscript sollya_lib_postscript();
postscriptfile sollya_lib_postscriptfile();
perturb sollya_lib_perturb();
RD sollya_lib_round_down();
RU sollya_lib_round_up();
RZ sollya_lib_round_towards_zero();
RN sollya_lib_round_to_nearest();
honorcoeffprec sollya_lib_honorcoeffprec();
true sollya_lib_true();
false sollya_lib_false();
void sollya_lib_void();
default sollya_lib_default();
decimal sollya_lib_decimal();
absolute sollya_lib_absolute();
relative sollya_lib_relative();
fixed sollya_lib_fixed();
floating sollya_lib_floating();
error sollya_lib_error();
D, double sollya_lib_double_obj();
SG, single sollya_lib_single_obj();
QD, quad sollya_lib_quad_obj();
HP, halfprecision sollya_lib_halfprecision_obj();
DE, doubleextended sollya_lib_doubleextended_obj();
DD, doubledouble sollya_lib_double_double_obj();
TD, tripledouble sollya_lib_triple_double_obj();
"Hello" sollya_lib_string("Hello")
[1, 3.5] sollya_lib_range_from_interval(a);
[1, 3.5] sollya_lib_range_from_bounds(b, c);
[1, 3.5] sollya_lib_range(d, e);

In the last lines of the table, a is a mpfi_t containing the interval [1, 3.5], b and c are mpfr_t respectively containing the numbers 1 and 3.5, and d and e are sollya_obj_t respectively containing the numbers 1 and 3.5. Conversion from a mpfi_t or a mpfr_t to a sollya_obj_t is always exact.

10.5.4 - Lists

There are actually two kinds of lists: regular lists (such as, e.g., [|1, 2, 3|]) and semi-infinite lists (such as, e.g., [|1, 2...|]). Withing the interactive tool, the ellipsis “...” can sometimes be used as a shortcut to define regular lists, e.g., [|1, 2, ..., 10|].

In the library, there is no symbol for the ellipsis, and there are two distinct types: one for regular lists and one for semi-infinite lists (called end-elliptic). Defining a regular list with an ellipsis is not possible in the library (except of course with sollya_lib_parse_string).

Constructing regular lists is achieved through three functions:

Following the same conventions, end-elliptic lists can be constructed with the following functions:

10.5.5 - Structures

Sollya structures are also available in library mode as any other Sollya object. The support for Sollya structures is however minimal and creating them might seem cumbersome (users are encouraged to make well-founded feature requests if they feel the need for better support of structures). The only function available to create structures is
int sollya_lib_create_structure(sollya_obj_t *res, sollya_obj_t s, char *name,
                                sollya_obj_t val).

This function returns a boolean integer: false means failure, and true means success. Three cases of success are possible. In all cases, the function creates a new object and stores it at the address referred to by res.

Please notice that s is not changed by this function: the structure stored in *res is a new one that does not refer to any of the components of s. As a consequence, one should not forget to explicitly clear s as well as *res when they become useless.

10.5.6 - Library functions, library constants and procedure functions

In addition to the mathematical base functions and constants provided by Sollya and listed in the Section above, the user may bind other mathematical functions and constants to Sollya objects under the condition that they can provide code to evaluate these functions or constants. The mechanism behind is similar to the one available in interactive Sollya through the library, libraryconstant and function commands (see commands library, libraryconstant and function).

With the Sollya library, this binding is done through one of the following functions:

10.5.7 - External procedures

Similarly to library functions or library constants, the binding of which is discussed in Section Library functions, library constants and procedure functions, Sollya allows external procedural code to be bound and then used inside Sollya in a procedure-like manner. This is provided in the interactive tool with the externalproc command, described in command externalproc. The same mechanism is available in the Sollya library thanks to the following functions:

Possible return and argument types for external procedures
SOLLYA_EXTERNALPROC_TYPE_VOID
SOLLYA_EXTERNALPROC_TYPE_CONSTANT
SOLLYA_EXTERNALPROC_TYPE_FUNCTION
SOLLYA_EXTERNALPROC_TYPE_RANGE
SOLLYA_EXTERNALPROC_TYPE_INTEGER
SOLLYA_EXTERNALPROC_TYPE_STRING
SOLLYA_EXTERNALPROC_TYPE_BOOLEAN
SOLLYA_EXTERNALPROC_TYPE_OBJECT
SOLLYA_EXTERNALPROC_TYPE_CONSTANT_LIST
SOLLYA_EXTERNALPROC_TYPE_FUNCTION_LIST
SOLLYA_EXTERNALPROC_TYPE_RANGE_LIST
SOLLYA_EXTERNALPROC_TYPE_INTEGER_LIST
SOLLYA_EXTERNALPROC_TYPE_STRING_LIST
SOLLYA_EXTERNALPROC_TYPE_BOOLEAN_LIST
SOLLYA_EXTERNALPROC_TYPE_OBJECT_LIST

10.6 - Getting the type of an object

Functions are provided that allow the user to test the type of a Sollya object. They are listed in Table Testing the type of a Sollya object. They all return an int interpreted as the boolean result of the test. Please note that from a typing point of view, a mathematical constant and a non-constant functional expression are both functions.

Testing the type of a Sollya object (Returns non-zero if true, 0 otherwise)
sollya_lib_obj_is_function(obj)
sollya_lib_obj_is_range(obj)
sollya_lib_obj_is_string(obj)
sollya_lib_obj_is_list(obj)
sollya_lib_obj_is_end_elliptic_list(obj)
sollya_lib_obj_is_structure(obj)
sollya_lib_obj_is_procedure(obj)
sollya_lib_obj_is_externalprocedure(obj)
sollya_lib_obj_is_error(obj)
sollya_lib_is_on(obj)
sollya_lib_is_off(obj)
sollya_lib_is_dyadic(obj)
sollya_lib_is_powers(obj)
sollya_lib_is_binary(obj)
sollya_lib_is_hexadecimal(obj)
sollya_lib_is_file(obj)
sollya_lib_is_postscript(obj)
sollya_lib_is_postscriptfile(obj)
sollya_lib_is_perturb(obj)
sollya_lib_is_round_down(obj)
sollya_lib_is_round_up(obj)
sollya_lib_is_round_towards_zero(obj)
sollya_lib_is_round_to_nearest(obj)
sollya_lib_is_honorcoeffprec(obj)
sollya_lib_is_true(obj)
sollya_lib_is_false(obj)
sollya_lib_is_void(obj)
sollya_lib_is_default(obj)
sollya_lib_is_decimal(obj)
sollya_lib_is_absolute(obj)
sollya_lib_is_relative(obj)
sollya_lib_is_fixed(obj)
sollya_lib_is_floating(obj)
sollya_lib_is_double_obj(obj)
sollya_lib_is_single_obj(obj)
sollya_lib_is_quad_obj(obj)
sollya_lib_is_halfprecision_obj(obj)
sollya_lib_is_doubleextended_obj(obj)
sollya_lib_is_double_double_obj(obj)
sollya_lib_is_triple_double_obj(obj)
sollya_lib_is_pi(obj)

10.7 - Recovering the value of a range

If a sollya_obj_t is a range, it is possible to recover the values corresponding to the bounds of the range. The range can be recovered either as a mpfi_t or as two mpfr_t (one per bound). This is achieved with the following conversion functions:

They return a boolean integer: false means failure (i.e., if the sollya_obj_t is not a range) and true means success. These functions follow the same conventions as those of the MPFR and MPFI libraries: the variables res, res_left and res_right must be initialized beforehand, and are used to store the result of the conversion. Also, the functions sollya_lib_get_something_from_range do not change the internal precision of res, res_left and res_right. If the internal precision is sufficient to perform the conversion without rounding, then it is guaranteed to be exact. If, on the contrary, the internal precision is not sufficient, the actual bounds of the range stored in arg will be rounded at the target precision using a rounding mode that ensures that the inclusion property remains valid, i.e., arg is a subset of res (resp. arg is a subset of [res_left, res_right]).

Function int sollya_lib_get_prec_of_range(mp_prec_t *prec, sollya_obj_t arg) stores at *prec a precision that is guaranteed to be sufficient to represent the range stored in arg without rounding. The returned value of this function is a boolean that follows the same convention as above. In conclusion, this is an example of a completely safe conversion:

  ...
  mp_prec_t prec;
  mpfr_t a, b;

  if (!sollya_lib_get_prec_of_range(&prec, arg)) {
    sollya_lib_printf("Unexpected error: %b is not a range\n", arg);
  }
  else {
    mpfr_init2(a, prec);
    mpfr_init2(b, prec);
    sollya_lib_get_bounds_from_range(a, b, arg);

    /* Now [a, b] = arg exactly */
  }
  ...

10.8 - Recovering the value of a numerical constant or a constant expression

From a conceptual point of view, a numerical constant is nothing but a very simple constant functional expression. Hence there is no difference in Sollya between the way constants and constant expressions are handled. The functions presented in this section allow one to recover the value of such constants or constant expressions into usual C data types.

A constant expression being given, three cases are possible:

From now on, we suppose that arg is a sollya_obj_t that contains a constant expression (or, as a particular case, a numerical constant). The general scheme followed by the conversion functions is the following: Sollya chooses an initial working precision greater than the target precision. If the value of arg is easily proved to be exactly representable at that precision, Sollya first computes this exact value and then rounds it to the nearest number of the target format (ties-to-even). Otherwise, Sollya tries to adapt the working precision automatically in order to ensure that the result of the conversion is one of both numbers in the target format that are closest to the exact value (a faithful rounding). A warning message indicates that the conversion is not exact and that a faithful rounding has been performed. In some cases really hard to evaluate, the algorithm can even fail to find a faithful rounding. In that case, too, a warning message is emitted indicating that the result of the conversion should not be trusted. Let us remark that these messages can be caught instead of being displayed and adapted handling can be provided by the user of the library at each emission of a warning (see Section Warning messages in library mode).

The conversion functions are the following. They return a boolean integer: false means failure (i.e., arg is not a constant expression) and true means success.

Function int sollya_lib_get_prec_of_constant(mp_prec_t *prec, sollya_obj_t arg) tries to find a precision that would be sufficient to exactly represent the value of arg without rounding. If it manages to find such a precision, it stores it at *prec and returns true. If it does not manage to find such a precision, or if arg is not a constant expression, it returns false and *prec is left unchanged.

In conclusion, here is an example of use for converting a constant expression to a mpfr_t:

  ...
  mp_prec_t prec;
  mpfr_t a;
  int test = 0;

  test = sollya_lib_get_prec_of_constant(&prec, arg);
  if (test) {
    mpfr_init2(a, prec);
    sollya_lib_get_constant(a, arg); /* Exact conversion */
  }
  else {
    mpfr_init2(a, 165); /* Initialization at some default precision */
    test = sollya_lib_get_constant(a, arg);
    if (!test) {
      sollya_lib_printf("Error: %b is not a constant expression\n", arg);
    }
  }
  ...

10.9 - Converting a string from Sollya to C

If arg is a sollya_obj_t that contains a string, that string can be recovered using
int sollya_lib_get_string(char **res, sollya_obj_t arg).
If arg really is a string, this function allocates enough memory on the heap to store the corresponding string, it copies the string at that newly allocated place, and sets *res so that it points to it. The function returns a boolean integer: false means failure (i.e., arg is not a string) and true means success.

Since this function allocates memory on the heap, this memory should manually be cleared by the user with sollya_lib_free once it becomes useless.

10.10 - Recovering the contents of a Sollya list

It is possible to recover the i-th element of a list arg (as one would do using arg[i] withing Sollya) with the following function:
int sollya_lib_get_element_in_list(sollya_obj_t *res, sollya_obj_t arg, int i).
It returns a boolean integer: false means failure (i.e., arg is not a list or the index is out of range) and true means success. In case of success, a copy of the i-th element of arg is stored at the address referred to by res. Since it is a copy, it should be cleared with sollya_lib_clear_obj when it becomes useless. Please notice that this function works with regular lists as well as with end-elliptic lists, just as within the interactive tool.

Another function allows user to recover all elements of a list in a single call. This function returns a C array of sollya_obj_t objects and has the following signature:
int sollya_lib_get_list_elements(sollya_obj_t **L, int *n, int *end_ell,
                                 sollya_obj_t arg).
Three cases are possible:

In case of success, please notice that (*L)[0], ..., (*L)[N-1] should manually be cleared with sollya_lib_clear_obj when they become useless. Also, the pointer *L itself should be cleared with sollya_lib_free since it points to a segment of memory allocated on the heap by Sollya.

10.11 - Recovering the contents of a Sollya structure

If arg is a sollya_obj_t that contains a structure, the contents of a given field can be recovered using
int sollya_lib_get_element_in_structure(sollya_obj_t *res, char *name,
                                        sollya_obj_t arg).
If arg really is a structure and if that structure has a field named after the string name, this function copies the contents of that field into the Sollya object *res. The function returns a boolean integer: false means failure (i.e., if arg is not a structure or if it does not have a field named after name) and true means success.

It is also possible to get all the field names and their contents. This is achieved through the function
int sollya_lib_get_structure_elements(char ***names, sollya_obj_t **objs, int *n,
                                      sollya_obj_t arg).
If arg really is a structure, say with N fields called “fieldA”, ..., “fieldZ”, this functions sets *n to N, allocates and fills an array of N strings and sets *names so that it points to that segment of memory (hence (*names)[0] is the string “fieldA”, ..., (*names)[N-1] is the string “fieldZ”). Moreover, it allocates memory for N sollya_obj_t, sets *objs so that it points on that memory segment, and copies the contents of each of the N fields at (*objs)[0], ..., (*objs)[N-1]. Finally it returns true. If arg is not a structure, the function simply returns false without doing anything. Please note that since *names and *objs point to memory segments that have been dynamically allocated, they should manually be cleared by the user with sollya_lib_free once they become useless.

10.12 - Decomposing a functional expression

If a sollya_obj_t contains a functional expression, one can decompose the expression tree using the following functions. These functions all return a boolean integer: true in case of success (i.e., if the sollya_obj_t argument really contains a functional expression) and false otherwise.

List of values defined in type sollya_base_function_t
SOLLYA_BASE_FUNC_COS SOLLYA_BASE_FUNC_DOUBLE SOLLYA_BASE_FUNC_LOG
SOLLYA_BASE_FUNC_ACOS SOLLYA_BASE_FUNC_DOUBLEDOUBLE SOLLYA_BASE_FUNC_LOG_2
SOLLYA_BASE_FUNC_ACOSH SOLLYA_BASE_FUNC_DOUBLEEXTENDED SOLLYA_BASE_FUNC_LOG_10
SOLLYA_BASE_FUNC_COSH SOLLYA_BASE_FUNC_TRIPLEDOUBLE SOLLYA_BASE_FUNC_LOG_1P
SOLLYA_BASE_FUNC_SIN SOLLYA_BASE_FUNC_HALFPRECISION SOLLYA_BASE_FUNC_EXP
SOLLYA_BASE_FUNC_ASIN SOLLYA_BASE_FUNC_SINGLE SOLLYA_BASE_FUNC_EXP_M1
SOLLYA_BASE_FUNC_ASINH SOLLYA_BASE_FUNC_QUAD SOLLYA_BASE_FUNC_NEG
SOLLYA_BASE_FUNC_SINH SOLLYA_BASE_FUNC_FLOOR SOLLYA_BASE_FUNC_SUB
SOLLYA_BASE_FUNC_TAN SOLLYA_BASE_FUNC_CEIL SOLLYA_BASE_FUNC_ADD
SOLLYA_BASE_FUNC_ATAN SOLLYA_BASE_FUNC_NEARESTINT SOLLYA_BASE_FUNC_MUL
SOLLYA_BASE_FUNC_ATANH SOLLYA_BASE_FUNC_LIBRARYCONSTANT SOLLYA_BASE_FUNC_DIV
SOLLYA_BASE_FUNC_TANH SOLLYA_BASE_FUNC_LIBRARYFUNCTION SOLLYA_BASE_FUNC_POW
SOLLYA_BASE_FUNC_ERF SOLLYA_BASE_FUNC_PROCEDUREFUNCTION SOLLYA_BASE_FUNC_SQRT
SOLLYA_BASE_FUNC_ERFC SOLLYA_BASE_FUNC_FREE_VARIABLE SOLLYA_BASE_FUNC_PI
SOLLYA_BASE_FUNC_ABS SOLLYA_BASE_FUNC_CONSTANT

To construct a functional expression, functions are provided that precisely undo what sollya_lib_decompose_function does. These functions are the following:

As an example of use of the functions described in the present section, the following code returns 1 if f denotes a functional expression made only of constants (i.e., without the free variable), and returns 0 otherwise:

#include <sollya.h>

/* Note: we suppose that the library has already been initialized */
int is_made_of_constants(sollya_obj_t f) {
  sollya_obj_t tmp1 = NULL;
  sollya_obj_t tmp2 = NULL;
  int n, r, res;
  sollya_base_function_t type;

  r = sollya_lib_decompose_function(f, &type, &n, &tmp1, &tmp2, NULL);
  if (!r) { sollya_lib_printf("Not a mathematical function\n"); res = 0; }
  else if (n >= 3) {
    sollya_lib_printf("Unexpected error: %b has more than two arguments.\n", f);
    res = 0;
  }
  else {
    switch (type) {
      case SOLLYA_BASE_FUNC_FREE_VARIABLE: res = 0; break;
      case SOLLYA_BASE_FUNC_PI: res = 1; break;
      case SOLLYA_BASE_FUNC_CONSTANT: res = 1; break;
      case SOLLYA_BASE_FUNC_LIBRARYCONSTANT: res = 1; break;
      default:
        res = is_made_of_constants(tmp1);
        if ((res) && (n==2)) res = is_made_of_constants(tmp2);
    }
  }

  if (tmp1) sollya_lib_clear_obj(tmp1);
  if (tmp2) sollya_lib_clear_obj(tmp2);

  return res;
}

Functions are provided to allow the user to retrieve further information from library function, library constant, procedure function and external procedure objects:

10.13 - Faithfully evaluate a functional expression

Let us suppose that f is a functional expression and a is a numerical value or a constant expression. One of the very convenient features of the interactive tool is that the user can simply write f(a) at the prompt: the tool automatically adapts its internal precision in order to compute a value that is a faithful rounding (at the current tool precision) of the true value f(a). Sometimes it does not achieve to find a faithful rounding, but in any case, if the result is not proved to be exact, a warning is displayed explaining how confident one should be with respect to the returned value. The object a can also be an interval, in which case Sollya automatically performs the evaluation using an enhanced interval arithmetic, e.g., using L'Hopital's rule to produce finite (yet valid of course) enclosures even in cases when f exhibits removable singularities (for instance sin(x)/x over an interval containing 0). This behavior is reproduced in the library with the sollya_lib_apply function (this function is in fact to be used to reproduce any construction of the form obj1(obj2, obj3, ...) within the library; for instance obj1 might also be a procedure. See Section Commands and functions for a more detailed description of this function). More precisely if f and a are two sollya_obj_t representing respectively a univariate function and a constant or an interval, the following call returns a new sollya_obj_t representing the object that would be produced as a result of typing f(a); at the interactive prompt:
b = sollya_lib_apply(f, a, NULL);

However, when using the library, it might be interesting to have access to this feature when the argument a is not a Sollya object but rather directly a multiprecision constant of type mpfr_t or mpfi_t. Also, in this case, one may want to have a finer-grain access to the evaluation algorithm, e.g., to correctly react to cases where a faithful rounding has not been achieved without having to catch warning messages emitted by Sollya. This is the reason why the library proposes the following functions.

To evaluate a unary function at a constant expression or constant value, the library provides the two following functions:

In the former, the argument a is any sollya_obj_t containing a numerical constant or a constant expression, while in the latter a is a constant already stored in a mpfr_t. These functions store the result in res and return a sollya_fp_result_t which is an enum type described in Table List of values defined in type sollya_fp_result_t). In order to understand the role of the cutoff parameter and the value returned by the function, it is necessary to describe the algorithm in a nutshell:

Input: a functional expression f, a constant expression a, a target precision q, a parameter epsilon.
Choose an initial working precision p.
Evaluate a with interval arithmetic, performing the computations at precision p.
Replace the occurrences of the free variable in f by the interval obtained at step 2. Evaluate the resulting expression with interval arithmetic, performing the computations at precision p. This yields an interval I = [x,y].
Examine the following cases successively (RN denotes rounding to nearest at precision q):
  1. If RN(x) = RN(y), set res to that value and return.
  2. If I does not contain any floating-point number at precision q, set res to one of both floating-point numbers enclosing I and return.
  3. If I contains exactly one floating-point number at precision q, set res to that number and return.
  4. If all numbers in I are smaller than epsilon in absolute value, then set res to 0 and return.
  5. If p has already been increased many times, then set res to some value in I and return.
  6. Otherwise, increase p and go back to step 2.

The target precision q is chosen to be the precision of the mpfr_t variable res. The parameter epsilon corresponds to the parameter cutoff. The reason why cutoff is a pointer is that, most of the time, the user may not want to provide it, and using a pointer makes it possible to pass NULL instead. So, if NULL is given, epsilon is set to 0. If cutoff is not NULL, the absolute value of *cutoff is used as value for epsilon. Using a non-zero value for epsilon can be useful when one does not care about the precise value of f(a) whenever its absolute value is below a given threshold. Typically, if one wants to compute the maximum of |f(a1)|, ..., |f(an)|, it is not necessary to spend too much effort on the computation of |f(ai)| if one already knows that it is smaller than epsilon = max {|f(a1)|,...,|f(ai-1)|}.

List of values defined in type sollya_fp_result_t
Value Meaning
SOLLYA_FP_OBJ_NO_FUNCTION f is not a functional expression.
SOLLYA_FP_EXPRESSION_NOT_CONSTANT a is not a constant expression.
SOLLYA_FP_FAILURE The algorithm ended up at step (e) and I contained NaN. This typically happens when a is not in the definition domain of f.
SOLLYA_FP_CUTOFF_IS_NAN cutoff was not NULL and the value of *cutoff is NaN.
SOLLYA_FP_INFINITY The algorithm ended up at step (a) with I of the form [+infinity, +infinity] or [-infinity, -infinity]. Hence f(a) is proved to be an exact infinity.
SOLLYA_FP_PROVEN_EXACT The algorithm ended up at step (a) with a finite value and x = RN(x) = RN(y) = y.
SOLLYA_FP_CORRECTLY_ROUNDED_PROVEN_INEXACT The algorithm ended up at step (b) with a finite value and res < x <= y or x <= y < res.
SOLLYA_FP_CORRECTLY_ROUNDED The algorithm ended up at step (a) with a finite value and x <= res <= y. (Please notice that this means that the algorithm did not manage to conclude whether the result is exact or not. However, it might have been able to conclude if the working precision had been increased.)
SOLLYA_FP_FAITHFUL_PROVEN_INEXACT The algorithm ended up at step (b) with a finite value and res < x <= y or x <= y < res.
SOLLYA_FP_FAITHFUL The algorithm ended up at step (c) with a finite value. (again, the algorithm did not manage to conclude whether the result is exact or not, but it might have been able to conclude with a larger working precision).
SOLLYA_FP_BELOW_CUTOFF The algorithm ended up at step (d).
SOLLYA_FP_NOT_FAITHFUL_ZERO_CONTAINED_BELOW_THRESHOLD The algorithm ended up at step (e) and I was of the form [-delta1, delta2] where 0 < delta1, delta2 << 1 (below some threshold of the algorithm). This typically happens when f(a) exactly equals zero, but the algorithm does not manage to prove this exact equality.
SOLLYA_FP_NOT_FAITHFUL_ZERO_CONTAINED_NOT_BELOW_THRESHOLD The algorithm ended up at step (e) with an interval I containing 0 but too large to fall in the above case. (In general, this should be considered as a case of failure and the value stored in res might be completely irrelevant.)
SOLLYA_FP_NOT_FAITHFUL_ZERO_NOT_CONTAINED The algorithm ended up at step (e) with an interval I that does not contain 0. (Again, this should be considered as a case of failure.)
SOLLYA_FP_NOT_FAITHFUL_INFINITY_CONTAINED The algorithm ended up at step (e) and (at least) one of the bounds of I was infinite. This typically happens when the limit of f(x) when x goes to a is infinite.

To evaluate a unary function on an interval, the following function is provided:
int sollya_lib_evaluate_function_over_interval(mpfi_t res, sollya_obj_t f, mpfi_t a).

This function returns a boolean integer: false means failure (i.e., f is not a functional expression), in which case res is left unchanged, and true means success, in which case res contains the result of the evaluation. The function might succeed, and yet res might contain something useless such as an unbounded interval or even [NaN, NaN] (this happens for instance when a contains points that lie in the interior of the complement of the definition domain of f). It is the user's responsibility to check afterwards whether the computed interval is bounded, unbounded or NaN.

10.14 - Comparing objects structurally and computing hashes on Sollya objects

The library provides function
int sollya_lib_cmp_objs_structurally(sollya_obj_t obj1, sollya_obj_t obj2)
to allow the user to perform a structural comparison of any two Sollya objects. It returns an integer (interpreted as a boolean) that is true if and only if obj1 and obj2 are syntactically the same (as opposed to mathematically). For instance the fractions 2/3 and 4/6 are recognized as mathematically equal by Sollya when compared with == (or sollya_lib_cmp_equal with the library) but are syntactically different.

Certain language bindings require hashes to be available for any object represented. In order to help with such language bindings, the Sollya library supports a function that computes a 64 bit unsigned integer as a hash for a given Sollya object:
uint64_t sollya_lib_hash(sollya_obj_t obj).
The Sollya library guarantees that any two objects that are syntactically equal (as when compared with sollya_lib_cmp_objs_structurally) will have the same hash value. For some particular objects (e.g., polynomials) Sollya can normalize the expression before computing the hash value and in this case two objects that are mathematically equal (even though they are not structurally equal) will have the same hash value. However, except in such particular cases, two objects that are syntactically different are likely to have different hashes (although this is not guaranteed, of course).

Computing the hash of an object takes a time proportional to the size of the directed acyclic graph internally used to represent that object. However, Sollya will cache an object's hash value for further use after it has been computed, so the cost of computing the hash of a given object is paid only once.

The user should also be aware that the hash value for a given object is currently not guaranteed to be portable between platforms nor over consecutive Sollya versions.

10.15 - Executing Sollya procedures

Objects representing procedures written in Sollya language (see also Section Procedures) can be created using the Sollya library functions sollya_lib_parse_string and sollya_lib_parse or through execution of a Sollya script using sollya_lib_execute.

In order to execute such procedure objects on arguments, available as Sollya objects, too, the functions

may be used. These functions apply the given procedure proc on the following arguments (or the elements in the argument list arglist). If no argument is needed to execute the procedure, the variadic argument list shall immediately be terminated using NULL; otherwise the argument list shall be terminated with an extra NULL argument. An arity test is performed by Sollya before the procedure is executed: if the arity of the given procedure does not correspond to the actual number of given arguments (and the Sollya procedure is not variadic), an error object is returned instead of the procedure's result.

When the functions are used to execute procedures that return a Sollya object, the object is returned by the function. When the procedure does not use the Sollya return statement or returns the Sollya void object, a Sollya void object is returned. The user should not forget to deallocate that void object.

10.16 - Name of the free variable

The default name for the free variable is the same in the library and in the interactive tool: it is _x_. In the interactive tool, this name is automatically changed at the first use of an undefined symbol. Accordingly in library mode, if an object is defined by sollya_lib_parse_string with an expression containing an undefined symbol, that symbol will become the free variable name if it has not already been changed before. But what if one does not use sollya_lib_parse_string (because it is not efficient) but one wants to change the name of the free variable? The name can be changed with sollya_lib_name_free_variable("some_name").

It is possible to get the current name of the free variable with sollya_lib_get_free_variable_name(). This function returns a char * containing the current name of the free variable. Please note that this char * is dynamically allocated on the heap and should be cleared after its use with sollya_lib_free() (see below).

10.17 - Commands and functions

Besides some exceptions, every command and every function available in the Sollya interactive tool has its equivalent (with a very close syntax) in the library. Section List of available commands of the present documentation gives the library syntax as well as the interactive tool syntax of each commands and functions. The same information is available within the interactive tool by typing help some_command. So if one knows the name of a command or function in the interactive tool, it is easy to recover its library name and signature.

There are some commands and functions available in interactive mode which, for syntactical reasons, have a different function name in the Sollya library:

A particular point is worth mentioning: some functions of the tool such as remez for instance have a variable number of arguments. For instance, one might call remez(exp(x), 4, [0,1]) or remez(1, 4, [0,1], 1/exp(x)). This feature is rendered in the C library by the use of variadic functions (functions with an arbitrary number of arguments), as they are permitted by the C standard. The notable difference is that there must always be an explicit NULL argument at the end of the function call. Hence one can write sollya_lib_remez(a, b, c, NULL) or sollya_lib_remez(a, b, c, d, NULL). It is very easy to forget the NULL argument and to use for instance sollya_lib_remez(a, b, c). This is completely wrong because the memory will be read until a NULL pointer is found. In the best case, this will lead to an error or a result obviously wrong, but it could also lead to subtle, not-easy-to-debug errors. The user is advised to be particularly careful with respect to this point.

Each command or function accepting a variable number of arguments comes in a sollya_lib_v_ version accepting a va_list parameter containing the list of optional arguments. For instance, one might write a function that takes as arguments a function f, an interval I, optionally a weight function w, optionally a quality parameter q. That function would display the minimax obtained when approximating f over I (possibly with weight w and quality q) by polynomials of degree n=2 to 20. So, that function would get a variable number of arguments (i.e., a va_list in fact) and pass them straight to remez. In that case, one needs to use the v_remez version, as the following code shows:

#include <sollya.h>
#include <stdarg.h>

/* Note: we suppose that the library has already been initialized */
void my_function(sollya_obj_t f, sollya_obj_t I, ...) {
  sollya_obj_t n, res;
  int i;
  va_list va;

  for(i=2;i<=20;i++) {
    n = SOLLYA_CONST(i);
    va_start(va, I);
    res = sollya_lib_v_remez(f, n, I, va);
    sollya_lib_printf("Approximation of degree %b is %b\n", n, res);
    va_end(va);
    sollya_lib_clear_obj(n);
    sollya_lib_clear_obj(res);
  }

  return;
}

10.18 - Warning messages in library mode

10.18.1 - Catching warning messages

The philosophy of Sollya is “whenever something is not exact, explicitly warn about that”. This is a nice feature since this ensures that the user always perfectly knows the degree of confidence they can have in a result (is it exact? or only faithful? or even purely numerical, without any warranty?) However, it is sometimes desirable to hide some (or all) of these messages. This is especially true in library mode where messages coming from Sollya are intermingled with the messages of the main program. The library hence provides a specific mechanism to catch all messages emitted by the Sollya core and handle each of them specifically: installation of a callback for messages.

Before describing the principle of the message callback, it seems appropriate to recall that several mechanisms are available in the interactive tool to filter the messages emitted by Sollya. These mechanisms are also available in library mode for completeness. When a message is emitted, it has two characteristics: a verbosity level and an id (a number uniquely identifying the message). After it has been emitted, it passes through the following steps where it can be filtered. If it has not been filtered (and only in this case) it is displayed.

  1. If the verbosity level of the message is greater than the value of the environment variable verbosity, it is filtered.
  2. If the environment variable roundingwarnings is set to off and if the message informs the user that a rounding occurred, it is filtered.
  3. If the id of the message has been registered with the suppressmessage command, the message is filtered.
  4. If a message callback has been installed and if the message has not been previously filtered, it is handled by the callback, which decides to filter it or to permit its displaying.

A message callback is a function of the form int my_callback(sollya_msg_t msg, void *data). It receives as input an object representing the message and a user-defined pointer. It performs whatever treatment seems appropriate and returns an integer interpreted as a boolean. If the returned value is false, the message is not displayed. If, on the contrary, the returned value is true, the message is displayed as usual. By default, no callback is installed and all messages are displayed. To install a callback, use sollya_lib_install_msg_callback(my_callback, data). The (void *) pointer data is arbitrary (it can be NULL) and is simply transmitted as second argument at each call of the callback. It can be used, e.g., to point to a segment of memory where some information should be stored from a call of the callback to another.

Please remember that, if a message is filtered because of one of the three other mechanisms, it will never be transmitted to the callback. Hence, in library mode, if one wants to catch every single message through the callback, one should set the value of verbosity to MAX_INT, set roundingwarnings to on (this is the default anyway) and one should not use the suppressmessage mechanism.

It is possible to come back to the default behavior, using sollya_lib_uninstall_msg_callback(). Please notice that callbacks do not stack over each other: i.e., if some callback callback1 is installed, and if one installs another one callback2, then the effect of sollya_lib_uninstall_msg_callback() is to come back to the default behavior, and not to come back to callback callback1.

Both sollya_lib_install_msg_callback and sollya_lib_uninstall_msg_callback return an integer interpreted as a boolean: false means failure and true means success.

It is possible to get the currently installed callback using sollya_lib_get_msg_callback(cb_ptr, data_ptr). This stores the current callback at the address referred to by cb_ptr (the type of cb_ptr is hence int (**)(sollya_msg_t, void *)) and stores the current data pointer at the address referred to by data_ptr (which has hence (void **) type). The arguments cb_ptr and data_ptr can be NULL in which case the corresponding argument is not retrieved (please take care of the difference between data_ptr being NULL and data_ptr pointing to a (void *) pointer which value is NULL). If no callback is currently installed, the NULL value is stored at the addresses referred to by cb_ptr and data_ptr.

The type sollya_msg_t is indeed a pointer and its content is only accessible during the callback call: it does not make sense to keep it for further use after the callback call. Currently the type has only two accessors:

In the future, other accessors could be added (to get the verbosity level at which the message has been emitted, to get data associated with the message, etc.) The developers of Sollya are open to suggestions and feature requests on this subject.

As an illustration let us give a few examples of possible use of callbacks:

Example 1: A callback that filters everything.

int hide_everything(sollya_msg_t msg, void *data) {
  return 0;
}

Example 2: filter everything but the messages indicating that a comparison is uncertain.

int keep_comparison_warnings(sollya_msg_t msg, void *data) {
  switch(sollya_lib_get_msg_id(msg)) {
    case SOLLYA_MSG_TEST_RELIES_ON_FP_RESULT_THAT_IS_NOT_FAITHFUL:
    case SOLLYA_MSG_TEST_RELIES_ON_FP_RESULT:
    case SOLLYA_MSG_TEST_RELIES_ON_FP_RESULT_FAITHFUL_BUT_UNDECIDED:
    case SOLLYA_MSG_TEST_RELIES_ON_FP_RESULT_FAITHFUL_BUT_NOT_REAL:
      return 1;
    default:
      return 0;
  }
}

Example 3: ensuring perfect silence for a particular function call (uses the callback defined in Example 1).

...
int (*old_callback)(sollya_msg_t, void *);
void *old_data;
sollya_lib_get_msg_callback(&old_callback, &old_data);
sollya_lib_install_msg_callback(hide_everything, NULL);
  /* Here takes place the function call that must be completely silent */
if (old_callback) sollya_lib_install_msg_callback(old_callback, old_data);
...

Example 4: using the (void *) data argument to store information from a call to another.

int set_flag_on_problem(sollya_msg_t msg, void *data) {
  switch(sollya_lib_get_msg_id(msg)) {
    case SOLLYA_MSG_DOUBLE_ROUNDING_ON_CONVERSION:
      *((int *)(data)) = 1;
  }
  return 1;
}

...

int main() {
  int flag_double_rounding = 0;
  ...
  sollya_lib_init();
  sollya_lib_install_msg_callback(set_flag_on_problem, &flag_double_rounding);
  ...
}

More involved examples are possible: for instance, instead of setting a flag, it is possible to keep in some variable what the last message was. One may even implement a stack mechanism and store the messages in a stack, in order to handle them later. (Please remember however that sollya_msg_t is a pointer type and that the sollya_msg_t object received as argument of a callback call has no more meaning once the callback call returned. If a stack mechanism is implemented it should store information such as the message ID, or the message text, as given by sollya_lib_get_msg_id and sollya_lib_msg_to_text, but not the sollya_msg_t object itself.)

10.18.2 - Emitting warning messages

The Sollya library offers a way to print a message, as if it were produced by the Sollya core. Such a message will go through the entire process described in the previous section, and can eventually provoke a callback call if a callback is installed. The function supporting this feature is
void sollya_lib_printlibrarymessage(int verb, const char *str).
The first argument verb is the least verbosity level at which that warning shall be displayed. The second argument str is the message to be displayed.

When a message is produced with this function, its message ID (when caught by a callback) is SOLLYA_MSG_GENERIC_SOLLYA_LIBRARY_MSG. An important notice is that the character string returned by sollya_lib_msg_to_text when such a message is caught by a callback is currently not the argument str provided to sollya_lib_printlibrarymessage, but is instead a generic message. This behavior might change in the future.

10.19 - Using Sollya in a program that has its own allocation functions

Sollya uses its own allocation functions: as a consequence, pointers that have been allocated by Sollya functions must be freed using sollya_lib_free instead of the usual free function. Another consequence is that Sollya registers its own allocation functions to the GMP library, using the mechanism provided by GMP, so that GMP also uses Sollya allocation functions behind the scene, when the user performs a call to, e.g., mpz_init, mpfr_init2, etc.

In general, this is completely harmless and the user might even not notice it. However, this is a problem if Sollya is used in a program that also uses its own allocation functions and that has already registered these functions to GMP. Actually:

In order to solve this issue, Sollya provides a chaining mechanism that we are now going to describe. The idea is the following: suppose that the main program should use a function custom_malloc. The user should not use mp_set_memory_functions as usual, but should instead initialize Sollya with the initializing function described above. This will cause Sollya to register an allocation function sollya_lib_malloc to GMP. This function overloads custom_malloc: when called, it uses custom_malloc to perform the actual allocation and does nothing else but some internal accounting and verification for that allocation. To repeat, the actual allocation is done by custom_malloc; hence from the point of view of the user, the mechanism is completely transparent and equivalent to directly registering custom_malloc to GMP. The same holds for all other allocation functions: in particular, this is true for free as well: if a function custom_free is given at the initialization of Sollya, then the function sollya_lib_free eventually uses custom_free to free the memory.

The initialization function providing this mechanism is:
int sollya_lib_init_with_custom_memory_functions(
         void *(*custom_malloc)(size_t),
         void *(*custom_calloc)(size_t, size_t),
         void *(*custom_realloc)(void *, size_t),
         void (*custom_free)(void *),
         void *(*custom_realloc_with_size)(void *, size_t, size_t),
         void (*custom_free_with_size)(void *, size_t)).
None of the arguments is mandatory: if the user does not want to provide an argument, they may use NULL as a placeholder for that argument. In that case, the corresponding Sollya default function will be used. Indeed, the default initializing function sollya_lib_init() is just an alias to sollya_lib_init_with_custom_memory_functions(NULL, NULL, NULL, NULL, NULL, NULL).

Please notice, that if custom_malloc is provided, then the function sollya_lib_malloc will be defined as an overloaded version of custom_malloc. Hence, custom_malloc will eventually be used for all the allocations performed by Sollya (including the allocation of memory for its own purpose). This is true also for custom_calloc, custom_realloc and custom_free. However, this is not the case for custom_realloc_with_size and custom_free_with_size: these functions are only required for the registration to GMP and are not used by Sollya itself (except of course when Sollya allocates function through a call to a GMP, MPFR or MPFI function). Thus, to sum up:

Of course, even if the user registers custom_malloc, custom_free, etc., at the initialization of Sollya, they stay free to use them for their own allocation needs: only allocations performed by GMP (and consequently MPFR and MPFI) and allocations performed by Sollya have to use the chaining mechanism. However, for the convenience of the user, the library also provides access to the allocation functions of Sollya. They are the following:

No access to the overloaded version of custom_realloc_with_size and custom_free_with_size is provided, but if the user really wants to retrieve them, they can do it with mp_get_memory_functions since they are registered to GMP.