oxiz 0.3.0

Next-Generation SMT Solver in Pure Rust
Documentation

OxiZ

Next-Generation SMT Solver in Pure Rust

Crates.io Documentation License

Version: 0.3.0 | Status: Meta-crate | Tests: 1

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.

OxiZ tracks honest, non-fabricated parity against a real Z3 binary via bench/z3_parity: 154/168 Correct, 0 Wrong on the extended 19-logic suite as of this writing (16 of 19 logic families are at 100%, including all 8 quickstart-core logics — QF_LIA, QF_LRA, QF_NIA, QF_BV, QF_DT, QF_A, QF_S, QF_FP — now 88/88; three quantified logics, UFLIA/UFLRA/AUFLIA, are not). See the README and CHANGELOG for current status and known limitations before relying on it for production workloads.

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.3.0"  # Default: std + core solver

With specific features:

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

All features:

[dependencies]
oxiz = { version = "0.3.0", 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

Feature Description Default
std Standard library support (core solver requires this for SMT-LIB2 parsing) ✓
nlsat Nonlinear real arithmetic (implies std)
optimization MaxSMT and optimization (implies std)
spacer CHC solver for verification (implies std)
proof Proof generation (implies std)
standard Common features (nlsat + optimization + proof)
full All features (standard + spacer)

Note: the core SAT/theory solver (Solver, TermManager) is always available — it is not gated behind a solver feature.

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

License

Licensed under Apache License 2.0 (LICENSE).