Skip to content

Commit

Permalink
Nest function
Browse files Browse the repository at this point in the history
  • Loading branch information
tothtamas28 committed Nov 29, 2024
1 parent c5e5ac7 commit 058b0aa
Showing 1 changed file with 22 additions and 23 deletions.
45 changes: 22 additions & 23 deletions pyk/src/pyk/kore/rule.py
Original file line number Diff line number Diff line change
Expand Up @@ -62,29 +62,28 @@ def from_axiom(axiom: Axiom) -> Rule:

@staticmethod
def extract_all(defn: Definition) -> list[Rule]:
return [Rule.from_axiom(axiom) for axiom in defn.axioms if Rule._is_rule(axiom)]

@staticmethod
def _is_rule(axiom: Axiom) -> bool:
if axiom == _INJ_AXIOM:
return False

if any(attr in axiom.attrs_by_key for attr in _SKIPPED_ATTRS):
return False

if 'simplification' in axiom.attrs_by_key:
match axiom.pattern:
case Implies(
left=Top() | Equals(),
right=Equals(
left=Ceil() | Equals(),
right=And(ops=(_, Top() | Equals())),
),
):
_LOGGER.info(fr'Skipping \ceil or \equals simplification rule: {axiom.text}')
return False

return True
def is_rule(axiom: Axiom) -> bool:
if axiom == _INJ_AXIOM:
return False

if any(attr in axiom.attrs_by_key for attr in _SKIPPED_ATTRS):
return False

if 'simplification' in axiom.attrs_by_key:
match axiom.pattern:
case Implies(
left=Top() | Equals(),
right=Equals(
left=Ceil() | Equals(),
right=And(ops=(_, Top() | Equals())),
),
):
_LOGGER.info(fr'Skipping \ceil or \equals simplification rule: {axiom.text}')
return False

return True

return [Rule.from_axiom(axiom) for axiom in defn.axioms if is_rule(axiom)]


@final
Expand Down

0 comments on commit 058b0aa

Please sign in to comment.