Module rewrite 

Pattern-matching rewrite rules engine for TLExpr transformation.

This module provides a composable, extensible rule engine that applies structural rewrites to tensorlogic_ir::TLExpr trees until a fixed point is reached (no further rules apply).

Design

• Rules implement the RewriteRule trait.
• The RewriteEngine holds a collection of rules and drives iteration.
• Rewrites are applied bottom-up: children are transformed first, then the root node is offered to each rule in order.
• Iteration continues until no rule fires in a full pass (fixed point) or max_iterations is reached.

Built-in rules

Rule struct	Transformation
EliminateDoubleNeg	Not(Not(x)) → x
FlattenNestedAnd	And(And(a,b),c) → And(a,And(b,c))
FlattenNestedOr	Or(Or(a,b),c) → Or(a,Or(b,c))
EliminateAndTrue	And(True,x) / And(x,True) → x
EliminateOrFalse	Or(False,x) / Or(x,False) → x

Example

use tensorlogic_compiler::rewrite::{RewriteEngine, EliminateDoubleNeg};
use tensorlogic_ir::{TLExpr, Term};

let expr = TLExpr::negate(TLExpr::negate(TLExpr::pred("p", vec![Term::var("x")])));

let (result, stats) = RewriteEngine::new()
    .add_rule(Box::new(EliminateDoubleNeg))
    .rewrite(expr);

// Not(Not(p(x))) → p(x)
assert_eq!(stats.total_rewrites, 1);
println!("{}", stats.summary());

Structs

EliminateAndTrue

Identity for conjunction: And(True, x) or And(x, True) → x.

EliminateDoubleNeg

Eliminate double negation: Not(Not(x)) → x.

EliminateOrFalse

Identity for disjunction: Or(False, x) or Or(x, False) → x.

FlattenNestedAnd

Right-associate a left-nested And: And(And(a,b),c) → And(a,And(b,c)).

FlattenNestedOr

Right-associate a left-nested Or: Or(Or(a,b),c) → Or(a,Or(b,c)).

RewriteEngine

Applies a set of RewriteRules to a TLExpr tree until a fixed point.

RewriteStats

Accumulated statistics for a rewrite pass (or the full fixed-point loop).

Traits

RewriteRule

A single pattern-matching rewrite rule.

Functions

builtin_rules

Return one boxed instance of each built-in rule.