diff --git a/packages/imandrax-api-models/CHANGELOG.md b/packages/imandrax-api-models/CHANGELOG.md index 35bd92d4..f48588cc 100644 --- a/packages/imandrax-api-models/CHANGELOG.md +++ b/packages/imandrax-api-models/CHANGELOG.md @@ -4,6 +4,11 @@ Versioning scheme: .. ## [Unreleased] +## [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 - Add qcheck models and endpoints diff --git a/packages/imandrax-api-models/pyproject.toml b/packages/imandrax-api-models/pyproject.toml index 1851e83e..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 = [ @@ -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", 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/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..210a5bac --- /dev/null +++ b/packages/imandrax-api-models/src/imandrax_api_models/region_decomp.py @@ -0,0 +1,505 @@ +"""Post-processing (Hierarchical groupping) 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 + +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 + + +@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 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, + *, + 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_regions() for rg in groups]) + max_depth = _max_depth_of_groups(groups) + + 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, + ) -> 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: + """ + 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 + + 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 self.n_regions() - 1 + + +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_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 + + +class RegionGroupSummarizer(Protocol): + def __call__(self, group: RegionGroup) -> str: ... + + +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 _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.children: + lines.append( + 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.children): + _tree_lines( + lines, + child, + prefix=child_prefix, + is_last=i == len(group.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. + + 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: + 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( + constraints=rg_constraints, + region=rg_region, + children=rg_children, + label_path=new_idx_path[::-1], + 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'][::-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] = {} + + 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['n_descendant_regions'] = data.n_descendant_regions() + if data.children: + if depth_limit is None or depth_limit <= 0: + mapping['children'] = data.children + # return dumper.represent_mapping('tag:yaml.org,2002:map', mapping) + 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 new file mode 100644 index 00000000..368aca89 --- /dev/null +++ b/packages/imandrax-api-models/tests/test_grouped_region_decomp.py @@ -0,0 +1,380 @@ +import imandrax_api +from imandrax_api.lib import RegionStr +from inline_snapshot import snapshot + +from imandrax_api_models.region_decomp import HumDecomposeRes, RegionGroup + + +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() + 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: + 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: '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: [] +""") 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)) - - -""") 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" },