From 93672349064dfd35c819c6e33de85927dae1df97 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Thu, 2 Apr 2026 17:15:07 +0100
Subject: [PATCH 01/25] region decomp groupping and viz

---
 .../src/imandrax_api_models/region_decomp.py  | 188 ++++++++++++++++++
 1 file changed, 188 insertions(+)
 create mode 100644 packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
new file mode 100644
index 00000000..8b01040c
--- /dev/null
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -0,0 +1,188 @@
+"""Post-processing (Hierarchical groupping) for region decomposition."""
+
+# %%
+from __future__ import annotations
+
+from dataclasses import dataclass
+from functools import reduce
+from typing import NoReturn, TypedDict
+
+from imandrax_api.lib import RegionStr
+from rich.console import Console, RenderableType
+from rich.text import Text
+from rich.tree import Tree
+
+
+@dataclass
+class RegionGroup:
+    rg_constraints: list[str]
+    rg_label_path: list[int]
+    rg_region: RegionStr | None
+    rg_children: list[RegionGroup]
+    rg_weight: int
+
+
+def group_regions(regions: list[RegionStr]) -> list[RegionGroup]:
+    return _loop_group_regions([], [], regions)
+
+
+def _loop_group_regions(
+    idx_path: list[int], constraint_path: list[str], regions: list[RegionStr]
+) -> list[RegionGroup]:
+    def raise_(exc: BaseException) -> NoReturn:
+        raise exc
+
+    # all_constraints_with_dup
+    constraints_: list[list[str]] = [
+        (
+            r.constraints_str
+            if r.constraints_str
+            else raise_(ValueError(f'Region {r} has no constraint string'))
+        )
+        for r in regions
+    ]
+    constraints: list[str] = [c for cs in constraints_ for c in cs]
+    all_constraints_with_dup: list[str] = [
+        c for c in constraints if c not in constraint_path
+    ]
+
+    # constraints_by_most_frequent
+    def mk_counter(ls: list[str]) -> dict[str, int]:
+        counter: dict[str, int] = {}
+
+        def update_counter(s: str) -> None:
+            curr_count = counter.get(s)
+            if curr_count is None:
+                counter[s] = 1
+            else:
+                counter[s] = curr_count + 1
+
+        for s in ls:
+            update_counter(s)
+        return counter
+
+    counter = mk_counter(all_constraints_with_dup)
+    assoc_list: list[tuple[str, int]] = [(k, v) for (k, v) in counter.items()]
+    sorted(assoc_list, key=lambda kv: kv[1], reverse=True)
+    constraints_by_most_frequent: list[str] = [kv[0] for kv in assoc_list]
+
+    # grouped: tuple[list[RegionGroup], list[RegionStr]]
+    class Acc(TypedDict):
+        groups: list[RegionGroup]
+        regions: list[RegionStr]
+        idx_path: list[int]
+        constraint_path: list[str]
+
+    def loop(
+        # 'acc
+        acc: Acc,
+        # groups: list[RegionGroup],
+        # regions: list[RegionStr],
+        # idx_path: list[int],
+        # constraint_path: list[str],
+        # 'a
+        konstraint: str,
+    ) -> Acc:
+        # ) -> tuple[list[RegionGroup], list[RegionStr], list[int], list[str]]:
+        groups = acc['groups']
+        regions = acc['regions']
+        idx_path = acc['idx_path']
+        constraint_path = acc['constraint_path']
+
+        has: list[RegionStr] = []
+        without: list[RegionStr] = []
+        for r in regions:
+            assert r.constraints_str, 'region has no constraint_str'
+            if konstraint in r.constraints_str:
+                has.append(r)
+            else:
+                without.append(r)
+        i = len(groups) + 1
+        if len(without) == 0 and (not (len(has) == 1)):
+            new_idx_path = idx_path
+        else:
+            new_idx_path: list[int] = [i, *idx_path]
+        new_constraint_path: list[str] = [konstraint, *constraint_path]
+
+        if len(has) > 0:
+            rg_children = _loop_group_regions(new_idx_path, new_constraint_path, has)
+            group: RegionGroup
+            if len(rg_children) == 1:
+                group = rg_children[0]
+            else:
+                rg_constraints = new_constraint_path[::-1]
+                rg_region: RegionStr | None
+                if len(has) == 1:
+                    rg_region = has[0]
+                else:
+                    rg_region = None
+                rg_weight = len(has)
+                group = RegionGroup(
+                    rg_constraints=rg_constraints,
+                    rg_region=rg_region,
+                    rg_children=rg_children,
+                    rg_label_path=new_idx_path,
+                    rg_weight=rg_weight,
+                )
+            res = [group, *groups], without
+        else:
+            res = groups, without
+        return Acc(
+            groups=res[0],
+            regions=res[1],
+            idx_path=new_idx_path,
+            constraint_path=new_constraint_path,
+        )
+
+    init = Acc(
+        groups=[], regions=regions, idx_path=idx_path, constraint_path=constraint_path
+    )
+    return reduce(loop, constraints_by_most_frequent, init)['groups']
+
+
+def renderable_of_rg(rg: RegionGroup):
+    buf = ''
+    buf += f'{rg.rg_label_path}'
+    buf += f'; {len(rg.rg_constraints)} constraints'
+    n_children = len(rg.rg_children)
+    if n_children != 0:
+        buf += f', {n_children} children'
+    return buf
+
+
+def rich_tree_of_groups(region_groups: list[RegionGroup]) -> Tree:
+
+    def add_children(tree: Tree, region_groups: list[RegionGroup]) -> Tree:
+        top_regions: list[tuple[Tree, RegionGroup]] = [
+            (tree.add(renderable_of_rg(rg)), rg) for rg in region_groups
+        ]
+
+        for tree, rg in top_regions:
+            add_children(tree, rg.rg_children)
+        return tree
+
+    root = Tree('Region Decomposition')
+
+    return add_children(root, region_groups)
+
+
+def str_of_renderables(
+    *renderables: RenderableType | object,
+    plain: bool = True,
+) -> str:
+    console = Console(
+        record=True,
+        width=80,
+        color_system='standard',
+        force_terminal=False,
+        force_interactive=False,
+        force_jupyter=False,
+    )
+    with console.capture() as capture:
+        for renderable in renderables:
+            console.print(renderable)
+    exported_text = capture.get()
+    if plain:
+        return Text.from_ansi(exported_text).plain
+    else:
+        return exported_text

From ec941bd54751bf65876845e713538da03561f4a9 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Tue, 7 Apr 2026 14:15:12 +0100
Subject: [PATCH 02/25] descendant region count

---
 .../src/imandrax_api_models/region_decomp.py                  | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index 8b01040c..c92d962c 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -21,8 +21,12 @@ class RegionGroup:
     rg_children: list[RegionGroup]
     rg_weight: int
 
+    def n_descendant_regions(self) -> int:
+        return sum(c.n_descendant_regions() for c in self.rg_children)
+
 
 def group_regions(regions: list[RegionStr]) -> list[RegionGroup]:
+    """Group regions hierarchically based on constraints."""
     return _loop_group_regions([], [], regions)
 
 

From fdc6c1c3634db213d5bebbe76713847e0cdca266 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Tue, 7 Apr 2026 14:52:24 +0100
Subject: [PATCH 03/25] CHORE

---
 packages/imandrax-api-models/pyproject.toml | 25 ++++++++++++---------
 1 file changed, 14 insertions(+), 11 deletions(-)

