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.

Converting from Herbie 0.9

Herbie 0.9 used a different input format, which is no longer supported in Herbie 1.0. 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

Supported functions

The full list of supported functions and is as follows:

+, -, *, /, abs

The usual arithmetic functions
- is both negation and subtraction

sqr, sqrt

Squares and square roots

exp, log

Natural exponent and natural log

pow

Exponentiation; raising a value to a power

sin, cos, tan, cotan

The trigonometric functions

asin, acos, atan, atan2

The inverse trigonometric functions
atan2 is the two-argument inverse tangent

sinh, cosh, tanh

The hyperbolic trigonometric functions

expm1, log1p, hypot

Specialized numeric functions, as in math.h

FPCore writes conditional expressions using if:

(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

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 you can't use one variable in the value of another; nest 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 PI and E.

Properties

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

:name string

Herbie prints this name in its output when a name is required.

:pre condition

Only points where the condition is true are sampled by Herbie.

:herbie-samplers samplers

Change the distribution with which variables are sampled (see below).

Distributions

Herbie allows you to specify what distribution is used to randomly sample values for each variable with the :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 for y. Not all variables need to be given distributions; if a variable isn't given a distribution, the default distribution will be used.

default

Interpret a random bit pattern as a float

(uniform a b)

A uniform real value between a and b
Both bounds must be numeric constants