OxiZ 0.2.2 Released — Real CDCL Internals, Deeper Z3 Compatibility, ML-Guided Branching

The stubs are gone. The internals are real.

Today we released OxiZ 0.2.2 — a maintenance-and-depth release that swaps placeholder solver internals for production CDCL, simplex, and ML machinery, and extends Z3 compatibility so Z3-shaped code ports more directly.

No C. No C++. No Fortran. While Z3 and the rest of the C++ SMT/SAT world drag along their build toolchains, system headers, and ABI quirks, OxiZ ships as a single static Rust binary — or a sub-2MB WASM bundle (against Z3’s ~20MB). The solver that decides your constraints should not be the hardest thing in your dependency graph to build.

Why OxiZ 0.2.2 is a game changer

Z3 is brilliant and battle-tested, but living with it means living with its packaging: a C++ build, an FFI boundary, and a 20MB-class WASM artifact when you try to take it to the browser. Worse, when you want to understand why the solver did what it did — which clauses it kept, which branches it took — you are staring into a C++ engine that was never meant to be read.

0.2.2 is about making the OxiZ engine genuinely competitive on the inside, not just on the build sheet:

• Real LBD (Literal Block Distance) clause scoring now replaces the old stub in the CDCL core. LBD is the modern gold standard for deciding which learned clauses are worth keeping; with real scoring, clause deletion gets smarter and the CDCL loop gets faster on hard instances.
• An LRU lemma cache keeps frequently activated learned clauses hot, so long incremental sessions stop relearning the same facts.
• Big-M primal simplex for LP lands in the simplex solver, giving linear-arithmetic reasoning a proper phase-I/phase-II method instead of a placeholder.
• ML conflict hook + regression-tree predictor wire machine-learned guidance into branching heuristics — the solver learns from conflicts to pick better decision variables.
• Deeper Z3 compatibility: the TacticRegistry is now wired straight into the solver pipeline, FuncInterp is supported in EUF, and the Z3 sort / substitution / pattern APIs (z3_compat_ext2) are in place. Tactic and quantifier code written against Z3 maps over with far less rework.
• Recursive BV term encoding handles nested bit-vector expressions correctly, and structured conflict diagnostics in BvSolver make BV-heavy debugging far less of a guessing game.

None of this came at the cost of correctness. OxiZ 0.2.2 holds 6,735 tests passing at a 100% pass rate and 100% Z3 parity across 88 benchmarks (8/8 logics at 100%). That parity has been the floor since 0.1.3; 0.2.2 builds on top of it.

Technical Deep Dive: where the real work landed

OxiZ 0.2.2 spans 17 crates and 419,576 lines of production Rust. Four layers carry most of this release.

oxiz-sat — the CDCL SAT core. This is the engine room: CDCL with VSIDS, LRB, VMTF, and CHB decision heuristics, two-watched-literals propagation, and DRAT proof logging. In 0.2.2 the LBD score is finally a real Literal Block Distance computation rather than a stub, feeding clause-deletion decisions properly, and the new LRU lemma cache lets the core reuse hot learned clauses across restarts and incremental calls.

oxiz-theories — the theory solvers. EUF, LRA, LIA, BV, Arrays, Strings, FP, and Datatypes live here. 0.2.2 adds FuncInterp support in the EUF solver (so uninterpreted-function models behave the Z3 way) and recursive BV term encoding so nested bit-vector expressions are built and reasoned about without flattening surprises. The structured BV conflict diagnostics also originate in this layer.

oxiz-math + oxiz-solver — arithmetic and orchestration. oxiz-math carries the polynomial, matrix, and LP/simplex machinery; the Big-M primal simplex method and Sylvester-matrix determinant computation for resultant-based reasoning both land here. oxiz-solver is the CDCL(T) brain — orchestration, MBQI for quantifiers, and the TacticRegistry — and 0.2.2 wires LIA heuristic improvements into the solving loop.

oxiz-ml — learned branching. This crate hosts neural-net and regression-tree branching heuristics. In 0.2.2 the regression-tree predictor is wired into the ML branching subsystem and the ML conflict hook feeds back into branch selection, so the solver’s variable choices improve as it sees conflicts.

