Next-Generation SMT Solver in Pure Rust

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.

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

• 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 with_writer(w) constructors and enable_writer(&mut self, w) methods enable in-memory proof capture via Cursor<Vec<u8>>.

• 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.
• leading_coefficient now delegates to Polynomial::leading_coeff_wrt(var) instead of cloning the full polynomial.
• estimate_derivative_sign fills the univariate stub: uses root isolation for constant-sign detection plus point evaluation.

• ArithSolver::notify_equality now actually enforces x − y = 0 via the simplex tableau.
• ArithSolver::derive_shared_equalities implements sound model-based equality detection (probe-and-pop).
• New simplex_opt module: Simplex::optimize_linexpr 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.

• OptContext::check_sat calls the real oxiz_solver::Solver (was always returning Unknown).
• OptContext::optimize_maxsmt implements selector-variable binary-search MaxSMT encoding.
• OptContext::optimize_single_objective and optimize_pareto delegate to oxiz_solver::Optimizer.
• New OptResult::Unbounded variant; pareto_front() and config() accessors added.

• Bmc::check_bad_at_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.
• extract_model uses Context::eval_in_model for concrete counterexample extraction.

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

• 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

• 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)

• 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

• 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

• QF_DT (Datatypes) - 100.0% (10/10 tests)
  • Constructor exclusivity enforcement
  • Tester predicate evaluation
  • Selector function semantics
  • Cross-variable constraint propagation
  • Enumeration type handling

• QF_A (Arrays) - 100.0% (10/10 tests)
  • Read-over-write axioms
  • Extensionality reasoning
  • Store propagation (101 unit tests)

• 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

• 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

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

• ✅ 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

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.

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)

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

# 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"] }

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

cargo nextest run --all-features

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

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);
    }
}

• 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

• 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)

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

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

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

OxiZ follows a layered CDCL(T) architecture:

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

OxiZ goes beyond Z3 with Rust-native features:

• 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

• 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

1. Enhanced Proof Systems (168% of Z3)

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

2. WebAssembly Optimization

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

3. ML-Guided Heuristics (Alpha)

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

4. Advanced Type Safety

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

5. Developer Experience

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

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

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.assert_term(tm.mk_gt(x, tm.mk_int(0)), tm)
solver.assert_term(tm.mk_eq(tm.mk_add([x, y]), tm.mk_int(10)), tm)

if solver.check_sat(tm) == oxiz.SolverResult.Sat:
    print(solver.get_model(tm))

OxiZ can be compiled to WebAssembly for browser use:

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

Contributions are welcome! Please see our contributing guidelines.

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

Apache-2.0

COOLJAPAN OU (Team KitaSan)

Performance comparison on SMT-LIB benchmarks (preliminary):

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

• Export unintegrated modules
• Fix API compatibility issues
• Complete enhanced MaxSAT solvers

• SMT Integration Layer Enhancement (+40K lines)
• Math Libraries Expansion (+35K lines)
• Quantifier Elimination Expansion (+25K lines)
• Tactics System Expansion (+30K lines)

• ✅ Comprehensive error handling (+20K lines)
• ✅ Trait-based architecture (+25K lines)
• ✅ SIMD & parallel optimizations (+30K lines)
• ✅ Property-based testing (+10K lines)
• ✅ Documentation generation

• ✅ Machine-checkable proof export (Coq/Lean/Isabelle) (+15K lines)
• ✅ WebAssembly optimization (+10K lines)
• ✅ ML-guided heuristics (+15K lines)

• Additional rewriters (+15K lines)
• Muz/Datalog expansion (+40K lines)
• SAT solver enhancements (+25K lines)

This project is inspired by and references the algorithms in:

• Z3 (Microsoft Research) - Primary reference implementation
• CVC5 (Stanford/Iowa) - Theory integration techniques
• MiniSat/Glucose - CDCL SAT solving
• Various academic papers on SMT solving

• "Satisfiability Modulo Theories" (Barrett et al., 2018)
• "Programming Z3" (de Moura & Bjørner, 2008)
• "DPLL(T): Fast Decision Procedures" (Ganzinger et al., 2004)
• "Efficient E-matching for SMT Solvers" (de Moura & Bjørner, 2007)