diff --git a/packages/imandrax-api-models/src/imandrax_api_models/context_utils.py b/packages/imandrax-api-models/src/imandrax_api_models/context_utils.py
index c8955789..1c55fe60 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/context_utils.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/context_utils.py
@@ -15,6 +15,7 @@
Position,
VerifyRes,
)
+from imandrax_api_models.region_decomp import EnrichedDecomposeRes
from imandrax_api_models.yaml_utils import ImandraXAPIModelDumper
@@ -317,3 +318,19 @@ def format_decomp_res(decomp_res: DecomposeRes) -> str:
data = remove_art_and_task_fields(data)
return yaml.dump(data, Dumper=ImandraXAPIModelDumper, width=120)
+
+
+def format_enriched_decomp_res(decomp_res: EnrichedDecomposeRes) -> dict[str, Any]:
+ # TOOD: use remove_fields_rec
+ d: dict[str, Any] = {}
+ if decomp_res.regions_str is not None:
+ enriched_regions = decomp_res.regions()
+ d['descr'] = f'Decomp succeeded with {len(enriched_regions)} regions'
+ d['regions'] = enriched_regions
+ else:
+ d['descr'] = 'Decomp failed'
+ d |= remove_art_and_task_fields(decomp_res.model_dump())
+ d.pop('regions_str')
+ d.pop('region_groups')
+
+ return d
diff --git a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp/__init__.py b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp/__init__.py
index f25edc2c..6be0cc01 100644
--- a/packages/imandrax-api-models/src/imandrax_api_models/region_decomp/__init__.py
+++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp/__init__.py
@@ -1,168 +1,112 @@
-"""Post-processing (Hierarchical groupping) for region decomposition."""
+"""Post-processing (hierarchical grouping) for region decomposition."""
from __future__ import annotations
-import itertools
-from collections.abc import Callable
-from dataclasses import dataclass
-from functools import partial, reduce
-from typing import Any, Literal, NoReturn, Protocol, Self, TypedDict
+from collections.abc import Callable, Mapping, Sequence
+from dataclasses import asdict
+from functools import reduce
+from typing import NoReturn, Self, TypedDict
-import yaml
from devtools import pformat
from imandrax_api.lib import RegionStr
+from pydantic import BaseModel, Field, model_validator
-from imandrax_api_models.proto_models import DecomposeRes, Error
-from imandrax_api_models.yaml_utils import str_representer
+from imandrax_api_models.proto_models import DecomposeRes
from .icicle_widget import mk_icicle_widget_html
-@dataclass
-class HumDecomposeRes:
- """Human readable decomp result"""
+class EnrichedDecomposeRes(DecomposeRes):
+ """A `DecomposeRes` augmented with hierarchical region grouping."""
- _variants: (
- tuple[Literal['Success'], list[RegionGroup]]
- | tuple[Literal['Fail'], list[Error]]
+ region_groups: list[RegionGroup] = Field(
+ default_factory=list,
+ description='Region groups grouped by constraints, containing child groups recursively. Empty when no regions are available (decomposition 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 from_decomp_res(cls, v: DecomposeRes) -> HumDecomposeRes:
- return hum_of_decomp_res(v)
+ @model_validator(mode='after')
+ def populate_region_groups(self) -> Self:
+ if not self.region_groups and self.regions_str:
+ self.region_groups = group_regions(self.regions_str)
+ return self
@classmethod
- def from_regions(cls, regions: list[RegionStr]) -> HumDecomposeRes:
- groups = group_regions(regions)
- return HumDecomposeRes.mk_success(groups)
+ def from_decomp_res(cls, v: DecomposeRes) -> EnrichedDecomposeRes:
+ return cls.model_validate(v.model_dump())
+
+ def regions(self) -> JSONArray:
+ """Leaf region groups (concrete regions) with hierarchical grouping info."""
+ leaf_groups = get_leaf_groups(self.region_groups)
+ ds = []
+ for leaf_group in leaf_groups:
+ d: JSONObject = {}
+ assert leaf_group.region is not None, 'Leaf group must be concrete'
+ d['label_path'] = '.'.join(map(str, leaf_group.label_path))
+ d['weight'] = leaf_group.weight
+ d |= asdict(leaf_group.region)
+ ds.append(d)
+ return ds
def to_tree_str(
self,
*,
depth_limit: int | None = None,
- summarize: RegionGroupSummarizer | None = None,
+ summarize: Callable[[RegionGroup], str] | 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):
- return {
- 'n_regions': _count_leaf_regions(groups),
- # 'n_regions': sum(rg.n_regions() for rg in groups),
- # 'n_leaf_regions': _count_leaf_regions(groups),
- # 'max_depth': _max_tree_depth_of_groups(groups),
- # 'max_label_depth': _max_label_depth_of_groups(groups),
- # 'max_constraints_per_region': _max_constraints_per_region(groups),
- }
-
- @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,
+ if self.errors:
+ return pformat(self.errors, indent=2)
+ return render_region_groups(
+ self.region_groups, depth_limit=depth_limit, tree_repr=summarize
)
- 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 _repr_html_(self) -> str:
- match self._variants:
- case ('Fail', errs):
- return f'{pformat(errs, indent=2)}'
- case ('Success', groups):
- return mk_icicle_widget_html(groups)
-
-
-def hum_of_decomp_res(decomp_res: DecomposeRes) -> HumDecomposeRes:
- if decomp_res.err is None:
- regions = decomp_res.regions_str
- if regions is None:
- raise ValueError(
- 'DecomposeRes has no `regions_str`; humanizing regions requires '
- 'the decomposition to be requested with `string_results=True`.'
- )
- groups = group_regions(regions)
- return HumDecomposeRes.mk_success(groups)
-
- else:
- return HumDecomposeRes.mk_fail(decomp_res.errors)
-
-
-@dataclass
-class RegionGroup:
+ if self.errors:
+ return f'{pformat(self.errors, indent=2)}'
+ return mk_icicle_widget_html(self.region_groups)
+
+
+type JSONValue = (
+ str | int | float | bool | None | Mapping[str, JSONValue] | Sequence[JSONValue]
+)
+type JSONObject = dict[str, JSONValue]
+type JSONArray = list[JSONValue]
+
+
+class RegionGroup(BaseModel):
"""
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
- children: list[RegionGroup]
- weight: int
+ constraints: list[str] = Field(
+ description=(
+ '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: list[int] = Field(
+ description=(
+ '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.'
+ )
+ )
+ weight: int = Field(
+ description="Number of regions in the partition at this node's level."
+ )
+ region: RegionStr | None = Field(
+ default=None, description='The concrete region. Present iff at leaf nodes.'
+ )
+ children: list[RegionGroup] = Field(
+ default_factory=list, description='Sub-groups under this node.'
+ )
def n_regions(self) -> int:
"""Total regions in this subtree, including self."""
@@ -173,155 +117,88 @@ def n_descendant_regions(self) -> int:
return self.n_regions() - 1
def n_leaf_regions(self) -> int:
- """Total leaf regions in this subtree, including self if no children."""
+ """Total leaf regions in this subtree, counting self if no children."""
if not self.children:
return 1
return sum(c.n_leaf_regions() for c in self.children)
- def to_dict(self) -> dict[str, Any]:
- """Core fields shared by all serialization formats."""
- d: dict[str, Any] = {
- 'label_path': '.'.join(map(str, self.label_path)),
- 'constraints': self.constraints,
- 'introduced_constraint': self.constraints[-1] if self.constraints else '',
- 'weight': self.weight,
- 'n_children_regions': len(self.children),
- 'n_descendant_regions': self.n_descendant_regions(),
- 'n_leaf_regions': self.n_leaf_regions(),
- }
+ def describe(self) -> JSONObject:
+ d: JSONObject = {}
+ d['label_path'] = '.'.join(map(str, self.label_path))
+ d['constraints'] = self.constraints
+ d['introduced_constraint'] = self.constraints[-1] if self.constraints else ''
+ d['weight'] = self.weight
+ d['n_children_regions'] = len(self.children)
+ d['n_descendant_regions'] = self.n_descendant_regions()
+ d['n_leaf_regions'] = self.n_leaf_regions()
if (r := self.region) is not None:
d['invariant'] = r.invariant_str
d['example_input'] = r.model_str
d['example_output'] = r.model_eval_str
return d
- def to_json_dict(self) -> dict[str, Any]:
- """Serialize to a d3-hierarchy-compatible dict."""
- d = self.to_dict()
+ def to_json_dict(self) -> JSONObject:
+ """Serialize to a d3-hierarchy-compatible dict, recursing into children."""
+ d = self.describe()
if self.children:
d['children'] = [c.to_json_dict() for c in self.children]
return d
-
-def group_regions(regions: list[RegionStr]) -> list[RegionGroup]:
- """Group regions hierarchically based on constraints."""
- 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
- depth: int # 1-indexed depth
-
-
-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 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]
-
- irg = IndexedRegionGroup(
- id=id,
- constraints=rg.constraints,
- label_path=rg.label_path,
- 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, 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, 1)
- return acc
-
-
-def _max_label_depth_of_groups(groups: list[RegionGroup]) -> int:
- """
- Max length of any label_path in the tree (index-chain depth).
-
- Counts collapsed singleton levels since label_path is built before
- singleton promotion in `_loop_group_regions`.
- """
- 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
-
-
-def _max_tree_depth_of_groups(groups: list[RegionGroup]) -> int:
- """Max nesting depth of RegionGroup nodes (matches visual tree)."""
-
- def depth(rg: RegionGroup) -> int:
- return 1 + max((depth(c) for c in rg.children), default=0)
-
- return max((depth(g) for g in groups), default=0)
-
-
-def _count_leaf_regions(groups: list[RegionGroup]) -> int:
- """Count of nodes carrying a concrete RegionStr (region is not None)."""
- total = 0
- for g in groups:
- if g.region is not None:
- total += 1
- total += _count_leaf_regions(g.children)
- return total
+ def repr_line(self) -> str:
+ """One-line representation of the region group."""
+ d = self.describe()
+ parts: list[str] = []
+ parts.append(f'[{d["label_path"]}]')
+ parts.append(f"new_constraint='{d['introduced_constraint']}'")
+ if d.get('invariant'):
+ parts.append(f"invariant='{d['invariant']}'")
+ n_leaf_regions = d['n_leaf_regions']
+ if n_leaf_regions != 1:
+ parts.append(f'n_leaf_regions={n_leaf_regions}')
+ else:
+ parts.append('is_leaf=True')
+ return ' '.join(parts)
-def _max_constraints_per_region(groups: list[RegionGroup]) -> int:
- """Longest constraints list across all nodes."""
+def get_leaf_groups(groups: list[RegionGroup]) -> list[RegionGroup]:
+ leaves = []
+ for group in groups:
+ if not group.children:
+ leaves.append(group)
+ else:
+ leaves.extend(get_leaf_groups(group.children))
+ return leaves
- def walk(rg: RegionGroup) -> int:
- return max(len(rg.constraints), *(walk(c) for c in rg.children), 0)
- return max((walk(g) for g in groups), default=0)
+def group_regions(regions: list[RegionStr]) -> list[RegionGroup]:
+ """Group regions hierarchically based on constraints."""
+ return _loop_group_regions([], [], regions)
-class RegionGroupSummarizer(Protocol):
- def __call__(self, group: RegionGroup) -> str: ...
+# Tree rendering
+# ====================
-def default_region_group_summary(group: RegionGroup) -> str:
- label = '.'.join(map(str, group.label_path))
- # rg_constraints is the full path from root; [-1] is this node's own constraint.
- constraint = group.constraints[-1] if group.constraints else '?'
- invariant: str | None = None
- if (region := group.region) is not None:
- invariant = region.invariant_str
- parts = [
- f'[{label}]',
- f'{constraint=}',
- f'{invariant=}',
- f'(w={group.weight}, n_children={len(group.children)}, n_descendants={group.n_descendant_regions()})',
- ]
- return ' '.join(parts)
+def render_region_groups(
+ groups: list[RegionGroup],
+ *,
+ depth_limit: int | None = None,
+ tree_repr: Callable[[RegionGroup], str] | None = None,
+) -> str:
+ """Render a forest of `RegionGroup`s as a tree in text."""
+ tree_repr_ = tree_repr or RegionGroup.repr_line
+ 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=tree_repr_,
+ )
+ return '\n'.join(lines)
def _tree_lines(
@@ -331,7 +208,7 @@ def _tree_lines(
prefix: str,
is_last: bool,
depth_limit: int | None,
- summarize: RegionGroupSummarizer,
+ summarize: Callable[[RegionGroup], str],
) -> None:
connector = '└── ' if is_last else '├── '
lines.append(f'{prefix}{connector}{summarize(group)}')
@@ -354,6 +231,10 @@ def _tree_lines(
)
+# Grouping algorithm
+# ====================
+
+
def _loop_group_regions(
idx_path: list[int], constraint_path: list[str], regions: list[RegionStr]
) -> list[RegionGroup]:
@@ -386,8 +267,10 @@ def _loop_group_regions(
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['idx_path']` and `acc['constraint_path']` stay constant across
+ iterations (they describe this level). The current `konstraint` is only
+ prepended for the `has` branch's recursion, never carried into later
+ iterations, which process `without` regions that lack `konstraint`.
- `acc['groups']` only grows: new groups are prepended when `has` is non-empty.
"""
@@ -424,8 +307,10 @@ def update_counter(s: str) -> None:
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)
+ # Most frequent first, ties broken alphabetically.
+ assoc_list: list[tuple[str, int]] = sorted(
+ counter.items(), key=lambda kv: (-kv[1], kv[0])
+ )
constraints_by_most_frequent: list[str] = [kv[0] for kv in assoc_list]
# grouped: tuple[list[RegionGroup], list[RegionStr]]
@@ -489,85 +374,19 @@ def loop(
res = [group, *groups], without
else:
res = groups, without
+ # `idx_path` / `constraint_path` describe this level and must stay
+ # constant across reduce iterations. Only the `has` branch (recursed
+ # above) gets the extended `new_idx_path` / `new_constraint_path`; the
+ # `without` regions handled by later iterations do not contain
+ # `konstraint`, so it must not leak into their path.
return Acc(
groups=res[0],
regions=res[1],
- idx_path=new_idx_path,
- constraint_path=new_constraint_path,
+ idx_path=idx_path,
+ constraint_path=constraint_path,
)
init = Acc(
groups=[], regions=regions, idx_path=idx_path, constraint_path=constraint_path
)
return reduce(loop, constraints_by_most_frequent, init)['groups'][::-1]
-
-
-# YAML Dump
-# ====================
-
-
-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] = data.to_dict()
- if data.children:
- if depth_limit is None or depth_limit <= 0:
- mapping['children'] = data.children
- return dumper.represent_mapping('!RegionGroup', mapping)
-
-
-def _indexed_region_group_representer(
- dumper: yaml.Dumper, data: IndexedRegionGroup
-) -> 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
- 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 mk_dumper(*, depth_limit: int | None = None) -> type[yaml.Dumper]:
- class RegionDecompDumper(yaml.Dumper):
- pass
-
- RegionDecompDumper.add_representer(
- RegionStr,
- _region_str_representer,
- )
-
- 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)
-
- RegionDecompDumper.add_representer(RegionGroup, _rg_representer)
- RegionDecompDumper.add_representer(
- IndexedRegionGroup, _indexed_region_group_representer
- )
- RegionDecompDumper.add_representer(str, str_representer)
- return RegionDecompDumper
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 0e057cc3..f59ebadf 100644
--- a/packages/imandrax-api-models/tests/test_grouped_region_decomp.py
+++ b/packages/imandrax-api-models/tests/test_grouped_region_decomp.py
@@ -1,14 +1,18 @@
+import os
+
import imandrax_api
from imandrax_api.lib import RegionStr
from inline_snapshot import snapshot
-from imandrax_api_models.region_decomp import HumDecomposeRes, RegionGroup
-
+from imandrax_api_models.proto_models import DecomposeRes
+from imandrax_api_models.region_decomp import (
+ EnrichedDecomposeRes,
+ RegionGroup,
+ get_leaf_groups,
+)
-def trust():
- import os
- from typing import NoReturn
+def trust() -> DecomposeRes:
import dotenv
from imandrax_api_models.client import ImandraXClient
@@ -31,356 +35,92 @@ def trust():
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
+ return c.decompose(name='classify', string_results=True, prune=True)
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',
- ),
- ]
+ decomp_res = trust()
+ edr = EnrichedDecomposeRes.from_decomp_res(decomp_res)
- 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()
- 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']
- ]
+ assert edr.regions_str
+ leaf_groups = get_leaf_groups(edr.region_groups)
+ assert len(leaf_groups) == len(edr.regions_str)
+ for leaf_group in leaf_groups:
+ assert len(leaf_group.children) == 0
+ assert leaf_group.region, 'Leaf group must be concrete'
+ assert leaf_group.region.constraints_str
+ assert set(leaf_group.constraints) == set(leaf_group.region.constraints_str)
- # ::: 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 edr.regions_str == snapshot(
+ [
+ RegionStr(
+ constraints_str=['y <= 0', 'x <= 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=['y >= (-10)', 'y <= 0', 'x >= 1'],
+ invariant_str='4',
+ model_str={'x': '1', 'y': '0'},
+ model_eval_str='4',
+ ),
+ RegionStr(
+ constraints_str=['y <= (-11)', 'x >= 1'],
+ invariant_str='3',
+ model_str={'x': '1', 'y': '(-11)'},
+ model_eval_str='3',
+ ),
+ RegionStr(
+ constraints_str=['x <= y', 'y >= 1', 'x >= 1'],
+ invariant_str='2',
+ model_str={'x': '1', 'y': '1'},
+ model_eval_str='2',
+ ),
+ RegionStr(
+ constraints_str=['x > y', 'y >= 1', 'x >= 1'],
+ invariant_str='1',
+ model_str={'x': '2', 'y': '1'},
+ model_eval_str='1',
+ ),
+ ]
)
- # :::
- assert (hdr.dumper_func()(hdr_dict_hierarchy)) == snapshot("""\
-summary:
- n_regions: 6
-region_groups:
-- !RegionGroup
- label_path: '1'
- constraints:
- - x <= 0
- introduced_constraint: x <= 0
- weight: 2
- n_children_regions: 2
- n_descendant_regions: 2
- n_leaf_regions: 2
- children:
- - !RegionGroup
- label_path: '1.1'
- constraints:
- - x <= 0
- - y <= 0
- introduced_constraint: y <= 0
- weight: 1
- n_children_regions: 0
- n_descendant_regions: 0
- n_leaf_regions: 1
- invariant: '6'
- example_input:
- x: '0'
- y: '0'
- example_output: '6'
- - !RegionGroup
- label_path: 1.1.2
- constraints:
- - x <= 0
- - y <= 0
- - y >= 1
- introduced_constraint: y >= 1
- weight: 1
- n_children_regions: 0
- n_descendant_regions: 0
- n_leaf_regions: 1
- invariant: '5'
- example_input:
- x: '0'
- y: '1'
- example_output: '5'
-- !RegionGroup
- label_path: 1.2.1.1
- constraints:
- - x <= 0
- - y <= 0
- - x >= 1
- - y >= (-10)
- introduced_constraint: y >= (-10)
- weight: 1
- n_children_regions: 0
- n_descendant_regions: 0
- n_leaf_regions: 1
- invariant: '4'
- example_input:
- x: '1'
- y: '0'
- example_output: '4'
-- !RegionGroup
- label_path: 1.2.3
- constraints:
- - x <= 0
- - y <= 0
- - y >= 1
- introduced_constraint: y >= 1
- weight: 2
- n_children_regions: 2
- n_descendant_regions: 2
- n_leaf_regions: 2
- children:
- - !RegionGroup
- label_path: 1.2.3.1.1
- constraints:
- - x <= 0
- - y <= 0
- - y >= 1
- - x <= y
- - x >= 1
- introduced_constraint: x >= 1
- weight: 1
- n_children_regions: 0
- n_descendant_regions: 0
- n_leaf_regions: 1
- invariant: '2'
- example_input:
- x: '1'
- y: '1'
- example_output: '2'
- - !RegionGroup
- label_path: 1.2.3.1.2.1
- constraints:
- - x <= 0
- - y <= 0
- - y >= 1
- - x <= y
- - x >= 1
- - not (x <= y)
- introduced_constraint: not (x <= y)
- weight: 1
- n_children_regions: 0
- n_descendant_regions: 0
- n_leaf_regions: 1
- invariant: '1'
- example_input:
- x: '2'
- y: '1'
- example_output: '1'
-- !RegionGroup
- label_path: 1.2.3.4.1
- constraints:
- - x <= 0
- - y <= 0
- - y >= 1
- - x >= 1
- - y <= (-11)
- introduced_constraint: y <= (-11)
- weight: 1
- n_children_regions: 0
- n_descendant_regions: 0
- n_leaf_regions: 1
- invariant: '3'
- example_input:
- x: '1'
- y: (-11)
- example_output: '3'
+ # region_groups is auto-populated on validation from regions_str.
+ assert edr.to_tree_str() == snapshot("""\
+├── [1] new_constraint='x >= 1' n_leaf_regions=4
+│ ├── [1.1] new_constraint='y >= 1' n_leaf_regions=2
+│ │ ├── [1.1.1] new_constraint='x <= y' invariant='2' is_leaf=True
+│ │ └── [1.1.2] new_constraint='x > y' invariant='1' is_leaf=True
+│ ├── [1.2] new_constraint='y <= (-11)' invariant='3' is_leaf=True
+│ └── [1.3.1] new_constraint='y >= (-10)' invariant='4' is_leaf=True
+├── [2.1] new_constraint='x <= 0' invariant='5' is_leaf=True
+└── [3.1] new_constraint='y <= 0' invariant='6' is_leaf=True\
""")
- assert (hdr.dumper_func()(hdr_dict_flat)) == snapshot("""\
-summary:
- n_regions: 6
-region_groups:
-- 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
- introduced_constraint: y <= 0
- invariant: '6'
- example_input:
- x: '0'
- y: '0'
- example_output: '6'
- 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: '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: '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: '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: '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: '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: []
-""")
+ # (label_path, full constraint path) for every node, depth-first.
+ def _walk(groups: list[RegionGroup]) -> list[tuple[str, list[str]]]:
+ out: list[tuple[str, list[str]]] = []
+ for g in groups:
+ out.append(('.'.join(map(str, g.label_path)), g.constraints))
+ out.extend(_walk(g.children))
+ return out
+
+ assert _walk(edr.region_groups) == snapshot(
+ [
+ ('1', ['x >= 1']),
+ ('1.1', ['x >= 1', 'y >= 1']),
+ ('1.1.1', ['x >= 1', 'y >= 1', 'x <= y']),
+ ('1.1.2', ['x >= 1', 'y >= 1', 'x > y']),
+ ('1.2', ['x >= 1', 'y <= (-11)']),
+ ('1.3.1', ['x >= 1', 'y <= 0', 'y >= (-10)']),
+ ('2.1', ['y >= 1', 'x <= 0']),
+ ('3.1', ['x <= 0', 'y <= 0']),
+ ]
+ )