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 src/arithmetic and 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.

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.

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, \(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 \(x\), compute the range of \(f(x)\).

enforce

Given the range of \(f(x)\), compute a stricter range of it.

absolute_error

Given no range, compute the range of \(f(x) - x\).

relative_error

Given no range, compute the range of \(\frac{f(x) - x}{x}\).

absolute_error_from_exact_bnd

Given the range of \(x\), compute the range of \(f(x) - x\).

absolute_error_from_exact_abs

Given the range of \(|x|\), compute the range of \(f(x) - x\).

absolute_error_from_approx_bnd

Given the range of \(f(x)\), compute the range of \(f(x) - x\).

absolute_error_from_approx_abs

Given the range of \(|f(x)|\), compute the range of \(f(x) - x\).

relative_error_from_exact_bnd

Given the range of \(x\), compute the range of \(\frac{f(x) - x}{x}\).

relative_error_from_exact_abs

Given the range of \(|x|\), compute the range of \(\frac{f(x) - x}{x}\).

relative_error_from_approx_bnd

Given the range of \(f(x)\), compute the range of \(\frac{f(x) - x}{x}\).

relative_error_from_approx_abs

Given the range of \(|f(x)|\), compute the range of \(\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 \([1,1.3)\) or \((1.7,2]\). For practical reasons, \([1,1]\) and \([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.

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.

default_function_generator::default_function_generator(const char *, function_class const *);