Skip to content

Commit

Permalink
refactor a better way for as_rules
Browse files Browse the repository at this point in the history
  • Loading branch information
Stevengre committed Aug 23, 2024
1 parent 63ff927 commit 69759ac
Showing 1 changed file with 7 additions and 2 deletions.
9 changes: 7 additions & 2 deletions pyk/src/pyk/proof/reachability.py
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@
from pathlib import Path
from typing import Any, Final, TypeVar

from ..kast.outer import KClaim, KDefinition, KFlatModuleList
from ..kast.outer import KClaim, KDefinition, KFlatModuleList, KRuleLike
from ..kcfg import KCFGExplore
from ..kcfg.explore import KCFGExtendResult
from ..kcfg.kcfg import CSubst, NodeIdLike
Expand Down Expand Up @@ -444,7 +444,12 @@ def as_rules(self, priority: int = 20, direct_rule: bool = False) -> list[KRule]
or (self.admitted and not self.kcfg.predecessors(self.target))
):
return [self.as_rule(priority=priority)]
return [rule for rule in self.kcfg.to_rules(self.rule_id, priority=priority) if isinstance(rule, KRule)]

def _return_rule(r: KRuleLike) -> KRule:
assert isinstance(r, KRule)
return r

return [_return_rule(rule) for rule in self.kcfg.to_rules(self.rule_id, priority=priority)]

def as_rule(self, priority: int = 20) -> KRule:
_edge = KCFG.Edge(self.kcfg.node(self.init), self.kcfg.node(self.target), depth=0, rules=())
Expand Down

0 comments on commit 69759ac

Please sign in to comment.