Skip to content

Commit

Permalink
Add method filter_rewrites to KoreDefn (#4739)
Browse files Browse the repository at this point in the history
Restrict rewrite rules to specific labels.

Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>
  • Loading branch information
1 parent e5a79fc commit 14697a2
Showing 1 changed file with 7 additions and 0 deletions.
7 changes: 7 additions & 0 deletions pyk/src/pyk/kore/internal.py
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@
from .syntax import App, Axiom, SortApp, SortDecl, String, Symbol, SymbolDecl

if TYPE_CHECKING:
from collections.abc import Iterable

from .syntax import Definition


Expand Down Expand Up @@ -140,6 +142,11 @@ def let(
functions=self.functions if functions is None else functions,
)

def filter_rewrites(self, labels: Iterable[str]) -> KoreDefn:
"""Keep only rewrite rules with certain labels in the definition."""
should_keep = set(labels)
return self.let(rewrites=tuple(rewrite for rewrite in self.rewrites if rewrite.label in should_keep))

def project_to_symbols(self) -> KoreDefn:
"""Project definition to symbols present in the definition."""
symbol_sorts = {sort for symbol in self.symbols for sort in self._symbol_sorts(symbol)}
Expand Down

0 comments on commit 14697a2

Please sign in to comment.