Herbie's input format is designed for expressing mathematical functions, which Herbie can then search for accurate implementations of. It also allows specifying the distribution that Herbie draws inputs from when evaluating the accuracy of an expression.
Herbie uses the FPCore format for its input expression, which looks like this:
(FPCore (inputs ...) properties ... expression)
Each input is a variable, like
x, which can be used
in the expression, whose accuracy Herbie will try to improve.
Properties are described below.
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 (+ (sqr a) (sqr b))))
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, far from the full list, include:
-is both negation and subtraction
Herbie also supports the constants
if for conditional expressions:
(if cond if-true if-false)
if epxression evaluates the
cond and returns either
it is true or
if-false if it is not. Conditionals may use:
Note that unlike the arithmetic operators, these functions can take any number of arguments.
Intermediate variables can be defined using
(let ([variable value] ...) body)
let expression, all the values are evaluated
first, and then are bound to their variables in the body. This
means that the value of one variable can't refer to another
variable in the same
let block; nest
constructs if you want to do that. 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.
Herbie also uses several FPCore properties for additional meta-data:
Several additional properties can be found in the benchmark suite and are used for testing, but they are not supported and can change without warning.
Herbie 0.9 used a different input
format, which is not supported Herbie 1.0 and later. To
simplify the transition, the
converts from the old to the new format.
To use the conversion tool, run:
racket infra/convert.rkt file.rkt > file.fpcore