oxiz-math
| Crates.io | oxiz-math |
| lib.rs | oxiz-math |
| version | 0.1.2 |
| created_at | 2026-01-12 04:23:57.094526+00 |
| updated_at | 2026-01-21 05:18:07.300368+00 |
| description | Mathematical foundations for OxiZ SMT solver |
| homepage | |
| repository | https://github.com/cool-japan/oxiz |
| max_upload_size | |
| id | 2036987 |
| size | 711,864 |
KitaSan (cool-japan)
documentation
README
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
MIT OR Apache-2.0