Skip to main content

optimize_quantifiers

Function optimize_quantifiers 

Source
pub fn optimize_quantifiers(expr: &TLExpr) -> (TLExpr, QuantifierOptStats)
Expand description

Apply quantifier optimizations to an expression.

This pass hoists loop-invariant expressions and optimizes quantifier nesting when beneficial.

§Arguments

  • expr - The expression to optimize

§Returns

A tuple of (optimized expression, statistics)