What the name means

QF means quantifier-free. UF means uninterpreted functions; the language also permits abstract sorts, or kinds of values.

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

An uninterpreted function has a fixed input and output sort, but no supplied implementation. The solver chooses a function that meets the constraints. A function must give equal outputs for equal inputs.

Different inputs may still have the same output. No rule says the function is one-to-one, increasing, or cryptographically secure. Extra properties need explicit constraints or a richer theory.

Worked example

Check consistent lookups

Accounts a and b have the same identifier. A function region maps an identifier to a region value. Can the lookups disagree?

  1. Require a = b.
  2. Require region(a) ≠ region(b).
  3. Because a and b are equal, both calls give the same input to the same function. Their outputs must be equal.

The query is unsat. Equality of function inputs forces equality of their outputs.

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

Require a ≠ b and region(a) = region(b) instead. This is sat: distinct accounts can share a region. Equal outputs do not force equal inputs.

Use cases

  • Check program transformations while treating a pure helper function as an abstract operation.
  • Model identifiers and consistent lookups without encoding the contents of every implementation.

Modeling caution

A stateful or random operation cannot be represented as a function of its visible argument alone. Include the relevant state or random input in the model.

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.