Lesson 04

Adding arithmetic and machine values

What changes when constraints contain integers, strings, or fixed-width arithmetic?

Satisfiability modulo theories retains the meaning of operations such as addition and comparison while using Boolean search to coordinate the resulting constraints.

Core component Open the SMT implementation page

After this lesson, you should be able to

Explain the difference between SAT and satisfiability modulo theories.
Read the declarations, assertions, and result of a short SMT-LIB query.
Describe theory solving, rewriting, bit-blasting, and model replay as separate reasoning steps.

4.1

Theories give operations their meaning

A SAT solver can treat the statements x < 2 and x > 5 as unrelated Boolean variables. An arithmetic theory knows that they cannot both hold for the same integer x. SMT combines this domain reasoning with Boolean structure.

Each variable has a sort. The sort determines its values and legal operations. Integer addition is unbounded, while eight-bit addition wraps after 255. A solver must preserve that difference.

4.2

SMT-LIB states the query

SMT-LIB is a standard language for declaring sorts and functions, asserting constraints, and requesting results. A logic name describes the permitted fragment. QF_BV means quantifier-free bit-vectors.

A solver may parse more constructs than it can decide completely. Coverage reports therefore need to distinguish accepted syntax, decided queries, correct answers, and performance.

4.3

Different terms take different routes

Rewriting removes or normalizes structure through meaning-preserving rules. A theory solver can decide selected arithmetic or string constraints directly. Bit-vector terms can be bit-blasted into a Boolean circuit and passed to SAT.

Each route creates a separate checking question. Model replay evaluates sat assignments against the original terms. Unsat evidence may need a theory certificate, a checked reduction to SAT, or another route appropriate to the fragment.

4.4

Axeyum's SMT component

Axeyum implements typed terms, SMT-LIB parsing, rewriting, theory-specific procedures, bit-blasting, SAT search, models, and selected certificates in Rust. Z3, cvc5, and Bitwuzla are comparison systems and optional test oracles.

Logic coverage and speed vary by fragment. A result for QF_BV does not establish support for nonlinear arithmetic, floating point, strings, or another named logic.

Worked example

Schedule two jobs with integer constraints

Job A lasts two hours, job B lasts one hour, and both use one machine. A starts at hour 0. B must finish by hour 4 and cannot overlap A.

Declare
Let b be B's integer start time, with b ≥ 0.
Set the deadline
B lasts one hour, so b + 1 ≤ 4.
Prevent overlap
A occupies [0, 2). Since B cannot finish before A starts, require b ≥ 2.
Find a model
The value b = 2 satisfies all three constraints.
Replay
Substitute 2 into the original assertions: 2 ≥ 0, 2 + 1 ≤ 4, and 2 ≥ 2 are all true.

Result. The query is sat, and b = 2 is a replayable integer model.

4.5

Check your understanding

Answer each question before opening the explanation.

1 Why should x < 2 and x > 5 not be represented as independent Boolean facts?

Their shared integer meaning makes the conjunction impossible, and independent Boolean variables would lose that fact.

2 Why can eight-bit x + 1 equal zero when integer x + 1 cannot?

Eight-bit arithmetic wraps modulo 256, while mathematical integer addition is unbounded.

Concept wiki

Terms in this lesson

All concepts