What the name means

QF means quantifier-free. UF adds uninterpreted functions; LRA supplies linear real arithmetic.

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

Real arithmetic can show that two expressions name the same input to a function. The solver must keep the function results equal. It can also apply linear constraints to those results without knowing a formula for the function.

An uninterpreted real-valued function need not be continuous or increasing. Those properties do not follow from using real numbers. The permitted linear arithmetic still excludes products of unknown quantities.

Worked example

Compare a reading at the same time

A function reading maps a real-valued time to a real-valued measurement. Two expressions describe the same time.

  1. Require time = 1/2 and later = time + 1/2.
  2. Ask whether reading(later) < reading(1).
  3. The constraints give later = 1. Both calls therefore return the same value, which cannot be strictly less than itself.

The query is unsat under exact real arithmetic and consistent function application.

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

The condition reading(1/2) > reading(1) is sat when those are distinct inputs. A model can assign the earlier reading a larger value.

Use cases

  • Check linear control conditions while abstracting a sensor's response function.
  • Reason about exact real-valued interfaces without encoding each module's internal formula.

Modeling caution

An abstract sensor function has no built-in error bound or physical law. Add the relevant constraints before interpreting a model as a possible measurement.

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 has no row in the site's retained regression scoreboard. Consult the engine's support documentation for the relevant route.

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.