OxiZ

Next-Generation SMT Solver in Pure Rust

About

OxiZ is a high-performance SMT (Satisfiability Modulo Theories) solver written entirely in Pure Rust, designed to achieve feature parity with Z3 while leveraging Rust's safety, performance, and concurrency features.

🎉 Major Milestone: OxiZ v0.1.3 has achieved 100% correctness parity with Z3 across all 88 benchmark tests spanning 8 core SMT-LIB logics, validating it as a production-ready solver.

Features

• Pure Rust Implementation: No C/C++ dependencies, complete memory safety
• Z3-Compatible: Extensive theory support and familiar API patterns
• High Performance: Optimized SAT core with advanced heuristics
• Modular Design: Use only what you need via feature flags
• SMT-LIB2 Support: Full parser and printer for standard format
• WebAssembly Ready: Run in browsers via WASM bindings

Quick Start

Installation

Add OxiZ to your Cargo.toml:

[dependencies]
oxiz = "0.1.3"  # Default includes solver

With specific features:

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

All features:

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

Basic Usage

use oxiz::{Solver, TermManager, SolverResult};
use num_bigint::BigInt;

let mut solver = Solver::new();
let mut tm = TermManager::new();

// Create variables
let x = tm.mk_var("x", tm.sorts.int_sort);
let y = tm.mk_var("y", tm.sorts.int_sort);

// x + y = 10
let sum = tm.mk_add([x, y]);
let ten = tm.mk_int(BigInt::from(10));
let eq = tm.mk_eq(sum, ten);

// x > 5
let five = tm.mk_int(BigInt::from(5));
let gt = tm.mk_gt(x, five);

// Assert and solve
solver.assert(eq, &mut tm);
solver.assert(gt, &mut tm);

match solver.check(&mut tm) {
    SolverResult::Sat => println!("SAT"),
    SolverResult::Unsat => println!("UNSAT"),
    SolverResult::Unknown => println!("Unknown"),
}

Feature Flags

Theory Support

• EUF: Equality and uninterpreted functions
• LRA: Linear real arithmetic
• LIA: Linear integer arithmetic
• NRA: Nonlinear real arithmetic (with nlsat feature)
• Arrays: Theory of arrays
• BitVectors: Bit-precise reasoning
• Strings: String operations with regex
• Datatypes: Algebraic data types
• Floating-Point: IEEE 754 semantics

Documentation

• API Documentation
• GitHub Repository
• Examples

License

Licensed under Apache License 2.0 (LICENSE).