Herbie automatically transforms floating point expressions into more accurate forms. This page catalogs questions frequently asked questions about Herbie.
Several Herbie error messages refer to this page for additional information and debugging tips.
This error means you mis-formatted Herbie's input. Common errors
include misspelling function names and parenthesizing expressions
that must not be parenthesized. For example, in
(- (exp (x)) 1),
(x) is incorrect:
x is a variable so isn't parenthesized.
x) 1) would be the correct way of writing that expression.
Please review the input format
documentation for more.
Herbie uses random sampling to select the points which it will use
to evaluate the error of an expression. This error occurs when it
is not able to find enough valid points. For example, consider the
(acos (+ 1000 x)). This expression yields
a valid result only when
x is between -1001 and -999,
a rather narrow range.
The solution is to help out Herbie by specifying a precondition.
:pre (< -1001 x -999) for the example
above. Herbie will use the precondition to improve its sampling
This error indicates that your precondition excludes all possible
inputs. For example, the precondition
(< 3 x 2)
excludes all inputs. Herbie raises this exception only when it can
determine that no inputs work. The solution is to fix the
precondition to allow some inputs. Note that sufficiently complex
unsatisfiable preconditions instead raise the error above.
Herbie computes "ground truth" results using
MPFR. For some expressions,
(sin (exp x)), using MPFR in this way requires
exponentially many bits to compute a correct result. Instead of
simply timing out in such cases, Herbie limits the MPFR precision
to 10,000 bits and raises this error when it hits that limit.
When using Chrome to view web pages on your local machine, Chrome
disables certain APIs for security reasons; this prevents the
Herbie reports from drawing the chart. Run Chrome
--allow-file-access-from-files to fix this error.
Some systems may not support a native implementation for all
operations that Herbie uses. Herbie provides a default fallback
implementation which is used by default for functions whose
native implementation is not found. You can disable this fallback