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
|
Customizing Gappa
=================
These sections explain how rounding operators and back-ends are defined
in the tool. They are meant for developers rather than users of Gappa and
involve manipulating C++ classes defined in the :file:`src/arithmetic`
and :file:`src/backends` directories.
Defining a generator for a new formal system
--------------------------------------------
To be written.
Defining rounding operators for a new arithmetic
------------------------------------------------
Function classes
~~~~~~~~~~~~~~~~
A rounding operator derives from the ``function_class`` class. This class is an
interface to the name of the function, its associated real operator, and
twelve theorems.
.. code-block:: cpp
struct function_class
{
function_class(int mask);
virtual interval round (interval const &, std::string &) const;
virtual interval enforce (interval const &, std::string &) const;
virtual interval absolute_error (std::string &) const;
virtual interval relative_error (std::string &) const;
virtual interval absolute_error_from_exact_bnd (interval const &, std::string &) const;
virtual interval absolute_error_from_exact_abs (interval const &, std::string &) const;
virtual interval absolute_error_from_approx_bnd(interval const &, std::string &) const;
virtual interval absolute_error_from_approx_abs(interval const &, std::string &) const;
virtual interval relative_error_from_exact_bnd (interval const &, std::string &) const;
virtual interval relative_error_from_exact_abs (interval const &, std::string &) const;
virtual interval relative_error_from_approx_bnd(interval const &, std::string &) const;
virtual interval relative_error_from_approx_abs(interval const &, std::string &) const;
virtual std::string description() const = 0;
virtual std::string pretty_name() const = 0;
virtual ~function_class();
};
The ``description`` method should return the internal name of the
rounding operator. It will be used when generating the notations of the
proof. When the generated notation cannot be reduced to a simple name,
comma-separated additional parameters can be appended. The back-end will
take care of formatting the final string. This remark also applies to
names returned by the theorem methods (see below). The ``pretty_name``
method should return a name that can be used in messages displayed to the
user. Ideally, this string can be reused in an input script.
All the methods representing theorems have a similar specification. If
the result is the undefined interval ``interval()``, the theorem was
unsuccessful. Otherwise, the last argument is updated with the name of the
theorem that was used for computing the returned interval. The proof
generator will then generate an internal node from the two intervals and
the name.
When defining a new rounding operator, overloading does not
have to be comprehensive; some methods may be skipped and the engine
will work around the missing theorems. For performance reasons,
it is better for the proof engine to ignore theorems that can never
return a useful range. That is the role of the ``mask`` argument of the
constructor of ``function_class``. It is a combination of the following
flags, which indicate which theorems are supported.
.. code-block:: cpp
struct function_class
{
static const int TH_RND, TH_ENF, TH_ABS, TH_REL,
TH_ABS_EXA_BND, TH_ABS_EXA_ABS, TH_ABS_APX_BND, TH_ABS_APX_ABS,
TH_REL_EXA_BND, TH_REL_EXA_ABS, TH_REL_APX_BND, TH_REL_APX_ABS;
};
In the following, :math:`f` denotes the rounding operator. The range
of an absolute value actually denotes the interval of an ``ABS``
property, while the range of a fraction actually denotes the interval
of ``REL`` property.
``round``
Given the range of :math:`x`, compute the range of :math:`f(x)`.
``enforce``
Given the range of :math:`f(x)`, compute a stricter range of it.
``absolute_error``
Given no range, compute the range of :math:`f(x) - x`.
``relative_error``
Given no range, compute the range of :math:`\frac{f(x) - x}{x}`.
``absolute_error_from_exact_bnd``
Given the range of :math:`x`, compute the range of :math:`f(x) - x`.
``absolute_error_from_exact_abs``
Given the range of :math:`|x|`, compute the range of :math:`f(x) - x`.
``absolute_error_from_approx_bnd``
Given the range of :math:`f(x)`, compute the range of :math:`f(x) - x`.
``absolute_error_from_approx_abs``
Given the range of :math:`|f(x)|`, compute the range of :math:`f(x) - x`.
``relative_error_from_exact_bnd``
Given the range of :math:`x`, compute the range of :math:`\frac{f(x) - x}{x}`.
``relative_error_from_exact_abs``
Given the range of :math:`|x|`, compute the range of :math:`\frac{f(x) - x}{x}`.
``relative_error_from_approx_bnd``
Given the range of :math:`f(x)`, compute the range of :math:`\frac{f(x) - x}{x}`.
``relative_error_from_approx_abs``
Given the range of :math:`|f(x)|`, compute the range of :math:`\frac{f(x) - x}{x}`.
The ``enforce`` theorem is meant to trim the bounds of a range. For
example, if the bounded expression is an integer between 1.7 and 3.5, then it
is also a real number between 2 and 3. This property is especially
useful when performing a dichotomy, since some of the smaller
intervals may be reduced to a single exact value through this theorem.
Since the undefined interval means that a theorem failed, it
cannot be used by ``enforce`` to flag an empty interval in case of
a contradiction. The method should instead return an interval that does
not intersect the initial interval. Moreover, for the sake of formal verification,
the interval should lie in the outward-rounded enclosure of
the original interval. For example, if the expression is an integer
between 1.3 and 1.7, then the method should return an interval contained
in :math:`[1,1.3)` or :math:`(1.7,2]`. For practical
reasons, :math:`[1,1]` and :math:`[2,2]` are the most interesting
answers.
Function generators
~~~~~~~~~~~~~~~~~~~
Because rounding operators can be parameterized, they have to be
generated by the parser on the fly. This is done by invoking the
functional method of an object derived from the ``function_generator``
class. For identical parameters, the same ``function_class`` object
should be returned, which means that they have to be cached by the generator.
.. code-block:: cpp
struct function_generator {
function_generator(const char *);
virtual function_class const *operator()(function_params const &) const = 0;
virtual ~function_generator();
};
The constructor of this class requires the name of the function
template, so that it gets registered by the parser. Method ``operator()`` is
called with a vector of encoded parameters.
If a rounding operator has no parameters, the
``default_function_generator`` class can be used instead to register it.
The first argument of the constructor is the function name. The second
one is the address of the ``function_class`` object.
.. code-block:: cpp
default_function_generator::default_function_generator(const char *, function_class const *);
|
