diff --git a/pyk/src/pyk/kcfg/exploration.py b/pyk/src/pyk/kcfg/exploration.py index 406ecccc25..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) -> None: - KCFGMinimizer(self.kcfg).minimize() + def minimize_kcfg(self, merge: bool = False) -> None: + KCFGMinimizer(self.kcfg).minimize(merge=merge) 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() 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}