What the name means

QF means quantifier-free. UF adds uninterpreted functions, and BV supplies fixed-width bit-vectors.

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

Bit-vector operations have exact rules for wrapping and bit manipulation. An uninterpreted function has no supplied implementation, but equal inputs still require equal outputs. The combined logic lets those rules interact.

The solver can discover that different-looking expressions denote the same bit pattern. It must then enforce the same function result for both expressions, even when their written forms differ.

Worked example

An abstract operation after wraparound

An abstract device operation maps eight-bit inputs to eight-bit outputs. Compare its result on zero with its result on 255 plus one.

  1. Compute the sum at eight-bit width. The result of 255 plus one is zero.
  2. Ask whether device(255 + 1) ≠ device(0), with that bit-vector addition.
  3. Both calls have the same input pattern, so their outputs must agree.

The query is unsat, regardless of which function the model assigns to device.

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

The constraint device(1) = device(2) is sat. Nothing requires this abstract operation to distinguish different inputs.

Use cases

  • Check hardware control logic while replacing a data-processing block with an abstract function.
  • Analyze machine-word code without expanding every pure helper call.

Modeling caution

An arbitrary function admits behaviors a real device may never have. A sat model can be a consequence of the abstraction and need checking against the concrete device.

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.

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.