Skip to content

Releases: Yatrogenesis/rz3

rz3 v0.1.2 — first public release

14 Jun 06:58
@Yatrogenesis Yatrogenesis
v0.1.2
589790e

Choose a tag to compare

View all tags
rz3 v0.1.2 — first public release Latest
Latest

First public release of rz3: a deterministic, exact-rational SMT solver in pure Rust.

Highlights

  • DPLL(T)/CDCL with a complete linear-arithmetic core — never returns unknown on a linear-arithmetic query. Strict inequalities use a symbolic δ-infinitesimal (Dutertre–de Moura); the feasibility Simplex avoids cycling via lexicographic ε-perturbation.
  • Exact arithmetic: arbitrary-precision rationals, no floating-point in the decision core.
  • Deterministic: run-to-run bit-identical, verified by an n=30 SHA-256 harness.
  • Zero native dependencies → WebAssembly-deployable.
  • Difference-Logic fragment decided by native Bellman-Ford negative-cycle detection.

Scope and limitations (vs. Z3)

Smaller theory coverage, no optimization (MaxSMT/OMT), partial proof/unsat-core, a subset of SMT-LIB, less performance tuning. See README.

License

Dual-licensed MIT OR Apache-2.0.

Verified: suite 87/0, clippy clean, cargo publish --dry-run valid.

Assets 2
Loading