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.