z3rs 0.0.3

A pure-Rust port of the Z3 theorem prover, free of third-party and native dependencies
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91

# z3rs

[![CI](https://github.com/KarpelesLab/z3rs/actions/workflows/ci.yml/badge.svg)](https://github.com/KarpelesLab/z3rs/actions/workflows/ci.yml)
[![crates.io](https://img.shields.io/crates/v/z3rs.svg)](https://crates.io/crates/z3rs)
[![docs.rs](https://img.shields.io/docsrs/z3rs)](https://docs.rs/z3rs)
[![MSRV](https://img.shields.io/badge/MSRV-1.88-blue.svg)](https://blog.rust-lang.org/)
[![License: MIT](https://img.shields.io/badge/license-MIT-blue.svg)](LICENSE)

A **pure-Rust, `no_std`** port of the [Z3 theorem prover](https://github.com/Z3Prover/z3),
free of any third-party or native dependency.

`z3rs` reimplements Z3 (pinned at **v4.17.0**) as a single Rust crate with **no
GMP, no C, no `-sys` crate**. Its only dependency is our own pure-Rust,
dependency-free numeric core [`puremp`](https://github.com/KarpelesLab/puremp),
so the resolved dependency tree is just `z3rs → puremp`. The library is
`no_std` (needs only `alloc`); the optional `std` feature adds std-backed
conveniences. It aims to be behaviourally faithful to upstream Z3.

> ⚠️ **Status: early, in progress.** In place: a hash-consing AST, a simplifying
> rewriter, a **CDCL SAT core** (DIMACS), and a **lazy DPLL(T) SMT engine** that
> decides **QF_UF / QF_LRA / QF_LIA / QF_AX** and their combinations — congruence
> closure (incl. predicate congruence), Fourier–Motzkin linear arithmetic,
> integer branch-and-bound, read-over-write + extensionality arrays, and
> **bidirectional Nelson–Oppen** theory combination — plus a **bit-blasting engine
> for QF_BV** (bitwise, add/sub/mul, shifts, signed/unsigned compares,
> concat/extract, extend). It is **sound and terminating** (a work budget yields a
> sound `unknown` rather than a wrong answer or a hang) and
> **differential-tested against upstream z3** across three rounds of fuzzing. A
> full **SMT-LIB 2 front end** drives it (`check-sat(-assuming)`, `get-value`,
> `get-model`, `get-unsat-core`, `push`/`pop`, `define-fun`, …). Still ahead:
> quantifiers, more theories, the fixedpoint/optimization engines, and the C API.
> See [`ROADMAP.md`](ROADMAP.md).
>
> ```sh
> $ z3rs problem.cnf          # DIMACS CNF
> s SATISFIABLE
> v 1 2 3 0
>
> $ z3rs problem.smt2         # SMT-LIB2 (QF_UF/LRA/LIA/AX/BV)
> unsat
> ```

## Why

- **No native dependencies.** `cargo add z3rs` and go — no linking GMP or a C++
  toolchain, no `-sys` crate, works anywhere Rust does (incl. cross-compilation).
- **`no_std` + `alloc`.** The reasoning core runs without the standard library
  (embedded, wasm, kernel); `std` is an opt-in feature for timers/threads/I-O.
- **Memory safety.** A safe Rust surface over an SMT solver.
- **Legibility.** Ported file-by-file from Z3 so the two stay diffable.

## Layout

```
z3rs/
├── Cargo.toml        # package `z3rs`; only dependency is our own `puremp`
├── src/
│   ├── lib.rs        # module tree (mirrors z3/src), dependency-ordered
│   ├── main.rs       # the `z3rs` binary (CLI-compatible with `z3`)
│   ├── util/         # Phase 0: foundation (numerals via `puremp`)
│   ├── math/  ast/  params/          # Phase 1
│   ├── rewriter/                     # Phase 2
│   ├── model/  tactic/               # Phase 3
│   ├── sat/                          # Phase 4
│   ├── nlsat/  smt/                  # Phase 5
│   ├── solver/  cmd_context/         # Phase 6
│   ├── qe/  muz/  opt/               # Phase 7
│   ├── parsers/                      # Phase 8
│   └── api/                          # Phase 9
├── ROADMAP.md        # the master plan
├── PORTING.md        # how we translate C++ → Rust + testing strategy
└── z3/               # upstream Z3 4.17.0 (reference oracle; git-ignored)
```

## Build

```sh
cargo build                    # no_std library + `z3rs` binary
cargo run -- --version
cargo test
cargo build --lib --target thumbv7em-none-eabi   # proves the lib is no_std
```

The library is `no_std` by default. Enable std-backed features with
`--features std`. (The bundled `z3rs` binary links std itself for CLI I/O.)

## License & attribution

MIT. `z3rs` is a derivative work of Z3 (© Microsoft Corporation, MIT-licensed).
Not affiliated with or endorsed by Microsoft. See [`LICENSE`](LICENSE) and
[`NOTICE`](NOTICE).