What the name means

QF means quantifier-free. DT means datatypes. An algebraic datatype defines its values through named constructors that build each allowed form.

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

A constructor identifies a form and can hold fields. A small color datatype can have the constructors red and blue. A list datatype can have empty and cons, where cons holds an element and the rest of the list.

Different constructors produce different values. Equal values built by the same constructor have equal fields. Inductive datatypes contain finite constructor trees, so a list cannot equal a cons cell whose tail is that same list.

Worked example

Keep message tags distinct

Define a message datatype with nullary constructors accepted and rejected. Nullary means a constructor has no fields.

  1. Let message be a value of this datatype.
  2. Require message = accepted and message = rejected.
  3. The two distinct constructors cannot denote the same value, so message cannot meet both constraints.

The query is unsat. The datatype declaration gives the tags their distinct meanings.

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 message = accepted or message = rejected instead. The query is sat; either constructor supplies a value.

Use cases

  • Check code that branches on tagged messages or result variants.
  • Reason about the shape of parsed expressions and finite tree values.

Modeling caution

Recursive datatype support does not automatically provide induction for every list or tree. A quantifier-free query and a theorem about all recursively built values are different tasks.

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.