Herbie uses the FPCore input format to specify mathematical expressions, which Herbie searches for accurate implementations of.

FPCore format 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 (+ (* a a) (* b 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:

`+`

,`-`

,`*`

,`/`

,`fabs`

- The usual arithmetic functions

(where`-`

is both negation and subtraction) `sqrt`

,`cbrt`

- Square and cube roots
`pow`

,`exp`

,`log`

- Various exponentiations and logarithms
`sin`

,`cos`

,`tan`

- The trigonometric functions
`asin`

,`acos`

,`atan`

,`atan2`

- The inverse trigonometric functions
`sinh`

,`cosh`

,`tanh`

- The hyperbolic functions
`asinh`

,`acosh`

,`atanh`

- The inverse hyperbolic functions
`fma`

,`expm1`

,`log1p`

,`hypot`

- Specialized numeric functions

Herbie also supports the constants `PI`

and `E`

. The arithmetic operators associate to the
left.

Herbie links against `libm`

to ensure that every
function has the same behavior in Herbie as in your code. However,
on Windows platforms some functions are not available in the
system `libm`

. In these cases Herbie will use a fallback
implementation and print a warning; turning off the
the `precision:fallback` option
disables those functions instead.

FPCore uses `if`

for conditional expressions:

(ifcondif-trueif-false)

The conditional

may use:
`cond`

`==`

,`!=`

,`<`

,`>`

,`<=`

,`>=`

- The usual comparison operators
`and`

,`or`

,`not`

- The usual logical operators
`TRUE`

,`FALSE`

- The two boolean values

The comparison functions can take any number of arguments and implement chained comparisons.

Intermediate variables can be defined using `let`

:

(let ([variablevalue]...)body)

In a `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 `let`

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.

By default, the arguments to formulas are assumed to be arbitrary
floating-point numbers. However, in many cases only a range of
argument values are possible. In Herbie, you can describe valid
arguments with the `:pre`

property (for
“precondition”).

Preconditions comparison and boolean operators, just
like conditional statements. Herbie is
particularly efficient when when the precondition is
an `and`

of ranges for each variable, such as:

(FPCore (x) :pre (< 1 x 10) (/ 1 (- x 1)))

More complex preconditions *do* work, but may cause
the “Cannot sample enough
valid points” error if it is too hard to find points that
satisfy the precondition.

Herbie supports both single- and double-precision values; you can
specify the precision with the `:precision`

property:

`binary32`

- Single-precision IEEE-754 floating point
`binary64`

- Double-precision IEEE-754 floating point

By default, `binary64`

is assumed. Herbie also has
a plugin system to load additional
precisions.

Herbie includes experimental support for complex numbers; however, this support is currently limited to a few basic operations.

All input parameters to an FPCore are real numbers; complex
numbers must be constructed with `complex`

. The
functions `re`

, `im`

, and `conj`

are available on complex numbers, along with the arithmetic
operators, `exp`

, `log`

, `pow`

,
and `sqrt`

. Complex and real operations use the same
syntax, but cannot be mixed: `(+ (complex 1 2) 1)`

is not
valid. Herbie reports type errors in such situations.

Complex operations use the Racket implementation, so results may differ (slightly) from complex numbers in some other language, especially for non-finite complex numbers. Unfortunately, complex number arithmetic is not as standardized as float-point arithmetic.

In the future, we hope to support complex-number arguments and fully support all complex-number operations.

Herbie uses the `:name`

property to name FPCores in
its UI. Its value ought to be a string.

Herbie's out uses custom FPCore properties to provide additional information about the Herbie improvement process:

`:herbie-status`

`status``status`describes whether Herbie worked: it is one of`success`

,`timeout`

,`error`

, or`crash`

.`:herbie-time`

`ms`- The time, in milliseconds, used by Herbie to find a more accurate formula.
`:herbie-error-input`

([`pts``err`] ...)- The computed average error of the input program, evaluated on
`pts`points. Multiple entries correspond to multiple training or test sets. `:herbie-error-output`

([`pts``err`] ...)- The computed average error of the output program, like above.

Herbie's passes through `:name`

,
`:pre`

, and `:precision`

properties to its
outputs.

The benchmark suite uses other properties (such
as `:herbie-target`

) for testing, but these are not
supported and their use is discouraged.