All activity
Logician lets Rust developers use SMT solvers like Z3 and CVC5 without compiling C++ bindings.
Build formulas with a fluent API that catches sort mismatches immediately. Z3 times out? Auto-retry on CVC5. Hung solver? Watchdog kills it.
✓ Type-safe Term API with runtime invariants
✓ Multi-solver fallback
✓ Process watchdog with clean termination
✓ Optional async (tokio)
✓ MIT licensed, free forever
Perfect for constraint solving, verification, and SAT/SMT without FFI pain.
LogicianType-safe SMT solver driver for Rust—no C++ toolchain needed
Mike Kuykendallleft a comment
Hey PH! 👋 I built Logician because using Z3 from Rust was either: 1. FFI bindings → C++ toolchain hell 2. String-based → pray your SMT-LIB parses Logician is a subprocess driver. You install Z3 normally, and Logician talks to it via stdin/stdout with a type-safe Rust API. What it does: • Panics immediately if you mix Bool and Int terms • Tries Z3, falls back to CVC5 if it fails • Kills hung...
LogicianType-safe SMT solver driver for Rust—no C++ toolchain needed