# Supported arithmetic¶

## Rounding directions¶

Some of the classes of operators presented in the following sections are templated by a rounding direction. This is the direction chosen when converting a real number that cannot be exactly represented in the destination format.

There are eleven directions:

zr
toward zero
aw
away from zero
dn
toward minus infinity (down)
up
toward plus infinity
od
to odd mantissas
ne
to nearest, tie breaking to even mantissas
no
to nearest, tie breaking to odd mantissas
nz
to nearest, tie breaking toward zero
na
to nearest, tie breaking away from zero
nd
to nearest, tie breaking toward minus infinity
nu
to nearest, tie breaking toward plus infinity

The rounding directions mandated by the IEEE-754 standard are ne (default mode, rounding to nearest), zr, dn, up, and na (introduced for decimal arithmetic).

## Floating-point operators¶

This class of operators covers all the formats whose number sets are $$F(p,d) = \{m \cdot 2^e; |m| < 2^p, e \ge d\}$$. In particular, IEEE-754 floating-point formats (with subnormal numbers) are part of this class, if we set apart overflow issues. Both parameters p and d select a particular format. The last parameter selects the rounding direction.

float< precision, minimum_exponent, rounding_direction >(...)


Formats with no minimal exponent (and thus no underflow) are also available:

float< precision, rounding_direction >(...)


Having to remember the precision and minimum exponent parameters may be a bit tedious, so an alternate syntax is provided: instead of these two parameters, a name can be given to the float class.

float< name, rounding_direction >(...)


There are four predefined formats:

ieee_32
IEEE-754 single precision
ieee_64
IEEE-754 double precision
ieee_128
x86_80
extended precision on x86-like processors

## Fixed-point operators¶

This class of operators covers all the formats whose number sets are $$F(e) = \{m \cdot 2^e\}$$. The first parameter selects the weight of the least significant bit. The second parameter selects the rounding direction.

fixed< lsb_weight, rounding_direction >(...)


Rounding to integer is a special case of fixed point rounding of weight 0. A syntactic shortcut is provided.

int< rounding_direction >(...)


## Miscellaneous operators¶

The following operators are underspecified and therefore not suitable for formal proofs.

### Functions with relative error¶

This set of functions is defined with related theorems on relative error. They can be used to express properties that cannot be directly expressed through unary rounding operators.

{add|sub|mul}_rel< precision [, minimum_exponent] >(..., ...)


If the minimum exponent is not provided, the bound on the relative error is assumed to be valid on the entire domain. Otherwise the interval $$[-2^e,2^e]$$ is excluded from the domain.

Talking about the expression add_rel<20,-60>(a,b) is like talking about a fresh expression c such that not |a + b| <= 1b-60 -> |c -/ (a + b)| <= 1b-20.

To be written.