What the name means

QF_SEQ is the sequence label used in Axeyum's benchmark data. QF means quantifier-free, and SEQ refers to sequences. It is not a portable logic declaration across solvers.

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

A sequence has a length and an element sort, meaning the kind of value it holds. A sequence of integers can represent an event trace or a list of measurements. Its values need not be text characters.

Operations include joining sequences, extracting a section, and reading an element at a position. Solver syntax varies. For example, cvc5 documents sequence examples under QF_SLIA with an explicit Seq sort.

Worked example

Append an event to a trace

A trace is the integer sequence [4, 7]. Append the single-element sequence [9] to it.

  1. The joined sequence is [4, 7, 9]. Joining preserves the order of both inputs.
  2. Its length is three. With positions counted from zero, the element at position two is 9.
  3. Ask whether the resulting sequence has length three and element 9 at position two. Both conditions hold.

The constraints are sat. The explicit sequence gives a model for the trace.

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 the same result to have length two. That contradicts the length of the joined sequence, so the query is unsat.

Use cases

  • Check event ordering and concatenation in finite protocol traces.
  • Reason about slices and lengths of typed lists without converting every element to a character.

Modeling caution

Constrain an index to be within the sequence before reading it. An out-of-range read may have an unspecified value under the chosen solver's semantics rather than raise a program exception.

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.