sml-smt

A small SMT solver in pure Standard ML, built on the vendored sml-sat DPLL core via the classic lazy DPLL(T) ("offline" SMT) loop:

1. abstract every distinct theory atom to a Boolean variable;
2. Tseitin-encode the formula's Boolean structure to CNF;
3. ask the SAT solver for a propositional model;
4. check the assigned theory literals for theory consistency;
5. if T-inconsistent, add the blocking clause and go back to step 3; otherwise report SAT.

Two quantifier-free theories are supported, over disjoint signatures so the combination is sound without Nelson-Oppen:

• EUF — equality with uninterpreted functions, decided by congruence closure over a union-find;
• LRA — linear real (rational) arithmetic, decided by Fourier-Motzkin elimination. Atoms are <= 0 and < 0; build = 0, >= 0, > 0 with the smart constructors. Feasibility uses arbitrary-precision integers internally, so Fourier-Motzkin never overflows.

No FFI, no threads, no clock, no randomness: the same inputs always produce the same outputs under MLton and Poly/ML, and the DPLL(T) refinement loop is deterministic.

API

structure Smt : sig
  datatype term = Const of string | Fn of string * term list
  type linear = (string * int) list * int      (* c1*x1 + ... + cn*xn + k *)
  datatype atom = Eq of term * term | Le of linear | Lt of linear
  datatype formula =
      Atom of atom | Not of formula
    | And of formula * formula | Or of formula * formula
    | Imp of formula * formula | Iff of formula * formula
    | TrueF | FalseF
  datatype result = SAT | UNSAT

  val le : linear -> formula      val lt : linear -> formula
  val ge : linear -> formula      val gt : linear -> formula
  val eqZero : linear -> formula
  val negLin : linear -> linear   val constLin : int -> linear
  val varLin : string -> linear

  val solve  : formula -> result
  val isSat  : formula -> bool
  val rounds : formula -> int     (* DPLL(T) refinement rounds used *)

  val eufConsistent : (term * term) list -> (term * term) list -> bool
  val lraFeasible   : (linear * bool) list -> bool
end

Example

val a = Smt.Const "a" and b = Smt.Const "b" and c = Smt.Const "c"
fun f x = Smt.Fn ("f", [x])
fun eq x y = Smt.Atom (Smt.Eq (x, y))
fun ne x y = Smt.Not (eq x y)

(* a = b & b = c & f(a) <> f(c)  is UNSAT by congruence *)
val Smt.UNSAT = Smt.solve (Smt.And (eq a b, Smt.And (eq b c, ne (f a) (f c))))

(* 0 < x & x < 1 is SAT over the rationals *)
val Smt.SAT = Smt.solve (Smt.And (Smt.gt (Smt.varLin "x"), Smt.lt ([("x", 1)], ~1)))

Running examples/demo.sml with make example prints:

EUF (equality + uninterpreted functions):
  a = b  &  b = c  &  f(a) <> f(c)
    => UNSAT  (after 2 DPLL(T) rounds)
  a = b  &  f(a) = f(c)
    => SAT

LRA (linear rational arithmetic):
  x >= 2  &  x + y <= 2  &  y >= 1
    => UNSAT
  0 < x  &  x < 1   (satisfiable over the rationals)
    => SAT

Disjunction handled by the SAT engine:
  (a = b | b = c)  &  a <> b  &  b <> c
    => UNSAT

Scope

This is a teaching-grade lazy SMT solver: complete and sound for quantifier-free EUF and LRA and their Boolean combinations over disjoint signatures. Theory combination with shared terms (Nelson-Oppen), integer arithmetic (LIA), bit vectors, arrays, and model extraction are intentionally out of scope. The propositional search is delegated wholesale to sml-sat.

Build & test

Requires MLton and/or Poly/ML.

make test        # build + run the suite under MLton
make test-poly   # run the suite under Poly/ML
make all-tests   # both
make example     # build + run the demo
make clean

Installing with smlpkg

smlpkg add github.com/sjqtentacles/sml-smt
smlpkg sync

sml-smt vendors sml-sat under lib/github.com/sjqtentacles/sml-sat/ (a byte-identical copy of the upstream library). Reference lib/github.com/sjqtentacles/sml-smt/smt.mlb from your own .mlb (MLton / MLKit), or feed sources.mlb to tools/polybuild (Poly/ML).

Layout

sml.pkg                                      smlpkg manifest (requires sml-sat)
Makefile                                     MLton + Poly/ML targets
.github/workflows/ci.yml                     CI: MLton + Poly/ML
lib/github.com/sjqtentacles/
  sml-smt/   smt.sig smt.sml sources.mlb smt.mlb
  sml-sat/   vendored DPLL core (byte-identical copy)
examples/
  demo.sml      EUF / LRA / disjunction walkthrough
test/
  harness.sml / test.sml                     29 reference checks
  entry.sml / main.sml
tools/polybuild                              Poly/ML build wrapper

Tests

29 deterministic checks: EUF congruence closure (transitivity + congruence refuting disequalities, including a 2-ary function), the same EUF cores routed through the solver, LRA feasibility/infeasibility via Fourier-Motzkin (a strict-inequality system satisfiable only over the rationals), Boolean structure (disjunctions and constants handled by the SAT engine), the lazy refinement loop (rounds), and combined EUF+LRA queries. Run make all-tests to verify identical output under both compilers.

License

MIT. See LICENSE.