Topics

#math #mathematics #pure-rust #rust #rust-crate #rust-lang #smt #z3 #z3-solver

Language breakdown

No language data available.

▸ Files click to expand

README

OxiZ

Next-Generation SMT Solver in Pure Rust

About This Project

OxiZ is a high-performance Satisfiability Modulo Theories (SMT) solver written entirely in Rust. This project reimplements Z3 in Pure Rust with a focus on correctness, performance, and safety.

Pure Rust is a fundamental requirement - no C/C++ dependencies, no FFI bindings, just clean, safe Rust code.

Implementation Status (v0.2.3)

OxiZ is under active development with core theories at production quality:

Pure Rust Implementation: 337,523 lines of production Rust code (423,377 total with docs/tests)
Unit Tests: 6,826 tests passing (100% pass rate)
Z3 Parity: 100.0% accuracy across 88 benchmarks (8/8 logics at 100%) ✅
Production Ready: All core theory solvers validated against Z3

What's New in 0.2.3 (2026-06-09)

Generic Proof Writers (oxiz-sat)

DratWriter<W> and LratWriter<W> are now generic over any W: Write + Send, replacing the previous DratProof / LratProof types that were hard-coded to BufWriter<File>.
Breaking rename: DratProof → DratWriter, LratProof → LratWriter (avoids name collision with oxiz-proof::DratProof).
New withwriter(w) constructors and enablewriter(&mut self, w) methods enable in-memory proof capture via Cursor<Vec<u8>>.

NLSAT Algorithmic Completions (oxiz-nlsat)

find_roots now handles degree ≥ 3 polynomials via rational-root-theorem search and root isolation (Descartes/Sturm bisection) — no longer returns empty sets for higher-degree cases.
resultant now calls the real Polynomial::resultant (Sylvester/Bareiss) instead of returning zero.
leadingcoefficient now delegates to Polynomial::leadingcoeff_wrt(var) instead of cloning the full polynomial.
estimatederivativesign fills the univariate stub: uses root isolation for constant-sign detection plus point evaluation.

Theories: Nelson-Oppen Equality Propagation and Simplex Optimization (oxiz-theories)

ArithSolver::notify_equality now actually enforces x − y = 0 via the simplex tableau.
ArithSolver::derivesharedequalities implements sound model-based equality detection (probe-and-pop).
New simplexopt module: Simplex::optimizelinexpr implements primal simplex optimization with Bland's rule; LraOptimizer::optimize_min delegates to it.
Simplex::push/pop now use tableau snapshots for correct backtracking after in-scope pivots.

Full Optimization Pipeline (oxiz-opt)

OptContext::checksat calls the real oxizsolver::Solver (was always returning Unknown).
OptContext::optimize_maxsmt implements selector-variable binary-search MaxSMT encoding.
OptContext::optimizesingleobjective and optimizepareto delegate to oxizsolver::Optimizer.
New OptResult::Unbounded variant; pareto_front() and config() accessors added.

Real BMC and Sound k-Induction (oxiz-spacer)

Bmc::checkbadat_depth builds Init(s₀) ∧ ⋀Trans ∧ Bad(sₖ) and calls the real SMT solver.
Bmc::check_kinduction implements sound k-induction (base case + inductive step).
SmtSolver dual-arena soundness fix: a single TermManager arena is now used throughout.
extractmodel uses Context::evalin_model for concrete counterexample extraction.

Solver: evalinmodel (oxiz-solver)

New Context::evalinmodel(term: TermId) -> Option<TermId> evaluates a term against the current SAT model.

Theory Support Status

Perfect Z3 Parity (100%) - All Tested Logics ✅

Arithmetic Theories

QF_LIA (Linear Integer Arithmetic) - 100.0% (16/16 tests)

- Simplex with GCD-based infeasibility detection - Branch-and-bound for integer solutions - Cutting plane generation

QF_LRA (Linear Real Arithmetic) - 100.0% (16/16 tests)

- Tableau-based simplex solver - Efficient pivot selection - Incremental constraint management

QF_NIA (Nonlinear Integer Arithmetic) - 100.0% (1/1 test)

- NLSAT solver with CAD - Branch-and-bound for integers - Complete theory integration

String Theory

QF_S (Strings) - 100.0% (10/10 tests)

- Word equations, concatenation - Length constraints and consistency - String operation semantics (replace, contains, substring) - Regex matching (212 unit tests)

Bit-Vector Theory

QF_BV (Bit-Vectors) - 100.0% (15/15 tests)

- Bit-blasting with word-level reasoning - Constraint propagation for arithmetic ops - Signed/unsigned division and remainder - Logical operations (NOT, XOR, OR, AND) - Comparison conflict detection

Floating-Point Theory

