ordeal 0.12.0

Ordeal — a specialized, certificate-checked QF_BV SMT solver for the PulseEngine toolchain.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

//! Bit-blasting rules: each QF_BV operation lowered to AIG gates
//! (DES-005..DES-009), one module per op family.
//!
//! Words are LSB-first [`Word`](crate::aig::Word)s. Every rule is verified
//! against the concrete evaluator (DES-001): exhaustively at width 8,
//! randomized at widths 32/64. A rule that has not passed its UV measure is
//! not enabled in the pipeline (the P1 kill criterion).

pub mod arith;
pub mod bitwise;
pub mod muldiv;
pub mod shift;
pub mod structural;

/// Kani proofs of blaster ⇄ evaluator equivalence (FEAT-004 / P4).
#[cfg(kani)]
mod proofs;