diff --git a/docs/conf.py b/docs/conf.py index 9cfd90d04..ea98e2f3c 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.766' -release = '0.1.766' +version = '0.1.767' +release = '0.1.767' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index f28396555..d6039d690 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.766 +0.1.767 diff --git a/pyproject.toml b/pyproject.toml index 556bee4f9..77b7b75c8 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.766" +version = "0.1.767" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index a18c86dbf..e57e5ac17 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/src/pyk/kcfg/kcfg.py @@ -1080,8 +1080,8 @@ def lift_splits(self) -> bool: """ def _lift_split(finder: Callable, lifter: Callable) -> bool: + result = False while True: - result = False splits_to_lift = sorted( [ node.id @@ -1097,7 +1097,7 @@ def _lift_split(finder: Callable, lifter: Callable) -> bool: for id in splits_to_lift: lifter(id) result = True - if not result or len(splits_to_lift) == 0: + if len(splits_to_lift) == 0: break return result diff --git a/src/tests/unit/test_kcfg.py b/src/tests/unit/test_kcfg.py index 53364fa55..7aa0e8a75 100644 --- a/src/tests/unit/test_kcfg.py +++ b/src/tests/unit/test_kcfg.py @@ -661,7 +661,7 @@ def test_lifting_functions_automatic() -> None: assert contains_edge(cfg, 15, 7, 50, ('r1', 'r2', 'r3', 'r4')) -def test_minimize() -> None: +def test_minimize_01() -> None: cfg = minimization_test_kcfg() cfg.minimize() @@ -701,6 +701,57 @@ def test_minimize() -> None: assert contains_edge(cfg, 15, 13, 155, ('r1', 'r2', 'r3', 'r4', 'r6', 'r7', 'r8')) +def test_minimize_02() -> None: + x_ge_0 = mlEqualsTrue(geInt(KVariable('X'), intToken(0))) + x_lt_0 = mlEqualsTrue(ltInt(KVariable('X'), intToken(0))) + + d = { + 'next': 7, + 'nodes': node_dicts(6, config=x_config()), + 'edges': edge_dicts( + (1, 2, 10, ('r1',)), + (3, 5, 20, ('r2',)), + (4, 6, 30, ('r3',)), + ), + 'splits': split_dicts( + (2, [(3, x_ge_0), (4, x_lt_0)]), + csubst=x_subst(), + ), + } + cfg = KCFG.from_dict(d) + propagate_split_constraints(cfg) + # 20 + # 10 /-- X >=Int 0 --> 3 --> 5 + # 1 --> 2 30 + # \-- X 4 --> 6 + + cfg.minimize() + # 30 + # /-- X >=Int 0 --> 7 --> 5 + # 1 40 + # \-- X 8 --> 6 + + assert cfg._deleted_nodes == {2, 3, 4} + + node_7 = KCFG.Node(7, x_node(1).cterm.add_constraint(x_ge_0)) + node_8 = KCFG.Node(8, x_node(1).cterm.add_constraint(x_lt_0)) + assert cfg.node(7) == node_7 + assert cfg.node(8) == node_8 + assert cfg._node_id == 9 + + assert cfg.contains_split( + KCFG.Split( + x_node(1), + [ + (node_7, to_csubst_node(x_node(1), node_7, [x_ge_0])), + (node_8, to_csubst_node(x_node(1), node_8, [x_lt_0])), + ], + ) + ) + assert contains_edge(cfg, 7, 5, 30, ('r1', 'r2')) + assert contains_edge(cfg, 8, 6, 40, ('r1', 'r3')) + + def test_split_csubsts() -> None: cfg = KCFG() cfg.create_node(term(11))