Sollya User's Manual

Name:

== equality test operator

Library name:

sollya_obj_t sollya_lib_cmp_equal(sollya_obj_t, sollya_obj_t)

Usage:

expr1 == expr2 : (any type, any type) -> boolean

Parameters:

expr1 and expr2 represent expressions

Description:

The test expr1 == expr2 returns true when expr1 and expr2 are syntactically equal and different from error, @NaN@ and [@NaN@, @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@, [@NaN, @NaN@] and error share the property that they compare not equal to anything, including themselves. This means if a variable a contains @NaN@, [@NaN, @NaN@] or error and whatever the content of variable b is, the test a == b returns false. The traditional way of testing if a contains @NaN@, [@NaN@, @NaN@] or error is indeed to check if a == a returns false. error can be distinguished from @NaN@ and [@NaN@, @NaN@] using the != operator. In order to distinguish @NaN@ from [@NaN@, @NaN@], a match ... with ... construct must be used. In general, match ... with ... constructs work on all of @NaN@, [@NaN, @NaN@] and error and are able to distinguish between all of these.

Example 1:

   > "Hello" == "Hello";
   true
   > "Hello" == "Salut";
   false
   > "Hello" == 5;
   false
   > 5 + x == 5 + x;
   true

Example 2:

   > verbosity = 1!;
   > asin(1) * 2 == pi;
   true
   > cos(3)^2 == 1 - sin(3)^2;
   Warning: the tool is unable to decide an equality test by evaluation even though faithful evaluation of the terms has been possible. The terms will be considered to be equal.
   true
   > exp(5) == log(4);
   false

Example 3:

   > autosimplify=off;
   Automatic pure tree simplification has been deactivated.
   > exp(1+x) == exp(x+1);
   false
   > autosimplify=on;
   Automatic pure tree simplification has been activated.
   > exp(1+x) == exp(x+1);
   false
   > (1/3+x)^2 == x^2 + 1/9 + (5-3)*x/3;
   true
   > log(x)/log(10) == log10(x);
   false

Example 4:

   > prec = 12;
   The precision has been set to 12 bits.
   > verbosity = 1!;
   > 16384.1 == 16385.1;
   Warning: Rounding occurred when converting the constant "16384.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   Warning: Rounding occurred when converting the constant "16385.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   true
   > 16384 == 16384.25;
   false
   > 0.1 == 1/10;
   Warning: Rounding occurred when converting the constant "0.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   false
   > 0.1 == round(1/10, prec, RN);
   Warning: Rounding occurred when converting the constant "0.1" to floating-point with 12 bits.
   If safe computation is needed, try to increase the precision.
   true

Example 5:

   > error == error;
   false
   > error != error;
   false
   > @NaN@ == @NaN@;
   false
   > @NaN@ != @NaN@;
   true
   > [@NaN@,@NaN@] == [@NaN@,@NaN@];
   false
   > [@NaN@,@NaN@] != [@NaN@,@NaN@];
   true
   > error == @NaN@;
   false
   > error != @NaN@;
   false
   > a = error;
   > match a with
     @NaN@ : ("a contains @NaN@")
     [@NaN@, @NaN@] : ("a contains [@NaN@, @NaN@]")
     default:("a contains something else");
   a contains something else
   > a = @NaN@;
   > match a with
     @NaN@ : ("a contains @NaN@")
     [@NaN@, @NaN@] : ("a contains [@NaN@, @NaN@]")
     default:("a contains something else");
   a contains @NaN@
   > a = [@NaN@, @NaN@];
   > match a with
     @NaN@ : ("a contains @NaN@")
     [@NaN@, @NaN@] : ("a contains [@NaN@, @NaN@]")
     default:("a contains something else");
   a contains [@NaN@, @NaN@]

See also: !=, >, >=, <=, <, in, !, &&, ||, error, prec, autosimplify

Go back to the list of commands