Struct DeadCodeEliminator 

pub struct DeadCodeEliminator { /* private fields */ }

The dead code elimination pass for TLExpr trees.

Run with DeadCodeEliminator::run for a full fixed-point iteration, or run_pass for a single traversal.

Implementations

impl DeadCodeEliminator

pub fn is_free(&self, var: &str, expr: &TLExpr) -> bool

Returns true if var appears free (as a predicate argument or inside a binder that does not shadow it) anywhere in expr.

Variable occurrences in TLExpr live in two places:

1. Term::Var(name) inside Pred args
2. AllDifferent { variables } variable name lists
3. Any binder (Exists, ForAll, Let, Lambda, LeastFixpoint, etc.) that introduces a new scope — we stop counting the variable as free inside the scope if the binder’s name equals var.

impl DeadCodeEliminator

pub fn count_nodes(expr: &TLExpr) -> u64

Count the total number of nodes in an expression tree.

Every node (leaf or internal) counts as 1.

impl DeadCodeEliminator

pub fn new(config: DceConfig) -> Self

Create a new eliminator with the given configuration.

pub fn with_default() -> Self

Create a new eliminator with default configuration.

pub fn run(&self, expr: TLExpr) -> (TLExpr, DceStats)

Run DCE to a fixed point (or until config.max_passes is reached).

Returns the simplified expression and collected DceStats.

Trait Implementations

impl Default for DeadCodeEliminator

fn default() -> Self

Returns the “default value” for a type.