What the name means

QF means quantifier-free. UF adds uninterpreted functions; LIA supplies linear integer arithmetic.

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

Integer constraints can establish equalities that affect function calls. The function has no fixed formula, but it must return one consistent value for each input. Arithmetic can also place linear bounds on its outputs.

A fixed multiple of an integer-valued function result can be linear. Multiplying two unknown results is nonlinear. The UF letters do not remove the arithmetic restrictions in LIA.

Worked example

Equal indices imply equal costs

An abstract function cost assigns an integer cost to each integer item index. Two indices differ by one before an increment.

  1. Let i and j be integers and require i + 1 = j.
  2. Ask whether cost(i + 1) > cost(j).
  3. The arithmetic equality makes the function arguments equal, so the two costs must be equal as well.

The query is unsat. A strict inequality between those two calls cannot hold.

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

With i = 0 and j = 2, the condition cost(i + 1) > cost(j) is sat. A function can assign cost(1) = 5 and cost(2) = 4.

Use cases

  • Check loop-index reasoning around abstract integer lookup functions.
  • Combine inventory constraints with unspecified but consistent cost or capacity functions.

Modeling caution

A function called cost can return negative values unless the formula excludes them. Names carry no mathematical assumptions, including nonnegativity or monotonicity.

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.