Around these sit oxiz-core (AST, sorts, the SMT-LIB parser, tactics, rewriters), oxiz-nlsat (CAD, algebraic numbers, resultants), oxiz-opt (MaxSAT/OMT), oxiz-spacer (CHC with PDR/IC3 and BMC), oxiz-proof, oxiz-wasm, oxiz-cli, oxiz-smtcomp, and oxiz-py.

Getting Started

cargo add oxiz

A minimal solve with the builder API:

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"),
}

Prefer SMT-LIB2? The script API (Context::execute_script) is also available, and feature flags (nlsat, optimization, proof, full) unlock nonlinear arithmetic, MaxSMT/OMT, and proof export.

What’s New in 0.2.2

Added

• Recursive BV term encoding for nested bit-vector expressions in BvSolver.
• Enhanced conflict reporting with structured diagnostics in BvSolver.
• Z3 compatibility extensions: TacticRegistry wired to the solver pipeline, FuncInterp support in EUF, and Z3 sort / substitution / pattern APIs (z3_compat_ext2).
• ML conflict hook integration for branching heuristics.
• LRU lemma cache for reuse of frequently activated learned clauses.
• LRU caches in the EUF solver and the simplification layer.
• CLI peak memory reporting.
• CUDA-accelerated computation stubs (feature-gated; the pure-Rust path stays default).

Changed

• Real LBD (Literal Block Distance) scoring replaces the stub implementation in CDCL.
• Big-M primal simplex method for LP in SimplexSolver.
• Sylvester matrix determinant computation for resultant-based reasoning.
• Regression tree predictor wired into the ML branching subsystem.
• Dead proof code removed; a dead-code policy is now enforced across 40+ modules.
• LIA heuristic improvements wired into the solver.

Fixed

• Z3 compatibility layer: sort handling, term substitution, and pattern-matching correctness.
• Production-path dead code warnings eliminated across multiple solver modules.

The CUDA stubs are strictly opt-in behind a feature flag — the default build is 100% pure Rust, and that does not change.

Tips

• Porting from Z3? Reach for the z3_compat_ext2 APIs (sorts, substitution, patterns) together with the now-wired TacticRegistry and FuncInterp in EUF. Tactic pipelines and quantifier/uninterpreted-function code map over with far less hand-translation than before.

• Long incremental sessions benefit most from this release. The LRU lemma cache and real LBD scoring keep useful learned clauses around, so reuse a single Solver across many check() calls rather than rebuilding it:

  let mut solver = Solver::new();
  // assert base constraints once, then push/check/pop per query —
  // the lemma cache carries learned clauses across iterations.
  

• Stay pure Rust by default. CUDA acceleration is an opt-in feature; if you do nothing, you get the pure-Rust path with no C/C++/Fortran in the build.

• BV-heavy formulas now get recursive nested-term encoding plus structured conflict diagnostics in BvSolver — when a bit-vector query goes UNSAT unexpectedly, the structured diagnostics tell you which constraint clashed instead of leaving you to bisect by hand.

• Profiling large queries? Use the CLI’s peak-memory reporting (added in 0.2.2) to see how much memory a query actually consumes before you scale it up.

This is the foundation

OxiZ is the formal-reasoning core of the COOLJAPAN ecosystem. OxiLean, our Lean-4-style theorem prover, uses OxiZ as its SMT proof backend. OxiRS leans on it for Semantic Web validation. Legalis-RS uses OxiZ for legal formal verification, and OxigenAI — our GovTech legal AI — builds on Legalis-RS + OxiZ to bring verified reasoning to government legal work. Underneath, OxiZ itself rides on pure-Rust OxiARC (oxiarc-deflate, oxiarc-brotli) for compression, and shares the ecosystem with OxiBLAS, Oxicode, and OxiFFT. Every layer is C/C++/Fortran-free by default.

Repository: https://github.com/cool-japan/oxiz

Star the repo if you want an SMT solver you can actually read, build anywhere, and ship to the browser. Pure Rust formal reasoning is here — fast, safe, and sovereign.

— KitaSan at COOLJAPAN OÜ June 1, 2026