1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
\subsection{$==$}
\label{labequal}
\noindent Name: \textbf{$==$}\\
\phantom{aaa}equality test operator\\[0.2cm]
\noindent Library name:\\
\verb| sollya_obj_t sollya_lib_cmp_equal(sollya_obj_t, sollya_obj_t)|\\[0.2cm]
\noindent Usage:
\begin{center}
\emph{expr1} \textbf{$==$} \emph{expr2} : (\textsf{any type}, \textsf{any type}) $\rightarrow$ \textsf{boolean}\\
\end{center}
Parameters:
\begin{itemize}
\item \emph{expr1} and \emph{expr2} represent expressions
\end{itemize}
\noindent Description: \begin{itemize}
\item The test \emph{expr1} \textbf{$==$} \emph{expr2} returns \textbf{true} when \emph{expr1} and \emph{expr2} are
syntactically equal and different from \textbf{error} and @NaN@. Conversely if \emph{expr1}
and \emph{expr2} are objects that are mathematically different and \sollya manages
to figure it out, the test returns \textbf{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 \textbf{true}, without a warning. In the case when \emph{expr1} and \emph{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 \textbf{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 \textbf{false}.
\item The level of simplifications performed by \sollya to determine if
expressions are mathematically equal depends on the value of \textbf{autosimplify}.
If it is \textbf{off}, no formal simplification is performed, hence expression trees
as simple as x+1 and 1+x will be considered not equal. Conversely, if
\textbf{autosimplify} is set to \textbf{on}, polynomial subexpressions that are mathematically
equal will in general be recognized as being equal.
\item 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
\textbf{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 \textbf{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).
\item Notice that @NaN@ and \textbf{error} share the property that they both compare equal
and different to anything, i.e., if the variable \emph{a} contains @NaN@ or \textbf{error}
and whatever the content of variable \emph{b} is, the tests \emph{a} \textbf{$==$} \emph{b} and
\emph{a} \textbf{!$=$} \emph{b} both return \textbf{false}. The standard way of testing if \emph{a} contains
@NaN@ or \textbf{error} is indeed to check if \emph{a} \textbf{$==$} \emph{a} returns false. In such a
case, it is however impossible to determine what is the actual value of \emph{a}
amongst both possibilities using only \textbf{$==$} or \textbf{!$=$}. The standard way to
discriminate this situation is to use the match ... with ... construct.
\end{itemize}
\noindent Example 1:
\begin{center}\begin{minipage}{15cm}\begin{Verbatim}[frame=single]
> "Hello" == "Hello";
true
> "Hello" == "Salut";
false
> "Hello" == 5;
false
> 5 + x == 5 + x;
true
\end{Verbatim}
\end{minipage}\end{center}
\noindent Example 2:
\begin{center}\begin{minipage}{15cm}\begin{Verbatim}[frame=single]
> 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 considere
d to be equal.
true
> exp(5) == log(4);
false
\end{Verbatim}
\end{minipage}\end{center}
\noindent Example 3:
\begin{center}\begin{minipage}{15cm}\begin{Verbatim}[frame=single]
> 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
\end{Verbatim}
\end{minipage}\end{center}
\noindent Example 4:
\begin{center}\begin{minipage}{15cm}\begin{Verbatim}[frame=single]
> 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-po
int with 12 bits.
If safe computation is needed, try to increase the precision.
Warning: Rounding occurred when converting the constant "16385.1" to floating-po
int 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
\end{Verbatim}
\end{minipage}\end{center}
\noindent Example 5:
\begin{center}\begin{minipage}{15cm}\begin{Verbatim}[frame=single]
> error == error;
false
> error != error;
false
> @NaN@ == @NaN@;
false
> @NaN@ != @NaN@;
false
> error == @NaN@;
false
> error != @NaN@;
false
> a = error;
> match a with
@NaN@ : ("a contains @NaN@")
default:("a contains something else");
error
> a = @NaN@;
> match a with
@NaN@ : ("a contains @NaN@")
default:("a contains something else");
a contains @NaN@
\end{Verbatim}
\end{minipage}\end{center}
See also: \textbf{!$=$} (\ref{labneq}), \textbf{$>$} (\ref{labgt}), \textbf{$>=$} (\ref{labge}), \textbf{$<=$} (\ref{lable}), \textbf{$<$} (\ref{lablt}), \textbf{in} (\ref{labin}), \textbf{!} (\ref{labnot}), \textbf{$\&\&$} (\ref{laband}), \textbf{$||$} (\ref{labor}), \textbf{error} (\ref{laberror}), \textbf{prec} (\ref{labprec}), \textbf{autosimplify} (\ref{labautosimplify})
|