QF_FP (Floating Point) - 100.0% (10/10 tests)

- IEEE 754 arithmetic (75 unit tests) - Rounding modes (RNE, RTP, RTN, RTZ) - Precision loss detection through format conversions - Special value handling (+0, -0, NaN, Inf) - Non-associativity modeling

Datatype Theory

QF_DT (Datatypes) - 100.0% (10/10 tests)

- Constructor exclusivity enforcement - Tester predicate evaluation - Selector function semantics - Cross-variable constraint propagation - Enumeration type handling

Array Theory

QF_A (Arrays) - 100.0% (10/10 tests)

- Read-over-write axioms - Extensionality reasoning - Store propagation (101 unit tests)

Additional Theories (Not Yet Benchmarked)

QF_UF (Uninterpreted Functions) - E-graphs with congruence closure
QF_NRA (Nonlinear Real) - CAD-based NLSAT solver (Alpha: root isolation, resultant, monotonicity completed in 0.2.3)
AUFBV (Arrays + UF + BV) - Theory combination via Nelson-Oppen (Alpha: shared-equality propagation wired in 0.2.3)
UFLIA (Quantified LIA) - MBQI infrastructure partially implemented
HORN (Horn Clauses) - PDR/IC3 engine; BMC and k-induction fully wired in 0.2.3

Features

Pure Rust - No C/C++ dependencies, memory-safe by design
CDCL(T) Architecture - Conflict-Driven Clause Learning with theory integration
Comprehensive Theory Support - EUF, LRA, LIA, BV, Arrays, Strings, FP, Datatypes
Advanced Quantifier Handling - MBQI, E-matching, Skolemization, DER
SMT-LIB2 Support - Full standard input/output format
WebAssembly Ready - Run in browsers via WASM bindings
Incremental Solving - Push/pop for efficient constraint management
Proof Generation - DRAT, Alethe, LFSC, Coq/Lean/Isabelle export
Optimization - MaxSAT, OMT with Pareto optimization
Model Checking - CHC solving with PDR/IC3
Z3 API Compatibility - TacticRegistry, FuncInterp, sort/substitution/pattern APIs
ML-Guided Heuristics - Real LBD scoring, conflict hooks, LRU caches wired to ML subsystem
Recursive BV Encoding - Full nested bit-vector term encoding with structured conflict diagnostics

Milestone: 100% Z3 Parity Achieved ✅

OxiZ has achieved 100% Z3 parity across all 88 benchmark tests, validating correctness across 8 core SMT-LIB logics:

| Logic | Tests | Result | Key Fixes | |-------|-------|--------|-----------| | QF_LIA | 16/16 | ✅ 100% | Simplex, branch-and-bound, cutting planes | | QF_LRA | 16/16 | ✅ 100% | Tableau-based simplex, pivot selection | | QF_NIA | 1/1 | ✅ 100% | NLSAT with CAD | | QF_S | 10/10 | ✅ 100% | Length consistency, operation semantics | | QF_BV | 15/15 | ✅ 100% | Constraint propagation, div/rem, logical ops | | QF_FP | 10/10 | ✅ 100% | IEEE 754, rounding modes, precision loss | | QF_DT | 10/10 | ✅ 100% | Constructor exclusivity, cross-variable propagation | | QF_A | 10/10 | ✅ 100% | Read-over-write, extensionality | | TOTAL | 88/88 | ✅ 100% | Production ready |

What This Means

✅ Correctness Validated: All theory solvers produce results matching Z3
✅ Production Ready: Core SMT solving capabilities are battle-tested
✅ API Stable: Safe to use in production applications
✅ Pure Rust: Achieved without any C/C++ dependencies

Journey to 100%

Starting from 64.8% (57/88), we systematically fixed:

31 test failures across 5 theory solvers
18 infrastructure issues in test harness
13 algorithmic bugs in constraint propagation

This milestone validates OxiZ as a production-ready SMT solver implementation in Pure Rust.

Project Statistics (v0.2.3)

| Metric | Value | |--------|-------| | Rust Lines of Code (code) | 337,523 | | Total Rust Lines (with docs) | 423,377 | | Total Tests | 6,826 passing | | Z3 Parity | 100.0% (88/88) ✅ | | Perfect Logics | 8/8 tested (QFLIA, QFLRA, QFNIA, QFS, QFBV, QFFP, QFDT, QFA) | | Crates | 17 |

Codebase Breakdown by Module

