What the name means

QF means quantifier-free. S adds strings, and LIA adds linear integer arithmetic, including constraints on string lengths.

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

A length operation connects a string to an integer. A query can require a prefix, relate an integer variable to the string's length, and limit a combined message size. Both the text and its count must agree in the model.

Joining two strings adds their lengths. That arithmetic can rule out a string equation before a solver tries individual characters. String length counts characters in the theory; encoded byte length is a separate quantity.

Worked example

Fit a prefixed identifier

An identifier begins with 'ID-' and has total length seven. Its remaining text is an unknown suffix.

  1. Require identifier = 'ID-' joined with suffix.
  2. Require length(identifier) = 7. The prefix has length three, so suffix must have length four.
  3. Choose suffix = '0042'. The complete identifier 'ID-0042' meets both requirements.

The query is sat. The model meets the string equation and its integer length constraint.

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

Also require length(suffix) ≤ 3. The identifier can then have length at most six, so the changed query is unsat.

Use cases

  • Test input-validation rules that combine text patterns with length limits.
  • Analyze string-building code whose branches also depend on counters or offsets.

Modeling caution

A character count is not generally a UTF-8 byte count. State the encoding when a buffer limit is measured in bytes, and check the solver's supported character range.

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.