Refactor KCFG

* Remove field split
* Remove field loop
* Remove field terminal
* Remove field frontier
* Remove field subsumptions
* Remove method getTermHash
* Remove method getNodeAttributes
* Refactor and rename method getStateIdByShortHash
* Refactor and rename insertNode
* Refactor and rename removeNode
* Remove class attribute _NODE_ATTRS
* Refactor methods to_dict and from_dict
* Add type annotations for fields
* Change fields from List to Set where possible
* Rename field states to _nodes
* Create class KCFG.Node
* Rename method add_node to create_node
* Remove methods _encode and _decode
* Create class KCFG.Edge
* Rename field graph to _edges
* Change edge type
* Remove methods _assign and invalidateStates
* Add method get_edge
* Remove method getEdges
* Rename get_node to node
* Rename get_edge to edge
* Add optional parameters to method edges
* Remove methods getSuccessors and getPredecessors
* Make return type of method edge Optional
* Remove method getEdgeCondition
* Remove methods markEdge*
* Refactor abstractions
* Refactor method getEdgeSentence to Edge.to_rule
* Remove method getModule
* Add class KCFG.Cover
* Add class KCFG.EdgeLike
* Simplify to_dot
* Reimplement path algorithm
* Reimplement transitive closure
* Implement property frontier
* Rename init to _init
* Rename target to _target
* Rename stuck to _stuck
* Refactor getPathCondition
* Add method prune
* Add class FrozenDict
* Add class Subst
* Change KAtt backing data type from frozenset to FrozenDict
* Change return type of KCFG.Cover.subst to Subst
* Rename kastManip.removeGeneratedCells
* Refactor and rename countVarOccurances
* Add function if_ktype
* Add function count_rhs_vars
* Add further utils
* Add class KRuleLike
* Add class CTerm
* Make kast.to_hash a cached property
* Add properties for sets of nodes
* Change type of KCFG.Node.term to CTerm
* Change CTerm.constraints from FrozenSet to Tuple
* Rename inline_generated_top
* Move class Subst to module subst
* Add tests for count_vars
* Move AST traversal functions to module kast
* Change return type of kastManip.match to Subst
* Move function match from kastManip to subst
* Add tests for matching property

k-distribution/src/main/scripts/lib/pyk/pyk/cterm.py

@@ -0,0 +1,57 @@
+from dataclasses import dataclass
+from functools import cached_property
+from itertools import chain
+from typing import Iterable, Optional, Tuple
+
+from .kast import TOP, KInner, flattenLabel
+from .kastManip import match, splitConfigAndConstraints
+from .prelude import mlAnd, mlImplies
+from .subst import Subst
+
+
+@dataclass(frozen=True)
+class CTerm:
+    config: KInner  # TODO Optional?
+    constraints: Tuple[KInner, ...]
+
+    def __init__(self, cterm: KInner) -> None:
+        config, constraint = splitConfigAndConstraints(cterm)
+        constraints = tuple(flattenLabel('#And', constraint))
+        object.__setattr__(self, 'config', config)
+        object.__setattr__(self, 'constraints', constraints)
+
+    def __iter__(self):
+        return chain([self.config], self.constraints)
+
+    @cached_property
+    def cterm(self) -> KInner:
+        return mlAnd(self)
+
+    @property
+    def hash(self) -> str:
+        return self.cterm.hash
+
+    def match(self, pattern: 'CTerm') -> Optional[Tuple[Subst, KInner]]:
+        subst = match(pattern=pattern.config, term=self.config)
+
+        if subst is None:
+            return None
+
+        obligation = self._ml_impl(self.constraints, map(subst, pattern.constraints))
+
+        return subst, obligation
+
+    @staticmethod
+    def _ml_impl(antecedents: Iterable[KInner], consequents: Iterable[KInner]) -> KInner:
+        antecedents = set(antecedents)
+
+        antecedent = mlAnd(antecedents)
+        consequent = mlAnd(set(term for term in consequents if term not in antecedents))
+
+        if antecedent == TOP:
+            return consequent
+
+        if consequent == TOP:
+            return TOP
+
+        return mlImplies(antecedent, consequent)

k-distribution/src/main/scripts/lib/pyk/pyk/kast.py

@@ -3,6 +3,7 @@
 from abc import ABC, abstractmethod
 from dataclasses import InitVar, dataclass
 from enum import Enum
