diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 99bb41cac0a..4eeac4cf109 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -570,8 +570,6 @@ class LogEntry(ABC): @classmethod def from_dict(cls: type[LE], dct: Mapping[str, Any]) -> LE: match dct['tag']: - case 'processing-time': - return LogTiming.from_dict(dct) # type: ignore case 'rewrite': return LogRewrite.from_dict(dct) # type: ignore case _: @@ -581,27 +579,6 @@ def from_dict(cls: type[LE], dct: Mapping[str, Any]) -> LE: def to_dict(self) -> dict[str, Any]: ... -@final -@dataclass(frozen=True) -class LogTiming(LogEntry): - class Component(Enum): - KORE_RPC = 'kore-rpc' - BOOSTER = 'booster' - PROXY = 'proxy' - - time: float - component: Component | None - - @classmethod - def from_dict(cls, dct: Mapping[str, Any]) -> LogTiming: - return LogTiming( - time=dct['time'], component=LogTiming.Component(dct['component']) if 'component' in dct else None - ) - - def to_dict(self) -> dict[str, Any]: - return {'tag': 'processing-time', 'time': self.time, 'component': self.component} - - @final @dataclass(frozen=True) class LogRewrite(LogEntry): @@ -1025,7 +1002,6 @@ def execute( module_name: str | None = None, log_successful_rewrites: bool | None = None, log_failed_rewrites: bool | None = None, - log_timing: bool | None = None, ) -> ExecuteResult: params = filter_none( { @@ -1039,7 +1015,6 @@ def execute( 'state': self._state(pattern), 'log-successful-rewrites': log_successful_rewrites, 'log-failed-rewrites': log_failed_rewrites, - 'log-timing': log_timing, } ) @@ -1052,14 +1027,12 @@ def implies( consequent: Pattern, *, module_name: str | None = None, - log_timing: bool | None = None, ) -> ImpliesResult: params = filter_none( { 'antecedent': self._state(antecedent), 'consequent': self._state(consequent), 'module': module_name, - 'log-timing': log_timing, } ) @@ -1071,13 +1044,11 @@ def simplify( pattern: Pattern, *, module_name: str | None = None, - log_timing: bool | None = None, ) -> tuple[Pattern, tuple[LogEntry, ...]]: params = filter_none( { 'state': self._state(pattern), 'module': module_name, - 'log-timing': log_timing, } ) diff --git a/pyk/src/tests/integration/kore/test_kore_client.py b/pyk/src/tests/integration/kore/test_kore_client.py index de0059ca9cf..0eca981a969 100644 --- a/pyk/src/tests/integration/kore/test_kore_client.py +++ b/pyk/src/tests/integration/kore/test_kore_client.py @@ -40,7 +40,6 @@ InvalidModuleError, LogOrigin, LogRewrite, - LogTiming, RewriteFailure, RewriteSuccess, SatResult, @@ -625,48 +624,6 @@ def test( assert actual == expected[server_type] -class TestTimeLogging(KoreClientTest): - KOMPILE_DEFINITION = """ - module TIMING-TEST - imports INT - configuration $PGM:Int - endmodule - """ - KOMPILE_MAIN_MODULE = 'TIMING-TEST' - KOMPILE_ARGS = {'syntax_module': 'TIMING-TEST'} - LLVM_ARGS = KOMPILE_ARGS - - @staticmethod - def config(i: int) -> Pattern: - return generated_top((k(kseq((inj(INT, SORT_K_ITEM, int_dv(i)),))), generated_counter(int_dv(0)))) - - def test_execute(self, kore_client: KoreClient) -> None: - # When - response = kore_client.execute(self.config(0), log_timing=True) - logs = response.logs - - # Then - assert logs - assert all(isinstance(log, LogTiming) for log in logs) - - def test_implies(self, kore_client: KoreClient) -> None: - # When - response = kore_client.implies(EVar('X', INT), int_top, log_timing=True) - logs = response.logs - - # Then - assert logs - assert all(isinstance(log, LogTiming) for log in logs) - - def test_simplify(self, kore_client: KoreClient) -> None: - # When - _, logs = kore_client.simplify(int_top, log_timing=True) - - # Then - assert logs - assert all(isinstance(log, LogTiming) for log in logs) - - class TestAddModule(KoreClientTest): KOMPILE_DEFINITION = """ module INT-CONFIG