Expand description
E-graph encoding for layout constraint optimization.
Maps layout constraints to an expression language that can be optimized via equality saturation. The key insight: many equivalent layout configurations exist for a given constraint set; an e-graph compactly represents all of them and extracts the cheapest one.
§Expression Language
Expr ::= Num(u16) -- concrete pixel value
| Var(NodeId) -- widget reference
| Add(Expr, Expr) -- constraint arithmetic
| Sub(Expr, Expr)
| Max(Expr, Expr)
| Min(Expr, Expr)
| Div(Expr, Expr)
| Mul(Expr, Expr)
| HFlex(Vec<Expr>) -- horizontal flex container
| VFlex(Vec<Expr>) -- vertical flex container
| Clamp(min, max, Expr) -- size clamping
| Fill(Expr) -- fill remaining space§Rewrite Rules
Add(a, Num(0)) => a -- identity
Max(a, a) => a -- idempotent
Min(a, a) => a -- idempotent
Add(a, b) => Add(b, a) -- commutative
Max(a, b) => Max(b, a) -- commutative
Min(a, b) => Min(b, a) -- commutative
Add(Add(a, b), c) => Add(a, Add(b, c)) -- associative
Clamp(0, MAX, a) => a -- unclamped
HFlex(a, HFlex(b, c)) => HFlex(a, b, c) -- flatten nested (when weights allow)§Example
use ftui_layout::egraph::*;
let mut graph = EGraph::new();
let a = graph.add(Expr::Num(100));
let b = graph.add(Expr::Num(0));
let sum = graph.add(Expr::Add(a, b));
graph.apply_rules();
// After saturation: sum is equivalent to a (Add(x, 0) => x)
assert!(graph.equiv(sum, a));Structs§
- EGraph
- An equivalence graph for layout expressions.
- Evidence
Record - A structured evidence record for a saturation run, serializable to JSONL.
- Id
- An identifier for an equivalence class in the e-graph.
- NodeId
- A widget node identifier for layout references.
- Saturation
Config - Configuration for equality saturation.
- Saturation
Result - Result of an equality saturation run.
Enums§
- Expr
- A layout expression in the e-graph.
- Guard
Triggered - Which guard triggered early termination, if any.
Functions§
- encode_
constraint - Encode a layout constraint as an e-graph expression.
- encode_
flex - Encode a flex layout as an e-graph expression.
- solve_
layout - Solve a set of layout constraints via equality saturation.
- solve_
layout_ default - Solve layout with default configuration.