Avoid using merge_nodes by default (#4647)

Default: Avoid using merge_nodes, as they offer a more abstract rule
instead of the original ones.

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)

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()

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}