From 8757594842a364961e4af4d3f6d403b8ede82072 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 6 Sep 2024 00:52:15 +0000 Subject: [PATCH] cterm/cterm: do not include identity substiutions in CSubst.pred --- pyk/src/pyk/cterm/cterm.py | 2 +- pyk/src/tests/unit/test_cterm.py | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index baa9b7c13e..ce9b5ac688 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -323,7 +323,7 @@ def pred(self, sort_with: KDefinition | None = None, subst: bool = True, constra """Return an ML predicate representing this substitution.""" _preds: list[KInner] = [] if subst: - for k, v in self.subst.items(): + for k, v in self.subst.minimize().items(): sort = K if not (sort_with and sort_with.sort(v)) else not_none(sort_with.sort(v)) _preds.append(mlEquals(KVariable(k, sort=sort), v, arg_sort=sort)) if constraints: diff --git a/pyk/src/tests/unit/test_cterm.py b/pyk/src/tests/unit/test_cterm.py index e2364f7345..df4849673d 100644 --- a/pyk/src/tests/unit/test_cterm.py +++ b/pyk/src/tests/unit/test_cterm.py @@ -192,6 +192,7 @@ def test_from_kast(test_id: str, kast: KInner, expected: CTerm) -> None: ML_PRED_TEST_DATA: Final = ( ('empty', CSubst(Subst({})), mlTop()), ('singleton', CSubst(Subst({'X': TRUE})), mlEquals(KVariable('X', sort=K), TRUE, arg_sort=K)), + ('identity', CSubst(Subst({'X': KVariable('X')})), mlTop()), ( 'double', CSubst(Subst({'X': TRUE, 'Y': intToken(4)})),