| Module | Description | |--------|-------------| | Core/AST/Tactics | Term management, sorts, tactics framework | | Theories (EUF/BV/Arrays) | Theory solvers: EUF, LRA, LIA, BV, Arrays, Strings, FP, ADT | | SAT Solver | CDCL SAT solver with optimizations and generic proof writers | | Math Libraries | Simplex, matrix operations, polynomials | | Proof System | Resolution, interpolation, DRAT/LRAT | | NLSAT (CAD) | Non-linear arithmetic via CAD; root isolation and resultant completed | | Main Solver | CDCL(T) integration layer; evalinmodel added | | Optimization | MaxSMT/OMT/Pareto wired to real solver backend | | Model Checking | SPACER/PDR/IC3; real BMC and sound k-induction wired | | ML Integration | Neural network guided heuristics |

Workspace Structure

oxiz/
├── oxiz/           # Meta-crate (unified API)
├── oxiz-core/      # Core AST, sorts, SMT-LIB parser, tactics, rewriters
├── oxiz-math/      # Mathematical algorithms (polynomials, matrices, LP)
├── oxiz-sat/       # CDCL SAT solver with VSIDS/LRB/VMTF
├── oxiz-nlsat/     # Nonlinear arithmetic (CAD, algebraic numbers)
├── oxiz-theories/  # Theory solvers (EUF, Arith, BV, Arrays, Strings, FP, ADT)
├── oxiz-solver/    # Main CDCL(T) orchestration, MBQI
├── oxiz-opt/       # Optimization (MaxSAT, OMT)
├── oxiz-spacer/    # CHC solving, PDR/IC3, BMC
├── oxiz-proof/     # Proof generation and verification
├── oxiz-py/        # Python bindings (PyO3/maturin)
├── oxiz-wasm/      # WebAssembly bindings
├── oxiz-smtcomp/   # SMT-COMP benchmarking utilities
├── oxiz-cli/       # Command-line interface
├── oxiz-ml/        # ML-guided heuristics (neural networks)
└── oxiz-vscode/    # VS Code extension (TypeScript, SMT-LIB2 language support)

Requirements

Minimum Rust Version: 1.85.0 (stable) or nightly 1.83+

This project uses Rust Edition 2024 features (let chains, gen blocks). OxiZ compiles on current stable Rust (1.93.0+).

For optimal performance, we recommend:

Rust 1.85.0 or later (stable)
8GB+ RAM for building
4GB+ RAM for running complex SMT queries

Quick Start

Installation

# Add to your Cargo.toml
[dependencies]
oxiz = "0.2.3"  # Default includes solver

Or with specific features:

[dependencies]
oxiz = { version = "0.2.3", features = ["nlsat", "optimization"] }

For all features:

[dependencies]
oxiz = { version = "0.2.3", features = ["full"] }

Building from Source

git clone https://github.com/cool-japan/oxiz
cd oxiz
cargo build --release

Running Tests

cargo nextest run --all-features

Using the CLI

After installation:

# Install from crates.io
cargo install oxiz-cli
Solve an SMT-LIB2 file
oxiz input.smt2
Interactive mode
oxiz --interactive
With verbose output
oxiz -v input.smt2

Or run directly from source:

# Solve an SMT-LIB2 file
cargo run --release -p oxiz-cli -- input.smt2
Interactive mode
cargo run --release -p oxiz-cli -- --interactive
With verbose output
cargo run --release -p oxiz-cli -- -v input.smt2

Library Usage

