Gappa rewrites expressions by matching them with well-known patterns. The enclosure of an unmatchable expression will necessarily have to be computed through interval arithmetic. As a consequence, to ensure that the expressions will benefit from as much rewriting as possible, special care needs to be taken when expressing the computational errors.

Let `exact`

be an arithmetic expression and `approx`

an approximation of `exact`

. The approximation usually contains
rounding operators while the exact expression does not. The absolute error
between these two expressions is their difference: `approx - exact`

.

Writing the errors differently will prevent Gappa from applying
theorems on rounding errors: `-(x - rnd(x))`

may lead to a
worse enclosure than `rnd(x) - x`

.

The situation is similar for the relative error. It should be
expressed as the quotient between the absolute error and the exact value:
`(approx - exact) / exact`

. For enclosures of relative errors,
this is the same: `approx -/ exact`

.

The `approx`

and `exact`

expressions need to have
a similar structure in order for the rewriting rules to kick in. E.g., if
`exact`

is a sum of two terms `a`

and `b`

,
then `approx`

has to be the sum of two terms `c`

and
`d`

such that `c`

and `d`

are approximations
of `a`

and `b`

respectively.

Indeed the rewriting rule for the absolute error of the addition is:
`(a + b) - (c + d) -> (a - c) + (b - d)`

. Similarly, the
rewriting rules for the multiplication keep the same ordering of sub-terms.
For example, one of the rules is:
`a * b - c * d -> (a - c) * b + c * (b - d)`

. Therefore,
one should try not to mess with the structure of expressions.

If the two sides of an error expression happen to not have a
similar structure, then a user rewriting rule has to be added in order to
put them in a suitable state. For instance, let us assume we are
interested in the absolute error between `a`

and
`d`

, but they have dissimilar structures. Yet there are two
expressions `b`

and `c`

that are equal and with
structures similar to `a`

for `b`

and
`d`

for `c`

. Then we just have to add the following
hints to help Gappa:

b - c -> 0; # or "b-c in [0,0]" as a hypothesis a ~ b; # a is an approximation of b c ~ d; # c is an approximation of d

When an expression is known to take a few separate values that are
not equally distributed, a disjunction is the simplest solution but it
can be avoided if needed. For instance, if `x`

can only be 0,
2, or 17, one can write:

x = i * (19b-1 * i - 15b-1); { @FIX(i, 0) /\ i in [-1,1] -> ... } $ i in 3; # this dichotomy hint helps Gappa to understand that i is either -1, 0, or 1

When the goal of a formula contains a disjunction, one of the sides of this disjunction has to always hold with respect to the set of hypotheses. This is especially important when performing dichotomies. Even if Gappa is able to prove the formula in each particular branch of a dichotomy, if a different property of the disjunction is used each time, the tool will fail to prove the formula in the general case. Note that, whenever a contradiction is found for a specific set of hypotheses, whichever side of the disjunction holds no longer matter, since Gappa can infer any of them.