More simplifications to the KCFG class

package/version

@@ -1 +1 @@
-0.1.339
+0.1.340

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.339"
+version = "0.1.340"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/kast/manip.py

@@ -51,16 +51,9 @@ def sort_assoc_label(label: str, kast: KInner) -> KInner:
     return kast
 
 
-def sort_ac_collections(definition: KDefinition, kast: KInner) -> KInner:
-    ac_hooks = {'MAP.concat', 'SET.concat', 'BAG.concat'}
-    ac_collections = [
-        prod.klabel.name
-        for prod in definition.productions
-        if prod.klabel is not None and 'hook' in prod.att and prod.att['hook'] in ac_hooks
-    ]
-
+def sort_ac_collections(kast: KInner) -> KInner:
     def _sort_ac_collections(_kast: KInner) -> KInner:
-        if type(_kast) is KApply and _kast.label.name in ac_collections:
+        if type(_kast) is KApply and (_kast.label.name in {'_Set_', '_Map_'} or _kast.label.name.endswith('CellMap_')):
             return sort_assoc_label(_kast.label.name, _kast)
         return _kast
 

src/pyk/kast/pretty.py

@@ -90,7 +90,7 @@ def print(self, kast: KAst) -> str:
             if self._unalias:
                 kast = undo_aliases(self.definition, kast)
             if self._sort_collections:
-                kast = sort_ac_collections(self.definition, kast)
+                kast = sort_ac_collections(kast)
             return self._print_kinner(kast)
         raise AssertionError(f'Error unparsing: {kast}')
 

src/pyk/kcfg/explore.py

@@ -378,10 +378,10 @@ def extend(
         cut_point_rules: Iterable[str] = (),
         terminal_rules: Iterable[str] = (),
     ) -> None:
-        if not kcfg.is_frontier(node.id):
-            raise ValueError(f'Cannot extend non-frontier node {self.id}: {node.id}')
-
-        kcfg.add_expanded(node.id)
+        if not kcfg.is_leaf(node.id):
+            raise ValueError(f'Cannot extend non-leaf node {self.id}: {node.id}')
+        if kcfg.is_stuck(node.id):
+            raise ValueError(f'Cannot extend stuck node {self.id}: {node.id}')
 
         _LOGGER.info(f'Extending KCFG from node {self.id}: {shorten_hashes(node.id)}')
         depth, cterm, next_cterms, next_node_logs = self.cterm_execute(
@@ -399,6 +399,7 @@ def extend(
 
         # Stuck
         elif len(next_cterms) == 0:
+            kcfg.add_stuck(node.id)
             _LOGGER.info(f'Found stuck node {self.id}: {shorten_hashes(node.id)}')
 
         # Cut Rule