What the name means

QF means quantifier-free. A adds arrays, UF adds uninterpreted functions, and BV adds 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.

An array records values at addresses. An uninterpreted function can name an address calculation or a pure operation whose implementation is omitted. The solver combines array read and write rules with arithmetic and function consistency.

A function still gives the same result for equal inputs. That equality can make two computed addresses refer to the same array cell. A sat model may choose any function behavior that the constraints permit.

Worked example

Read through an abstract address function

Let address map eight-bit keys to eight-bit addresses. Keys left and right are equal. Store byte 9 at address(left).

  1. Require left = right, so address(left) = address(right).
  2. Define updated = store(memory, address(left), 9).
  3. Ask whether select(updated, address(right)) ≠ 9. Both addresses select the written cell.

The query is unsat. Function consistency and the store rule together determine the read.

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

Distinct keys do not guarantee distinct addresses. The model can map both keys to one address unless further constraints prevent that collision.

Use cases

  • Check memory access through an abstract address-translation function.
  • Model hardware with word arithmetic, memory, and abstract data-processing blocks in the same query.

Modeling caution

An uninterpreted address function is not automatically injective: different inputs can collide. If the device guarantees unique addresses, encode the guarantee for the needed inputs.

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.