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
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
\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}, @NaN@ and [@NaN@, @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@, [@NaN, @NaN@] and \textbf{error} share the property that they
compare not equal to anything, including themselves. This means if a variable
\emph{a} contains @NaN@, [@NaN, @NaN@] or \textbf{error} and whatever the content of
variable \emph{b} is, the test \emph{a} \textbf{$==$} \emph{b} returns \textbf{false}. The traditional way of
testing if \emph{a} contains @NaN@, [@NaN@, @NaN@] or \textbf{error} is indeed to check if
\emph{a} \textbf{$==$} \emph{a} returns false. \textbf{error} can be distinguished from @NaN@ and
[@NaN@, @NaN@] using the \textbf{!$=$} 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 \textbf{error}
and are able to distinguish between all of these.
\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@;
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@]
\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})
|
