morok-schedule 0.1.0-alpha.2

Optimization passes and pattern engine for the Morok ML compiler
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

//! Z3/SMT verification for symbolic optimizations.
//!
//! This module provides Z3-based verification that pattern rewrites preserve semantics.
//! It follows Tinygrad's architecture but adapted for Rust idioms.

pub mod alu;
pub mod convert;
pub mod verify;

pub use verify::{CounterExample, verify_equivalence};

/// Check if Z3 is available and working.
pub fn is_z3_available() -> bool {
    // Try to create a simple Z3 solver
    std::panic::catch_unwind(|| {
        let _solver = z3::Solver::new();
    })
    .is_ok()
}