Expand description
§z3rs — a pure-Rust port of the Z3 theorem prover
z3rs is a from-scratch reimplementation of
Z3 (v4.17.0) in safe, idiomatic Rust.
The goal is a 1:1 behavioural port of 100% of Z3 with no third-party or
native dependency — no GMP, no C. The crate is no_std (needs only
alloc) by default; the optional std feature adds std-backed conveniences.
Its sole dependency is our own pure-Rust, dependency-free numeric core
puremp, re-exported below and used directly throughout the port.
This is a large, multi-phase effort. See ROADMAP.md for the
staged plan, and PORTING.md for the porting methodology and
differential-testing strategy against upstream Z3.
§Attribution
z3rs is a derivative work of Z3, Copyright (c) Microsoft Corporation, used
under the MIT License. See LICENSE and NOTICE.
§Architecture
The module tree mirrors Z3’s src/ component layering. Modules are ordered
bottom-up by dependency (each layer only uses layers above it in this list):
| Module | Phase | Upstream z3/src/… |
|---|---|---|
util | 0 | util (bignum, containers, symbols, params infra) |
math | 1 | math/* (polynomial, interval, simplex, dd, lp, …) |
ast | 1 | ast (terms, sorts, decls, theory decl_plugins) |
params | 1 | params |
rewriter | 2 | ast/rewriter, ast/euf, ast/normal_forms, … |
model | 3 | model |
tactic | 3 | tactic + tactic portfolio |
sat | 4 | sat, sat/smt |
nlsat | 5 | nlsat, math/realclosure |
smt | 5 | smt (core SMT engine) |
solver | 6 | solver |
cmd_context | 6 | cmd_context, parsers/smt2 |
qe | 7 | qe, qe/mbp |
muz | 7 | muz (Datalog / Spacer / Horn) |
opt | 7 | opt (MaxSAT / optimization) |
parsers | 8 | parsers |
api | 9 | api (C ABI + safe Rust surface) |
Most modules are functional (see ROADMAP.md for live
phase status); a few upper-layer components remain documented scaffolds.
Re-exports§
pub use puremp;
Modules§
- api
api— C-compatible API surface + safe idiomatic Rust API- ast
ast— expression / sort / decl representation and the theory decl plugins- cmd_
context cmd_context— SMT-LIB2 command interpreter- math
math— Exact math: polynomial arithmetic, intervals, simplex, decision diagrams, Groebner, linear programming- model
model— Models and model evaluation- muz
muz— Fixedpoint / Datalog / Spacer (Horn clauses)- nlsat
nlsat— Nonlinear arithmetic SAT, real closed fields- opt
opt— Optimization: MaxSAT, MaxSMT, Pareto- params
params— Parameter descriptor tables (param_descrs) for every module- parsers
parsers— the frontend parsers, gathered as one entry point- qe
qe— Quantifier elimination, model-based projection- rewriter
rewriter— term rewriting and simplification- sat
sat— propositional SAT core- smt
smt— core SMT engine- solver
solver— Solver abstraction, combined/parallel solvers- tactic
tactic— Goals, the tactic framework, probes, and the combinators- util
util— Foundation: numerals, containers, hashtables, symbols, vectors, params infra, rlimit, memory, sexpr
Constants§
- VERSION
- z3rs crate version.
- Z3_
UPSTREAM_ VERSION - The upstream Z3 version this port tracks.