Skip to content

Commit

Permalink
cterm/cterm: simplify expression of sort for predicate equalities
Browse files Browse the repository at this point in the history
  • Loading branch information
ehildenb committed Sep 5, 2024
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
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit 6475931

Please sign in to comment.