1from __future__ import annotations
2
3from abc import ABC, abstractmethod
4from typing import TYPE_CHECKING
5
6if TYPE_CHECKING:
7 from ..cterm import CTerm, CTermSymbolic
8 from .kcfg import KCFGExtendResult
9
10
[docs]
11class KCFGSemantics(ABC):
[docs]
12 @abstractmethod
13 def is_terminal(self, c: CTerm) -> bool: ...
14
15 """Check whether or not a given ``CTerm`` is terminal."""
16
[docs]
17 @abstractmethod
18 def abstract_node(self, c: CTerm) -> CTerm: ...
19
20 """Implement an abstraction mechanism."""
21
[docs]
22 @abstractmethod
23 def is_loop(self, c: CTerm) -> bool: ...
24
25 """Check whether or not the given ``CTerm`` represents a loop head."""
26
[docs]
27 @abstractmethod
28 def same_loop(self, c1: CTerm, c2: CTerm) -> bool: ...
29
30 """Check whether or not the two given ``CTerm``s represent the same loop head."""
31
[docs]
32 @abstractmethod
33 def can_make_custom_step(self, c: CTerm) -> bool: ...
34
35 """Check whether or not the semantics can make a custom step from a given ``CTerm``."""
36
[docs]
37 @abstractmethod
38 def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None: ...
39
40 """Implement a custom semantic step."""
41
[docs]
42 @abstractmethod
43 def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool: ...
44
45 """Check whether or not the two given ``CTerm``s are mergeable. Must be transitive, commutative, and reflexive."""
46
47
[docs]
48class DefaultSemantics(KCFGSemantics):
[docs]
49 def is_terminal(self, c: CTerm) -> bool:
50 return False
51
[docs]
52 def abstract_node(self, c: CTerm) -> CTerm:
53 return c
54
[docs]
55 def is_loop(self, c: CTerm) -> bool:
56 return False
57
[docs]
58 def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
59 return False
60
[docs]
61 def can_make_custom_step(self, c: CTerm) -> bool:
62 return False
63
[docs]
64 def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None:
65 return None
66
[docs]
67 def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool:
68 return False