From 4e9a4098f34d1ea5f27ba89730652ca0b66b156d Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 22 Jul 2024 16:01:08 +0800 Subject: [PATCH] add node merging heuristic --- pyk/src/pyk/kcfg/semantics.py | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/pyk/src/pyk/kcfg/semantics.py b/pyk/src/pyk/kcfg/semantics.py index 05134f82e00..9d8ab27e72f 100644 --- a/pyk/src/pyk/kcfg/semantics.py +++ b/pyk/src/pyk/kcfg/semantics.py @@ -21,6 +21,9 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool: ... @abstractmethod def custom_step(self, c: CTerm) -> KCFGExtendResult | None: ... + @abstractmethod + def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool: ... + class DefaultSemantics(KCFGSemantics): def is_terminal(self, c: CTerm) -> bool: @@ -34,3 +37,6 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool: def custom_step(self, c: CTerm) -> KCFGExtendResult | None: return None + + def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool: + return False