Herbie uses the FPCore format to specify an input program, and has extensive options for precisely describing its context.
FPCore format looks like this:
(FPCore (inputs ...) properties ... expression)
(FPCore name (inputs ...) properties ... expression)
Each input is a variable name, like
used in the expression. Properties are used to specify
additional information about the expression's context.
As of version 1.5, Herbie supports named functions.
If name is specified, the function can be inlined
within any subsequent FPCore in the file.
The expression is written in prefix form, with every function call parenthesized, as in Lisp. For example, the formula for the hypotenuse of a triangle with legs a and b is:
(FPCore (a b) (sqrt (+ (* a a) (* b b))))
The semicolon (;) character introduces a line comment.
We recommend the
.fpcore file extension for Herbie input files.
Herbie supports all functions from math.h with floating-point-only inputs and outputs. The best supported functions include:
Herbie also supports the constants
E. The arithmetic operators associate to the left,
- is used for both subtraction and negation.
Herbie links against your computer's
evaluate these functions. So, each function has the same behavior in
Herbie as in your code.
On Windows, the Bessel functions are not available in the
libm, so Herbie will use a fallback
implementation and print a warning. Turn off the
the precision:fallback option
to disable those functions instead.
if for conditional expressions:
(if cond if-true if-false)
cond may use:
The comparison functions implement chained comparisons with more than two arguments.
Intermediate variables can be defined
(let ([variable value] ...) body)
each variable is bound to its value and can be
used in the body. The difference between
let* is what order the values are
letexpression, all the values are evaluated in parallel, before they are bound to their variables. This means that later values can't refer to earlier variables in the same
let*block looks the same as a
letblock, except the values are evaluated one at a time, and later values can refer to earlier variables.
Note that Herbie treats intermediate values only as a notational convenience, and inlines their values before improving the formula's accuracy. Using intermediate variables will not help Herbie improve a formula's accuracy or speed up its run-time.
By default, the arguments to formulas are assumed to be
arbitrarily large or small floating-point numbers. However, in most
programs a smaller range of argument values is possible.
:pre property (for “precondition”) describes this
Preconditions use comparison and boolean operators, just like conditional statements:
(FPCore (x) :pre (< 1 x 10) (/ 1 (- x 1)))
Herbie is particularly efficient when when the precondition is
and of ranges for each variable, but more complex
preconditions also work.
Herbie supports both single- and double-precision values; you can
specify the precision with the
binary64 is assumed. Herbie also has
a plugin system to load additional
Herbie supports conversions between different precisions.
All conversions are assumed to be bi-directional. You can
specify conversions with the
([prec1 prec2] ...)
prec1, Herbie is allowed to rewrite all (or some) of the expression so it is computed with precision
For example, to let Herbie introduce single-precision
:precision is set to
binary64 or vice versa,
:herbie-conversions ((binary64 binary32))
In some cases, your input program is an approximation of some
more complex mathematical expression. The
“specification”) lets you specify the more complex ideal case.
Herbie will then try to modify the input program to make it more
accurately evaluate the specification.
For example, suppose you want to evaluate
via a series expansion. Write:
(FPCore (x) :spec (sin (/ 1 x)) (+ (/ 1 x) (/ 1 (* 6 (pow x 3)))))
Herbie will only use the
:spec expression to
evaluate error, not to search for accurate expressions.
Herbie uses the
:name property to name FPCores in
its UI. Its value ought to be a string.
Herbie's output provide additional information in custom properties:
([pts err] ...)
([pts err] ...)
Herbie's benchmark suite also uses properties such
:herbie-target for continuous integration, but these
are not supported and their use is discouraged.