## Warning messages during parsing

### Warning: renaming identifier 'foo' as 'bar'...

When a definition `foo = expr`

is given to Gappa, the name
`foo`

is associated to the expression `expr`

. This name
is then used whenever Gappa outputs `expr`

. If another definition
`bar = expr`

is later provided, the new name supersedes the name
given previously.

a = 42;
b = 42;
{ a - b in ? }

Warning: renaming identifier 'a' as 'b' at line 2 column 7
b - b in [0, 0]

### Warning: although present in a quotient, the expression foo may not
have been tested for non-zeroness.

When Gappa verifies that both sides of a user rewriting rule are
equivalent, it does not generate additional constraints to verify that
denominators appearing in the expressions are not zero. For example, the rule
`1 / (1 / x) -> x`

only applies when `x`

is not zero;
yet Gappa does not test for it.

No warning messages are displayed when constraints are added to the
rewriting rule (whether these constraints are sufficient or not).
E.g. `1 / (1/ x) -> x { x <> 0 }`

.

Option switch: `-W[no-]null-denominator`

.

### Warning: foo and bar are not trivially equal.

When Gappa verifies the rule `foo -> bar`

, it first
performs the subtraction of both sides. Then it normalizes this expression in
the field of polynomial fractions with integer coefficients. If this result is
not zero, Gappa warns about it.

As the normalization only deals with polynomials and integers, false
positive may appear when the expressions involve numerical values or square
roots or absolute values.

{ 1 in ? }
x * (y - 2) -> x * y - x; # not equal
1b-2 -> 0.2 + 0.05; # equal, but needs numerical computations
sqrt(x * x) -> |x|; # equal, but involves square root and absolute value

Warning: x * (y - 2) and x * y - x are not trivially equal.
Difference: -(x)
Warning: 1b-2 and 2e-1 + 5e-2 are not trivially equal.
Difference: -(2e-1) - (5e-2) + (1b-2)
Warning: sqrt(x * x) and |x| are not trivially equal.
Difference: (sqrt(x * x)) - (|x|)
Results:
1 in [1, 1]

Option switch: `-W[no-]hint-difference`

.

### Warning: bar is a variable without definition, yet it is unbound.

Identifier `bar`

neither represents an expression nor
is it a sub-term of any of the bounded expressions of the logical property.
This may mean an identifier was mistyped.

{ x - x in ? }

Warning: x is a variable without definition, yet it is unbound.

Option switch: `-W[no-]unbound-variable`

.

### Warning: no path was found for foo.

The expression `foo`

appears in one of the goals, yet Gappa
does not have any theorem that could be used to compute this expression or one
of its sub-terms.