From 14697a24cd925c4ea8ec61c28467571c391b7336 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 20 Jan 2025 21:02:24 +0100 Subject: [PATCH] Add method `filter_rewrites` to `KoreDefn` (#4739) Restrict rewrite rules to specific labels. Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com> --- pyk/src/pyk/kore/internal.py | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/pyk/src/pyk/kore/internal.py b/pyk/src/pyk/kore/internal.py index 95eb918bc7..588bcf35b3 100644 --- a/pyk/src/pyk/kore/internal.py +++ b/pyk/src/pyk/kore/internal.py @@ -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 @@ -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)}