11 posts
OxiZ 0.3.2 is a soundness release driven by an external differential-testing report: 8 pull requests, 0 merged, every fix independently reimplemented from scratch and backed by a regression test. EUF congruence, Bool/EUF encoding, Arithmetic⇄EUF combination, and NLSAT conflict analysis are all corrected — 168/168 Correct on the Z3 parity suite, 9,953 tests passing. Pure Rust, Apache-2.0.
OxiZ 0.3.1 is a soundness-and-honesty release: five reported GitHub issues plus 40+ bugs of the same silently-wrong-answer shape are fixed, wide (>64-bit) bit-vectors are now exact via BigUint, and MBQI completeness brings the Z3 differential parity suite to 168/168 Correct, 0 Wrong. 9,668 tests passing. Pure Rust, Apache-2.0.
OxiZ 0.3.0 is a hardening-and-capability wave: a new ground string decision procedure and concrete floating-point model finder lift qf_s and qf_fp from partial to 10/10 on the Z3 parity suite, MBQI SAT certification advances three quantified logics, and a dozen soundness bugs are fixed — 8,119 tests passing, 0 Wrong verdicts across 154 decisive Z3 comparisons. Pure Rust, Apache-2.0.
OxiZ is a high-performance SMT solver in pure Rust — a Z3 replacement. 0.2.4 lands the results of a 19-agent production-readiness audit and five fix waves — real Sturm sequences, sound SAT conflict analysis, honest Cooper QE, corrected BV division — plus new oxiz-py string, floating-point, and quantifier bindings, with 7,666 tests passing workspace-wide.
OxiZ is a high-performance SMT solver in pure Rust — a Z3 replacement. 0.2.3 lands sound incremental BV & Simplex solving, a full term-level MaxSMT/OMT optimization pipeline, real BMC and k-induction model checking, and generic in-memory DRAT/LRAT proof writers — with 6,826 tests passing and 100% Z3 parity.
OxiZ is a pure-Rust SMT solver reimplementing Z3. 0.2.2 ships real LBD clause scoring (replacing the old stub), Big-M primal simplex for LP, an LRU lemma cache, ML conflict-hook branching, and deeper Z3-compat APIs — all with 100% Z3 parity and zero C/C++/Fortran.
OxiZ is a pure-Rust SMT solver and Z3 replacement. 0.2.1 sharpens the EUF (congruence-closure) hot path: reusable allocation buffers, O(k) incremental pop() via a sig_table/fingerprint_table trail, cache-friendly ENode layout, and new production EUF criterion benchmarks. 100% Z3 parity, still pure Rust.
OxiZ 0.2.0 ships an ergonomic EasySolver builder, no_std support for bare-metal/zkVM (RISC-V), a Pure-Rust ML heuristics crate (oxiz-ml), Skolemization, a modular WASM js_api, and 100% Z3 parity across 88 benchmarks. Zero C/C++.
OxiZ 0.1.2 adds PyO3 Python bindings (oxiz-py), a Pure-Rust BLAS + multi-precision (MPFR-style) math layer, an SMT-COMP benchmark suite, and a vastly expanded CLI (dashboard/server/distributed/TPTP/interpolation). A Pure Rust Z3 replacement with zero C/C++.
OxiZ is a Pure Rust Satisfiability Modulo Theories solver reimplementing Z3 — a full CDCL(T) architecture with EUF/LRA/LIA/BV/Arrays/Strings/FP/Datatypes theories, SMT-LIB2 support, and roughly 90% Z3 feature parity, all with zero C/C++. This is its first public release.
OxiZ 0.1.1 ships a new unified `oxiz` meta-crate with feature-flagged modular usage (solver/nlsat/optimization/spacer/proof/full), plus MBQI and CDCL(T) theory-propagation fixes. A Pure Rust Z3 replacement with zero C/C++.