From d5bcbd2b3d5ca7068c21078a2281fb10147db35a Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Tue, 20 Aug 2024 16:55:42 +0800 Subject: [PATCH] fix `match_with_constraint` and `CSubst.appy` fix `match_with_constraint` and `CSubst.appy` --- pyk/src/pyk/cterm/cterm.py | 8 +++----- pyk/src/tests/unit/test_cterm.py | 30 ++++++++++++++++++++++++++++-- 2 files changed, 31 insertions(+), 7 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 7fc790eced0..ee16972922b 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -166,16 +166,14 @@ 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)) - - return CSubst(subst=subst, constraints=[constraint]) + return CSubst(subst=subst, constraints=cterm.constraints) @staticmethod def _ml_impl(antecedents: Iterable[KInner], consequents: Iterable[KInner]) -> KInner: antecedent = mlAnd(unique(antecedents), GENERATED_TOP_CELL) consequent = mlAnd(unique(term for term in consequents if term not in set(antecedents)), GENERATED_TOP_CELL) - if mlTop(GENERATED_TOP_CELL) in {antecedent, consequent}: + if mlTop(GENERATED_TOP_CELL) in [antecedent, consequent]: return consequent return mlImplies(antecedent, consequent, GENERATED_TOP_CELL) @@ -333,7 +331,7 @@ 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) + _kast = self.subst(cterm.config) return CTerm(_kast, [self.constraint]) diff --git a/pyk/src/tests/unit/test_cterm.py b/pyk/src/tests/unit/test_cterm.py index c9991f9fcde..76c0d44dcac 100644 --- a/pyk/src/tests/unit/test_cterm.py +++ b/pyk/src/tests/unit/test_cterm.py @@ -10,7 +10,7 @@ from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KVariable from pyk.kast.outer import KClaim from pyk.prelude.k import GENERATED_TOP_CELL -from pyk.prelude.kint import INT, intToken +from pyk.prelude.kint import INT, geInt, intToken from pyk.prelude.ml import mlAnd, mlEqualsTrue from .utils import a, b, c, f, g, h, k, x, y, z @@ -34,8 +34,12 @@ v1_sorted = KVariable('V1', sort=INT) +def generated_top(term: KInner) -> KApply: + return KApply(KLabel('', GENERATED_TOP_CELL), term) + + def _as_cterm(term: KInner) -> CTerm: - return CTerm(KApply(KLabel('', GENERATED_TOP_CELL), term)) + return CTerm(generated_top(term)) MATCH_TEST_DATA: Final[tuple[tuple[KInner, KInner], ...]] = ( @@ -74,6 +78,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'))),