Skip to main content

Crate oxiz_math

Crate oxiz_math 

Source
Expand description

§oxiz-math

Mathematical foundations for the OxiZ SMT solver.

This crate provides Pure Rust implementations of mathematical algorithms required for SMT solving, including:

§Linear Arithmetic

  • Simplex: Dual simplex algorithm for linear programming (LRA theory)
  • Interior Point: Primal-dual interior point method for large-scale LP
  • Matrix: Dense and sparse matrix operations with Gaussian elimination
  • Interval: Interval arithmetic for bound propagation
  • Delta Rational: Support for strict inequalities in simplex
  • BLAS: High-performance BLAS operations for large-scale LP (1000+ variables)

§Non-Linear Arithmetic

  • Polynomial: Multivariate polynomial arithmetic with GCD and factorization
  • Rational Function: Arithmetic on quotients of polynomials (p/q operations)
  • Gröbner: Gröbner basis computation (Buchberger, F4, and F5 algorithms)
  • Real Closure: Algebraic number representation and root isolation
  • Hilbert: Hilbert basis computation for integer cones

§Decision Diagrams

  • BDD: Reduced Ordered Binary Decision Diagrams
  • ZDD: Zero-suppressed BDDs for sparse set representation
  • ADD: Algebraic Decision Diagrams for rational-valued functions

§Numerical Utilities

  • Rational: Arbitrary precision rational arithmetic utilities
  • MPFR: Arbitrary precision floating-point arithmetic (MPFR-like)

§Examples

§Polynomial Arithmetic

use oxiz_math::polynomial::{Polynomial, Var};

// Create polynomial for variable x (index 0)
let x: Var = 0;

// Create polynomial representing just x
let p = Polynomial::from_var(x);

// Compute x * x = x^2
let p_squared = p.clone() * p.clone();

§BDD Operations

use oxiz_math::bdd::BddManager;

let mut mgr = BddManager::new();

// Create variables (VarId is u32)
let x = mgr.variable(0);
let y = mgr.variable(1);

// Compute x AND y
let and_xy = mgr.and(x, y);

// Compute x OR y
let or_xy = mgr.or(x, y);

§BLAS Operations

use oxiz_math::blas::{ddot, dgemv, Transpose};

// Vector dot product
let x = vec![1.0, 2.0, 3.0];
let y = vec![4.0, 5.0, 6.0];
let dot = ddot(&x, &y);
assert_eq!(dot, 32.0);

§Arbitrary Precision Floats

use oxiz_math::mpfr::{ArbitraryFloat, Precision, RoundingMode};

let prec = Precision::new(128);
let a = ArbitraryFloat::from_f64(3.14159, prec);
let b = ArbitraryFloat::from_f64(2.71828, prec);
let sum = a.add(&b, RoundingMode::RoundNearest);

Modules§

algebraic_number
Real Algebraic Numbers.
bdd
Binary Decision Diagrams (BDDs) for efficient boolean function representation.
blas
OxiBLAS: High-Performance BLAS Operations for Large-Scale LP
blas_ops
BLAS abstraction layer for large-scale linear programming.
delta_rational
Delta-rational numbers for handling strict inequalities.
fast_rational
Fast rational number type for Simplex performance.
grobner
Gröbner Basis Computation
hilbert
Hilbert basis computation for integer cones.
interior_point
Interior point method for linear programming.
interval
Interval arithmetic for bound propagation.
lp
Linear Programming and Mixed Integer Programming.
lp_core
Unified LP/MIP Solver
matrix
Dense matrix operations for linear programming and linear algebra.
mpfr
Arbitrary Precision Floating-Point Arithmetic (MPFR-like)
polynomial
Polynomial arithmetic for non-linear theories.
rational
Arbitrary precision rational arithmetic utilities.
rational_function
Rational function arithmetic.
realclosure
Real closure and algebraic number representation.
realclosure_advanced
Advanced Real Closure Operations.
simd
SIMD-Accelerated Mathematical Operations.
simplex
Simplex algorithm for linear arithmetic.
simplex_parametric
Parametric Simplex for Sensitivity Analysis.