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 0.9 used a different input
format, which is no longer supported in Herbie 1.0. 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
The full list of supported functions and is as follows:
-is both negation and subtraction
atan2is the two-argument inverse tangent
FPCore writes conditional expressions using
(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:
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 you can't use one variable in the value of another;
let constructs if you want to do that.
Note that Herbie treats these intermediate values only as a
notational convenience, and inlines their values before improving
the formula's accuracy.
Herbie also supports the constants
Herbie also uses several FPCore properties for additional meta-data:
Herbie allows you to specify what distribution is used to randomly
sample values for each variable with
:herbie-samplers property. For example:
:herbie-samplers ([x (uniform 0 1)] [y (uniform -1 1)])
This property tells Herbie to use a uniform distribution to sample
a value between 0 and 1 for
x, and between -1 and 1
y. Not all variables need to be given distributions;
if a variable isn't given a distribution, the
distribution will be used.
(uniform a b)