From 4d66899051318be96cf54e86bf07308c408e1804 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 23 Sep 2024 09:08:51 +0800 Subject: [PATCH 1/4] 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 77e035aba0ea0097097088a03ab4b61c9b8f265e Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 23 Sep 2024 09:14:48 +0800 Subject: [PATCH 2/4] 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} From 1644251ed08a3a3a45a840d268a94587e1cb54db Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Tue, 24 Sep 2024 11:38:38 +0800 Subject: [PATCH 3/4] update refs --- pyk/src/pyk/kcfg/exploration.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/kcfg/exploration.py b/pyk/src/pyk/kcfg/exploration.py index 406ecccc25..9ac1b5c65a 100644 --- a/pyk/src/pyk/kcfg/exploration.py +++ b/pyk/src/pyk/kcfg/exploration.py @@ -109,5 +109,5 @@ def to_dict(self) -> dict[str, Any]: # # Minimizing the KCFG - def minimize_kcfg(self) -> None: - KCFGMinimizer(self.kcfg).minimize() + def minimize_kcfg(self, merge: bool = True) -> None: + KCFGMinimizer(self.kcfg).minimize(merge=merge) From 0c5e31e629b0639945d2a274e88b69be30897252 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 7 Oct 2024 10:18:46 +0800 Subject: [PATCH 4/4] both default false --- pyk/src/pyk/kcfg/exploration.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/kcfg/exploration.py b/pyk/src/pyk/kcfg/exploration.py index 9ac1b5c65a..ac47640ce5 100644 --- a/pyk/src/pyk/kcfg/exploration.py +++ b/pyk/src/pyk/kcfg/exploration.py @@ -109,5 +109,5 @@ def to_dict(self) -> dict[str, Any]: # # Minimizing the KCFG - def minimize_kcfg(self, merge: bool = True) -> None: + def minimize_kcfg(self, merge: bool = False) -> None: KCFGMinimizer(self.kcfg).minimize(merge=merge)