Description:

• The test expr1 == expr2 returns true when expr1 and expr2 are syntactically equal and different from error and @NaN@. Conversely if expr1 and expr2 are objects that are mathematically different and Sollya manages to figure it out, the test returns false. In between these two cases, there is the grey zone of expressions that are not syntactically equal but are mathematically equal. In such a case, Sollya normally tries to determine if the expressions are mathematically equal and if it manages to prove it, it returns true, without a warning. In the case when expr1 and expr2 are two constant expressions, Sollya will in particular try to evaluate their difference: in the case when the difference is 0 or is so small that Sollya does not manage to obtain a faithful rounding of the real value, it will return true (with a warning if it has not been possible to actually prove that the real value is 0). In any other case, when both expressions are not syntactically equal and Sollya has not been able to prove that they are mathematically equal, it returns false.
• The level of simplifications performed by Sollya to determine if expressions are mathematically equal depends on the value of autosimplify. If it is off, no formal simplification is performed, hence expression trees as simple as x+1 and 1+x will be considered not equal. Conversely, if autosimplify is set to on, polynomial subexpressions that are mathematically equal will in general be recognized as being equal.
• The user should always keep in mind that a litteral constant written in decimal arithmetic (such as 0.1 for instance) is not considered as an exact constant by Sollya (unless it is exactly representable in binary without requiring too much precision) and is first correctly rounded at precision prec, prior to any other operation. Of course, this leads to a rounding warning, but it is important to remember that this is done before the expression trees are compared, possibly leading to two expressions comparing equal, while they are obviously mathematically different, just because they contain different constants that have been rounded to the same value at precision prec. As a general rule, to avoid this behavior, the user should represent constants in an exact format such as hexadecimal or represent decimal constants as integer fractions (e.g., 0.1 represented by the constant expression 1/10).
• Notice that @NaN@ and error share the property that they both compare equal and different to anything, i.e., if the variable a contains @NaN@ or error and whatever the content of variable b is, the tests a == b and a != b both return false. The standard way of testing if a contains @NaN@ or error is indeed to check if a == a returns false. In such a case, it is however impossible to determine what is the actual value of a amongst both possibilities using only == or !=. The standard way to discriminate this situation is to use the match ... with ... construct.