From 9c876e427960fc5882023f82ac793dcd3fd1668f Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Tue, 20 Aug 2024 16:55:42 +0800 Subject: [PATCH 01/12] fix `match_with_constraint` --- pyk/src/pyk/cterm/cterm.py | 11 ++++++----- pyk/src/tests/unit/test_cterm.py | 23 ++++++++++++++++++++++- 2 files changed, 28 insertions(+), 6 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 9ff3bc9737..776865d8f5 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -163,13 +163,14 @@ def match(self, cterm: CTerm) -> Subst | None: def match_with_constraint(self, cterm: CTerm) -> CSubst | None: """Find `CSubst` instantiating this `CTerm` to the other, return `None` if no such `CSubst` exists.""" subst = self.config.match(cterm.config) - + if subst is None: return None - - constraint = self._ml_impl(cterm.constraints, map(subst, self.constraints)) - - return CSubst(subst=subst, constraints=[constraint]) + + source_constraints = [subst(c) for c in self.constraints] + constraints = [c for c in cterm.constraints if c not in source_constraints] + + return CSubst(subst, constraints) @staticmethod def _ml_impl(antecedents: Iterable[KInner], consequents: Iterable[KInner]) -> KInner: diff --git a/pyk/src/tests/unit/test_cterm.py b/pyk/src/tests/unit/test_cterm.py index 955894504f..39e576d674 100644 --- a/pyk/src/tests/unit/test_cterm.py +++ b/pyk/src/tests/unit/test_cterm.py @@ -13,7 +13,6 @@ from pyk.prelude.kbool import TRUE from pyk.prelude.kint import INT, intToken from pyk.prelude.ml import mlAnd, mlEquals, mlEqualsTrue, mlTop - from .utils import a, b, c, f, g, ge_ml, h, k, lt_ml, x, y, z if TYPE_CHECKING: @@ -75,6 +74,28 @@ def test_no_cterm_match(term: KInner, pattern: KInner) -> None: assert subst is None +MATCH_WITH_CONSTRAINT_TEST_DATA: Final = ( + (CTerm(generated_top(x)), CTerm(generated_top(x))), + (CTerm(generated_top(x)), CTerm(generated_top(y))), + (CTerm(generated_top(x)), CTerm(generated_top(y), (mlEqualsTrue(geInt(y, intToken(0))),))), + ( + CTerm(generated_top(x), (mlEqualsTrue(geInt(y, intToken(0))),)), + CTerm(generated_top(y), (mlEqualsTrue(geInt(y, intToken(5))),)), + ), +) + + +@pytest.mark.parametrize('t1, t2', MATCH_WITH_CONSTRAINT_TEST_DATA, ids=count()) +def test_cterm_match_with_constraint(t1: CTerm, t2: CTerm) -> None: + # When + c_subst1 = t1.match_with_constraint(t2) + c_subst2 = t2.match_with_constraint(t1) + + # Then + assert c_subst1 is not None and c_subst1.apply(t1) == t2 + assert c_subst2 is not None and c_subst2.apply(t2) == t1 + + BUILD_RULE_TEST_DATA: Final = ( ( T(k(KVariable('K_CELL')), mem(KVariable('MEM_CELL'))), From 744a943a2b1014915339e927fe346fa9c08ba61b Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Fri, 20 Sep 2024 10:34:44 +0800 Subject: [PATCH 02/12] fix tests --- pyk/src/pyk/cterm/cterm.py | 6 +++--- pyk/src/tests/unit/test_cterm.py | 21 +++++++++++++-------- pyk/src/tests/unit/test_kcfg.py | 2 +- 3 files changed, 17 insertions(+), 12 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 776865d8f5..95049ce65e 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -163,13 +163,13 @@ def match(self, cterm: CTerm) -> Subst | None: def match_with_constraint(self, cterm: CTerm) -> CSubst | None: """Find `CSubst` instantiating this `CTerm` to the other, return `None` if no such `CSubst` exists.""" subst = self.config.match(cterm.config) - + if subst is None: return None - + source_constraints = [subst(c) for c in self.constraints] constraints = [c for c in cterm.constraints if c not in source_constraints] - + return CSubst(subst, constraints) @staticmethod diff --git a/pyk/src/tests/unit/test_cterm.py b/pyk/src/tests/unit/test_cterm.py index 39e576d674..50490870d3 100644 --- a/pyk/src/tests/unit/test_cterm.py +++ b/pyk/src/tests/unit/test_cterm.py @@ -11,8 +11,9 @@ from pyk.kast.outer import KClaim from pyk.prelude.k import GENERATED_TOP_CELL, K from pyk.prelude.kbool import TRUE -from pyk.prelude.kint import INT, intToken +from pyk.prelude.kint import INT, geInt, intToken from pyk.prelude.ml import mlAnd, mlEquals, mlEqualsTrue, mlTop + from .utils import a, b, c, f, g, ge_ml, h, k, lt_ml, x, y, z if TYPE_CHECKING: @@ -75,12 +76,18 @@ def test_no_cterm_match(term: KInner, pattern: KInner) -> None: MATCH_WITH_CONSTRAINT_TEST_DATA: Final = ( - (CTerm(generated_top(x)), CTerm(generated_top(x))), - (CTerm(generated_top(x)), CTerm(generated_top(y))), - (CTerm(generated_top(x)), CTerm(generated_top(y), (mlEqualsTrue(geInt(y, intToken(0))),))), + (CTerm(k(x)), CTerm(k(x))), + (CTerm(k(x)), CTerm(k(y))), + (CTerm(k(x)), CTerm(k(y), (mlEqualsTrue(geInt(y, intToken(0))),))), ( - CTerm(generated_top(x), (mlEqualsTrue(geInt(y, intToken(0))),)), - CTerm(generated_top(y), (mlEqualsTrue(geInt(y, intToken(5))),)), + CTerm(k(x), (mlEqualsTrue(geInt(y, intToken(0))),)), + CTerm( + k(y), + ( + mlEqualsTrue(geInt(y, intToken(0))), + mlEqualsTrue(geInt(y, intToken(5))), + ), + ), ), ) @@ -89,11 +96,9 @@ def test_no_cterm_match(term: KInner, pattern: KInner) -> None: def test_cterm_match_with_constraint(t1: CTerm, t2: CTerm) -> None: # When c_subst1 = t1.match_with_constraint(t2) - c_subst2 = t2.match_with_constraint(t1) # Then assert c_subst1 is not None and c_subst1.apply(t1) == t2 - assert c_subst2 is not None and c_subst2.apply(t2) == t1 BUILD_RULE_TEST_DATA: Final = ( diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index de40de7e67..2c141aaa93 100644 --- a/pyk/src/tests/unit/test_kcfg.py +++ b/pyk/src/tests/unit/test_kcfg.py @@ -3,7 +3,6 @@ from typing import TYPE_CHECKING, Final import pytest -from unit.utils import ge_ml, k, lt_ml from pyk.cterm import CSubst, CTerm from pyk.kast.inner import KApply, KRewrite, KToken, KVariable, Subst @@ -17,6 +16,7 @@ from pyk.utils import not_none, single from .mock_kprint import MockKPrint +from .utils import ge_ml, k, lt_ml if TYPE_CHECKING: from collections.abc import Iterable From 50526e524e5f908788b08758b7b6a802198483c5 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Fri, 20 Sep 2024 10:51:47 +0800 Subject: [PATCH 03/12] update CTerm.add_constraint --- 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 95049ce65e..c68b396e1e 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -184,7 +184,8 @@ def _ml_impl(antecedents: Iterable[KInner], consequents: Iterable[KInner]) -> KI def add_constraint(self, new_constraint: KInner) -> CTerm: """Return a new `CTerm` with the additional constraints.""" - return CTerm(self.config, [new_constraint] + list(self.constraints)) + new_constraint = flatten_label('#And', new_constraint) + return CTerm(self.config, new_constraint + list(self.constraints)) def anti_unify( self, other: CTerm, keep_values: bool = False, kdef: KDefinition | None = None From da55234570d89ed7a60bba3df8bfdb42dda72f15 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Fri, 20 Sep 2024 10:52:03 +0800 Subject: [PATCH 04/12] update KCFG.split_on_constraints --- pyk/src/pyk/kcfg/kcfg.py | 4 ---- 1 file changed, 4 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 5289bf210a..763e62263a 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -1091,10 +1091,6 @@ def split_on_constraints(self, source_id: NodeIdLike, constraints: Iterable[KInn source = self.node(source_id) branch_node_ids = [self.create_node(source.cterm.add_constraint(c)).id for c in constraints] csubsts = [not_none(source.cterm.match_with_constraint(self.node(id).cterm)) for id in branch_node_ids] - csubsts = [ - reduce(CSubst.add_constraint, flatten_label('#And', constraint), csubst) - for (csubst, constraint) in zip(csubsts, constraints, strict=True) - ] self.create_split(source.id, zip(branch_node_ids, csubsts, strict=True)) return branch_node_ids From 77cd7f14a3c2854d1a5561f8c999e9efedd8be10 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Fri, 20 Sep 2024 11:00:11 +0800 Subject: [PATCH 05/12] refactor lift_split_edge --- pyk/src/pyk/kcfg/minimize.py | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/pyk/src/pyk/kcfg/minimize.py b/pyk/src/pyk/kcfg/minimize.py index 5bd91a802a..8c7982eb52 100644 --- a/pyk/src/pyk/kcfg/minimize.py +++ b/pyk/src/pyk/kcfg/minimize.py @@ -96,17 +96,10 @@ def lift_split_edge(self, b_id: NodeIdLike) -> None: # Ensure split can be lifted soundly (i.e., that it does not introduce fresh variables) assert ( len(split_from_b.source_vars.difference(a.free_vars)) == 0 - and len(split_from_b.target_vars.difference(split_from_b.source_vars)) == 0 + and len(split_from_b.target_vars.difference(split_from_b.source_vars)) == 0 # <-- Can we delete this check? ) # Create CTerms and CSubsts corresponding to the new targets of the split - new_cterms_with_constraints = [ - (CTerm(a.cterm.config, a.cterm.constraints + csubst.constraints), csubst.constraint) for csubst in csubsts - ] - # Generate substitutions for new targets, which all exist by construction - new_csubsts = [ - not_none(a.cterm.match_with_constraint(cterm)).add_constraint(constraint) - for (cterm, constraint) in new_cterms_with_constraints - ] + new_cterms_with_constraints = [csubst(a.cterm) for csubst in csubsts] # Remove the node `B`, effectively removing the entire initial structure self.kcfg.remove_node(b_id) # Create the nodes `[ A #And cond_I | I = 1..N ]`. @@ -115,7 +108,7 @@ def lift_split_edge(self, b_id: NodeIdLike) -> None: for i in range(len(ai)): self.kcfg.create_edge(ai[i], ci[i], a_to_b.depth, a_to_b.rules) # Create the split `A --[cond_1, ..., cond_N]--> [A #And cond_1, ..., A #And cond_N] - self.kcfg.create_split(a.id, zip(ai, new_csubsts, strict=True)) + self.kcfg.create_split(a.id, zip(ai, csubsts, strict=True)) def lift_split_split(self, b_id: NodeIdLike) -> None: """Lift a split up a split directly preceding it, joining them into a single split. From b0b507386082211cadecf70a5b8b1efe79e89926 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Fri, 20 Sep 2024 11:12:49 +0800 Subject: [PATCH 06/12] remove useless flatten --- pyk/src/pyk/cterm/cterm.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index c68b396e1e..95049ce65e 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -184,8 +184,7 @@ def _ml_impl(antecedents: Iterable[KInner], consequents: Iterable[KInner]) -> KI def add_constraint(self, new_constraint: KInner) -> CTerm: """Return a new `CTerm` with the additional constraints.""" - new_constraint = flatten_label('#And', new_constraint) - return CTerm(self.config, new_constraint + list(self.constraints)) + return CTerm(self.config, [new_constraint] + list(self.constraints)) def anti_unify( self, other: CTerm, keep_values: bool = False, kdef: KDefinition | None = None From 1036d81571daab98416feb063183fcddeb3cbd01 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Fri, 20 Sep 2024 11:38:34 +0800 Subject: [PATCH 07/12] refactor lift_split_split --- pyk/src/pyk/kcfg/minimize.py | 20 +++----------------- 1 file changed, 3 insertions(+), 17 deletions(-) diff --git a/pyk/src/pyk/kcfg/minimize.py b/pyk/src/pyk/kcfg/minimize.py index 8c7982eb52..096c64a3f8 100644 --- a/pyk/src/pyk/kcfg/minimize.py +++ b/pyk/src/pyk/kcfg/minimize.py @@ -131,29 +131,15 @@ def lift_split_split(self, b_id: NodeIdLike) -> None: a = split_from_a.source ci = list(splits_from_b.keys()) # Ensure split can be lifted soundly (i.e., that it does not introduce fresh variables) - assert ( + assert ( # <-- Does it will be a problem when using merging nodes, because it would introduce new variables? len(split_from_b.source_vars.difference(a.free_vars)) == 0 and len(split_from_b.target_vars.difference(split_from_b.source_vars)) == 0 ) - # Get the substitution for `B`, at the same time removing 'B' from the targets of `A`. - csubst_b = splits_from_a.pop(self.kcfg.node(b_id).id) - # Generate substitutions for additional targets `C_I`, which all exist by construction; - # the constraints are cumulative, resulting in `cond_B #And cond_I` - additional_csubsts = [ - not_none(a.cterm.match_with_constraint(self.kcfg.node(ci).cterm)) - .add_constraint(csubst_b.constraint) - .add_constraint(csubst.constraint) - for ci, csubst in splits_from_b.items() - ] - # Create the targets of the new split - ci = list(splits_from_b.keys()) - new_splits = zip( - list(splits_from_a.keys()) + ci, list(splits_from_a.values()) + additional_csubsts, strict=True - ) # Remove the node `B`, thereby removing the two splits as well self.kcfg.remove_node(b_id) + splits_from_a.pop(self.kcfg.node(b_id).id) # Create the new split `A --[..., cond_B #And cond_1, ..., cond_B #And cond_N, ...]--> [..., C_1, ..., C_N, ...]` - self.kcfg.create_split(a.id, new_splits) + self.kcfg.create_split_by_nodes(a.id, list(splits_from_a.keys()) + list(splits_from_b.keys())) def lift_splits(self) -> bool: """Perform all possible split liftings. From e5682ae91bb3376f527c4d67d88d9e003370532c Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Fri, 20 Sep 2024 11:44:45 +0800 Subject: [PATCH 08/12] refactor tests --- .../integration/proof/test_refute_node.py | 32 ++----------------- pyk/src/tests/unit/test_kcfg.py | 5 +-- 2 files changed, 5 insertions(+), 32 deletions(-) diff --git a/pyk/src/tests/integration/proof/test_refute_node.py b/pyk/src/tests/integration/proof/test_refute_node.py index e43e6f673e..e1ad864ef9 100644 --- a/pyk/src/tests/integration/proof/test_refute_node.py +++ b/pyk/src/tests/integration/proof/test_refute_node.py @@ -327,36 +327,8 @@ def test_apr_proof_refute_node_multiple_constraints( cfg.create_node(CTerm(config, [l_le_0, m_gt_0])) cfg.create_node(CTerm(config, [l_le_0, m_le_0])) - proof.kcfg.create_split( - 1, - [ - ( - 3, - not_none(cfg.node(1).cterm.match_with_constraint(cfg.node(3).cterm)) - .add_constraint(l_gt_0) - .add_constraint(m_gt_0), - ), - ( - 4, - not_none(cfg.node(1).cterm.match_with_constraint(cfg.node(4).cterm)) - .add_constraint(l_gt_0) - .add_constraint(m_le_0), - ), - ( - 5, - not_none(cfg.node(1).cterm.match_with_constraint(cfg.node(5).cterm)) - .add_constraint(l_le_0) - .add_constraint(m_gt_0), - ), - ( - 6, - not_none(cfg.node(1).cterm.match_with_constraint(cfg.node(6).cterm)) - .add_constraint(l_le_0) - .add_constraint(m_gt_0), - ), - ], - ) - + proof.kcfg.create_split_by_nodes(1, [3, 4, 5, 6]) + # When prover.advance_proof(proof, max_iterations=4) # After the minimization, nodes 7-10 created by the advancement of the proof diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index 2c141aaa93..254073ba3a 100644 --- a/pyk/src/tests/unit/test_kcfg.py +++ b/pyk/src/tests/unit/test_kcfg.py @@ -27,8 +27,9 @@ 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 + subst = term_1.config.match(term_2.config) + assert subst is not None + csubst = CSubst(subst, []) for constraint in constraints: csubst = csubst.add_constraint(constraint) return csubst From 5015121123aa3f563a003bdabe0a9f61125c3084 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Fri, 20 Sep 2024 11:55:58 +0800 Subject: [PATCH 09/12] delete cterm_match --- pyk/src/pyk/cterm/cterm.py | 21 +-------------------- pyk/src/pyk/kcfg/minimize.py | 9 ++++----- 2 files changed, 5 insertions(+), 25 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 95049ce65e..75c6c831e1 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -247,25 +247,6 @@ def remove_useless_constraints(self, keep_vars: Iterable[str] = ()) -> CTerm: return CTerm(self.config, new_constraints) -def cterm_match(cterm1: CTerm, cterm2: CTerm) -> CSubst | None: - """Find a substitution which can instantiate `cterm1` to `cterm2`. - - Args: - cterm1: `CTerm` to instantiate to `cterm2`. - cterm2: `CTerm` to instantiate `cterm1` to. - - Returns: - A `CSubst` which can instantiate `cterm1` to `cterm2`, or `None` if no such `CSubst` exists. - """ - # todo: delete this function and use cterm1.match_with_constraint(cterm2) directly after closing #4496 - subst = cterm1.config.match(cterm2.config) - if subst is None: - return None - source_constraints = [subst(c) for c in cterm1.constraints] - constraints = [c for c in cterm2.constraints if c not in source_constraints] - return CSubst(subst, constraints) - - def anti_unify(state1: KInner, state2: KInner, kdef: KDefinition | None = None) -> tuple[KInner, Subst, Subst]: """Return a generalized state over the two input states. @@ -462,5 +443,5 @@ def cterms_anti_unify( merged_cterm = cterms[0] for cterm in cterms[1:]: merged_cterm = merged_cterm.anti_unify(cterm, keep_values, kdef)[0] - csubsts = [not_none(cterm_match(merged_cterm, cterm)) for cterm in cterms] + csubsts = [not_none(merged_cterm.match_with_constraint(cterm)) for cterm in cterms] return merged_cterm, csubsts diff --git a/pyk/src/pyk/kcfg/minimize.py b/pyk/src/pyk/kcfg/minimize.py index 096c64a3f8..968d3f986c 100644 --- a/pyk/src/pyk/kcfg/minimize.py +++ b/pyk/src/pyk/kcfg/minimize.py @@ -3,9 +3,8 @@ from functools import reduce from typing import TYPE_CHECKING -from pyk.cterm import CTerm from pyk.cterm.cterm import cterms_anti_unify -from pyk.utils import not_none, partition, single +from pyk.utils import partition, single from .semantics import DefaultSemantics @@ -103,12 +102,12 @@ def lift_split_edge(self, b_id: NodeIdLike) -> None: # Remove the node `B`, effectively removing the entire initial structure self.kcfg.remove_node(b_id) # Create the nodes `[ A #And cond_I | I = 1..N ]`. - ai: list[NodeIdLike] = [self.kcfg.create_node(cterm).id for (cterm, _) in new_cterms_with_constraints] + ai: list[NodeIdLike] = [self.kcfg.create_node(cterm).id for cterm in new_cterms_with_constraints] # Create the edges `[A #And cond_1 --M steps--> C_I | I = 1..N ]` for i in range(len(ai)): self.kcfg.create_edge(ai[i], ci[i], a_to_b.depth, a_to_b.rules) # Create the split `A --[cond_1, ..., cond_N]--> [A #And cond_1, ..., A #And cond_N] - self.kcfg.create_split(a.id, zip(ai, csubsts, strict=True)) + self.kcfg.create_split_by_nodes(a.id, ai) def lift_split_split(self, b_id: NodeIdLike) -> None: """Lift a split up a split directly preceding it, joining them into a single split. @@ -129,7 +128,7 @@ def lift_split_split(self, b_id: NodeIdLike) -> None: split_from_a, split_from_b = single(self.kcfg.splits(target_id=b_id)), single(self.kcfg.splits(source_id=b_id)) splits_from_a, splits_from_b = split_from_a.splits, split_from_b.splits a = split_from_a.source - ci = list(splits_from_b.keys()) + list(splits_from_b.keys()) # Ensure split can be lifted soundly (i.e., that it does not introduce fresh variables) assert ( # <-- Does it will be a problem when using merging nodes, because it would introduce new variables? len(split_from_b.source_vars.difference(a.free_vars)) == 0 From 8f963f5533166e0a6a704028325f33acf061aee3 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Fri, 20 Sep 2024 11:56:03 +0800 Subject: [PATCH 10/12] fix --- pyk/src/pyk/kcfg/kcfg.py | 6 +----- pyk/src/tests/integration/proof/test_refute_node.py | 4 ++-- 2 files changed, 3 insertions(+), 7 deletions(-) diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 763e62263a..8d4c5a39c8 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -5,12 +5,9 @@ from abc import ABC, abstractmethod from collections.abc import Container from dataclasses import dataclass, field -from functools import reduce from threading import RLock from typing import TYPE_CHECKING, Final, List, Union, cast, final -from pyk.cterm.cterm import cterm_match - from ..cterm import CSubst, CTerm, cterm_build_claim, cterm_build_rule from ..kast import EMPTY_ATT from ..kast.inner import KApply @@ -18,7 +15,6 @@ bool_to_ml_pred, extract_lhs, extract_rhs, - flatten_label, inline_cell_maps, minimize_rule_like, rename_generated_vars, @@ -1062,7 +1058,7 @@ 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] try: - csubsts = [not_none(cterm_match(source.cterm, target.cterm)) for target in targets] + csubsts = [not_none(source.cterm.match_with_constraint(target.cterm)) for target in targets] except ValueError: return None return self.create_split(source.id, zip(target_ids, csubsts, strict=True)) diff --git a/pyk/src/tests/integration/proof/test_refute_node.py b/pyk/src/tests/integration/proof/test_refute_node.py index e1ad864ef9..34f99d4977 100644 --- a/pyk/src/tests/integration/proof/test_refute_node.py +++ b/pyk/src/tests/integration/proof/test_refute_node.py @@ -17,7 +17,7 @@ from pyk.prelude.ml import is_top, mlEqualsTrue from pyk.proof import APRProof, APRProver, ImpliesProver, ProofStatus, RefutationProof from pyk.testing import KCFGExploreTest, KProveTest -from pyk.utils import not_none, single +from pyk.utils import single from ..utils import K_FILES @@ -328,7 +328,7 @@ def test_apr_proof_refute_node_multiple_constraints( cfg.create_node(CTerm(config, [l_le_0, m_le_0])) proof.kcfg.create_split_by_nodes(1, [3, 4, 5, 6]) - + # When prover.advance_proof(proof, max_iterations=4) # After the minimization, nodes 7-10 created by the advancement of the proof From 2a32e80ba17b5c29bd6d3d2902fea3fcc9582eaf Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 23 Sep 2024 09:00:01 +0800 Subject: [PATCH 11/12] fix for cov-unit --- pyk/src/pyk/kcfg/minimize.py | 2 +- pyk/src/tests/unit/kcfg/test_minimize.py | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/pyk/src/pyk/kcfg/minimize.py b/pyk/src/pyk/kcfg/minimize.py index 968d3f986c..c886458f4f 100644 --- a/pyk/src/pyk/kcfg/minimize.py +++ b/pyk/src/pyk/kcfg/minimize.py @@ -135,8 +135,8 @@ def lift_split_split(self, b_id: NodeIdLike) -> None: and len(split_from_b.target_vars.difference(split_from_b.source_vars)) == 0 ) # Remove the node `B`, thereby removing the two splits as well - self.kcfg.remove_node(b_id) splits_from_a.pop(self.kcfg.node(b_id).id) + self.kcfg.remove_node(b_id) # Create the new split `A --[..., cond_B #And cond_1, ..., cond_B #And cond_N, ...]--> [..., C_1, ..., C_N, ...]` self.kcfg.create_split_by_nodes(a.id, list(splits_from_a.keys()) + list(splits_from_b.keys())) diff --git a/pyk/src/tests/unit/kcfg/test_minimize.py b/pyk/src/tests/unit/kcfg/test_minimize.py index b4f0d91a9b..00364837b0 100644 --- a/pyk/src/tests/unit/kcfg/test_minimize.py +++ b/pyk/src/tests/unit/kcfg/test_minimize.py @@ -205,7 +205,7 @@ def test_lifting_functions_automatic() -> None: [ (node_15, to_csubst_node(x_node(1), node_19, [x_lt_0])), (node_18, to_csubst_node(x_node(1), node_18, [x_ge_0, x_ge_5])), - (node_19, to_csubst_node(x_node(1), node_19, [x_ge_0, x_lt_5])), + (node_19, to_csubst_node(x_node(1), node_19, [x_lt_5, x_ge_0])), ], ) ) @@ -248,7 +248,7 @@ def test_minimize_01() -> None: [ (node_15, to_csubst_node(x_node(1), node_19, [x_lt_0])), (node_18, to_csubst_node(x_node(1), node_18, [x_ge_0, x_ge_5])), - (node_19, to_csubst_node(x_node(1), node_19, [x_ge_0, x_lt_5])), + (node_19, to_csubst_node(x_node(1), node_19, [x_lt_5, x_ge_0])), ], ) ) @@ -355,41 +355,41 @@ def x_lt(n: int) -> KApply: '┃\n' '┣━━┓ subst: .Subst\n' '┃ ┃ constraint:\n' + '┃ ┃ _=Int_ ( X , 0 )\n' '┃ ┃ _>=Int_ ( X , 32 )\n' - '┃ ┃ _=Int_ ( X , 0 )\n' '┃ ┃ _=Int_ ( X , 0 )\n' '┃ ┃ _>=Int_ ( X , 16 )\n' '┃ │\n' '┃ └─ 10 (leaf)\n' '┃\n' '┣━━┓ subst: .Subst\n' '┃ ┃ constraint:\n' - '┃ ┃ _>=Int_ ( X , 0 )\n' - '┃ ┃ _=Int_ ( X , 0 )\n' '┃ │\n' '┃ └─ 11 (leaf)\n' '┃\n' '┣━━┓ subst: .Subst\n' '┃ ┃ constraint:\n' '┃ ┃ _=Int_ ( X , -32 )\n' '┃ ┃ _>=Int_ ( X , -16 )\n' + '┃ ┃ _>=Int_ ( X , -32 )\n' '┃ │\n' '┃ └─ 12 (leaf)\n' '┃\n' '┣━━┓ subst: .Subst\n' '┃ ┃ constraint:\n' '┃ ┃ _=Int_ ( X , -32 )\n' '┃ ┃ _=Int_ ( X , -32 )\n' '┃ │\n' '┃ └─ 13 (leaf)\n' '┃\n' From 123c835a0d8e3fcc0d0b1fe6c1373eac02864252 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Mon, 7 Oct 2024 10:08:15 +0800 Subject: [PATCH 12/12] rename --- pyk/src/pyk/kcfg/minimize.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/kcfg/minimize.py b/pyk/src/pyk/kcfg/minimize.py index c886458f4f..78d2d0e6f6 100644 --- a/pyk/src/pyk/kcfg/minimize.py +++ b/pyk/src/pyk/kcfg/minimize.py @@ -98,11 +98,11 @@ def lift_split_edge(self, b_id: NodeIdLike) -> None: and len(split_from_b.target_vars.difference(split_from_b.source_vars)) == 0 # <-- Can we delete this check? ) # Create CTerms and CSubsts corresponding to the new targets of the split - new_cterms_with_constraints = [csubst(a.cterm) for csubst in csubsts] + new_cterms = [csubst(a.cterm) for csubst in csubsts] # Remove the node `B`, effectively removing the entire initial structure self.kcfg.remove_node(b_id) # Create the nodes `[ A #And cond_I | I = 1..N ]`. - ai: list[NodeIdLike] = [self.kcfg.create_node(cterm).id for cterm in new_cterms_with_constraints] + ai: list[NodeIdLike] = [self.kcfg.create_node(cterm).id for cterm in new_cterms] # Create the edges `[A #And cond_1 --M steps--> C_I | I = 1..N ]` for i in range(len(ai)): self.kcfg.create_edge(ai[i], ci[i], a_to_b.depth, a_to_b.rules)