Crate smtkit 

Facade crate for SMT constraint tooling.

This crate is the stable entrypoint users depend on. It re-exports:

• smtkit-core: typed, backend-agnostic constraint IR
• smtkit-smtlib: SMT-LIB2 serialization and optional solver I/O

DX-first solver guidance

• Prefer z3-bin for most users: it runs an external z3 binary and avoids native headers/toolchains.
• Use z3-inproc only when you specifically want in-process Z3; it may require system Z3 headers (and/or a CMake toolchain if you enable bundled builds in the underlying Z3 crate).

Modules

core

Typed, backend-agnostic constraint IR.

session

Incremental SMT-LIB process session (solver-agnostic).

sexp

Tiny s-expression utilities for SMT-LIB2 I/O.

smt2

SMT-LIB2 script builder (SMT-LIB backend).

solver

External solver runners (optional, backend-specific).

Structs

SolveResult

A minimal solver result. model is backend-defined (e.g. an SMT-LIB s-expression).

Enums

SolveStatus

Backend-agnostic solver result shape (status + optional model payload).

Traits

SmtlibSessionLike

A small “SMT-LIB over stdio” session surface, stable at the smtkit facade.