+from functools import cached_property
 from itertools import chain
 from typing import (
     Any,
@@ -26,8 +27,11 @@
 from typing_extensions import TypeAlias
 
 from .cli_utils import fatal, warning
+from .utils import FrozenDict, hash_str
 
 T = TypeVar('T', bound='KAst')
+W = TypeVar('W', bound='WithKAtt')
+KI = TypeVar('KI', bound='KInner')
 
 
 class KAst(ABC):
@@ -50,6 +54,11 @@ def from_json(s: str) -> 'KAst':
     def to_json(self) -> str:
         return json.dumps(self.to_dict(), sort_keys=True)
 
+    @final
+    @cached_property
+    def hash(self) -> str:
+        return hash_str(self.to_json())
+
     @classmethod
     def _check_node(cls: Type[T], d: Dict[str, Any], expected: Optional[str] = None) -> None:
         expected = expected if expected is not None else cls.__name__
@@ -61,23 +70,19 @@ def _check_node(cls: Type[T], d: Dict[str, Any], expected: Optional[str] = None)
 @final
 @dataclass(frozen=True)
 class KAtt(KAst, Mapping[str, Any]):
-    _atts: FrozenSet[Tuple[str, Any]]
+    atts: FrozenDict[str, Any]
 
     def __init__(self, atts: Mapping[str, Any] = {}):
-        object.__setattr__(self, '_atts', frozenset(atts.items()))
-
-    def __getitem__(self, key: str) -> Any:
-        return self.atts[key]
+        object.__setattr__(self, 'atts', FrozenDict(atts))
 
     def __iter__(self) -> Iterator[str]:
-        return (k for k, _ in self._atts)
+        return iter(self.atts)
 
     def __len__(self) -> int:
-        return len(self._atts)
+        return len(self.atts)
 
-    @property
-    def atts(self) -> Dict[str, Any]:
-        return dict(self._atts)
+    def __getitem__(self, key: str) -> Any:
+        return self.atts[key]
 
     @staticmethod
     def of(**atts: Any) -> 'KAtt':
@@ -89,7 +94,7 @@ def from_dict(cls: Type['KAtt'], d: Dict[str, Any]) -> 'KAtt':
         return KAtt(atts=d['att'])
 
     def to_dict(self) -> Dict[str, Any]:
-        return {'node': 'KAtt', 'att': self.atts}
+        return {'node': 'KAtt', 'att': dict(self.atts)}
 
     def let(self, *, atts: Optional[Mapping[str, Any]] = None) -> 'KAtt':
         atts = atts if atts is not None else self.atts
@@ -102,10 +107,6 @@ def update(self, atts: Mapping[str, Any]) -> 'KAtt':
 EMPTY_ATT: Final = KAtt()
 
 
-W = TypeVar('W', bound='WithKAtt')
-KI = TypeVar('KI', bound='KInner')
-
-
 class WithKAtt(KAst, ABC):
     att: KAtt
 
@@ -784,9 +785,26 @@ def let_att(self, att: KAtt) -> 'KBubble':
         return self.let(att=att)
 
 
+class KRuleLike(KSentence, ABC):
+    body: KInner
+    requires: KInner
+    ensures: KInner
+
+    _RULE_LIKE_NODES: Final = {'KRule', 'KClaim'}
+
+    @classmethod
+    @abstractmethod
+    def from_dict(cls: Type['KRuleLike'], d: Dict[str, Any]) -> 'KRuleLike':
+        node = d['node']
+        if node in KRuleLike._RULE_LIKE_NODES:
+            return globals()[node].from_dict(d)
+
+        raise ValueError(f"Expected KRuleLike label as 'node' value, found: '{node}'")
+
+
 @final
 @dataclass(frozen=True)
-class KRule(KSentence):
+class KRule(KRuleLike):
     body: KInner
     requires: KInner
     ensures: KInner
@@ -830,7 +848,7 @@ def let_att(self, att: KAtt) -> 'KRule':
 
 @final
 @dataclass(frozen=True)
-class KClaim(KSentence):
+class KClaim(KRuleLike):
     body: KInner
     requires: KInner
     ensures: KInner
@@ -1076,6 +1094,25 @@ def let_att(self, att: KAtt) -> 'KDefinition':
         return self.let(att=att)
 
 
+# TODO make method of KInner
+def bottom_up(f: Callable[[KInner], KInner], kinner: KInner) -> KInner:
+    return f(kinner.map_inner(lambda _kinner: bottom_up(f, _kinner)))
+
+
+# TODO make method of KInner
+def top_down(f: Callable[[KInner], KInner], kinner: KInner) -> KInner:
+    return f(kinner).map_inner(lambda _kinner: top_down(f, _kinner))
+
+
+# TODO replace by method that does not reconstruct the AST
+def collect(callback: Callable[[KInner], None], kinner: KInner) -> None:
+    def f(kinner: KInner) -> KInner:
+        callback(kinner)
+        return kinner
+
+    bottom_up(f, kinner)
+
+
 def flattenLabel(label, kast):
     """Given a cons list, return a flat Python list of the elements.