Module simplify 

Structural simplification for classical expressions.

This module provides bottom-up algebraic simplification of ClassicalExpr ASTs. Simplification eliminates literal-driven redundancies and structural identities without evaluating runtime variable or value reads.

Rules

• Double negation: not(not(x)) → x
• Identity elements: and(x, true) → x, or(x, false) → x, xor(x, false) → x (and symmetric forms)
• Idempotence: and(x, x) → x, or(x, x) → x
• Self-inverse: xor(x, x) → false
• Complement: and(x, not(x)) → false, or(x, not(x)) → true, xor(x, not(x)) → true
• Comparison reflexivity: eq(x, x) → true, ne(x, x) → false, lt(x, x) → false, gt(x, x) → false, le(x, x) → true, ge(x, x) → true
• Select folding: select(true, a, b) → a, select(false, a, b) → b
• Cast folding: bit_to_bool(BitLiteral(v)) → BoolLiteral(v), bit_vec_to_uint(BitVecLiteral{w, v}) → UIntLiteral(w, v)

Non-goals

• Value-dependent constant folding (e.g. and(x, false) → false removes runtime variable reads and belongs to a higher-level optimization pass)
• Commutation normalization (e.g. and(a, b) → and(b, a))
• Bit-width-aware extract/concat inversion (deferred)

Functions

simplify

Returns a structurally simplified copy of expr.