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
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41

//! Test helpers for Z3 verification tests.

use std::sync::Arc;

use morok_ir::UOp;

use crate::rewrite::graph_rewrite;
use crate::symbolic::symbolic_simple;
use crate::z3::verify::verify_equivalence;

/// Verify that a pattern simplifies correctly and is semantically equivalent.
///
/// This helper:
/// 1. Applies symbolic simplification to the input
/// 2. Verifies the result is semantically equivalent using Z3
/// 3. Returns the simplified expression for further assertions
pub fn verify_simplifies_to(expr: Arc<UOp>, expected: Arc<UOp>) -> Arc<UOp> {
    let matcher = symbolic_simple();
    let simplified = graph_rewrite(&matcher, expr.clone(), &mut ());

    // Verify semantic equivalence
    verify_equivalence(&expr, &simplified).expect("Simplification should preserve semantics");

    // Also check structural equality with expected (optional but helpful for debugging)
    if !Arc::ptr_eq(&simplified, &expected) {
        // If not pointer-equal, they might still be structurally equivalent
        // This is okay - Z3 verification is the source of truth
    }

    simplified
}

/// Verify that simplification preserves semantics (even if structure changes).
pub fn verify_preserves_semantics(expr: Arc<UOp>) -> Arc<UOp> {
    let matcher = symbolic_simple();
    let simplified = graph_rewrite(&matcher, expr.clone(), &mut ());

    verify_equivalence(&expr, &simplified).expect("Simplification should preserve semantics");

    simplified
}