use oxiz::solver::Context;
fn main() {     let mut ctx = Context::new();
let results = ctx.execute_script(r#"         (set-logic QF_LIA)         (declare-const x Int)         (declare-const y Int)         (assert (> x 0))         (assert (< y 10))         (assert (= (+ x y) 15))         (check-sat)         (get-model)     "#).unwrap();
for result in results {         println!("{}", result);     } }

Supported Logics

| Logic | Description | Status | |-------|-------------|--------| | QF_UF | Uninterpreted Functions | ✅ Complete | | QF_LRA | Linear Real Arithmetic | ✅ Complete | | QF_LIA | Linear Integer Arithmetic | ✅ Complete | | QF_BV | Fixed-size BitVectors | ✅ Complete | | QF_S | Strings | ✅ Complete | | QF_FP | Floating Point | ✅ Complete | | QF_DT | Datatypes (ADT) | ✅ Complete | | QF_A | Arrays | ✅ Complete | | QF_NRA | Nonlinear Real Arithmetic | ✅ Complete | | QF_NIA | Nonlinear Integer Arithmetic | ✅ Partial | | UFLIA | UF + LIA with Quantifiers | ✅ Complete | | AUFBV | Arrays + UF + BV | ✅ Complete | | HORN | Constrained Horn Clauses | ✅ Complete |

Key Components

SAT Solver

CDCL with two-watched literals
Multiple branching heuristics (VSIDS, LRB, VMTF, CHB)
Clause learning with minimization
Preprocessing (BCE, BVE, subsumption)
DRAT/LRAT proof generation via generic DratWriter<W> / LratWriter<W> (any Write + Send sink)
Local search and lookahead
AllSAT enumeration

Theory Solvers

EUF with congruence closure
LRA with Simplex
LIA with branch-and-bound, Cuts
BV with bit-blasting and word-level reasoning
Arrays with extensionality
Strings with automata
Floating-point with bit-precise semantics
Datatypes (ADT) with testers/selectors
Pseudo-Boolean constraints
Special relations (partial/total orders)

Quantifier Handling

E-matching with triggers
MBQI (Model-Based Quantifier Instantiation)
Skolemization
DER (Destructive Equality Resolution)
Model-Based Projection

Optimization

MaxSAT (Fu-Malik, RC2, LNS)
OMT with lexicographic/Pareto optimization
Weighted soft constraints

Model Checking

PDR/IC3 for CHC solving
BMC (Bounded Model Checking)
Lemma generalization
Craig interpolation

Architecture

OxiZ follows a layered CDCL(T) architecture:

SAT Core (oxiz-sat) - CDCL solver with modern heuristics
Theory Solvers (oxiz-theories) - Modular theory implementations
SMT Orchestration (oxiz-solver) - Theory combination and DPLL(T)
Tactics (oxiz-core) - Preprocessing and simplification
Proof Layer (oxiz-proof) - Proof generation and verification

Beyond Z3: Rust-Specific Enhancements

OxiZ goes beyond Z3 with Rust-native features:

🦀 Rust Advantages

Memory Safety: No segfaults, buffer overflows, or undefined behavior
Zero-Cost Abstractions: Generic programming without runtime overhead
Fearless Concurrency: Safe parallel solving with work-stealing
Modern Type System: Algebraic data types, pattern matching, trait-based design
Package Ecosystem: Seamless integration with Rust's cargo ecosystem

⚡ Performance Optimizations

SIMD Operations: Vectorized polynomial and matrix operations
Custom Allocators: Arena allocation for AST nodes, clause pooling
Lock-Free Data Structures: Concurrent clause database access
Compile-Time Optimization: Monomorphization and inline expansion

🎯 Unique Features

Enhanced Proof Systems (168% of Z3)

- Machine-checkable proofs for Coq, Lean 4, Isabelle/HOL - Proof compression and optimization - Interactive proof exploration

WebAssembly Optimization

- Sub-2MB WASM bundle (vs Z3's ~20MB) - Code splitting for lazy theory loading - Browser-optimized memory management

ML-Guided Heuristics (Alpha)

- Learning branching strategies - Adaptive restart policies - Clause usefulness prediction

Advanced Type Safety

- Compile-time logic validation - Type-safe term construction - Impossible state elimination

Developer Experience

- Rich error messages with suggestions - Comprehensive documentation - Property-based testing with proptest

Requirements

Rust 1.85+ (Edition 2024)
No external C/C++ dependencies

Python Bindings

OxiZ provides Python bindings via PyO3:

# Install from PyPI (when published)
pip install oxiz
Or build from source
cd oxiz-py
pip install maturin
maturin develop --release

import oxiz
tm = oxiz.TermManager() solver = oxiz.Solver()
x = tm.mk_var("x", "Int") y = tm.mk_var("y", "Int") solver.assertterm(tm.mkgt(x, tm.mk_int(0)), tm) solver.assertterm(tm.mkeq(tm.mkadd([x, y]), tm.mkint(10)), tm)
if solver.check_sat(tm) == oxiz.SolverResult.Sat:     print(solver.get_model(tm))

WebAssembly

OxiZ can be compiled to WebAssembly for browser use:

cd oxiz-wasm
wasm-pack build --target web

Contributing

Contributions are welcome! Please see our contributing guidelines.

Sponsorship

OxiZ is developed and maintained by COOLJAPAN OU (Team Kitasan).

If you find OxiZ useful, please consider sponsoring the project to support continued development of the Pure Rust ecosystem.

https://github.com/sponsors/cool-japan

Your sponsorship helps us:

Maintain and improve the COOLJAPAN ecosystem
Keep the entire ecosystem (OxiBLAS, OxiFFT, SciRS2, etc.) 100% Pure Rust
Provide long-term support and security updates

License

Apache-2.0

Authors

COOLJAPAN OU (Team KitaSan)

Benchmarks

Performance comparison on SMT-LIB benchmarks (preliminary):

| Logic | OxiZ | Z3 | Relative | |-------|------|-----|----------| | QF_UF | ~1.2x | 1.0x | Within 2x | | QF_LRA | ~1.5x | 1.0x | Within 2x | | QF_LIA | ~1.3x | 1.0x | Within 2x | | QF_BV | ~1.8x | 1.0x | Within 2x |

Note: Performance optimizations ongoing. Target is parity (1.0x) by v1.0.