Skip to content

Commit

Permalink
short_name -> short_id
Browse files Browse the repository at this point in the history
  • Loading branch information
@nishantjr
nishantjr committed Jun 7, 2022
1 parent 498b2d2 commit fdba4e8
Show file tree
Hide file tree
Showing 2 changed files with 25 additions and 30 deletions.
15 changes: 5 additions & 10 deletions pyk/src/pyk/kcfg.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,12 +31,7 @@
substToMlPred,
)
from .ktool import KPrint
from .utils import (
add_indent,
compare_short_hashes,
shorten_hash,
shorten_hashes,
)
from .utils import add_indent, compare_short_hashes, shorten_hash


class KCFG(Container[Union['KCFG.Node', 'KCFG.Edge', 'KCFG.Cover']]):
Expand Down Expand Up @@ -267,7 +262,7 @@ def resolve(node_id: str) -> str:

return cfg

def short_name(self, node: Node) -> str:
def short_id(self, node: Node) -> str:
for alias, hash in self._aliases.items():
if node.id == hash:
return alias
Expand All @@ -276,7 +271,7 @@ def short_name(self, node: Node) -> str:
def short_names(self, value: Any, leftChars=6, rightChars=6) -> Any:
result: Any = None
if isinstance(value, KCFG.Node):
result = self.short_name(value)
result = self.short_id(value)
elif type(value) is tuple:
result = tuple([self.short_names(item) for item in value])
elif type(value) is list:
Expand All @@ -303,7 +298,7 @@ def from_json(s: str) -> 'KCFG':
def node_short_info(self, node: Node) -> str:
attrs = self.node_attrs(node.id)
attr_string = ' (' + ', '.join(attrs) + ')' if attrs else ''
return self.short_name(node) + attr_string
return self.short_id(node) + attr_string

def pretty_print(self, kprint: KPrint) -> List[str]:

Expand Down Expand Up @@ -360,7 +355,7 @@ def _short_label(label):
for node in self.nodes:
nodeAttrs = self.node_attrs(node.id)
classAttrs = ' '.join(nodeAttrs)
label = self.short_name(node) + (classAttrs and ' ' + classAttrs)
label = self.short_id(node) + (classAttrs and ' ' + classAttrs)
attrs = {'class': classAttrs} if classAttrs else {}
graph.node(name=node.id, label=label, **attrs)

Expand Down
40 changes: 20 additions & 20 deletions pyk/src/pyk/tests/test_kcfg.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -304,22 +304,22 @@ def test_aliases(self):

cfg = KCFG.from_dict(d)
self.assertEqual(cfg.node('foo'), node(1))
self.assertEqual(cfg.short_name(node(1)), 'foo')
self.assertEqual(cfg.short_id(node(1)), 'foo')

self.assertNotEqual(cfg.short_name(node(0)), 'bar')
self.assertNotEqual(cfg.short_id(node(0)), 'bar')
cfg.add_alias('bar', node(0).id)
self.assertEqual(cfg.node('bar'), node(0))
cfg.remove_alias('bar', node(0).id)
with self.assertRaisesRegex(ValueError, 'Bad short hash: bar'):
cfg.node('bar')
self.assertNotEqual(cfg.short_name(node(0)), 'bar')
self.assertNotEqual(cfg.short_id(node(0)), 'bar')

with self.assertRaisesRegex(ValueError, 'Unknown node: '):
cfg.add_alias('buzz', node(3).id)

cfg.remove_node(nid(1))
cfg.create_node(term(1))
self.assertNotEqual(cfg.short_name(node(1)), 'foo')
self.assertNotEqual(cfg.short_id(node(1)), 'foo')

def test_pretty_print(self):
d = {
Expand All @@ -339,43 +339,43 @@ def test_pretty_print(self):
}
cfg = KCFG.from_dict(d)

def _short_name(i) -> str:
return cfg.short_name(node(i))
def _short_id(i) -> str:
return cfg.short_id(node(i))

# TODO: Why are all nodes (besides the target) frontiers?
# TODO: Add a cover
self.maxDiff = None
actual = '\n'.join(cfg.pretty_print(mock_kprint())) + '\n'
self.assertMultiLineEqual(actual,
f"{_short_name(0)} (init, frontier)\n"
f"{_short_id(0)} (init, frontier)\n"
f"│ (1 step)\n"
f"├ {_short_name(1)} (frontier)\n"
f"├ {_short_id(1)} (frontier)\n"
f"│ (5 steps)\n"
f"├ {_short_name(2)} (frontier)\n"
f"├ {_short_id(2)} (frontier)\n"
f"│ (1 step)\n"
f"├ {_short_name(3)} (frontier)\n"
f"┢━ {_short_name(4)} (frontier)\n"
f"├ {_short_id(3)} (frontier)\n"
f"┢━ {_short_id(4)} (frontier)\n"
f"┃ │ (1 step)\n"
f"┃ ├ {_short_name(5)} (frontier)\n"
f"┃ ├ {_short_id(5)} (frontier)\n"
f"┃ │ (1 step)\n"
f"┃ ├ {_short_name(2)} (frontier)\n"
f"┃ ├ {_short_id(2)} (frontier)\n"
f"┃ ┊ (looped back)\n"
f"┃\n"
f"┣━ {_short_name(5)} (frontier)\n"
f"┣━ {_short_id(5)} (frontier)\n"
f"┃ ┊ (continues as previously)\n"
f"┃\n"
f"┣━ {_short_name(6)} (target, leaf)\n"
f"┣━ {_short_id(6)} (target, leaf)\n"
f"┃\n"
f"┣━ {_short_name(7)} (frontier)\n"
f"┣━ {_short_id(7)} (frontier)\n"
f"┃ │ (1 step)\n"
f"┃ └ {_short_name(6)} (target, leaf)\n"
f"┃ └ {_short_id(6)} (target, leaf)\n"
f"┃\n"
f"┗━ {_short_name(11)} (frontier)\n"
f"┗━ {_short_id(11)} (frontier)\n"
f" │ (1 step)\n"
f" ├ {_short_name(8)} (leaf)\n"
f" ├ {_short_id(8)} (leaf)\n"
f" │ constraint: KApply(label=KLabel(name='#Top', params=(KSort(name='GeneratedTopCell'),)), args=())\n"
f" │ subst:\n"
f" │ KApply(label=KLabel(name='#Equals', params=(KSort(name='K'), KSort(name='K'))), args=(KVariable(name='V11'), KToken(token='8', sort=KSort(name='Int'))))\n"
f" ├ {_short_name(11)} (frontier)\n"
f" ├ {_short_id(11)} (frontier)\n"
f" ┊ (looped back)\n\n"
)

0 comments on commit fdba4e8

Please sign in to comment.