feat(math): add tree decompositions domain with width, occurrences, adhesions, reroot, restrict, bag intersection (#1731)

[morluto]

Closes #1731.

Summary

Add the graphs/tree_decompositions domain implementing exact, bounded, deterministic tree-decomposition operations over an immutable well-formed TreeDecomposition value. This is the function-first Jacobian boundary for structural graph reasoning — well-formed tree decompositions and the exact quantities/normal forms derived from them — not treewidth search, threshold solving, or candidate verification.

Design and library choices

The domain uses an exact permutation/orbit kernel over immutable bag/tree-node identities. No treewidth optimization or minimum-width search is performed. Per the issue, these functions support structural graph reasoning and downstream dynamic programs without asking Jacobian to optimize treewidth or certify that a width is minimum.

Representation (values.py). TreeDecomposition binds one source SimpleUndirectedGraph to tree_nodes (unique finite IDs), tree_edges (a finite tree), and bags (exact map tree node -> finite subset of source graph vertices). The constructor admits only values satisfying the four decomposition axioms:

1. the decomposition graph is a tree;
2. every source vertex occurs in at least one bag;
3. every source edge has both endpoints in at least one bag;
4. for each source vertex, the tree nodes whose bags contain it form a connected subtree.

These are value-construction invariants, not a public .check operation. Invalid external JSON is rejected while parsing the value.

Operations (operations.py). All functions are deterministic and complete for accepted values.

• width.compute — bag cardinality per tree node, maximum bag cardinality, width (max bag cardinality minus 1), and maximum-bag node labels. The width of a decomposition supplies an upper bound on graph treewidth only.
• vertex_occurrences.compute — per-source-vertex connected occurrence subtree (node set, induced tree edges, count, leaf/extremal nodes).
• adhesions.compute — per-tree-edge adhesion, maximum adhesion, and size profile. A structural profile of the supplied decomposition, not a minimum-separator computation.
• reroot.compute — same underlying decomposition with parent/children/depth/root-to-node paths. Rerooting does not change the width, bags, or unrooted tree.
• restrict.compute — replace every bag B_t with B_t ∩ S, prune empty/redundant tree nodes, bind to induced G[S]. A direct transformation, not a better-decomposition search.
• bag_intersection_graph.compute — weighted tree with each edge labelled by adhesion set/size and each node by bag size.

Invariances verified by tests

• The width of the path graph decomposition (bags {a,b} and {b,c}) is 1.
• Rerooting to t1 gives parent[t1] = None, children[t1] = (t0,), depth[t1] = 0, depth[t0] = 1.
• The connectedness axiom is rejected when a vertex is in two non-adjacent tree nodes.
• Non-tree edge patterns, unsorted bags, undeclared vertices, vertex-coverage, and edge-coverage violations each produce named obstructions.

Validation

• make check lint + typecheck clean; 16 focused domain tests; all 1138 tests/math, tests/catalog, tests/dispatch tests pass.
• Frozen admission baselines updated (KEEP 239→245, candidates 399→405) and the tree_decompositions schema-snapshot fragment added (6 operations).

Continue this on Linzumi

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.

[morluto]

Review verdict: blocked — restrict can return something that is not a tree decomposition

1. Removing empty internal bags disconnects the decomposition tree

The cleanup deletes empty bags and then retains only original edges whose two endpoints survived. It does not contract/reconnect through a deleted internal node.

A valid counterexample is a three-node decomposition tree t0-t1-t2 of an edgeless graph on {a,b,c} with bags {a}, {b}, {c}. Restricting to {a,c} makes the middle bag empty. This implementation returns two tree nodes and zero tree edges, i.e. a forest, while the operation claims to return a tree decomposition.

Empty-node deletion must contract the tree deterministically (including degree > 2), and the final result should be constructed as an actual TreeDecomposition so all four axioms are replayed. Returning loose dict/tuple fields is currently allowing the invalid structure to escape.

2. Width fails on a valid empty-graph decomposition

SimpleUndirectedGraph admits the empty graph. A one-node tree with one empty bag is a valid decomposition of it. width() then produces max_bag_cardinality = 0 and width = -1, but WidthResult requires cardinality at least 1 and width at least 0, so the public operation raises during result construction. Either explicitly exclude the empty source graph at TreeDecomposition construction, or support the standard empty-decomposition convention consistently (commonly width -1).

3. The adhesion output does not implement its advertised contract

The tool description promises “left/right component vertex coverage after deleting tt'”. adhesions() returns only edge ID, intersection, and size. No component-side coverage is computed or represented. Either implement those fields or remove the claim.

Additional boundary tightening: RestrictRequest.subset should reject duplicates/foreign vertices before execution rather than relying on frozenset() collapse and a native ValueError.

The base TreeDecomposition validator, width for nonempty bags, occurrence subtrees, and reroot traversal otherwise look coherent. The transformation result is the merge blocker.

[morluto]

Deep review summary

Verdict: REQUEST CHANGES — restrict can return a forest rather than a tree decomposition.

1. Deleting an empty internal bag disconnects the decomposition tree

The cleanup removes empty bags and keeps only original edges whose endpoints survive; it never contracts or reconnects through a removed internal node.

Counterexample: a valid tree t0-t1-t2 for an edgeless graph on {a,b,c} with bags {a}, {b}, {c}. Restricting to {a,c} empties the middle bag. The implementation returns two nodes and zero edges, which is a forest, although the operation claims to return a tree decomposition.

Empty-node removal must deterministically contract the tree, including nodes of degree greater than two. Construct the final result as an actual TreeDecomposition so all axioms are replayed; loose dictionaries and tuples currently let invalid output escape.

2. Width fails on a valid empty-graph decomposition

The graph model admits the empty graph. A one-node tree with an empty bag is a valid decomposition. width() produces maximum bag size 0 and width -1, but WidthResult requires size at least 1 and width at least 0, so result construction raises. Either exclude empty source graphs explicitly or consistently support the standard empty-decomposition convention, commonly width -1.

3. Adhesion output does not match its advertised contract

The description promises left/right component vertex coverage after deleting a tree edge, but adhesions() returns only edge ID, intersection, and size. Implement those fields or remove the claim.

Also validate RestrictRequest.subset for duplicate and foreign vertices before execution rather than relying on frozenset() collapse and a native error.