From c3d249bf231065edfc220f11b7c7087106e9b2f1 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 23 Sep 2024 09:08:51 +0800 Subject: [PATCH 1/2] default: don't use merge_nodes, because they provide a more abstract rule rather than the orginal ones. --- pyk/src/pyk/kcfg/minimize.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/kcfg/minimize.py b/pyk/src/pyk/kcfg/minimize.py index 5bd91a802a..cfc50cd924 100644 --- a/pyk/src/pyk/kcfg/minimize.py +++ b/pyk/src/pyk/kcfg/minimize.py @@ -288,7 +288,7 @@ def _is_mergeable(x: KCFG.Edge | KCFG.MergedEdge, y: KCFG.Edge | KCFG.MergedEdge return True - def minimize(self) -> None: + def minimize(self, merge: bool = False) -> None: """Minimize KCFG by repeatedly performing the lifting transformations. The KCFG is transformed to an equivalent in which no further lifting transformations are possible. @@ -300,5 +300,5 @@ def minimize(self) -> None: repeat = self.lift_splits() or repeat repeat = True - while repeat: + while repeat and merge: repeat = self.merge_nodes() From 4f80e349d9cff2fcf3a11beda688de50209a0c60 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 23 Sep 2024 09:14:48 +0800 Subject: [PATCH 2/2] fix test --- pyk/src/tests/unit/kcfg/merge_node_data.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pyk/src/tests/unit/kcfg/merge_node_data.py b/pyk/src/tests/unit/kcfg/merge_node_data.py index c2c3854895..a453f34649 100644 --- a/pyk/src/tests/unit/kcfg/merge_node_data.py +++ b/pyk/src/tests/unit/kcfg/merge_node_data.py @@ -255,12 +255,12 @@ def util_check_constraint(constraint: KInner, merged_var: KVariable, under_check def check_merge_no(minimizer: KCFGMinimizer) -> None: - minimizer.minimize() + minimizer.minimize(merge=True) assert minimizer.kcfg.to_dict() == merge_node_test_kcfg().to_dict() def check_merged_one(minimizer: KCFGMinimizer) -> None: - minimizer.minimize() + minimizer.minimize(merge=True) # 1 --> merged bi: Merged Edge merged_edge = single(minimizer.kcfg.merged_edges(source_id=1)) edges = {2: 9, 3: 10, 16: 20, 17: 21, 18: 22, 19: 23, 6: 13, 7: 14, 8: 15}