What the name means

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

The standard division uses arrays with integer indices and integer elements. Abstract functions can calculate an index or return an integer value. Linear constraints relate those values to counts and bounds.

A solver may need arithmetic to identify equal indices, function consistency to identify equal values, and array rules to interpret a write. Every step concerns the same formula; the letters do not name independent tests.

Worked example

Update an item through a lookup

The function index maps an integer product identifier to an integer stock-table index. Product identifiers a and b are equal.

  1. Require a = b. It follows that index(a) = index(b).
  2. Store select(stock, index(a)) + 1 at index(a), forming updated.
  3. Ask whether select(updated, index(b)) ≤ select(stock, index(a)). The new count is exactly one greater than the old count.

The query is unsat under integer arithmetic. Reading through the equal identifier observes the increment.

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

If the increment were zero, the same non-strict comparison would be sat: the read would equal the old value.

Use cases

  • Check update code that accesses integer tables through pure lookup functions.
  • Model a bounded program path whose conditions combine arrays, counters, and abstract helper calls.

Modeling caution

The A prefix does not permit arbitrary array sorts in every named logic. QF_AUFLIA's standard array sort is (Array Int Int). Check another division before introducing nested or real-valued arrays.

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.