The Input Format

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.

General format

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.

Supported functions

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
- is both negation and subtraction

sqr, sqrt

Squares and square roots

cube, cbrt

Cubes 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.

Conditionals

FPCore uses if for conditional expressions:

(if cond if-true if-false)

An if epxression evaluates the conditional cond and returns either if-true if it is true or if-false if it is not. Conditionals may use:

==, !=, <, >, <=, >=

The usual comparison operators

and, or, not

The usual logical operators

Note that unlike the arithmetic operators, these functions can take any number of arguments.

Intermediate variables

Intermediate variables can be defined using let:

(let ([variable value] ...) 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.

Properties

Herbie also uses several FPCore properties for additional meta-data:

:name string

Herbie uses this name in its output

:pre test

Herbie samples only points that pass the test

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.

Converting from Herbie 0.9

Herbie 0.9 used a different input format, which is not supported Herbie 1.0 and later. To simplify the transition, the infra/convert.rkt script converts from the old to the new format.

To use the conversion tool, run:

racket infra/convert.rkt file.rkt > file.fpcore