fix match_with_constraint and CSubst.appy

runtimeverification · Aug 20, 2024 · b7c5bff · b7c5bff
1 parent 534217c
commit b7c5bff
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 7 deletions.
diff --git 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
@@ -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('<generatedTop>', GENERATED_TOP_CELL), term)
+
+
 def _as_cterm(term: KInner) -> CTerm:
-    return CTerm(KApply(KLabel('<generatedTop>', GENERATED_TOP_CELL), term))
+    return CTerm(generated_top(term))
 
 
 MATCH_TEST_DATA: Final[tuple[tuple[KInner, KInner], ...]] = (
@@ -74,6 +78,25 @@ 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'))),