This repository was archived by the owner on Apr 25, 2024. It is now read-only.
Tags: runtimeverification/pyk
Tags
Update dependency: deps/k_release (#1060) Co-authored-by: devops <[email protected]> Co-authored-by: Tamás Tóth <[email protected]>
Minimization algorithm correction (#1059) This PR corrects an error in the KCFG minimization algorithm, where the `_lift_split` function would incorrectly return `False` instead of `True` even though a lift has been performed successfully. It also contains a test that triggers the bug, that is, it fails using the current `master` branch and passes using this PR. --------- Co-authored-by: devops <[email protected]>
Add JSON-RPC server to pyk (#1014) Addresses: - #1019 Adds: - Class `JsonRpcServer`, an abstract class for exposing a JSON RPC interface over HTTP from pyk. - The server is initialized with a host and port. Methods are registered with `JsonRpcServer.register_method`, and the server is started with `JsonRpcServer.serve`. - A test that uses JSON-RPC methods to interact with a k configuration and request concrete execution steps on it. --------- Co-authored-by: devops <[email protected]>
Further KCFG-to-KCFG transformations (#1009) This PR expands on #995 by adding a transformation that joins consecutive `Split` nodes into a single `Split`. Additionally, the PR: - corrects a bug in `lift_splits` that led to infinite looping in the case a split could not be lifted due to freshly created variables; - corrects the substitution computation in `lift_split`; - non-destructively expands the testing helpers in `test_kcfg.py` to allow for more expressivity; - fixes a typo in the documentation of `CSubst.from_dict`. --------- Co-authored-by: devops <[email protected]> Co-authored-by: Palina Tolmach <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
Adjust overload axiom generation (#1028) Related: * runtimeverification/k#4136 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]>
Fix `SmtSolverError` (#1055) Related: * runtimeverification/haskell-backend#3748 --------- Co-authored-by: devops <[email protected]>
Enable inline K definitions in tests (#1050) * Add parameter `definition` to `Kompiler.__call__` * Add attribute `KOMPILE_DEFINITION` to `KompiledTest` * Inline small, single-use definitions * Remove unused definitions * Move `k-files` into `test-data` * Fix (most) kompilation warnings --------- Co-authored-by: devops <[email protected]>