From 8bf17a31e694e35b85ea6103c97be8652a16f93c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 7 Oct 2024 17:43:00 +0200 Subject: [PATCH] Fix `match_with_constraint` (#4499) Fixes #4496 --------- Co-authored-by: JianhongZhao Co-authored-by: Everett Hildenbrandt --- pyk/src/pyk/cterm/cterm.py | 26 ++---------- pyk/src/pyk/kcfg/kcfg.py | 10 +---- pyk/src/pyk/kcfg/minimize.py | 40 +++++-------------- .../integration/proof/test_refute_node.py | 32 +-------------- pyk/src/tests/unit/kcfg/test_minimize.py | 16 ++++---- pyk/src/tests/unit/test_cterm.py | 28 ++++++++++++- pyk/src/tests/unit/test_kcfg.py | 7 ++-- 7 files changed, 55 insertions(+), 104 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 9ff3bc9737..75c6c831e1 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -167,9 +167,10 @@ def match_with_constraint(self, cterm: CTerm) -> CSubst | None: if subst is None: return None - constraint = self._ml_impl(cterm.constraints, map(subst, self.constraints)) + 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=subst, constraints=[constraint]) + return CSubst(subst, constraints) @staticmethod def _ml_impl(antecedents: Iterable[KInner], consequents: Iterable[KInner]) -> KInner: @@ -246,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. @@ -461,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/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 5289bf210a..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)) @@ -1091,10 +1087,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 diff --git a/pyk/src/pyk/kcfg/minimize.py b/pyk/src/pyk/kcfg/minimize.py index cfc50cd924..944222eeff 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 @@ -96,26 +95,19 @@ 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 = [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) # 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_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. @@ -136,31 +128,17 @@ 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 ( + 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 + 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(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. diff --git a/pyk/src/tests/integration/proof/test_refute_node.py b/pyk/src/tests/integration/proof/test_refute_node.py index e43e6f673e..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 @@ -327,35 +327,7 @@ 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) 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' diff --git a/pyk/src/tests/unit/test_cterm.py b/pyk/src/tests/unit/test_cterm.py index 955894504f..50490870d3 100644 --- a/pyk/src/tests/unit/test_cterm.py +++ b/pyk/src/tests/unit/test_cterm.py @@ -11,7 +11,7 @@ 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 @@ -75,6 +75,32 @@ def test_no_cterm_match(term: KInner, pattern: KInner) -> None: assert subst is None +MATCH_WITH_CONSTRAINT_TEST_DATA: Final = ( + (CTerm(k(x)), CTerm(k(x))), + (CTerm(k(x)), CTerm(k(y))), + (CTerm(k(x)), CTerm(k(y), (mlEqualsTrue(geInt(y, intToken(0))),))), + ( + CTerm(k(x), (mlEqualsTrue(geInt(y, intToken(0))),)), + CTerm( + k(y), + ( + mlEqualsTrue(geInt(y, intToken(0))), + 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) + + # Then + assert c_subst1 is not None and c_subst1.apply(t1) == t2 + + BUILD_RULE_TEST_DATA: Final = ( ( T(k(KVariable('K_CELL')), mem(KVariable('MEM_CELL'))), diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index de40de7e67..254073ba3a 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 @@ -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