From 298df8ab1f849af9260c5d73136c1b5d169c349e Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Tue, 20 Aug 2024 16:55:42 +0800 Subject: [PATCH] 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'))),