4 releases
Uses new Rust 2024
| new 0.1.3 | Feb 6, 2026 |
|---|---|
| 0.1.2 | Jan 21, 2026 |
| 0.1.1 | Jan 12, 2026 |
| 0.1.0 | Jan 12, 2026 |
#2666 in Math
Used in 3 crates
(2 directly)
1MB
22K
SLoC
oxiz-math
Mathematical foundations for the OxiZ SMT solver.
Overview
This crate provides Pure Rust implementations of mathematical algorithms required for SMT solving. It serves as the foundation for arithmetic theories (LRA, LIA, NRA, NIA) and optimization.
Modules
| Module | Description | Z3 Reference |
|---|---|---|
simplex |
Simplex algorithm for linear programming | math/simplex/ |
polynomial |
Polynomial arithmetic | math/polynomial/ |
interval |
Interval arithmetic for bounds | math/interval/ |
rational |
Arbitrary precision rationals | - |
grobner |
Gröbner basis computation (planned) | math/grobner/ |
realclosure |
Real closed field arithmetic (planned) | math/realclosure/ |
Usage
use oxiz_math::simplex::Simplex;
use oxiz_math::polynomial::Polynomial;
use oxiz_math::interval::Interval;
Design Principles
- Pure Rust: No C/C++ dependencies
- Generic: Works with various numeric types
- Incremental: Supports incremental updates for SMT integration
- Efficient: Optimized for SMT workloads
License
Apache-2.0
Dependencies
~1.2–2MB
~41K SLoC