Hi Rustaceans!

I’m excited to share the first release of OxiZ, a purely Rust-based SMT solver.

Why another SMT solver? Like many of you, I love Z3, but I hate dealing with C++ bindings (FFI), complex build chains, and the difficulty of compiling for WASM or embedded targets. I wanted a solver that I could just add to Cargo.toml and compile anywhere—no system dependencies required.

Key Features of v0.1.1:

• Pure Rust: No C++ code. Zero unsafe blocks (mostly).
• Z3-Compatible API: Designed to look and feel like the Z3 Rust bindings, making migration easier.
• WASM Ready: Runs in the browser or on edge runtimes.
• Core Logic: Implements CDCL (Conflict-Driven Clause Learning) and basic theory solving.

Example Usage: It solves constraints just like you'd expect:

use oxiz::Context;

fn main() {
    let ctx = Context::new();
    let x = ctx.int_const("x");
    let y = ctx.int_const("y");
    
    let solver = ctx.solver();
    // x > 10 AND y < 5 AND x + y = 20
    solver.assert(&x.gt(&ctx.int_val(10)));
    solver.assert(&y.lt(&ctx.int_val(5)));
    solver.assert(&x.add(&y).eq(&ctx.int_val(20)));

    assert_eq!(solver.check(), Status::Satisfiable);
    // Model generation is coming soon!
}

Roadmap: This is still early alpha. We are working on:

• BitVectors and Array theory support.
• Performance optimization (currently focusing on correctness).
• Full SMT-LIB 2 parsing.

I wrote a blog post about the philosophy behind this project (and how it connects to my other projects like physics simulation): [ OxiZ 0.1.1: Why We Are Re-inventing the SMT Solver in Pure Rust (Z3-Compatible SMT Solver)]

I’d love to hear your feedback, and PRs are always welcome!

1 post - 1 participant

Read full topic