Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/develop' into lean-list-sort
Browse files Browse the repository at this point in the history
  • Loading branch information
JuanCoRo committed Jan 21, 2025
2 parents d8545f5 + 14697a2 commit a8c8c52
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 a8c8c52

Please sign in to comment.