Skip to content
This repository has been archived by the owner on Apr 25, 2024. It is now read-only.

Commit

Permalink
Minimization algorithm correction (#1059)
Browse files Browse the repository at this point in the history
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 <devops@runtimeverification.com>
  • Loading branch information
PetarMax and devops authored Apr 3, 2024
1 parent c139723 commit 291d66d
Showing 5 changed files with 58 additions and 7 deletions.
4 changes: 2 additions & 2 deletions docs/conf.py
Original file line number Diff line number Diff line change
@@ -9,8 +9,8 @@
project = 'pyk'
author = 'Runtime Verification, Inc'
copyright = '2024, Runtime Verification, Inc'
version = '0.1.766'
release = '0.1.766'
version = '0.1.767'
release = '0.1.767'

# -- General configuration ---------------------------------------------------
# https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration
2 changes: 1 addition & 1 deletion package/version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.766
0.1.767
2 changes: 1 addition & 1 deletion pyproject.toml
Original file line number Diff line number Diff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "pyk"
version = "0.1.766"
version = "0.1.767"
description = ""
authors = [
"Runtime Verification, Inc. <contact@runtimeverification.com>",
4 changes: 2 additions & 2 deletions src/pyk/kcfg/kcfg.py
Original file line number Diff line number Diff line change
@@ -1080,8 +1080,8 @@ def lift_splits(self) -> bool:
"""

def _lift_split(finder: Callable, lifter: Callable) -> bool:
result = False
while True:
result = False
splits_to_lift = sorted(
[
node.id
@@ -1097,7 +1097,7 @@ def _lift_split(finder: Callable, lifter: Callable) -> bool:
for id in splits_to_lift:
lifter(id)
result = True
if not result or len(splits_to_lift) == 0:
if len(splits_to_lift) == 0:
break
return result

53 changes: 52 additions & 1 deletion src/tests/unit/test_kcfg.py
Original file line number Diff line number Diff line change
@@ -661,7 +661,7 @@ def test_lifting_functions_automatic() -> None:
assert contains_edge(cfg, 15, 7, 50, ('r1', 'r2', 'r3', 'r4'))


def test_minimize() -> None:
def test_minimize_01() -> None:
cfg = minimization_test_kcfg()

cfg.minimize()
@@ -701,6 +701,57 @@ def test_minimize() -> None:
assert contains_edge(cfg, 15, 13, 155, ('r1', 'r2', 'r3', 'r4', 'r6', 'r7', 'r8'))


def test_minimize_02() -> None:
x_ge_0 = mlEqualsTrue(geInt(KVariable('X'), intToken(0)))
x_lt_0 = mlEqualsTrue(ltInt(KVariable('X'), intToken(0)))

d = {
'next': 7,
'nodes': node_dicts(6, config=x_config()),
'edges': edge_dicts(
(1, 2, 10, ('r1',)),
(3, 5, 20, ('r2',)),
(4, 6, 30, ('r3',)),
),
'splits': split_dicts(
(2, [(3, x_ge_0), (4, x_lt_0)]),
csubst=x_subst(),
),
}
cfg = KCFG.from_dict(d)
propagate_split_constraints(cfg)
# 20
# 10 /-- X >=Int 0 --> 3 --> 5
# 1 --> 2 30
# \-- X <Int 0 --> 4 --> 6

cfg.minimize()
# 30
# /-- X >=Int 0 --> 7 --> 5
# 1 40
# \-- X <Int 0 --> 8 --> 6

assert cfg._deleted_nodes == {2, 3, 4}

node_7 = KCFG.Node(7, x_node(1).cterm.add_constraint(x_ge_0))
node_8 = KCFG.Node(8, x_node(1).cterm.add_constraint(x_lt_0))
assert cfg.node(7) == node_7
assert cfg.node(8) == node_8
assert cfg._node_id == 9

assert cfg.contains_split(
KCFG.Split(
x_node(1),
[
(node_7, to_csubst_node(x_node(1), node_7, [x_ge_0])),
(node_8, to_csubst_node(x_node(1), node_8, [x_lt_0])),
],
)
)
assert contains_edge(cfg, 7, 5, 30, ('r1', 'r2'))
assert contains_edge(cfg, 8, 6, 40, ('r1', 'r3'))


def test_split_csubsts() -> None:
cfg = KCFG()
cfg.create_node(term(11))

0 comments on commit 291d66d

Please sign in to comment.