diff --git a/packages/imandrax-api-models/pyproject.toml b/packages/imandrax-api-models/pyproject.toml
index 1851e83e..c579b770 100644
--- a/packages/imandrax-api-models/pyproject.toml
+++ b/packages/imandrax-api-models/pyproject.toml
@@ -55,20 +55,23 @@ flake8-quotes = { inline-quotes = "single", multiline-quotes = "double" }
 mccabe = { max-complexity = 15 }
 ignore = [
   "SIM103",  # needless-bool
-  "SIM108", # if-else-block-instead-of-if-exp
-  "N801",   # Class name should use CapWords
+  "SIM108",  # if-else-block-instead-of-if-exp
+  "N801",  # Class name should use CapWords
   "PTH123", # `open()` should be replaced by `Path.open()`
-  "C417",   # Unnecessary `map()` usage (rewrite using a generator expression)
-  "D100", # ignore missing docstring in module
-  "D101", # ignore missing docstring in public class
-  "D102", # ignore missing docstring in public method
-  "D103", # ignore missing docstring in public function
-  "D104", # ignore missing docstring in public package
-  "D105", # ignore missing docstring in magic methods
-  "D106", # ignore missing docstring in public nested class
-  "D107", # ignore missing docstring in __init__ methods
+  "C417",  # Unnecessary `map()` usage (rewrite using a generator expression)
+  "D100",  # ignore missing docstring in module
+  "D101",  # ignore missing docstring in public class
+  "D102",  # ignore missing docstring in public method
+  "D103",  # ignore missing docstring in public function
+  "D104",  # ignore missing docstring in public package
+  "D105",  # ignore missing docstring in magic methods
+  "D106",  # ignore missing docstring in public nested class
+  "D107",  # ignore missing docstring in __init__ methods
   "D203",
   "D212",
+  "D400",
+  "D415",
+  "E741",  # Ambigous variable name
   # These are all enforced by, or incompatible with, the ruff formatter:
   "E203",
   "E501",

From 2dfefc3e6194130f8818491b4175e722b757336a Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Tue, 7 Apr 2026 14:57:21 +0100
Subject: [PATCH 04/25] show descendant

---
 .../src/imandrax_api_models/region_decomp.py      | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index c92d962c..2bbadf05 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -144,13 +144,24 @@ def loop(
     return reduce(loop, constraints_by_most_frequent, init)['groups']
 
 
-def renderable_of_rg(rg: RegionGroup):
+# Show
+# ====================
+
+
+def renderable_of_rg(rg: RegionGroup) -> str:
     buf = ''
-    buf += f'{rg.rg_label_path}'
+    buf += f'[{",".join([str(i) for i in rg.rg_label_path])}]'
     buf += f'; {len(rg.rg_constraints)} constraints'
     n_children = len(rg.rg_children)
+    n_descendants = rg.n_descendant_regions()
     if n_children != 0:
         buf += f', {n_children} children'
+    else:
+        buf += ', no child'
+    if n_descendants != 0:
+        buf += f', {n_descendants} descendants'
+    else:
+        buf += ', no descendants'
     return buf
 
 

From 25f1e740d69dcfb5765dfd56cde9a4b6e803cdb5 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Tue, 7 Apr 2026 15:03:15 +0100
Subject: [PATCH 05/25] yaml dumper for region group

---
 .../src/imandrax_api_models/region_decomp.py  | 106 ++++++++++--------
 1 file changed, 58 insertions(+), 48 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index 2bbadf05..07a1653e 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -7,10 +7,8 @@
 from functools import reduce
 from typing import NoReturn, TypedDict
 
+import yaml
 from imandrax_api.lib import RegionStr
-from rich.console import Console, RenderableType
-from rich.text import Text
-from rich.tree import Tree
 
 
 @dataclass
@@ -144,60 +142,72 @@ def loop(
     return reduce(loop, constraints_by_most_frequent, init)['groups']
 
 
-# Show
+# YAML Dump
 # ====================
 
 
-def renderable_of_rg(rg: RegionGroup) -> str:
-    buf = ''
-    buf += f'[{",".join([str(i) for i in rg.rg_label_path])}]'
-    buf += f'; {len(rg.rg_constraints)} constraints'
-    n_children = len(rg.rg_children)
-    n_descendants = rg.n_descendant_regions()
-    if n_children != 0:
-        buf += f', {n_children} children'
-    else:
-        buf += ', no child'
-    if n_descendants != 0:
-        buf += f', {n_descendants} descendants'
-    else:
-        buf += ', no descendants'
-    return buf
-
+def _region_str_representer(dumper: yaml.Dumper, data: RegionStr) -> yaml.Node:
+    mapping: dict[str, object] = {}
+    if data.constraints_str is not None:
+        mapping['constraints'] = data.constraints_str
+    if data.invariant_str is not None:
+        mapping['invariant'] = data.invariant_str
+    if data.model_str is not None:
+        mapping['model'] = data.model_str
+    if data.model_eval_str is not None:
+        mapping['model_eval'] = data.model_eval_str
+    return dumper.represent_mapping('!Region', mapping)
+
+
+def _region_group_representer(
+    dumper: yaml.Dumper, data: RegionGroup, *, depth_limit: int | None = None
+) -> yaml.Node:
+    mapping: dict[str, object] = {}
+    mapping['constraints'] = data.rg_constraints
+    mapping['label_path'] = data.rg_label_path
+    mapping['weight'] = data.rg_weight
+    mapping['descendant_regions'] = data.n_descendant_regions()
+    if data.rg_region is not None:
+        mapping['region'] = data.rg_region
+    if data.rg_children:
+        if depth_limit is not None and depth_limit <= 0:
+            mapping['children'] = f'<{len(data.rg_children)} children omitted>'
+        else:
+            mapping['children'] = data.rg_children
+    return dumper.represent_mapping('!RegionGroup', mapping)
 
-def rich_tree_of_groups(region_groups: list[RegionGroup]) -> Tree:
 
-    def add_children(tree: Tree, region_groups: list[RegionGroup]) -> Tree:
-        top_regions: list[tuple[Tree, RegionGroup]] = [
-            (tree.add(renderable_of_rg(rg)), rg) for rg in region_groups
-        ]
+def _make_dumper(*, depth_limit: int | None = None) -> type[yaml.Dumper]:
+    class RegionDumper(yaml.Dumper):
+        pass
 
-        for tree, rg in top_regions:
-            add_children(tree, rg.rg_children)
-        return tree
+    RegionDumper.add_representer(
+        RegionStr,
+        _region_str_representer,
+    )
 
-    root = Tree('Region Decomposition')
+    def _rg_representer(dumper: yaml.Dumper, data: RegionGroup) -> yaml.Node:
+        next_limit = None if depth_limit is None else depth_limit - 1
+        return _region_group_representer(dumper, data, depth_limit=next_limit)
 
-    return add_children(root, region_groups)
+    RegionDumper.add_representer(RegionGroup, _rg_representer)
+    return RegionDumper
 
 
-def str_of_renderables(
-    *renderables: RenderableType | object,
-    plain: bool = True,
+def dump_region_groups_yaml(
+    groups: list[RegionGroup],
+    *,
+    depth_limit: int | None = None,
 ) -> str:
-    console = Console(
-        record=True,
-        width=80,
-        color_system='standard',
-        force_terminal=False,
-        force_interactive=False,
-        force_jupyter=False,
+    """
+    Dump region groups to YAML.
+
+    Args:
+        groups: The region groups to dump.
+        depth_limit: Max depth of children to expand. None means unlimited.
+
+    """
+    dumper_cls = _make_dumper(depth_limit=depth_limit)
+    return yaml.dump(
+        groups, Dumper=dumper_cls, default_flow_style=False, sort_keys=False
     )
-    with console.capture() as capture:
-        for renderable in renderables:
-            console.print(renderable)
-    exported_text = capture.get()
-    if plain:
-        return Text.from_ansi(exported_text).plain
-    else:
-        return exported_text

From e4331c16070f7c333c945b390f63fe4c2e5ba834 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Tue, 7 Apr 2026 17:46:53 +0100
Subject: [PATCH 06/25] GroupedRegionDecomposition root class

---
 .../src/imandrax_api_models/region_decomp.py  | 44 ++++++++++++++-----
 1 file changed, 34 insertions(+), 10 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index 07a1653e..5572eed5 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -5,11 +5,20 @@
 
 from dataclasses import dataclass
 from functools import reduce
-from typing import NoReturn, TypedDict
+from typing import NoReturn, Self, TypedDict
 
 import yaml
 from imandrax_api.lib import RegionStr
 
+from imandrax_api_models.yaml_utils import str_representer
+
+__all__ = (
+    'RegionGroup',
+    'group_regions',
+    'dump_region_groups_yaml',
+    'GroupedRegionDecomposition',
+)
+
 
 @dataclass
 class RegionGroup:
@@ -28,6 +37,19 @@ def group_regions(regions: list[RegionStr]) -> list[RegionGroup]:
     return _loop_group_regions([], [], regions)
 
 
+@dataclass
+class GroupedRegionDecomposition:
+    groups: list[RegionGroup]
+
+    @classmethod
+    def from_groups(cls, groups: list[RegionGroup]) -> Self:
+        return cls(groups=groups)
+
+    @classmethod
+    def from_regions(cls, regions: list[RegionStr]) -> Self:
+        return cls.from_groups(group_regions(regions))
+
+
 def _loop_group_regions(
     idx_path: list[int], constraint_path: list[str], regions: list[RegionStr]
 ) -> list[RegionGroup]:
@@ -164,24 +186,25 @@ def _region_group_representer(
 ) -> yaml.Node:
     mapping: dict[str, object] = {}
     mapping['constraints'] = data.rg_constraints
-    mapping['label_path'] = data.rg_label_path
+    # mapping['label_path'] = data.rg_label_path
+    mapping['label_path'] = '.'.join(map(str, data.rg_label_path))
     mapping['weight'] = data.rg_weight
-    mapping['descendant_regions'] = data.n_descendant_regions()
+    mapping['n_children_regions'] = len(data.rg_children)
+    mapping['n_descendant_regions'] = data.n_descendant_regions()
     if data.rg_region is not None:
         mapping['region'] = data.rg_region
     if data.rg_children:
-        if depth_limit is not None and depth_limit <= 0:
-            mapping['children'] = f'<{len(data.rg_children)} children omitted>'
-        else:
+        if depth_limit is None or depth_limit <= 0:
             mapping['children'] = data.rg_children
+    # return dumper.represent_mapping('tag:yaml.org,2002:map', mapping)
     return dumper.represent_mapping('!RegionGroup', mapping)
 
 
 def _make_dumper(*, depth_limit: int | None = None) -> type[yaml.Dumper]:
-    class RegionDumper(yaml.Dumper):
+    class RegionGroupsDumper(yaml.Dumper):
         pass
 
-    RegionDumper.add_representer(
+    RegionGroupsDumper.add_representer(
         RegionStr,
         _region_str_representer,
     )
@@ -190,8 +213,9 @@ def _rg_representer(dumper: yaml.Dumper, data: RegionGroup) -> yaml.Node:
         next_limit = None if depth_limit is None else depth_limit - 1
         return _region_group_representer(dumper, data, depth_limit=next_limit)
 
-    RegionDumper.add_representer(RegionGroup, _rg_representer)
-    return RegionDumper
+    RegionGroupsDumper.add_representer(RegionGroup, _rg_representer)
+    RegionGroupsDumper.add_representer(str, str_representer)
+    return RegionGroupsDumper
 
 
 def dump_region_groups_yaml(

From c4b91b2e081879c37bb53becda4e37a3c456dd35 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Tue, 7 Apr 2026 18:07:51 +0100
Subject: [PATCH 07/25] make grouped RD formatting prettier

---
 .../src/imandrax_api_models/region_decomp.py  | 98 ++++++++++++++++++-
 1 file changed, 93 insertions(+), 5 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index 5572eed5..00d0199d 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -5,7 +5,7 @@
 
 from dataclasses import dataclass
 from functools import reduce
-from typing import NoReturn, Self, TypedDict
+from typing import NoReturn, Protocol, Self, TypedDict
 
 import yaml
 from imandrax_api.lib import RegionStr
@@ -49,10 +49,94 @@ def from_groups(cls, groups: list[RegionGroup]) -> Self:
     def from_regions(cls, regions: list[RegionStr]) -> Self:
         return cls.from_groups(group_regions(regions))
 
+    def to_tree(
+        self,
+        *,
+        depth_limit: int | None = None,
+        summarize: RegionGroupSummarizer | None = None,
+    ) -> str:
+        summarize_ = summarize or default_region_group_summary
+        lines: list[str] = []
+        for i, group in enumerate(self.groups):
+            is_last = i == len(self.groups) - 1
+            _tree_lines(
+                lines,
+                group,
+                prefix='',
+                is_last=is_last,
+                depth_limit=depth_limit,
+                summarize=summarize_,
+            )
+        return '\n'.join(lines)
+
+
+class RegionGroupSummarizer(Protocol):
+    def __call__(self, group: RegionGroup) -> str: ...
+
+
+def default_region_group_summary(group: RegionGroup) -> str:
+    label = '.'.join(map(str, group.rg_label_path))
+    # rg_constraints is the full path from root; [-1] is this node's own constraint.
+    constraint = group.rg_constraints[-1] if group.rg_constraints else '?'
+    invariant: str | None = None
+    if (region := group.rg_region) is not None:
+        invariant = region.invariant_str
+    parts = [
+        f'[{label}]',
+        f'{constraint=}',
+        f'{invariant=}',
+        f'(w={group.rg_weight}, children={len(group.rg_children)}, descendants={group.n_descendant_regions()})',
+    ]
+    return ' '.join(parts)
+
+
+def _tree_lines(
+    lines: list[str],
+    group: RegionGroup,
+    *,
+    prefix: str,
+    is_last: bool,
+    depth_limit: int | None,
+    summarize: RegionGroupSummarizer,
+) -> None:
+    connector = '└── ' if is_last else '├── '
+    lines.append(f'{prefix}{connector}{summarize(group)}')
+
+    child_prefix = prefix + ('    ' if is_last else '│   ')
+    if depth_limit is not None and depth_limit <= 0 and group.rg_children:
+        lines.append(
+            f'{child_prefix}└── ... ({len(group.rg_children)} children, {group.n_descendant_regions()} descendants)'
+        )
+        return
+    next_limit = None if depth_limit is None else depth_limit - 1
+    for i, child in enumerate(group.rg_children):
+        _tree_lines(
+            lines,
+            child,
+            prefix=child_prefix,
+            is_last=i == len(group.rg_children) - 1,
+            depth_limit=next_limit,
+            summarize=summarize,
+        )
+
 
 def _loop_group_regions(
     idx_path: list[int], constraint_path: list[str], regions: list[RegionStr]
 ) -> list[RegionGroup]:
+    """
+    Recursively group regions by shared constraints.
+
+    At each level, collects all constraints from the remaining regions (excluding
+    those already in ``constraint_path``), then iterates over them by frequency.
+    For each constraint, regions that contain it are split into a sub-group and
+    grouped recursively.
+
+    Each resulting ``RegionGroup.rg_constraints`` is the **full accumulated path**
+    of constraints from the root down to that node (chronological order). Therefore
+    ``rg_constraints[-1]`` is the constraint introduced at that node's own level,
+    while earlier elements are inherited from ancestors.
+    """
+
     def raise_(exc: BaseException) -> NoReturn:
         raise exc
 
@@ -185,14 +269,18 @@ def _region_group_representer(
     dumper: yaml.Dumper, data: RegionGroup, *, depth_limit: int | None = None
 ) -> yaml.Node:
     mapping: dict[str, object] = {}
-    mapping['constraints'] = data.rg_constraints
-    # mapping['label_path'] = data.rg_label_path
+
     mapping['label_path'] = '.'.join(map(str, data.rg_label_path))
     mapping['weight'] = data.rg_weight
+
+    mapping['introduced_constraint'] = data.rg_constraints[-1]
+    if (region := data.rg_region) is not None:
+        mapping['invariant'] = region.invariant_str
+        mapping['example_input'] = region.model_str
+        mapping['example_output'] = region.model_eval_str
+
     mapping['n_children_regions'] = len(data.rg_children)
     mapping['n_descendant_regions'] = data.n_descendant_regions()
-    if data.rg_region is not None:
-        mapping['region'] = data.rg_region
     if data.rg_children:
         if depth_limit is None or depth_limit <= 0:
             mapping['children'] = data.rg_children

From 2892e39d7369949d8de097c755261ce536e39aae Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Wed, 8 Apr 2026 10:49:35 +0100
Subject: [PATCH 08/25] to_yaml_str

---
 .../src/imandrax_api_models/region_decomp.py           | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index 00d0199d..c3b3fd4b 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -1,6 +1,5 @@
 """Post-processing (Hierarchical groupping) for region decomposition."""
 
-# %%
 from __future__ import annotations
 
 from dataclasses import dataclass
@@ -49,7 +48,7 @@ def from_groups(cls, groups: list[RegionGroup]) -> Self:
     def from_regions(cls, regions: list[RegionStr]) -> Self:
         return cls.from_groups(group_regions(regions))
 
-    def to_tree(
+    def to_tree_str(
         self,
         *,
         depth_limit: int | None = None,
@@ -69,6 +68,12 @@ def to_tree(
             )
         return '\n'.join(lines)
 
+    def to_yaml_str(
+        self,
+        depth_limit: int | None = None,
+    ) -> str:
+        return dump_region_groups_yaml(self.groups, depth_limit=depth_limit)
+
 
 class RegionGroupSummarizer(Protocol):
     def __call__(self, group: RegionGroup) -> str: ...
@@ -273,6 +278,7 @@ def _region_group_representer(
     mapping['label_path'] = '.'.join(map(str, data.rg_label_path))
     mapping['weight'] = data.rg_weight
 
+    mapping['constraints'] = data.rg_constraints
     mapping['introduced_constraint'] = data.rg_constraints[-1]
     if (region := data.rg_region) is not None:
         mapping['invariant'] = region.invariant_str

From a3562bcc824f9edb8404fc69310b1344bbf87627 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Wed, 8 Apr 2026 10:50:20 +0100
Subject: [PATCH 09/25] REFA: drop rg_ prefix for RegionGroup fields

---
 .../src/imandrax_api_models/region_decomp.py  | 54 +++++++++----------
 1 file changed, 27 insertions(+), 27 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index c3b3fd4b..09d0b7cc 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -21,14 +21,14 @@
 
 @dataclass
 class RegionGroup:
-    rg_constraints: list[str]
-    rg_label_path: list[int]
-    rg_region: RegionStr | None
-    rg_children: list[RegionGroup]
-    rg_weight: int
+    constraints: list[str]
+    label_path: list[int]
+    region: RegionStr | None
+    children: list[RegionGroup]
+    weight: int
 
     def n_descendant_regions(self) -> int:
-        return sum(c.n_descendant_regions() for c in self.rg_children)
+        return sum(c.n_descendant_regions() for c in self.children)
 
 
 def group_regions(regions: list[RegionStr]) -> list[RegionGroup]:
@@ -80,17 +80,17 @@ def __call__(self, group: RegionGroup) -> str: ...
 
 
 def default_region_group_summary(group: RegionGroup) -> str:
-    label = '.'.join(map(str, group.rg_label_path))
+    label = '.'.join(map(str, group.label_path))
     # rg_constraints is the full path from root; [-1] is this node's own constraint.
-    constraint = group.rg_constraints[-1] if group.rg_constraints else '?'
+    constraint = group.constraints[-1] if group.constraints else '?'
     invariant: str | None = None
-    if (region := group.rg_region) is not None:
+    if (region := group.region) is not None:
         invariant = region.invariant_str
     parts = [
         f'[{label}]',
         f'{constraint=}',
         f'{invariant=}',
-        f'(w={group.rg_weight}, children={len(group.rg_children)}, descendants={group.n_descendant_regions()})',
+        f'(w={group.weight}, children={len(group.children)}, descendants={group.n_descendant_regions()})',
     ]
     return ' '.join(parts)
 
@@ -108,18 +108,18 @@ def _tree_lines(
     lines.append(f'{prefix}{connector}{summarize(group)}')
 
     child_prefix = prefix + ('    ' if is_last else '│   ')
-    if depth_limit is not None and depth_limit <= 0 and group.rg_children:
+    if depth_limit is not None and depth_limit <= 0 and group.children:
         lines.append(
-            f'{child_prefix}└── ... ({len(group.rg_children)} children, {group.n_descendant_regions()} descendants)'
+            f'{child_prefix}└── ... ({len(group.children)} children, {group.n_descendant_regions()} descendants)'
         )
         return
     next_limit = None if depth_limit is None else depth_limit - 1
-    for i, child in enumerate(group.rg_children):
+    for i, child in enumerate(group.children):
         _tree_lines(
             lines,
             child,
             prefix=child_prefix,
-            is_last=i == len(group.rg_children) - 1,
+            is_last=i == len(group.children) - 1,
             depth_limit=next_limit,
             summarize=summarize,
         )
@@ -231,11 +231,11 @@ def loop(
                     rg_region = None
                 rg_weight = len(has)
                 group = RegionGroup(
-                    rg_constraints=rg_constraints,
-                    rg_region=rg_region,
-                    rg_children=rg_children,
-                    rg_label_path=new_idx_path,
-                    rg_weight=rg_weight,
+                    constraints=rg_constraints,
+                    region=rg_region,
+                    children=rg_children,
+                    label_path=new_idx_path,
+                    weight=rg_weight,
                 )
             res = [group, *groups], without
         else:
@@ -275,21 +275,21 @@ def _region_group_representer(
 ) -> yaml.Node:
     mapping: dict[str, object] = {}
 
-    mapping['label_path'] = '.'.join(map(str, data.rg_label_path))
-    mapping['weight'] = data.rg_weight
+    mapping['label_path'] = '.'.join(map(str, data.label_path))
+    mapping['weight'] = data.weight
 
-    mapping['constraints'] = data.rg_constraints
-    mapping['introduced_constraint'] = data.rg_constraints[-1]
-    if (region := data.rg_region) is not None:
+    mapping['constraints'] = data.constraints
+    mapping['introduced_constraint'] = data.constraints[-1]
+    if (region := data.region) is not None:
         mapping['invariant'] = region.invariant_str
         mapping['example_input'] = region.model_str
         mapping['example_output'] = region.model_eval_str
 
-    mapping['n_children_regions'] = len(data.rg_children)
+    mapping['n_children_regions'] = len(data.children)
     mapping['n_descendant_regions'] = data.n_descendant_regions()
-    if data.rg_children:
+    if data.children:
         if depth_limit is None or depth_limit <= 0:
-            mapping['children'] = data.rg_children
+            mapping['children'] = data.children
     # return dumper.represent_mapping('tag:yaml.org,2002:map', mapping)
     return dumper.represent_mapping('!RegionGroup', mapping)
 

From f707f93a720b400a0f4d61218cd7ad52216c1b20 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Wed, 8 Apr 2026 11:10:05 +0100
Subject: [PATCH 10/25] add indexed region group for flat structure

---
 .../src/imandrax_api_models/region_decomp.py  | 78 +++++++++++++++++--
 1 file changed, 73 insertions(+), 5 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index 09d0b7cc..74bdd414 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -2,6 +2,7 @@
 
 from __future__ import annotations
 
+import uuid
 from dataclasses import dataclass
 from functools import reduce
 from typing import NoReturn, Protocol, Self, TypedDict
@@ -36,6 +37,49 @@ def group_regions(regions: list[RegionStr]) -> list[RegionGroup]:
     return _loop_group_regions([], [], regions)
 
 
+@dataclass
+class IndexedRegionGroup:
+    """Equivalent to RegionGroup, but in flat structure."""
+
+    id: str
+    constraints: list[str]
+    label_path: list[int]
+    region: RegionStr | None
+    children: list[str]
+    weight: int
+
+
+def _gen_id() -> str:
+    return str(uuid.uuid4())[:8]
+
+
+def region_groups_to_indexed(groups: list[RegionGroup]) -> list[IndexedRegionGroup]:
+    def loop(
+        group_and_id_lst: list[tuple[RegionGroup, str]], acc: list[IndexedRegionGroup]
+    ) -> None:
+        for rg, id in group_and_id_lst:
+            c_ids = [_gen_id() for _ in rg.children]
+
+            irg = IndexedRegionGroup(
+                id=id,
+                constraints=rg.constraints,
+                label_path=rg.label_path,
+                region=rg.region,
+                children=c_ids,
+                weight=rg.weight,
+            )
+            acc.append(irg)
+
+            children_group_and_id_lst = list(zip(rg.children, c_ids, strict=True))
+            loop(children_group_and_id_lst, acc)
+
+    initial_ids = [_gen_id() for _ in groups]
+    group_and_id_lst = list(zip(groups, initial_ids, strict=True))
+    acc: list[IndexedRegionGroup] = []
+    loop(group_and_id_lst, acc)
+    return acc
+
+
 @dataclass
 class GroupedRegionDecomposition:
     groups: list[RegionGroup]
@@ -294,11 +338,32 @@ def _region_group_representer(
     return dumper.represent_mapping('!RegionGroup', mapping)
 
 
+def _indexed_region_group_representer(
+    dumper: yaml.Dumper, data: IndexedRegionGroup
+) -> yaml.Node:
+    mapping: dict[str, object] = {}
+
+    mapping['label_path'] = '.'.join(map(str, data.label_path))
+    mapping['weight'] = data.weight
+
+    mapping['constraints'] = data.constraints
+    mapping['introduced_constraint'] = data.constraints[-1]
+    if (region := data.region) is not None:
+        mapping['invariant'] = region.invariant_str
+        mapping['example_input'] = region.model_str
+        mapping['example_output'] = region.model_eval_str
+
+    mapping['n_children_regions'] = len(data.children)
+    mapping['children'] = data.children
+    # return dumper.represent_mapping('tag:yaml.org,2002:map', mapping)
+    return dumper.represent_mapping('!IndexedRegionGroup', mapping)
+
+
 def _make_dumper(*, depth_limit: int | None = None) -> type[yaml.Dumper]:
-    class RegionGroupsDumper(yaml.Dumper):
+    class RegionDecompDumper(yaml.Dumper):
         pass
 
-    RegionGroupsDumper.add_representer(
+    RegionDecompDumper.add_representer(
         RegionStr,
         _region_str_representer,
     )
@@ -307,9 +372,12 @@ def _rg_representer(dumper: yaml.Dumper, data: RegionGroup) -> yaml.Node:
         next_limit = None if depth_limit is None else depth_limit - 1
         return _region_group_representer(dumper, data, depth_limit=next_limit)
 
-    RegionGroupsDumper.add_representer(RegionGroup, _rg_representer)
-    RegionGroupsDumper.add_representer(str, str_representer)
-    return RegionGroupsDumper
+    RegionDecompDumper.add_representer(RegionGroup, _rg_representer)
+    RegionDecompDumper.add_representer(
+        IndexedRegionGroup, _indexed_region_group_representer
+    )
+    RegionDecompDumper.add_representer(str, str_representer)
+    return RegionDecompDumper
 
 
 def dump_region_groups_yaml(

From 8dedd7a2106c2fa581766983bde80ca43640cb41 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Wed, 8 Apr 2026 11:16:33 +0100
Subject: [PATCH 11/25] add depth to indexed rg, grouped rg to flat yaml

---
 .../src/imandrax_api_models/region_decomp.py  | 29 +++++++++++++++----
 1 file changed, 24 insertions(+), 5 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index 74bdd414..835405e9 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -47,6 +47,7 @@ class IndexedRegionGroup:
     region: RegionStr | None
     children: list[str]
     weight: int
+    depth: int
 
 
 def _gen_id() -> str:
@@ -55,7 +56,9 @@ def _gen_id() -> str:
 
 def region_groups_to_indexed(groups: list[RegionGroup]) -> list[IndexedRegionGroup]:
     def loop(
-        group_and_id_lst: list[tuple[RegionGroup, str]], acc: list[IndexedRegionGroup]
+        group_and_id_lst: list[tuple[RegionGroup, str]],
+        acc: list[IndexedRegionGroup],
+        depth: int,
     ) -> None:
         for rg, id in group_and_id_lst:
             c_ids = [_gen_id() for _ in rg.children]
@@ -67,16 +70,17 @@ def loop(
                 region=rg.region,
                 children=c_ids,
                 weight=rg.weight,
+                depth=depth,
             )
             acc.append(irg)
 
             children_group_and_id_lst = list(zip(rg.children, c_ids, strict=True))
-            loop(children_group_and_id_lst, acc)
+            loop(children_group_and_id_lst, acc, depth + 1)
 
     initial_ids = [_gen_id() for _ in groups]
     group_and_id_lst = list(zip(groups, initial_ids, strict=True))
     acc: list[IndexedRegionGroup] = []
-    loop(group_and_id_lst, acc)
+    loop(group_and_id_lst, acc, 0)
     return acc
 
 
@@ -118,6 +122,19 @@ def to_yaml_str(
     ) -> str:
         return dump_region_groups_yaml(self.groups, depth_limit=depth_limit)
 
+    def to_yaml_str_flat(
+        self,
+        depth_limit: int | None = None,
+    ) -> str:
+        dumper_cls = _make_dumper()
+        indexed_groups = region_groups_to_indexed(self.groups)
+        return yaml.dump(
+            indexed_groups,
+            Dumper=dumper_cls,
+            default_flow_style=False,
+            sort_keys=False,
+        )
+
 
 class RegionGroupSummarizer(Protocol):
     def __call__(self, group: RegionGroup) -> str: ...
@@ -343,7 +360,9 @@ def _indexed_region_group_representer(
 ) -> yaml.Node:
     mapping: dict[str, object] = {}
 
+    mapping['id'] = data.id
     mapping['label_path'] = '.'.join(map(str, data.label_path))
+    mapping['depth'] = data.depth
     mapping['weight'] = data.weight
 
     mapping['constraints'] = data.constraints
@@ -355,8 +374,8 @@ def _indexed_region_group_representer(
 
     mapping['n_children_regions'] = len(data.children)
     mapping['children'] = data.children
-    # return dumper.represent_mapping('tag:yaml.org,2002:map', mapping)
-    return dumper.represent_mapping('!IndexedRegionGroup', mapping)
+    return dumper.represent_mapping('tag:yaml.org,2002:map', mapping)
+    # return dumper.represent_mapping('!IndexedRegionGroup', mapping)
 
 
 def _make_dumper(*, depth_limit: int | None = None) -> type[yaml.Dumper]:

From bbb6a2b03803a4c0a7521829da509ca67797b4fb Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Wed, 8 Apr 2026 11:35:53 +0100
Subject: [PATCH 12/25] make yaml dumper generic

---
 .../src/imandrax_api_models/region_decomp.py  | 72 ++++++++++---------
 1 file changed, 40 insertions(+), 32 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index 835405e9..c670d7f4 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -3,8 +3,9 @@
 from __future__ import annotations
 
 import uuid
+from collections.abc import Callable
 from dataclasses import dataclass
-from functools import reduce
+from functools import partial, reduce
 from typing import NoReturn, Protocol, Self, TypedDict
 
 import yaml
@@ -47,7 +48,7 @@ class IndexedRegionGroup:
     region: RegionStr | None
     children: list[str]
     weight: int
-    depth: int
+    depth: int  # 1-indexed depth
 
 
 def _gen_id() -> str:
@@ -80,14 +81,34 @@ def loop(
     initial_ids = [_gen_id() for _ in groups]
     group_and_id_lst = list(zip(groups, initial_ids, strict=True))
     acc: list[IndexedRegionGroup] = []
-    loop(group_and_id_lst, acc, 0)
+    loop(group_and_id_lst, acc, 1)
     return acc
 
 
+def _max_depth_of_groups(groups: list[RegionGroup]) -> int:
+    init: int = 1
+
+    def loop(groups: list[RegionGroup]):
+        label_lengths: list[int] = [len(rg.label_path) for rg in groups]
+        nonlocal init
+        init = max(init, (max(label_lengths) if label_lengths else 0))
+        for rg in groups:
+            loop(rg.children)
+
+    loop(groups)
+    return init
+
+
 @dataclass
 class GroupedRegionDecomposition:
     groups: list[RegionGroup]
 
+    def summary(self) -> dict[str, str | int]:
+        n_regions = sum([rg.n_descendant_regions() for rg in self.groups])
+        max_depth = _max_depth_of_groups(self.groups)
+
+        return {'n_regions': n_regions, 'max_depth': max_depth}
+
     @classmethod
     def from_groups(cls, groups: list[RegionGroup]) -> Self:
         return cls(groups=groups)
@@ -116,24 +137,30 @@ def to_tree_str(
             )
         return '\n'.join(lines)
 
+    @staticmethod
+    def dumper_func(depth_limit: int | None = None) -> Callable[..., str]:
+        dumper_cls = make_dumper(depth_limit=depth_limit)
+        return partial(
+            yaml.dump,
+            Dumper=dumper_cls,
+            default_flow_style=False,
+            sort_keys=False,
+        )
+
     def to_yaml_str(
         self,
         depth_limit: int | None = None,
     ) -> str:
-        return dump_region_groups_yaml(self.groups, depth_limit=depth_limit)
+        to_dump = {'summary': self.summary(), 'region_groups': self.groups}
+        return self.dumper_func(depth_limit)(to_dump)
 
     def to_yaml_str_flat(
         self,
         depth_limit: int | None = None,
     ) -> str:
-        dumper_cls = _make_dumper()
         indexed_groups = region_groups_to_indexed(self.groups)
-        return yaml.dump(
-            indexed_groups,
-            Dumper=dumper_cls,
-            default_flow_style=False,
-            sort_keys=False,
-        )
+        to_dump = {'summary': self.summary(), 'region_groups': indexed_groups}
+        return self.dumper_func(depth_limit)(to_dump)
 
 
 class RegionGroupSummarizer(Protocol):
@@ -197,7 +224,7 @@ def _loop_group_regions(
     For each constraint, regions that contain it are split into a sub-group and
     grouped recursively.
 
-    Each resulting ``RegionGroup.rg_constraints`` is the **full accumulated path**
+    Each resulting ``RegionGroup.rg_constraints`` is the full accumulated path
     of constraints from the root down to that node (chronological order). Therefore
     ``rg_constraints[-1]`` is the constraint introduced at that node's own level,
     while earlier elements are inherited from ancestors.
@@ -378,7 +405,7 @@ def _indexed_region_group_representer(
     # return dumper.represent_mapping('!IndexedRegionGroup', mapping)
 
 
-def _make_dumper(*, depth_limit: int | None = None) -> type[yaml.Dumper]:
+def make_dumper(*, depth_limit: int | None = None) -> type[yaml.Dumper]:
     class RegionDecompDumper(yaml.Dumper):
         pass
 
@@ -397,22 +424,3 @@ def _rg_representer(dumper: yaml.Dumper, data: RegionGroup) -> yaml.Node:
     )
     RegionDecompDumper.add_representer(str, str_representer)
     return RegionDecompDumper
-
-
-def dump_region_groups_yaml(
-    groups: list[RegionGroup],
-    *,
-    depth_limit: int | None = None,
-) -> str:
-    """
-    Dump region groups to YAML.
-
-    Args:
-        groups: The region groups to dump.
-        depth_limit: Max depth of children to expand. None means unlimited.
-
-    """
-    dumper_cls = _make_dumper(depth_limit=depth_limit)
-    return yaml.dump(
-        groups, Dumper=dumper_cls, default_flow_style=False, sort_keys=False
-    )

From 9ca45896a97bceeb673e4d76b0c091559f8bb75b Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Wed, 8 Apr 2026 11:50:28 +0100
Subject: [PATCH 13/25] CHORE

---
 .../src/imandrax_api_models/region_decomp.py             | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index c670d7f4..e53c3ff9 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -16,7 +16,6 @@
 __all__ = (
     'RegionGroup',
     'group_regions',
-    'dump_region_groups_yaml',
     'GroupedRegionDecomposition',
 )
 
@@ -55,7 +54,7 @@ def _gen_id() -> str:
     return str(uuid.uuid4())[:8]
 
 
-def region_groups_to_indexed(groups: list[RegionGroup]) -> list[IndexedRegionGroup]:
+def indexed_of_region_groups(groups: list[RegionGroup]) -> list[IndexedRegionGroup]:
     def loop(
         group_and_id_lst: list[tuple[RegionGroup, str]],
         acc: list[IndexedRegionGroup],
@@ -82,7 +81,7 @@ def loop(
     group_and_id_lst = list(zip(groups, initial_ids, strict=True))
     acc: list[IndexedRegionGroup] = []
     loop(group_and_id_lst, acc, 1)
-    return acc
+    return acc[::-1]  # Reverse to get top-bottom order
 
 
 def _max_depth_of_groups(groups: list[RegionGroup]) -> int:
@@ -158,7 +157,7 @@ def to_yaml_str_flat(
         self,
         depth_limit: int | None = None,
     ) -> str:
-        indexed_groups = region_groups_to_indexed(self.groups)
+        indexed_groups = indexed_of_region_groups(self.groups)
         to_dump = {'summary': self.summary(), 'region_groups': indexed_groups}
         return self.dumper_func(depth_limit)(to_dump)
 
@@ -322,7 +321,7 @@ def loop(
                     constraints=rg_constraints,
                     region=rg_region,
                     children=rg_children,
-                    label_path=new_idx_path,
+                    label_path=new_idx_path[::-1],
                     weight=rg_weight,
                 )
             res = [group, *groups], without

From 3fede1b33a265e5c476883d0ad3badbe43c33880 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Wed, 8 Apr 2026 11:59:32 +0100
Subject: [PATCH 14/25] DOCS: region grouping contract

---
 .../src/imandrax_api_models/region_decomp.py  | 49 +++++++++++++++++--
 1 file changed, 45 insertions(+), 4 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index e53c3ff9..a37dbc07 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -22,6 +22,27 @@
 
 @dataclass
 class RegionGroup:
+    """
+    A hierarchical group of regions sharing constraints.
+
+    Attributes:
+        constraints:
+            Full accumulated constraint path from root to this node (root-first).
+            `constraints[-1]` is the constraint introduced at this node's own level.
+        label_path:
+            Positional index path from root to this node (root-first, 1-indexed).
+            Each element is the sibling index at that depth. Displayed as e.g. `1.2.3`.
+            Levels where a constraint applies to all regions are skipped, so the path
+            length may be shorter than the tree depth.
+        region:
+            The concrete region, if this group contains exactly one.
+        children:
+            Sub-groups under this node.
+        weight:
+            Number of regions in the `has` partition at this node's level.
+
+    """
+
     constraints: list[str]
     label_path: list[int]
     region: RegionStr | None
@@ -223,10 +244,30 @@ def _loop_group_regions(
     For each constraint, regions that contain it are split into a sub-group and
     grouped recursively.
 
-    Each resulting ``RegionGroup.rg_constraints`` is the full accumulated path
-    of constraints from the root down to that node (chronological order). Therefore
-    ``rg_constraints[-1]`` is the constraint introduced at that node's own level,
-    while earlier elements are inherited from ancestors.
+    Preconditions:
+    - Every region in `regions` must have a non-empty `constraints_str`.
+    - `constraint_path` contains constraints already consumed by ancestor levels;
+      these are excluded from grouping at this level.
+    - `idx_path` is built in reverse (deepest-first); reversed to root-first
+      when stored in `RegionGroup.label_path`.
+
+    Postconditions:
+    - Every input region appears in exactly one output `RegionGroup` (partition).
+    - `RegionGroup.constraints` is the full accumulated constraint path from root
+      to that node (root-first). `constraints[-1]` is the constraint introduced
+      at that node's own level (its "own constraint").
+    - `RegionGroup.label_path` is root-first, 1-indexed. A level is skipped
+      (no index appended) when all remaining regions share the constraint and
+      there is more than one — i.e. the constraint doesn't discriminate.
+    - If recursion yields a single child group, that child is promoted (returned
+      directly) rather than wrapped, collapsing trivial intermediate nodes.
+
+    Invariants (across `reduce`/`loop` iterations):
+    - `acc['regions']` shrinks monotonically: each iteration moves regions into
+      `has` (grouped) or keeps them in `without` (remaining).
+    - `acc['constraint_path']` grows by one element per iteration (the current
+      `konstraint`), regardless of whether any regions matched.
+    - `acc['groups']` only grows: new groups are prepended when `has` is non-empty.
     """
 
     def raise_(exc: BaseException) -> NoReturn:

From 3236b8155460f0732854b6cb775585f64ee00e13 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Wed, 8 Apr 2026 13:25:32 +0100
Subject: [PATCH 15/25] CHORE

---
 .../src/imandrax_api_models/region_decomp.py               | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index a37dbc07..9c66c450 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -174,13 +174,10 @@ def to_yaml_str(
         to_dump = {'summary': self.summary(), 'region_groups': self.groups}
         return self.dumper_func(depth_limit)(to_dump)
 
-    def to_yaml_str_flat(
-        self,
-        depth_limit: int | None = None,
-    ) -> str:
+    def to_yaml_str_flat(self) -> str:
         indexed_groups = indexed_of_region_groups(self.groups)
         to_dump = {'summary': self.summary(), 'region_groups': indexed_groups}
-        return self.dumper_func(depth_limit)(to_dump)
+        return self.dumper_func()(to_dump)
 
 
 class RegionGroupSummarizer(Protocol):

From 7f66b1503f90db8185ffc13c3f70a5d721fc95f5 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Wed, 8 Apr 2026 16:55:11 +0100
Subject: [PATCH 16/25] human-readable decomp res, use sequential integer as id
 (determinsitic)

---
 .../src/imandrax_api_models/region_decomp.py  | 104 +++++++++++++++++-
 1 file changed, 98 insertions(+), 6 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index 9c66c450..5e5cb76d 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -2,15 +2,17 @@
 
 from __future__ import annotations
 
-import uuid
+import itertools
 from collections.abc import Callable
 from dataclasses import dataclass
 from functools import partial, reduce
-from typing import NoReturn, Protocol, Self, TypedDict
+from typing import Any, Literal, NoReturn, Protocol, Self, TypedDict
 
 import yaml
+from devtools import pformat
 from imandrax_api.lib import RegionStr
 
+from imandrax_api_models.proto_models import DecomposeRes, Error
 from imandrax_api_models.yaml_utils import str_representer
 
 __all__ = (
@@ -20,6 +22,93 @@
 )
 
 
+@dataclass
+class HumDecomposeRes:
+    """Human readable decomp result"""
+
+    _variants: (
+        tuple[Literal['Success'], list[RegionGroup]]
+        | tuple[Literal['Fail'], list[Error]]
+    )
+
+    @classmethod
+    def mk_success(cls, pl: list[RegionGroup]) -> Self:
+        return cls(_variants=('Success', pl))
+
+    @classmethod
+    def mk_fail(cls, pl: list[Error]) -> Self:
+        return cls(_variants=('Fail', pl))
+
+    @classmethod
+    def of_decomp_res(cls, v: DecomposeRes) -> HumDecomposeRes:
+        return hum_of_decomp_res(v)
+
+    def to_tree_str(
+        self,
+        *,
+        depth_limit: int | None = None,
+        summarize: RegionGroupSummarizer | None = None,
+    ) -> str:
+        match self._variants:
+            case ('Fail', errs):
+                return pformat(errs, indent=2)
+            case ('Success', groups):
+                summarize_ = summarize or default_region_group_summary
+                lines: list[str] = []
+                for i, group in enumerate(groups):
+                    is_last = i == len(groups) - 1
+                    _tree_lines(
+                        lines,
+                        group,
+                        prefix='',
+                        is_last=is_last,
+                        depth_limit=depth_limit,
+                        summarize=summarize_,
+                    )
+                return '\n'.join(lines)
+
+    def summary(self) -> dict[str, str | int] | None:
+        match self._variants:
+            case ('Fail', _):
+                return None
+            case ('Success', groups):
+                n_regions = sum([rg.n_descendant_regions() for rg in groups])
+                max_depth = _max_depth_of_groups(groups)
+
+                return {'n_regions': n_regions, 'max_depth': max_depth}
+
+    def to_dict_hierarchical(
+        self,
+        depth_limit: int | None = None,
+    ) -> dict[str, Any]:
+        match self._variants:
+            case ('Fail', errs):
+                return {'errors': errs}
+            case ('Success', groups):
+                return {'summary': self.summary(), 'region_groups': groups}
+
+    def to_dict_flat(
+        self,
+    ) -> dict[str, Any]:
+        match self._variants:
+            case ('Fail', errs):
+                return {'errors': errs}
+            case ('Success', groups):
+                indexed_groups = indexed_of_region_groups(groups)
+                return {'summary': self.summary(), 'region_groups': indexed_groups}
+
+
+def hum_of_decomp_res(decomp_res: DecomposeRes) -> HumDecomposeRes:
+    if decomp_res.err is None:
+        regions = decomp_res.regions_str
+        assert regions is not None
+        groups = group_regions(regions)
+        return HumDecomposeRes.mk_success(groups)
+
+    else:
+        return HumDecomposeRes.mk_fail(decomp_res.errors)
+
+
 @dataclass
 class RegionGroup:
     """
@@ -71,8 +160,11 @@ class IndexedRegionGroup:
     depth: int  # 1-indexed depth
 
 
+_counter = itertools.count()
+
+
 def _gen_id() -> str:
-    return str(uuid.uuid4())[:8]
+    return str(next(_counter))
 
 
 def indexed_of_region_groups(groups: list[RegionGroup]) -> list[IndexedRegionGroup]:
@@ -102,7 +194,7 @@ def loop(
     group_and_id_lst = list(zip(groups, initial_ids, strict=True))
     acc: list[IndexedRegionGroup] = []
     loop(group_and_id_lst, acc, 1)
-    return acc[::-1]  # Reverse to get top-bottom order
+    return acc
 
 
 def _max_depth_of_groups(groups: list[RegionGroup]) -> int:
@@ -159,7 +251,7 @@ def to_tree_str(
 
     @staticmethod
     def dumper_func(depth_limit: int | None = None) -> Callable[..., str]:
-        dumper_cls = make_dumper(depth_limit=depth_limit)
+        dumper_cls = mk_dumper(depth_limit=depth_limit)
         return partial(
             yaml.dump,
             Dumper=dumper_cls,
@@ -442,7 +534,7 @@ def _indexed_region_group_representer(
     # return dumper.represent_mapping('!IndexedRegionGroup', mapping)
 
 
-def make_dumper(*, depth_limit: int | None = None) -> type[yaml.Dumper]:
+def mk_dumper(*, depth_limit: int | None = None) -> type[yaml.Dumper]:
     class RegionDecompDumper(yaml.Dumper):
         pass
 

From 32ceaf04d4f9844403fa3a8e3e8bd17db60da55e Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Wed, 8 Apr 2026 17:08:22 +0100
Subject: [PATCH 17/25] FIX: count region should include itself

---
 .../src/imandrax_api_models/region_decomp.py                | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index 5e5cb76d..e0828bc0 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -72,7 +72,7 @@ def summary(self) -> dict[str, str | int] | None:
             case ('Fail', _):
                 return None
             case ('Success', groups):
-                n_regions = sum([rg.n_descendant_regions() for rg in groups])
+                n_regions = sum([rg.n_regions() for rg in groups])
                 max_depth = _max_depth_of_groups(groups)
 
                 return {'n_regions': n_regions, 'max_depth': max_depth}
@@ -138,6 +138,10 @@ class RegionGroup:
     children: list[RegionGroup]
     weight: int
 
+    def n_regions(self) -> int:
+        """Total regions in this subtree, including self."""
+        return 1 + sum(c.n_regions() for c in self.children)
+
     def n_descendant_regions(self) -> int:
         return sum(c.n_descendant_regions() for c in self.children)
 

From 37c9e505250773acb7d14b6a367bc2af7877411a Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Wed, 8 Apr 2026 17:31:52 +0100
Subject: [PATCH 18/25] bump version

---
 packages/imandrax-api-models/CHANGELOG.md   | 4 ++++
 packages/imandrax-api-models/pyproject.toml | 2 +-
 packages/imandrax-api-models/uv.lock        | 2 +-
 3 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/packages/imandrax-api-models/CHANGELOG.md b/packages/imandrax-api-models/CHANGELOG.md
index 35bd92d4..48afe46f 100644
--- a/packages/imandrax-api-models/CHANGELOG.md
+++ b/packages/imandrax-api-models/CHANGELOG.md
@@ -4,6 +4,10 @@ Versioning scheme: <IMANDRAX_API_VERSION>.<MINOR>.<PATCH>
 
 ## [Unreleased]
 
+## [19.1.0] - 2026-04-08
+
+- Add region decomp grouping and serialization utilities
+
 ## [19.0.0] - 2026-03-25
 
 - Add qcheck models and endpoints
diff --git a/packages/imandrax-api-models/pyproject.toml b/packages/imandrax-api-models/pyproject.toml
index c579b770..0f922635 100644
--- a/packages/imandrax-api-models/pyproject.toml
+++ b/packages/imandrax-api-models/pyproject.toml
@@ -1,6 +1,6 @@
 [project]
 name = "imandrax-api-models"
-version = "19.0.0"
+version = "19.1.0"
 description = "Add your description here"
 readme = "README.md"
 authors = [
diff --git a/packages/imandrax-api-models/uv.lock b/packages/imandrax-api-models/uv.lock
index c2647f76..b2e5d2cb 100644
--- a/packages/imandrax-api-models/uv.lock
+++ b/packages/imandrax-api-models/uv.lock
@@ -493,7 +493,7 @@ async = [
 
 [[package]]
 name = "imandrax-api-models"
-version = "19.0.0"
+version = "19.1.0"
 source = { editable = "." }
 dependencies = [
     { name = "devtools" },

From 0c864873e64b14e9c3d1db70a219f1cbfd13c7bf Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Wed, 8 Apr 2026 17:35:24 +0100
Subject: [PATCH 19/25] remove old goal state

---
 packages/imandrax-api-models/CHANGELOG.md     |  1 +
 .../src/imandrax_api_models/pp_goal_state.py  | 86 -------------------
 .../tests/test_pp_goal_state.py               | 79 -----------------
 3 files changed, 1 insertion(+), 165 deletions(-)
 delete mode 100644 packages/imandrax-api-models/src/imandrax_api_models/pp_goal_state.py
 delete mode 100644 packages/imandrax-api-models/tests/test_pp_goal_state.py

diff --git a/packages/imandrax-api-models/CHANGELOG.md b/packages/imandrax-api-models/CHANGELOG.md
index 48afe46f..f48588cc 100644
--- a/packages/imandrax-api-models/CHANGELOG.md
+++ b/packages/imandrax-api-models/CHANGELOG.md
@@ -7,6 +7,7 @@ Versioning scheme: <IMANDRAX_API_VERSION>.<MINOR>.<PATCH>
 ## [19.1.0] - 2026-04-08
 
 - Add region decomp grouping and serialization utilities
+- Remove outdated goal-state pretty-printing (see `imandrax-tools.goal_state` for new version).
 
 ## [19.0.0] - 2026-03-25
 
diff --git a/packages/imandrax-api-models/src/imandrax_api_models/pp_goal_state.py b/packages/imandrax-api-models/src/imandrax_api_models/pp_goal_state.py
deleted file mode 100644
index 41537d3f..00000000
--- a/packages/imandrax-api-models/src/imandrax_api_models/pp_goal_state.py
+++ /dev/null
@@ -1,86 +0,0 @@
-import os
-import subprocess
-import tempfile
-from collections.abc import Callable
-from pathlib import Path
-from typing import Final
-
-from imandrax_api import bindings as xbinding
-
-from imandrax_api_models import proto_models
-
-
-def option_map[T, U](v: T | None, f: Callable[[T], U]) -> U | None:
-    if v is None:
-        return None
-    else:
-        return f(v)
-
-
-PO_RES_PP_BIN_PATH: Final[Path | None] = option_map(
-    os.getenv('IMANDRAX_PO_RES_PP_BIN_PATH'), Path
-)
-
-
-def pp_goal_state(
-    po_res: Path
-    | xbinding.api_pb2.ArtifactZip
-    | proto_models.ArtifactZip
-    | proto_models.Art
-    | xbinding.artmsg_pb2.Art,
-) -> str:
-    """
-    Run the pp-goal-state binary on the given po-res file.
-
-    Args:
-        po_res:
-            - the zip path, or json path
-                - for zip file, it will contains manifest.json inside it
-                - the json file is assumed to be dumped Artifact, with
-                    kind, data, and api_version fields
-            - if it's an api_pb2.ArtifactZip, we create a temp zip file
-
-    """
-    if PO_RES_PP_BIN_PATH is None or (not PO_RES_PP_BIN_PATH.exists()):
-        raise FileNotFoundError('imandrax-pp-goal-state binary not found')
-
-    match po_res:
-        # Base case
-        # --------------------
-        case Path():
-            if po_res.suffix not in ('.zip', '.json'):
-                raise ValueError('po_res must be a zip or json file')
-            out = subprocess.run(
-                [
-                    f'{str(PO_RES_PP_BIN_PATH)}',
-                    f'{str(po_res)}',
-                ],
-                capture_output=True,
-            )
-            if out.returncode != 0:
-                raise RuntimeError(f'pp_goal_state failed: {out.stderr.decode()}')
-            return out.stdout.decode()
-        # Turn into base case
-        # --------------------
-        case xbinding.api_pb2.ArtifactZip() | proto_models.ArtifactZip():
-            with tempfile.NamedTemporaryFile(suffix='.zip') as tmp:
-                tmp.write(po_res.art_zip)
-                tmp.flush()
-                return pp_goal_state(Path(tmp.name))
-
-        case proto_models.Art():
-            with tempfile.NamedTemporaryFile(suffix='.json') as tmp:
-                tmp.write(bytes(po_res.model_dump_json(), encoding='utf-8'))
-                tmp.flush()
-                return pp_goal_state(Path(tmp.name))
-
-        case xbinding.artmsg_pb2.Art():
-            with tempfile.NamedTemporaryFile(suffix='.json') as tmp:
-                tmp.write(
-                    bytes(
-                        proto_models.Art.model_validate(po_res).model_dump_json(),
-                        encoding='utf-8',
-                    )
-                )
-                tmp.flush()
-                return pp_goal_state(Path(tmp.name))
diff --git a/packages/imandrax-api-models/tests/test_pp_goal_state.py b/packages/imandrax-api-models/tests/test_pp_goal_state.py
deleted file mode 100644
index ffd848fa..00000000
--- a/packages/imandrax-api-models/tests/test_pp_goal_state.py
+++ /dev/null
@@ -1,79 +0,0 @@
-# %%
-import os
-
-import imandrax_api.bindings as xbinding
-import pytest
-from imandrax_api import Client, url_dev, url_prod  # noqa: F401, RUF100
-from inline_snapshot import snapshot
-
-from imandrax_api_models import Task
-from imandrax_api_models.client import ImandraXClient
-from imandrax_api_models.pp_goal_state import PO_RES_PP_BIN_PATH, pp_goal_state
-
-
-@pytest.mark.skipif(
-    PO_RES_PP_BIN_PATH is None, reason='PO_res pretty-printer binary not set in env'
-)
-def test_pp_goal_state():
-    c = ImandraXClient(
-        url=url_dev,
-        auth_token=os.environ['IMANDRAX_API_KEY'],
-    )
-
-    IML = """
-    let rec prepend (x:'a) (sets:'a list list) : 'a list list =
-    match sets with
-    | [] -> []
-    | s::ss -> (x::s) :: prepend x ss
-    [@@measure (Ordinal.of_int (List.length sets))] [@@by auto]
-
-    (* Powerset of a list: P([]) = [[]]; P(x::xs) = P(xs) @ (map (x::) (P(xs))) *)
-    let rec powerset (xs:'a list) : 'a list list =
-    match xs with
-    | [] -> [[]]
-    | x::xt ->
-        let ps = powerset xt in
-        ps @ (prepend x ps)
-    [@@measure (Ordinal.of_int (List.length xs))] [@@by auto]
-
-    let rec pow (a:int) (n:int) : int =
-    if n <= 0 then 1 else a * pow a (n - 1)
-    [@@measure (Ordinal.of_int n)] [@@by auto]
-
-    theorem pow_zero a = pow a 0 = 1 [@@by auto]
-
-    theorem pow_succ a n =
-    n >= 0 ==> pow a (n + 1) = a * pow a n
-    [@@by intros @> auto]
-
-    theorem pow2_step n =
-    n >= 0 ==> pow 2 (n + 1) = 2 * pow 2 n
-    [@@by intros @> [%use pow_succ 2 n] @> auto]
-
-    lemma len_append x y =
-    List.length (x @ y) = List.length x + List.length y
-    """
-
-    eval_res = c.eval_src(IML)
-
-    task: Task = eval_res.tasks[0]
-    po_res_art_zip: xbinding.api_pb2.ArtifactZip = Client.get_artifact_zip(
-        c,
-        task.to_proto(),
-        kind='po_res',
-    )
-
-    assert po_res_art_zip.art_zip, 'No data in po_res zip'
-
-    goal_state_s = pp_goal_state(po_res_art_zip)
-
-    assert goal_state_s == snapshot("""\
-1 subgoal -
- \n\
-|------------------------------------------------------------
- (List.length (List.append x y))
- =
- ((List.length x) + (List.length y))
-
-
-""")

From 663c15679b1c57a2c445ccd6e7f779c17353fe4a Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Thu, 9 Apr 2026 10:22:00 +0100
Subject: [PATCH 20/25] deprecate grouped rd, sort region groups

---
 .../src/imandrax_api_models/region_decomp.py  | 85 +++----------------
 1 file changed, 14 insertions(+), 71 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index e0828bc0..928f8bc8 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -15,12 +15,6 @@
 from imandrax_api_models.proto_models import DecomposeRes, Error
 from imandrax_api_models.yaml_utils import str_representer
 
-__all__ = (
-    'RegionGroup',
-    'group_regions',
-    'GroupedRegionDecomposition',
-)
-
 
 @dataclass
 class HumDecomposeRes:
@@ -77,6 +71,16 @@ def summary(self) -> dict[str, str | int] | None:
 
                 return {'n_regions': n_regions, 'max_depth': max_depth}
 
+    @staticmethod
+    def dumper_func(depth_limit: int | None = None) -> Callable[..., str]:
+        dumper_cls = mk_dumper(depth_limit=depth_limit)
+        return partial(
+            yaml.dump,
+            Dumper=dumper_cls,
+            default_flow_style=False,
+            sort_keys=False,
+        )
+
     def to_dict_hierarchical(
         self,
         depth_limit: int | None = None,
@@ -143,7 +147,7 @@ def n_regions(self) -> int:
         return 1 + sum(c.n_regions() for c in self.children)
 
     def n_descendant_regions(self) -> int:
-        return sum(c.n_descendant_regions() for c in self.children)
+        return self.n_regions() - 1
 
 
 def group_regions(regions: list[RegionStr]) -> list[RegionGroup]:
@@ -198,7 +202,7 @@ def loop(
     group_and_id_lst = list(zip(groups, initial_ids, strict=True))
     acc: list[IndexedRegionGroup] = []
     loop(group_and_id_lst, acc, 1)
-    return acc
+    return acc[::-1]
 
 
 def _max_depth_of_groups(groups: list[RegionGroup]) -> int:
@@ -215,67 +219,6 @@ def loop(groups: list[RegionGroup]):
     return init
 
 
-@dataclass
-class GroupedRegionDecomposition:
-    groups: list[RegionGroup]
-
-    def summary(self) -> dict[str, str | int]:
-        n_regions = sum([rg.n_descendant_regions() for rg in self.groups])
-        max_depth = _max_depth_of_groups(self.groups)
-
-        return {'n_regions': n_regions, 'max_depth': max_depth}
-
-    @classmethod
-    def from_groups(cls, groups: list[RegionGroup]) -> Self:
-        return cls(groups=groups)
-
-    @classmethod
-    def from_regions(cls, regions: list[RegionStr]) -> Self:
-        return cls.from_groups(group_regions(regions))
-
-    def to_tree_str(
-        self,
-        *,
-        depth_limit: int | None = None,
-        summarize: RegionGroupSummarizer | None = None,
-    ) -> str:
-        summarize_ = summarize or default_region_group_summary
-        lines: list[str] = []
-        for i, group in enumerate(self.groups):
-            is_last = i == len(self.groups) - 1
-            _tree_lines(
-                lines,
-                group,
-                prefix='',
-                is_last=is_last,
-                depth_limit=depth_limit,
-                summarize=summarize_,
-            )
-        return '\n'.join(lines)
-
-    @staticmethod
-    def dumper_func(depth_limit: int | None = None) -> Callable[..., str]:
-        dumper_cls = mk_dumper(depth_limit=depth_limit)
-        return partial(
-            yaml.dump,
-            Dumper=dumper_cls,
-            default_flow_style=False,
-            sort_keys=False,
-        )
-
-    def to_yaml_str(
-        self,
-        depth_limit: int | None = None,
-    ) -> str:
-        to_dump = {'summary': self.summary(), 'region_groups': self.groups}
-        return self.dumper_func(depth_limit)(to_dump)
-
-    def to_yaml_str_flat(self) -> str:
-        indexed_groups = indexed_of_region_groups(self.groups)
-        to_dump = {'summary': self.summary(), 'region_groups': indexed_groups}
-        return self.dumper_func()(to_dump)
-
-
 class RegionGroupSummarizer(Protocol):
     def __call__(self, group: RegionGroup) -> str: ...
 
@@ -291,7 +234,7 @@ def default_region_group_summary(group: RegionGroup) -> str:
         f'[{label}]',
         f'{constraint=}',
         f'{invariant=}',
-        f'(w={group.weight}, children={len(group.children)}, descendants={group.n_descendant_regions()})',
+        f'(w={group.weight}, n_children={len(group.children)}, n_descendants={group.n_descendant_regions()})',
     ]
     return ' '.join(parts)
 
@@ -471,7 +414,7 @@ def loop(
     init = Acc(
         groups=[], regions=regions, idx_path=idx_path, constraint_path=constraint_path
     )
-    return reduce(loop, constraints_by_most_frequent, init)['groups']
+    return reduce(loop, constraints_by_most_frequent, init)['groups'][::-1]
 
 
 # YAML Dump

From 5338f4314e9ae1c457e4c159dd56258b176309c0 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Thu, 9 Apr 2026 10:44:19 +0100
Subject: [PATCH 21/25] rename hum-region-decomp-res factory methods

---
 .../src/imandrax_api_models/region_decomp.py               | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index 928f8bc8..98fdbfa2 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -34,9 +34,14 @@ def mk_fail(cls, pl: list[Error]) -> Self:
         return cls(_variants=('Fail', pl))
 
     @classmethod
-    def of_decomp_res(cls, v: DecomposeRes) -> HumDecomposeRes:
+    def from_decomp_res(cls, v: DecomposeRes) -> HumDecomposeRes:
         return hum_of_decomp_res(v)
 
+    @classmethod
+    def from_regions(cls, regions: list[RegionStr]) -> HumDecomposeRes:
+        groups = group_regions(regions)
+        return HumDecomposeRes.mk_success(groups)
+
     def to_tree_str(
         self,
         *,

From 94fffc7a92a4f3ecf61b30f23fc61cc9e8e57e14 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Thu, 9 Apr 2026 10:44:26 +0100
Subject: [PATCH 22/25] TEST: hum-rd-res

---
 .../tests/test_grouped_region_decomp.py       | 359 ++++++++++++++++++
 1 file changed, 359 insertions(+)
 create mode 100644 packages/imandrax-api-models/tests/test_grouped_region_decomp.py

diff --git a/packages/imandrax-api-models/tests/test_grouped_region_decomp.py b/packages/imandrax-api-models/tests/test_grouped_region_decomp.py
new file mode 100644
index 00000000..533659d0
--- /dev/null
+++ b/packages/imandrax-api-models/tests/test_grouped_region_decomp.py
@@ -0,0 +1,359 @@
+import imandrax_api
+from imandrax_api.lib import RegionStr
+from inline_snapshot import snapshot
+
+from imandrax_api_models.region_decomp import HumDecomposeRes
+
+
+def trust():
+    import os
+    from typing import NoReturn
+
+    import dotenv
+
+    from imandrax_api_models.client import ImandraXClient
+
+    dotenv.load_dotenv()
+    c = ImandraXClient(
+        url=imandrax_api.url_prod,
+        auth_token=os.environ['IMANDRAX_API_KEY'],
+    )
+    IML_CODE = """\
+    let classify (x : int) (y : int) : int =
+    if x > 0 then
+        if y > 0 then
+        if x > y then 1
+        else 2
+        else
+        if y < -10 then 3
+        else 4
+    else
+        if y > 0 then 5
+        else 6"""
+    _eval_res = c.eval_src(IML_CODE)
+    decomp_res = c.decompose(name='classify')
+
+    def raise_(exc: BaseException) -> NoReturn:
+        raise exc
+
+    regions: list[RegionStr] = (
+        decomp_res.regions_str
+        if (decomp_res.regions_str)
+        else (raise_(ValueError('No regions')))
+    )
+    return regions
+
+
+def test():
+    # regions = trust()
+    # assert regions == snapshot()
+    regions = [
+        RegionStr(
+            constraints_str=['x <= 0', 'y <= 0'],
+            invariant_str='6',
+            model_str={'x': '0', 'y': '0'},
+            model_eval_str='6',
+        ),
+        RegionStr(
+            constraints_str=['y >= 1', 'x <= 0'],
+            invariant_str='5',
+            model_str={'x': '0', 'y': '1'},
+            model_eval_str='5',
+        ),
+        RegionStr(
+            constraints_str=['x >= 1', 'y >= (-10)', 'y <= 0'],
+            invariant_str='4',
+            model_str={'x': '1', 'y': '0'},
+            model_eval_str='4',
+        ),
+        RegionStr(
+            constraints_str=['x >= 1', 'y <= (-11)'],
+            invariant_str='3',
+            model_str={'x': '1', 'y': '(-11)'},
+            model_eval_str='3',
+        ),
+        RegionStr(
+            constraints_str=['x <= y', 'x >= 1', 'y >= 1'],
+            invariant_str='2',
+            model_str={'x': '1', 'y': '1'},
+            model_eval_str='2',
+        ),
+        RegionStr(
+            constraints_str=['not (x <= y)', 'x >= 1', 'y >= 1'],
+            invariant_str='1',
+            model_str={'x': '2', 'y': '1'},
+            model_eval_str='1',
+        ),
+    ]
+
+    hdr = HumDecomposeRes.from_regions(regions)
+    assert hdr.to_tree_str() == snapshot("""\
+├── [1] constraint='x <= 0' invariant=None (w=2, n_children=2, n_descendants=2)
+│   ├── [1.1] constraint='y <= 0' invariant='6' (w=1, n_children=0, n_descendants=0)
+│   └── [1.1.2] constraint='y >= 1' invariant='5' (w=1, n_children=0, n_descendants=0)
+├── [1.2.1.1] constraint='y >= (-10)' invariant='4' (w=1, n_children=0, n_descendants=0)
+├── [1.2.3] constraint='y >= 1' invariant=None (w=2, n_children=2, n_descendants=2)
+│   ├── [1.2.3.1.1] constraint='x >= 1' invariant='2' (w=1, n_children=0, n_descendants=0)
+│   └── [1.2.3.1.2.1] constraint='not (x <= y)' invariant='1' (w=1, n_children=0, n_descendants=0)
+└── [1.2.3.4.1] constraint='y <= (-11)' invariant='3' (w=1, n_children=0, n_descendants=0)\
+""")
+    hdr_dict_hierarchy = hdr.to_dict_hierarchical()
+    hdr_dict_flat = hdr.to_dict_flat()
+
+    assert (hdr.dumper_func()(hdr_dict_hierarchy)) == snapshot("""\
+summary:
+  n_regions: 8
+  max_depth: 6
+region_groups:
+- !RegionGroup
+  label_path: '1'
+  weight: 2
+  constraints:
+  - x <= 0
+  introduced_constraint: x <= 0
+  n_children_regions: 2
+  n_descendant_regions: 2
+  children:
+  - !RegionGroup
+    label_path: '1.1'
+    weight: 1
+    constraints:
+    - x <= 0
+    - y <= 0
+    introduced_constraint: y <= 0
+    invariant: '6'
+    example_input:
+      x: '0'
+      y: '0'
+    example_output: '6'
+    n_children_regions: 0
+    n_descendant_regions: 0
+  - !RegionGroup
+    label_path: 1.1.2
+    weight: 1
+    constraints:
+    - x <= 0
+    - y <= 0
+    - y >= 1
+    introduced_constraint: y >= 1
+    invariant: '5'
+    example_input:
+      x: '0'
+      y: '1'
+    example_output: '5'
+    n_children_regions: 0
+    n_descendant_regions: 0
+- !RegionGroup
+  label_path: 1.2.1.1
+  weight: 1
+  constraints:
+  - x <= 0
+  - y <= 0
+  - x >= 1
+  - y >= (-10)
+  introduced_constraint: y >= (-10)
+  invariant: '4'
+  example_input:
+    x: '1'
+    y: '0'
+  example_output: '4'
+  n_children_regions: 0
+  n_descendant_regions: 0
+- !RegionGroup
+  label_path: 1.2.3
+  weight: 2
+  constraints:
+  - x <= 0
+  - y <= 0
+  - y >= 1
+  introduced_constraint: y >= 1
+  n_children_regions: 2
+  n_descendant_regions: 2
+  children:
+  - !RegionGroup
+    label_path: 1.2.3.1.1
+    weight: 1
+    constraints:
+    - x <= 0
+    - y <= 0
+    - y >= 1
+    - x <= y
+    - x >= 1
+    introduced_constraint: x >= 1
+    invariant: '2'
+    example_input:
+      x: '1'
+      y: '1'
+    example_output: '2'
+    n_children_regions: 0
+    n_descendant_regions: 0
+  - !RegionGroup
+    label_path: 1.2.3.1.2.1
+    weight: 1
+    constraints:
+    - x <= 0
+    - y <= 0
+    - y >= 1
+    - x <= y
+    - x >= 1
+    - not (x <= y)
+    introduced_constraint: not (x <= y)
+    invariant: '1'
+    example_input:
+      x: '2'
+      y: '1'
+    example_output: '1'
+    n_children_regions: 0
+    n_descendant_regions: 0
+- !RegionGroup
+  label_path: 1.2.3.4.1
+  weight: 1
+  constraints:
+  - x <= 0
+  - y <= 0
+  - y >= 1
+  - x >= 1
+  - y <= (-11)
+  introduced_constraint: y <= (-11)
+  invariant: '3'
+  example_input:
+    x: '1'
+    y: (-11)
+  example_output: '3'
+  n_children_regions: 0
+  n_descendant_regions: 0
+""")
+
+    assert (hdr.dumper_func()(hdr_dict_flat)) == snapshot("""\
+summary:
+  n_regions: 8
+  max_depth: 6
+region_groups:
+- id: '3'
+  label_path: 1.2.3.4.1
+  depth: 1
+  weight: 1
+  constraints:
+  - x <= 0
+  - y <= 0
+  - y >= 1
+  - x >= 1
+  - y <= (-11)
+  introduced_constraint: y <= (-11)
+  invariant: '3'
+  example_input:
+    x: '1'
+    y: (-11)
+  example_output: '3'
+  n_children_regions: 0
+  children: []
+- id: '7'
+  label_path: 1.2.3.1.2.1
+  depth: 2
+  weight: 1
+  constraints:
+  - x <= 0
+  - y <= 0
+  - y >= 1
+  - x <= y
+  - x >= 1
+  - not (x <= y)
+  introduced_constraint: not (x <= y)
+  invariant: '1'
+  example_input:
+    x: '2'
+    y: '1'
+  example_output: '1'
+  n_children_regions: 0
+  children: []
+- id: '6'
+  label_path: 1.2.3.1.1
+  depth: 2
+  weight: 1
+  constraints:
+  - x <= 0
+  - y <= 0
+  - y >= 1
+  - x <= y
+  - x >= 1
+  introduced_constraint: x >= 1
+  invariant: '2'
+  example_input:
+    x: '1'
+    y: '1'
+  example_output: '2'
+  n_children_regions: 0
+  children: []
+- id: '2'
+  label_path: 1.2.3
+  depth: 1
+  weight: 2
+  constraints:
+  - x <= 0
+  - y <= 0
+  - y >= 1
+  introduced_constraint: y >= 1
+  n_children_regions: 2
+  children:
+  - '6'
+  - '7'
+- id: '1'
+  label_path: 1.2.1.1
+  depth: 1
+  weight: 1
+  constraints:
+  - x <= 0
+  - y <= 0
+  - x >= 1
+  - y >= (-10)
+  introduced_constraint: y >= (-10)
+  invariant: '4'
+  example_input:
+    x: '1'
+    y: '0'
+  example_output: '4'
+  n_children_regions: 0
+  children: []
+- id: '5'
+  label_path: 1.1.2
+  depth: 2
+  weight: 1
+  constraints:
+  - x <= 0
+  - y <= 0
+  - y >= 1
+  introduced_constraint: y >= 1
+  invariant: '5'
+  example_input:
+    x: '0'
+    y: '1'
+  example_output: '5'
+  n_children_regions: 0
+  children: []
+- id: '4'
+  label_path: '1.1'
+  depth: 2
+  weight: 1
+  constraints:
+  - x <= 0
+  - y <= 0
+  introduced_constraint: y <= 0
+  invariant: '6'
+  example_input:
+    x: '0'
+    y: '0'
+  example_output: '6'
+  n_children_regions: 0
+  children: []
+- id: '0'
+  label_path: '1'
+  depth: 1
+  weight: 2
+  constraints:
+  - x <= 0
+  introduced_constraint: x <= 0
+  n_children_regions: 2
+  children:
+  - '4'
+  - '5'
+""")

From 328a3d3ae01eb515474657c52d4cec21e9f9ab10 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Thu, 9 Apr 2026 10:50:47 +0100
Subject: [PATCH 23/25] TEST: label path |-> n children map should match for
 flat and hierarchy case

---
 .../tests/test_grouped_region_decomp.py       | 23 ++++++++++++++++++-
 1 file changed, 22 insertions(+), 1 deletion(-)

diff --git a/packages/imandrax-api-models/tests/test_grouped_region_decomp.py b/packages/imandrax-api-models/tests/test_grouped_region_decomp.py
index 533659d0..17873f8e 100644
--- a/packages/imandrax-api-models/tests/test_grouped_region_decomp.py
+++ b/packages/imandrax-api-models/tests/test_grouped_region_decomp.py
@@ -2,7 +2,7 @@
 from imandrax_api.lib import RegionStr
 from inline_snapshot import snapshot
 
-from imandrax_api_models.region_decomp import HumDecomposeRes
+from imandrax_api_models.region_decomp import HumDecomposeRes, RegionGroup
 
 
 def trust():
@@ -99,6 +99,27 @@ def test():
 """)
     hdr_dict_hierarchy = hdr.to_dict_hierarchical()
     hdr_dict_flat = hdr.to_dict_flat()
+    label_path_n_children_map_flat: list[tuple[str, int]] = [
+        ('.'.join(map(str, irg.label_path)), len(irg.children))
+        for irg in hdr_dict_flat['region_groups']
+    ]
+
+    # ::: test-child-count
+    def _collect_hierarchy(groups: list[RegionGroup]) -> list[tuple[str, int]]:
+        result: list[tuple[str, int]] = []
+        for rg in groups:
+            result.append(('.'.join(map(str, rg.label_path)), len(rg.children)))
+            if rg.children:
+                result.extend(_collect_hierarchy(rg.children))
+        return result
+
+    label_path_n_children_map_hierarchy: list[tuple[str, int]] = _collect_hierarchy(
+        hdr_dict_hierarchy['region_groups']
+    )
+    assert sorted(label_path_n_children_map_flat) == sorted(
+        label_path_n_children_map_hierarchy
+    )
+    # :::
 
     assert (hdr.dumper_func()(hdr_dict_hierarchy)) == snapshot("""\
 summary:

From dafe3c143c841c7b10644fca80febb70a0774b96 Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Thu, 9 Apr 2026 11:09:29 +0100
Subject: [PATCH 24/25] refresh id generator when indexing

---
 .../src/imandrax_api_models/region_decomp.py       | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index 98fdbfa2..e5ad3d9e 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -173,21 +173,19 @@ class IndexedRegionGroup:
     depth: int  # 1-indexed depth
 
 
-_counter = itertools.count()
-
-
-def _gen_id() -> str:
-    return str(next(_counter))
+def indexed_of_region_groups(groups: list[RegionGroup]) -> list[IndexedRegionGroup]:
+    id_generator = (str(i) for i in itertools.count())
 
+    def gen_id() -> str:
+        return next(id_generator)
 
-def indexed_of_region_groups(groups: list[RegionGroup]) -> list[IndexedRegionGroup]:
     def loop(
         group_and_id_lst: list[tuple[RegionGroup, str]],
         acc: list[IndexedRegionGroup],
         depth: int,
     ) -> None:
         for rg, id in group_and_id_lst:
-            c_ids = [_gen_id() for _ in rg.children]
+            c_ids = [gen_id() for _ in rg.children]
 
             irg = IndexedRegionGroup(
                 id=id,
@@ -203,7 +201,7 @@ def loop(
             children_group_and_id_lst = list(zip(rg.children, c_ids, strict=True))
             loop(children_group_and_id_lst, acc, depth + 1)
 
-    initial_ids = [_gen_id() for _ in groups]
+    initial_ids = [gen_id() for _ in groups]
     group_and_id_lst = list(zip(groups, initial_ids, strict=True))
     acc: list[IndexedRegionGroup] = []
     loop(group_and_id_lst, acc, 1)

From a0363d99733e872ef6efc2bbffef0d01e7a3464e Mon Sep 17 00:00:00 2001
From: hongyu <linerwang1997@gmail.com>
Date: Thu, 9 Apr 2026 11:11:15 +0100
Subject: [PATCH 25/25] FIX: sort indexed region groups

---
 .../src/imandrax_api_models/region_decomp.py  |   2 +-
 .../tests/test_grouped_region_decomp.py       | 122 +++++++++---------
 2 files changed, 62 insertions(+), 62 deletions(-)

diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
index e5ad3d9e..210a5bac 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py
@@ -205,7 +205,7 @@ def loop(
     group_and_id_lst = list(zip(groups, initial_ids, strict=True))
     acc: list[IndexedRegionGroup] = []
     loop(group_and_id_lst, acc, 1)
-    return acc[::-1]
+    return acc
 
 
 def _max_depth_of_groups(groups: list[RegionGroup]) -> int:
diff --git a/packages/imandrax-api-models/tests/test_grouped_region_decomp.py b/packages/imandrax-api-models/tests/test_grouped_region_decomp.py
index 17873f8e..368aca89 100644
--- a/packages/imandrax-api-models/tests/test_grouped_region_decomp.py
+++ b/packages/imandrax-api-models/tests/test_grouped_region_decomp.py
@@ -250,59 +250,63 @@ def _collect_hierarchy(groups: list[RegionGroup]) -> list[tuple[str, int]]:
   n_regions: 8
   max_depth: 6
 region_groups:
-- id: '3'
-  label_path: 1.2.3.4.1
+- id: '0'
+  label_path: '1'
   depth: 1
+  weight: 2
+  constraints:
+  - x <= 0
+  introduced_constraint: x <= 0
+  n_children_regions: 2
+  children:
+  - '4'
+  - '5'
+- id: '4'
+  label_path: '1.1'
+  depth: 2
   weight: 1
   constraints:
   - x <= 0
   - y <= 0
-  - y >= 1
-  - x >= 1
-  - y <= (-11)
-  introduced_constraint: y <= (-11)
-  invariant: '3'
+  introduced_constraint: y <= 0
+  invariant: '6'
   example_input:
-    x: '1'
-    y: (-11)
-  example_output: '3'
+    x: '0'
+    y: '0'
+  example_output: '6'
   n_children_regions: 0
   children: []
-- id: '7'
-  label_path: 1.2.3.1.2.1
+- id: '5'
+  label_path: 1.1.2
   depth: 2
   weight: 1
   constraints:
   - x <= 0
   - y <= 0
   - y >= 1
-  - x <= y
-  - x >= 1
-  - not (x <= y)
-  introduced_constraint: not (x <= y)
-  invariant: '1'
+  introduced_constraint: y >= 1
+  invariant: '5'
   example_input:
-    x: '2'
+    x: '0'
     y: '1'
-  example_output: '1'
+  example_output: '5'
   n_children_regions: 0
   children: []
-- id: '6'
-  label_path: 1.2.3.1.1
-  depth: 2
+- id: '1'
+  label_path: 1.2.1.1
+  depth: 1
   weight: 1
   constraints:
   - x <= 0
   - y <= 0
-  - y >= 1
-  - x <= y
   - x >= 1
-  introduced_constraint: x >= 1
-  invariant: '2'
+  - y >= (-10)
+  introduced_constraint: y >= (-10)
+  invariant: '4'
   example_input:
     x: '1'
-    y: '1'
-  example_output: '2'
+    y: '0'
+  example_output: '4'
   n_children_regions: 0
   children: []
 - id: '2'
@@ -318,63 +322,59 @@ def _collect_hierarchy(groups: list[RegionGroup]) -> list[tuple[str, int]]:
   children:
   - '6'
   - '7'
-- id: '1'
-  label_path: 1.2.1.1
-  depth: 1
+- id: '6'
+  label_path: 1.2.3.1.1
+  depth: 2
   weight: 1
   constraints:
   - x <= 0
   - y <= 0
+  - y >= 1
+  - x <= y
   - x >= 1
-  - y >= (-10)
-  introduced_constraint: y >= (-10)
-  invariant: '4'
+  introduced_constraint: x >= 1
+  invariant: '2'
   example_input:
     x: '1'
-    y: '0'
-  example_output: '4'
+    y: '1'
+  example_output: '2'
   n_children_regions: 0
   children: []
-- id: '5'
-  label_path: 1.1.2
+- id: '7'
+  label_path: 1.2.3.1.2.1
   depth: 2
   weight: 1
   constraints:
   - x <= 0
   - y <= 0
   - y >= 1
-  introduced_constraint: y >= 1
-  invariant: '5'
+  - x <= y
+  - x >= 1
+  - not (x <= y)
+  introduced_constraint: not (x <= y)
+  invariant: '1'
   example_input:
-    x: '0'
+    x: '2'
     y: '1'
-  example_output: '5'
+  example_output: '1'
   n_children_regions: 0
   children: []
-- id: '4'
-  label_path: '1.1'
-  depth: 2
+- id: '3'
+  label_path: 1.2.3.4.1
+  depth: 1
   weight: 1
   constraints:
   - x <= 0
   - y <= 0
-  introduced_constraint: y <= 0
-  invariant: '6'
+  - y >= 1
+  - x >= 1
+  - y <= (-11)
+  introduced_constraint: y <= (-11)
+  invariant: '3'
   example_input:
-    x: '0'
-    y: '0'
-  example_output: '6'
+    x: '1'
+    y: (-11)
+  example_output: '3'
   n_children_regions: 0
   children: []
-- id: '0'
-  label_path: '1'
-  depth: 1
-  weight: 2
-  constraints:
-  - x <= 0
-  introduced_constraint: x <= 0
-  n_children_regions: 2
-  children:
-  - '4'
-  - '5'
 """)