Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
cterm/cterm: simplify expression of sort for predicate equalities
Browse files Browse the repository at this point in the history
ehildenb committed Sep 5, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
1 parent 06df00e commit 6475931
Showing 1 changed file with 2 additions and 5 deletions.
7 changes: 2 additions & 5 deletions pyk/src/pyk/cterm/cterm.py
Original file line number Diff line number Diff line change
@@ -24,7 +24,7 @@
from ..prelude.k import GENERATED_TOP_CELL, K
from ..prelude.kbool import andBool, orBool
from ..prelude.ml import is_bottom, is_top, mlAnd, mlBottom, mlEquals, mlEqualsTrue, mlImplies, mlTop
from ..utils import unique
from ..utils import not_none, unique

if TYPE_CHECKING:
from collections.abc import Iterable, Iterator
@@ -324,10 +324,7 @@ def pred(self, sort_with: KDefinition | None = None, subst: bool = True, constra
_preds: list[KInner] = []
if subst:
for k, v in self.subst.items():
sort = K
if sort_with is not None:
_sort = sort_with.sort(v)
sort = _sort if _sort is not None else sort
sort = K if sort_with is None or sort_with.sort(v) is None else not_none(sort_with.sort(v))
_preds.append(mlEquals(KVariable(k, sort=sort), v, arg_sort=sort))
if constraints:
_preds.extend(self.constraints)

0 comments on commit 6475931

Please sign in to comment.