What the name means

QF means quantifier-free. AX names the array theory with extensionality: arrays are equal when every corresponding read agrees.

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

An SMT array maps every index of its index sort to a value of its element sort. A sort is a kind of value. In QF_AX, indices and elements are abstract; their names do not carry integer arithmetic.

The operation select reads an element. The operation store returns an array with one changed element. Reads at other indices stay the same. The old array remains available, so a write is represented by a new value.

Worked example

Read the element just written

Let shelf be an array, slot an index, and item an element. Form updated by storing item at slot.

  1. Define updated = store(shelf, slot, item).
  2. Ask whether select(updated, slot) ≠ item.
  3. The store rule says the read at the written index returns item. The requested difference contradicts that rule.

The query is unsat. A read at the written index must return the written value.

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

A read at a different index remains equal to the old array's value there. It can differ from item if the element sort has distinct values.

Use cases

  • Check that an abstract map update preserves every other key.
  • Prove read-after-write properties before choosing a numeric representation for addresses or elements.

Modeling caution

An SMT array has a value at every index. It has no built-in length, allocation state, or invalid-address exception. Model those conditions separately.

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.