z3rs 0.0.2

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

//! # `muz` — Fixedpoint / Datalog / Spacer (Horn clauses)
//!
//! **Port phase 7.** Ported from the Z3 C++ component(s) below.
//! See [`ROADMAP.md`](../../ROADMAP.md) for the porting plan and status.
//!
//! ## Upstream C++ components to port
//! - [ ] `z3/src/muz`
//! - [ ] `z3/src/spacer`
//! - [ ] `z3/src/rel`
//! - [ ] `z3/src/transforms`
//! - [ ] `z3/src/bmc`
//! - [ ] `z3/src/clp`
//! - [ ] `z3/src/tab`
//! - [ ] `z3/src/ddnf`
//! - [ ] `z3/src/dataflow`
//! - [ ] `z3/src/fp`
//!
//! ## Status: SCAFFOLD (no functionality ported yet)

// Submodules will be declared here as components are ported, mirroring the
// upstream file layout (e.g. `pub mod mpz;` for `z3/src/util/mpz.{h,cpp}`).