Module quantifier_opt 

Quantifier optimization pass.

This module provides optimizations for quantified expressions:

• Loop-invariant code motion: Move expressions that don’t depend on the quantified variable outside the quantifier
• Quantifier reordering: Reorder nested quantifiers for better performance
• Quantifier fusion: Merge adjacent same-type quantifiers when possible

Examples

use tensorlogic_compiler::optimize::optimize_quantifiers;
use tensorlogic_ir::{TLExpr, Term};

// Loop invariant: EXISTS x. (a + p(x)) where a doesn't depend on x
// Can be optimized to: a + EXISTS x. p(x)
let a = TLExpr::pred("a", vec![Term::var("i")]);
let px = TLExpr::pred("p", vec![Term::var("x")]);
let expr = TLExpr::exists("x", "D", TLExpr::add(a, px));

let (optimized, stats) = optimize_quantifiers(&expr);
assert!(stats.invariants_hoisted > 0);

Structs

QuantifierOptStats

Statistics from quantifier optimization.

Functions

optimize_quantifiers

Apply quantifier optimizations to an expression.