From df51b441aa9793c6c05023bf607ed85ea5dbc9a6 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 2 Sep 2024 14:55:18 +0800 Subject: [PATCH 1/8] create split from source to targets without csubst --- pyk/src/pyk/kcfg/kcfg.py | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 2da3d3e921..4dd41095b9 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -1040,6 +1040,15 @@ def create_split(self, source_id: NodeIdLike, splits: Iterable[tuple[NodeIdLike, self.add_successor(split) return split + def create_split_by_nodes(self, source_id: NodeIdLike, target_ids: Iterable[NodeIdLike]) -> KCFG.Split | None: + source = self.node(source_id) + targets = [self.node(nid) for nid in list(target_ids)] + substs = [source.cterm.config.match(target.cterm.config) for target in targets] + if None in substs: + return None + csubsts = [CSubst(subst, target.cterm.constraints) for subst, target in zip(substs, targets, strict=True)] + return self.create_split(source.id, zip(target_ids, csubsts, strict=True)) + def ndbranches(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) -> list[NDBranch]: source_id = self._resolve(source_id) if source_id is not None else None target_id = self._resolve(target_id) if target_id is not None else None From 71cdf921b883343a4919c1f8b0eae5b5ceda705f Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 2 Sep 2024 15:35:58 +0800 Subject: [PATCH 2/8] add test --- pyk/src/pyk/kcfg/kcfg.py | 3 +- pyk/src/tests/unit/test_kcfg.py | 66 ++++++++++++++++++++++++++++++++- 2 files changed, 67 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 4dd41095b9..ec82c6ad0a 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -1041,8 +1041,9 @@ def create_split(self, source_id: NodeIdLike, splits: Iterable[tuple[NodeIdLike, return split def create_split_by_nodes(self, source_id: NodeIdLike, target_ids: Iterable[NodeIdLike]) -> KCFG.Split | None: + """Create a split without crafting a CSubst.""" source = self.node(source_id) - targets = [self.node(nid) for nid in list(target_ids)] + targets = [self.node(nid) for nid in target_ids] substs = [source.cterm.config.match(target.cterm.config) for target in targets] if None in substs: return None diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index 9ba68366a0..3697cae53f 100644 --- a/pyk/src/tests/unit/test_kcfg.py +++ b/pyk/src/tests/unit/test_kcfg.py @@ -10,7 +10,8 @@ from pyk.kcfg import KCFG, KCFGShow from pyk.kcfg.kcfg import KCFGNodeAttr from pyk.kcfg.show import NodePrinter -from pyk.prelude.ml import mlEquals, mlTop +from pyk.prelude.kint import geInt, intToken, ltInt +from pyk.prelude.ml import mlEquals, mlEqualsTrue, mlTop from pyk.prelude.utils import token from pyk.utils import not_none, single @@ -24,6 +25,22 @@ from pyk.kast import KInner +def lt(var: str, n: int) -> KApply: + return mlEqualsTrue(ltInt(KVariable(var), intToken(n))) + + +def ge(var: str, n: int) -> KApply: + return mlEqualsTrue(geInt(KVariable(var), intToken(n))) + + +def config(var: str) -> KApply: + return KApply('', KVariable(var)) + + +def config_int(n: int) -> KApply: + return KApply('', intToken(n)) + + def to_csubst_cterm(term_1: CTerm, term_2: CTerm, constraints: Iterable[KInner]) -> CSubst: csubst = term_1.match_with_constraint(term_2) assert csubst is not None @@ -849,3 +866,50 @@ def test_no_cell_rewrite_to_dots() -> None: result = no_cell_rewrite_to_dots(term) assert result == term + + +def split_kcfg0() -> KCFG: + kcfg = KCFG() + kcfg.create_node(CTerm(config('X'), (ge('X', 0),))) + kcfg.create_node(CTerm(config('X'), (ge('X', 0), lt('X', 3)))) + kcfg.create_node(CTerm(config('Y'), (ge('Y', 3), lt('Y', 5)))) + kcfg.create_node(CTerm(config('Z'), (ge('Z', 5),))) + return kcfg + + +def split_kcfg1() -> KCFG: + """KCFG for split with uncovered constraints.""" + kcfg = KCFG() + kcfg.create_node(CTerm(config('X'), (ge('X', 0),))) + kcfg.create_node(CTerm(config('Y'), (ge('Y', 3), lt('Y', 5)))) + kcfg.create_node(CTerm(config('Z'), (ge('Z', 5),))) + return kcfg + + +def split_kcfg2() -> KCFG: + """KCFG for split with conflicting constraints.""" + kcfg = KCFG() + kcfg.create_node(CTerm(config('X'), (ge('X', 0),))) + kcfg.create_node(CTerm(config('Y'), (lt('X', 3),))) + kcfg.create_node(CTerm(config('Z'), (ge('Z', 5),))) + return kcfg + + +SPLIT_TEST_CASES = [ + (split_kcfg0(), 1, [2, 3, 4]), + (split_kcfg1(), 1, [2, 3]), + (split_kcfg2(), 1, [2, 3]), +] + + +@pytest.mark.parametrize('kcfg, source_id, target_ids', SPLIT_TEST_CASES) +def test_create_split_by_nodes(kcfg: KCFG, source_id: int, target_ids: Iterable[int]) -> None: + # When + new_split = kcfg.create_split_by_nodes(source_id, target_ids) + + # Then + assert new_split + assert new_split.source == kcfg.node(source_id) + assert new_split.targets == tuple(kcfg.node(target_id) for target_id in target_ids) + # for target_id, csubst in new_split.splits.items(): + # assert csubst.apply(kcfg.node(source_id).cterm) == kcfg.node(target_id).cterm From 4d073e288e3e770771f02ca0e4b3d27c8fa10a54 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 2 Sep 2024 15:38:13 +0800 Subject: [PATCH 3/8] fix apply doesn't allow a CTerm with constraints --- pyk/src/pyk/cterm/cterm.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 10f9f1cb52..9b333db45e 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -333,8 +333,8 @@ def add_constraint(self, constraint: KInner) -> CSubst: def apply(self, cterm: CTerm) -> CTerm: """Apply this `CSubst` to the given `CTerm` (instantiating the free variables, and adding the constraints).""" - _kast = self.subst(cterm.kast) - return CTerm(_kast, [self.constraint]) + config = self.subst(cterm.config) + return CTerm(config, [self.constraint]) def cterm_build_claim( From f2edc5b8ea1583bc2bdab8c19038be1432fca932 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 2 Sep 2024 15:39:27 +0800 Subject: [PATCH 4/8] test pass --- pyk/src/tests/unit/test_kcfg.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index 3697cae53f..c139d72e86 100644 --- a/pyk/src/tests/unit/test_kcfg.py +++ b/pyk/src/tests/unit/test_kcfg.py @@ -911,5 +911,5 @@ def test_create_split_by_nodes(kcfg: KCFG, source_id: int, target_ids: Iterable[ assert new_split assert new_split.source == kcfg.node(source_id) assert new_split.targets == tuple(kcfg.node(target_id) for target_id in target_ids) - # for target_id, csubst in new_split.splits.items(): - # assert csubst.apply(kcfg.node(source_id).cterm) == kcfg.node(target_id).cterm + for target_id, csubst in new_split.splits.items(): + assert csubst.apply(kcfg.node(source_id).cterm) == kcfg.node(target_id).cterm From ab6238b3970c79f7e77a8cbc4a88bdd4c8b2c21a Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 2 Sep 2024 16:33:18 +0800 Subject: [PATCH 5/8] update test data --- pyk/src/tests/unit/test_kcfg.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index c139d72e86..2477fc376e 100644 --- a/pyk/src/tests/unit/test_kcfg.py +++ b/pyk/src/tests/unit/test_kcfg.py @@ -872,8 +872,8 @@ def split_kcfg0() -> KCFG: kcfg = KCFG() kcfg.create_node(CTerm(config('X'), (ge('X', 0),))) kcfg.create_node(CTerm(config('X'), (ge('X', 0), lt('X', 3)))) - kcfg.create_node(CTerm(config('Y'), (ge('Y', 3), lt('Y', 5)))) - kcfg.create_node(CTerm(config('Z'), (ge('Z', 5),))) + kcfg.create_node(CTerm(config('Y'), (ge('X', 0), ge('Y', 3), lt('Y', 5)))) + kcfg.create_node(CTerm(config('Z'), (ge('X', 0), ge('Z', 5),))) return kcfg @@ -881,8 +881,8 @@ def split_kcfg1() -> KCFG: """KCFG for split with uncovered constraints.""" kcfg = KCFG() kcfg.create_node(CTerm(config('X'), (ge('X', 0),))) - kcfg.create_node(CTerm(config('Y'), (ge('Y', 3), lt('Y', 5)))) - kcfg.create_node(CTerm(config('Z'), (ge('Z', 5),))) + kcfg.create_node(CTerm(config('Y'), (ge('X', 0), ge('Y', 3), lt('Y', 5)))) + kcfg.create_node(CTerm(config('Z'), (ge('X', 0), ge('Z', 5),))) return kcfg @@ -890,8 +890,8 @@ def split_kcfg2() -> KCFG: """KCFG for split with conflicting constraints.""" kcfg = KCFG() kcfg.create_node(CTerm(config('X'), (ge('X', 0),))) - kcfg.create_node(CTerm(config('Y'), (lt('X', 3),))) - kcfg.create_node(CTerm(config('Z'), (ge('Z', 5),))) + kcfg.create_node(CTerm(config('Y'), (ge('X', 0), lt('X', 3),))) + kcfg.create_node(CTerm(config('Z'), (ge('X', 0), ge('Z', 5),))) return kcfg From 0c7128d61b46dc66434f5face917a3677d794dd6 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 2 Sep 2024 16:37:47 +0800 Subject: [PATCH 6/8] combine the constraints for CSubst.apply --- pyk/src/pyk/cterm/cterm.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 9b333db45e..b4095df1d7 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -334,7 +334,8 @@ def add_constraint(self, constraint: KInner) -> CSubst: def apply(self, cterm: CTerm) -> CTerm: """Apply this `CSubst` to the given `CTerm` (instantiating the free variables, and adding the constraints).""" config = self.subst(cterm.config) - return CTerm(config, [self.constraint]) + constraints = [self.subst(constraint) for constraint in cterm.constraints] + list(self.constraints) + return CTerm(config, constraints) def cterm_build_claim( From f5098ccd04e80636baf229e14506ca4a80a448e8 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 2 Sep 2024 16:47:15 +0800 Subject: [PATCH 7/8] pass test --- pyk/src/pyk/kcfg/kcfg.py | 8 +++++- pyk/src/tests/unit/test_kcfg.py | 44 ++++++++++++++++++++++++++++----- 2 files changed, 45 insertions(+), 7 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index ec82c6ad0a..10103c52d9 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -1045,9 +1045,15 @@ def create_split_by_nodes(self, source_id: NodeIdLike, target_ids: Iterable[Node source = self.node(source_id) targets = [self.node(nid) for nid in target_ids] substs = [source.cterm.config.match(target.cterm.config) for target in targets] + csubsts: list[CSubst] = [] if None in substs: return None - csubsts = [CSubst(subst, target.cterm.constraints) for subst, target in zip(substs, targets, strict=True)] + for subst, target in zip(substs, targets, strict=True): + constraints: list[KInner] = [] + for c in target.cterm.constraints: + if c not in source.cterm.constraints: + constraints.append(c) + csubsts.append(CSubst(subst, constraints)) return self.create_split(source.id, zip(target_ids, csubsts, strict=True)) def ndbranches(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) -> list[NDBranch]: diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index 2477fc376e..7daecfb8b5 100644 --- a/pyk/src/tests/unit/test_kcfg.py +++ b/pyk/src/tests/unit/test_kcfg.py @@ -872,8 +872,16 @@ def split_kcfg0() -> KCFG: kcfg = KCFG() kcfg.create_node(CTerm(config('X'), (ge('X', 0),))) kcfg.create_node(CTerm(config('X'), (ge('X', 0), lt('X', 3)))) - kcfg.create_node(CTerm(config('Y'), (ge('X', 0), ge('Y', 3), lt('Y', 5)))) - kcfg.create_node(CTerm(config('Z'), (ge('X', 0), ge('Z', 5),))) + kcfg.create_node(CTerm(config('Y'), (ge('Y', 0), ge('Y', 3), lt('Y', 5)))) + kcfg.create_node( + CTerm( + config('Z'), + ( + ge('Z', 0), + ge('Z', 5), + ), + ) + ) return kcfg @@ -881,8 +889,16 @@ def split_kcfg1() -> KCFG: """KCFG for split with uncovered constraints.""" kcfg = KCFG() kcfg.create_node(CTerm(config('X'), (ge('X', 0),))) - kcfg.create_node(CTerm(config('Y'), (ge('X', 0), ge('Y', 3), lt('Y', 5)))) - kcfg.create_node(CTerm(config('Z'), (ge('X', 0), ge('Z', 5),))) + kcfg.create_node(CTerm(config('Y'), (ge('Y', 0), ge('Y', 3), lt('Y', 5)))) + kcfg.create_node( + CTerm( + config('Z'), + ( + ge('Z', 0), + ge('Z', 5), + ), + ) + ) return kcfg @@ -890,8 +906,24 @@ def split_kcfg2() -> KCFG: """KCFG for split with conflicting constraints.""" kcfg = KCFG() kcfg.create_node(CTerm(config('X'), (ge('X', 0),))) - kcfg.create_node(CTerm(config('Y'), (ge('X', 0), lt('X', 3),))) - kcfg.create_node(CTerm(config('Z'), (ge('X', 0), ge('Z', 5),))) + kcfg.create_node( + CTerm( + config('Y'), + ( + ge('Y', 0), + lt('Y', 3), + ), + ) + ) + kcfg.create_node( + CTerm( + config('Z'), + ( + ge('Z', 0), + ge('Z', 5), + ), + ) + ) return kcfg From b3e08f3a57dec5c4adb6db68b19f2c247359972d Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 2 Sep 2024 16:50:07 +0800 Subject: [PATCH 8/8] simplify the implementation --- pyk/src/pyk/kcfg/kcfg.py | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 10103c52d9..7b9b1cfad0 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -1044,16 +1044,15 @@ def create_split_by_nodes(self, source_id: NodeIdLike, target_ids: Iterable[Node """Create a split without crafting a CSubst.""" source = self.node(source_id) targets = [self.node(nid) for nid in target_ids] - substs = [source.cterm.config.match(target.cterm.config) for target in targets] csubsts: list[CSubst] = [] - if None in substs: - return None - for subst, target in zip(substs, targets, strict=True): - constraints: list[KInner] = [] - for c in target.cterm.constraints: - if c not in source.cterm.constraints: - constraints.append(c) + + for target in targets: + subst = source.cterm.config.match(target.cterm.config) + if subst is None: + return None + constraints = [c for c in target.cterm.constraints if c not in source.cterm.constraints] csubsts.append(CSubst(subst, constraints)) + return self.create_split(source.id, zip(target_ids, csubsts, strict=True)) def ndbranches(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) -> list[NDBranch]: