# SMT — Phases 1–4: SAT + EUF + LRA + Nelson–Oppen

A tutorial-grade SMT solver, written in C99 with no library
dependencies.

**Phase 1** implements the DPLL(T) integration of a CDCL SAT driver
with the theory of equality and uninterpreted functions (EUF) via
classical congruence closure.

**Phase 2** adds three techniques that turn the Phase 1 skeleton into
something actually usable: theory propagation, proof-forest
explanations, and use lists with on-merge aggregation.

**Phase 3** adds linear real arithmetic (LRA) and the combined-theory
machinery that lets the SAT solver talk to both back-ends. The LRA
solver is the Dutertre–de Moura *General Simplex for SMT*:
incremental tableau, bound trail, Bland's-rule pivoting,
delta-rationals for strict inequalities, and Farkas-style conflict
generation that reads minimal infeasibility certificates directly off
the failing row.

**Phase 4** makes the two theories actually talk to each other:
Nelson–Oppen combination. A `SmtShared` is a single logical object
that exists as both an EUF constant *and* an LRA real variable. For
every pair of shareds, three "bridge" atoms (eq, le, ge) plus three
linking clauses are installed eagerly. The clauses turn cross-theory
implications into ordinary SAT propagations: BCP carries the
EUF↔LRA exchange. Phase 4 also gives LRA bound propagation, so the
LRA→EUF arrow can fire when arithmetic *derives* an equality.

An SMT-LIB parser, lazy bridge installation, linear integer
arithmetic, and bigint rationals are planned for later phases.

## Companion documents

For the canonical write-up, see **Chapter 4 of *Practical Solvers***
(`../books/practical-solvers/practical-solvers.pdf`).

The earlier standalone materials are preserved in `../books/background/`:

  * `smt-book.{tex,pdf}` --- the implementation book covering all four
    phases of the build.
  * `smt-user-guide.{md,pdf}` --- a user guide focused on how to *use*
    the solver: modelling patterns, the mental model, and a set of
    UI-component-placement worked examples (ex10--ex13).

## Build

```
./build.zsh
```

Plain `sh`-compatible, works under bash and zsh. Compiles the five
core translation units, then the sanity tests, then the nine
examples, and runs them in order. Nineteen sanity tests should pass.

## Layout

```
src/
  rat.h, rat.c           rational arithmetic (int64 num/den) and
                         delta-rationals for strict bounds
  sat.h, sat.c           CDCL SAT solver with theory hooks
  euf.h, euf.c           congruence closure with proof forest, theory
                         propagation, aggregated use lists
  lra.h, lra.c           General Simplex with Farkas explanations
                         + bound propagation (Phase 4)
  smt.h, smt.c           combined-theory dispatch, SmtShared API,
                         pair-bridge installation (Phase 4)
examples/
  ex1_transitivity.c     chain a_0 = ... = a_N with a_0 != a_N
  ex2_branching.c        SAT must enumerate, theory refutes each branch
  ex3_arrays.c           read(mem, p) modelled as uninterpreted function
  ex4_equiv.c            combinational equivalence via EUF
  ex5_propagation.c      Phase 2: visible theory propagation
  ex6_lra_basic.c        Phase 3: classic Farkas UNSAT
  ex7_lra_branching.c    Phase 3: SAT branching over LRA atoms
  ex8_no_basic.c         Phase 4: NO, EUF -> LRA arrow
  ex9_no_arithmetic.c    Phase 4: NO, LRA -> EUF arrow
sanity.c                 smoke tests for the SMT layer
build.zsh                build script
```

## What it does

The SAT layer drives. After every round of unit propagation, each
theory is given a chance to check consistency of its asserted atoms.
If either theory finds a conflict, it returns a clause (the negation
of an inconsistent subset of asserted literals) which the SAT layer
ingests as a learned clause. Conflict analysis and backjump then run
as usual.

Phase 2 extends the search loop into a three-way fixpoint: BCP, then
theory check (consistency), then theory propagate (push implied
literals).

Phase 3 generalises the theory side: each atom is owned at
registration time by either EUF or LRA, and the combined-theory
dispatch routes each `assign` / `unassign` / `check` / `propagate`
call to the right back-end.

Phase 4 lets the two theories communicate. `SmtShared` creates an
EUF constant and an LRA variable in lockstep, plus, for every pair
of shareds, three bridge atoms (eq, le, ge) and three linking
clauses (eq→le, eq→ge, le∧ge→eq). EUF→LRA: an EUF merge propagates
eq via Phase 2 theory propagation, BCP on the bridge clauses forces
le and ge as new LRA bounds. LRA→EUF: bound propagation on the
bridge slacks fires le and ge, BCP forces eq, EUF receives it.

## What is left for later phases

- **An SMT-LIB v2 parser** plus automatic purification of mixed-sort
  terms.
- **Lazy bridge installation** so pair atoms are created on demand
  rather than eagerly at variable creation time (the current design
  is O(n²) in shareds).
- **Linear integer arithmetic** — non-convex, so NO needs to
  propagate disjunctions of equalities; needs branch-and-bound with
  Gomory cuts on top of LRA.
- **Bigint rationals.** int64 num/den is fine for small examples
  but pivots can square the size each step; production code uses GMP
  or its own bigint.
- **Theory-aware decision heuristics** and an **incremental push/pop
  API** continue to wait.

## License

Public domain / CC0.
