What the name means

QF means quantifier-free. FP means floating-point arithmetic, using a format with specified exponent and significand sizes.

Quantifier-free formulas have no explicit "for every" or "there exists" binders. They can still contain unknown values that the solver must find.

The significand holds the precision bits; the exponent sets their scale. Only a finite set of ordinary numbers fits a fixed format. Most arithmetic operations therefore need a rounding mode to choose a representable result.

The theory also has positive and negative infinity, signed zeros, and NaN, meaning 'not a number'. NaN is a special value used for invalid numerical results. It behaves differently from ordinary numbers in floating-point comparisons.

Worked example

Distinguish two kinds of equality

Let x be NaN in a chosen floating-point format. Compare x with itself using floating-point equality.

  1. Require fp.isNaN(x), which tests whether x is NaN.
  2. Also require not fp.eq(x, x). The fp.eq operation follows floating-point comparison rules.
  3. A NaN makes fp.eq(x, x) false, so both constraints hold.

The query is sat. A self-comparison can be false under floating-point equality.

This is an authored mathematical example, not captured Axeyum output. Here, sat means the constraints can all hold; unsat means they cannot.

A contrasting case

Replace fp.eq with SMT's ordinary equality symbol, =. The condition not (x = x) is unsat for every value, including NaN. Ordinary equality remains reflexive.

Use cases

  • Check numerical branches that behave differently for NaN or signed zero.
  • Find inputs where a compiler's proposed arithmetic rewrite changes a rounded result.

Modeling caution

Fix the format and rounding mode before comparing arithmetic expressions. Real-number identities do not automatically hold for their floating-point versions.

Axeyum coverage

The examples explain the logic's meaning. They do not establish complete Axeyum support for this division. Acceptance, solving, and evidence coverage depend on the input and the solver route.

This division appears in the site's retained regression scoreboard. Read the individual slices and their source records for the tested scope.

The results page also includes a retained comparison for this division. Its figures apply to the named benchmark list and resource budget.

A solver may return unknown if it cannot settle a query. That result establishes neither sat nor unsat. Parsing a declared logic name alone does not prove support for every formula in it.

Engine support documentation at the site's recorded snapshot, 03ae4a3c9, 2026-10-05.

Definitions and references

Definitions consulted September 6, 2026. The worked examples and use-case explanations are authored for this guide.