fix match_with_constraint

runtimeverification · Sep 20, 2024 · 298df8a · 298df8a
1 parent 59293b8
commit 298df8a
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 6 deletions.
diff --git 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
@@ -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'))),