From 046d1c0363df85c940ad2839c3159176c9a47d43 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 15:22:13 +0000 Subject: [PATCH 01/14] cterm/cterm: add staticmethod CSubst.from_pred --- pyk/src/pyk/cterm/cterm.py | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 10f9f1cb526..0b259913d4c 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -6,7 +6,7 @@ from typing import TYPE_CHECKING from ..kast import KInner -from ..kast.inner import KApply, KRewrite, KToken, Subst, bottom_up +from ..kast.inner import KApply, KRewrite, KToken, KVariable, Subst, bottom_up from ..kast.manip import ( abstract_term_safely, build_claim, @@ -322,6 +322,23 @@ def from_dict(dct: dict[str, Any]) -> CSubst: constraints = (KInner.from_dict(c) for c in dct['constraints']) return CSubst(subst=subst, constraints=constraints) + @staticmethod + def from_pred(pred: KInner) -> CSubst: + """Extract from a boolean predicate a CSubst.""" + _subst: dict[str, KInner] = {} + _constraints: list[KInner] = [] + for clause in flatten_label('#And', pred): + if ( + type(clause) is KApply + and clause.label.name == '#Equals' + and type(clause.args[0]) is KVariable + and clause.args[0].name not in _subst + ): + _subst[clause.args[0].name] = clause.args[1] + else: + _constraints.append(clause) + return CSubst(subst=Subst(_subst), constraints=_constraints) + @property def constraint(self) -> KInner: """Return the set of constraints as a single flattened constraint using `mlAnd`.""" From b1eb54d9c403e71c01e7e4119bb06230f54bad23 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 15:22:36 +0000 Subject: [PATCH 02/14] cterm/symbolic: use CSubst.from_pred to simplify code, avoid bad use of mlEquals --- pyk/src/pyk/cterm/symbolic.py | 17 +++-------------- 1 file changed, 3 insertions(+), 14 deletions(-) diff --git a/pyk/src/pyk/cterm/symbolic.py b/pyk/src/pyk/cterm/symbolic.py index 1ad00617d69..9cb52bbb4a6 100644 --- a/pyk/src/pyk/cterm/symbolic.py +++ b/pyk/src/pyk/cterm/symbolic.py @@ -25,7 +25,7 @@ kore_server, ) from ..prelude.k import GENERATED_TOP_CELL, K_ITEM -from ..prelude.ml import is_top, mlEquals +from ..prelude.ml import mlAnd if TYPE_CHECKING: from collections.abc import Iterable, Iterator @@ -267,19 +267,8 @@ def implies( raise ValueError('Received empty predicate for valid implication.') ml_subst = self.kore_to_kast(result.substitution) ml_pred = self.kore_to_kast(result.predicate) - ml_preds = flatten_label('#And', ml_pred) - if is_top(ml_subst): - csubst = CSubst(subst=Subst({}), constraints=ml_preds) - return CTermImplies(csubst, (), None, result.logs) - subst_pattern = mlEquals(KVariable('###VAR'), KVariable('###TERM')) - _subst: dict[str, KInner] = {} - for subst_pred in flatten_label('#And', ml_subst): - m = subst_pattern.match(subst_pred) - if m is not None and type(m['###VAR']) is KVariable: - _subst[m['###VAR'].name] = m['###TERM'] - else: - raise AssertionError(f'Received a non-substitution from implies endpoint: {subst_pred}') - csubst = CSubst(subst=Subst(_subst), constraints=ml_preds) + ml_subst_pred = mlAnd(flatten_label('#And', ml_subst) + flatten_label('#And', ml_pred)) + csubst = CSubst.from_pred(ml_subst_pred) return CTermImplies(csubst, (), None, result.logs) def assume_defined(self, cterm: CTerm, module_name: str | None = None) -> CTerm: From 6025afd11bae65e7d73173414f1769c9033b34d9 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 15:35:35 +0000 Subject: [PATCH 03/14] pyk/cterm/cterm: reuse kast.manip.extract_subst more robust routine --- pyk/src/pyk/cterm/cterm.py | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 0b259913d4c..58e7a85c85e 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -6,11 +6,12 @@ from typing import TYPE_CHECKING from ..kast import KInner -from ..kast.inner import KApply, KRewrite, KToken, KVariable, Subst, bottom_up +from ..kast.inner import KApply, KRewrite, KToken, Subst, bottom_up from ..kast.manip import ( abstract_term_safely, build_claim, build_rule, + extract_subst, flatten_label, free_vars, ml_pred_to_bool, @@ -325,19 +326,8 @@ def from_dict(dct: dict[str, Any]) -> CSubst: @staticmethod def from_pred(pred: KInner) -> CSubst: """Extract from a boolean predicate a CSubst.""" - _subst: dict[str, KInner] = {} - _constraints: list[KInner] = [] - for clause in flatten_label('#And', pred): - if ( - type(clause) is KApply - and clause.label.name == '#Equals' - and type(clause.args[0]) is KVariable - and clause.args[0].name not in _subst - ): - _subst[clause.args[0].name] = clause.args[1] - else: - _constraints.append(clause) - return CSubst(subst=Subst(_subst), constraints=_constraints) + subst, pred = extract_subst(pred) + return CSubst(subst=subst, constraints=flatten_label('#And', pred)) @property def constraint(self) -> KInner: From 8e7ea647960acae143db1f3c33930861c6af92d6 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 17:53:50 +0000 Subject: [PATCH 04/14] pyk/cterm/cterm: use kast.manip.remove_useless_constraints to filter constraints --- pyk/src/pyk/cterm/cterm.py | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 58e7a85c85e..e2a6c62c37b 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -218,17 +218,7 @@ def anti_unify( if KToken('true', 'Bool') not in [disjunct_lhs, disjunct_rhs]: new_cterm = new_cterm.add_constraint(mlEqualsTrue(orBool([disjunct_lhs, disjunct_rhs]))) - new_constraints = [] - fvs = new_cterm.free_vars - len_fvs = 0 - while len_fvs < len(fvs): - len_fvs = len(fvs) - for constraint in common_constraints: - if constraint not in new_constraints: - constraint_fvs = free_vars(constraint) - if any(fv in fvs for fv in constraint_fvs): - new_constraints.append(constraint) - fvs = fvs | constraint_fvs + new_constraints = remove_useless_constraints(common_constraints, new_cterm.free_vars) for constraint in new_constraints: new_cterm = new_cterm.add_constraint(constraint) From 91b6f49331523e66feeb3ea298c79ff9601df0e4 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 17:55:00 +0000 Subject: [PATCH 05/14] pyk/cterm/cterm: only compute self_unique_constraints and other_unique_constraints if needed --- pyk/src/pyk/cterm/cterm.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index e2a6c62c37b..0a47ac682bc 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -204,15 +204,15 @@ def anti_unify( """ new_config, self_subst, other_subst = anti_unify(self.config, other.config, kdef=kdef) common_constraints = [constraint for constraint in self.constraints if constraint in other.constraints] - self_unique_constraints = [ - ml_pred_to_bool(constraint) for constraint in self.constraints if constraint not in other.constraints - ] - other_unique_constraints = [ - ml_pred_to_bool(constraint) for constraint in other.constraints if constraint not in self.constraints - ] new_cterm = CTerm(config=new_config, constraints=()) if keep_values: + self_unique_constraints = [ + ml_pred_to_bool(constraint) for constraint in self.constraints if constraint not in other.constraints + ] + other_unique_constraints = [ + ml_pred_to_bool(constraint) for constraint in other.constraints if constraint not in self.constraints + ] disjunct_lhs = andBool([self_subst.pred] + self_unique_constraints) disjunct_rhs = andBool([other_subst.pred] + other_unique_constraints) if KToken('true', 'Bool') not in [disjunct_lhs, disjunct_rhs]: From a493079d2549fa1381a598d9449bd00d72ce5b84 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 18:35:18 +0000 Subject: [PATCH 06/14] pyk/cterm/cterm: add CSubst.pred for computing an ML predicate from a CSubst --- pyk/src/pyk/cterm/cterm.py | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 0a47ac682bc..e48cc1aae2d 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -6,7 +6,7 @@ from typing import TYPE_CHECKING from ..kast import KInner -from ..kast.inner import KApply, KRewrite, KToken, Subst, bottom_up +from ..kast.inner import KApply, KRewrite, KSort, KToken, KVariable, Subst, bottom_up from ..kast.manip import ( abstract_term_safely, build_claim, @@ -23,7 +23,7 @@ ) from ..prelude.k import GENERATED_TOP_CELL from ..prelude.kbool import andBool, orBool -from ..prelude.ml import is_bottom, is_top, mlAnd, mlBottom, mlEqualsTrue, mlImplies, mlTop +from ..prelude.ml import is_bottom, is_top, mlAnd, mlBottom, mlEquals, mlEqualsTrue, mlImplies, mlTop from ..utils import unique if TYPE_CHECKING: @@ -319,6 +319,20 @@ def from_pred(pred: KInner) -> CSubst: subst, pred = extract_subst(pred) return CSubst(subst=subst, constraints=flatten_label('#And', pred)) + def pred(self, sort_with: KDefinition | None = None, subst: bool = True, constraints: bool = True) -> KInner: + """Return an ML predicate representing this substitution.""" + _preds: list[KInner] = [] + if subst: + for k, v in self.subst.items(): + sort = KSort('K') + if sort_with is not None: + _sort = sort_with.sort(v) + sort = _sort if _sort is not None else sort + _preds.append(mlEquals(KVariable(k, sort=sort), v, arg_sort=sort)) + if constraints: + _preds.extend(self.constraints) + return mlAnd(_preds) + @property def constraint(self) -> KInner: """Return the set of constraints as a single flattened constraint using `mlAnd`.""" From f93b806a5deeee3456597318700f09366cdfb854 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 18:35:58 +0000 Subject: [PATCH 07/14] pyk/{kcfg/show,kcfg/tui,proof/reachability}: convert all uses of Subst.ml_pred to CSubst.pred --- pyk/src/pyk/kcfg/show.py | 4 +++- pyk/src/pyk/kcfg/tui.py | 12 ++++++++++-- pyk/src/pyk/proof/reachability.py | 6 ++++-- 3 files changed, 17 insertions(+), 5 deletions(-) diff --git a/pyk/src/pyk/kcfg/show.py b/pyk/src/pyk/kcfg/show.py index b4e2db73338..83eb51b4dd9 100644 --- a/pyk/src/pyk/kcfg/show.py +++ b/pyk/src/pyk/kcfg/show.py @@ -469,7 +469,9 @@ def dump(self, cfgid: str, cfg: KCFG, dump_dir: Path, dot: bool = False) -> None cover_file = covers_dir / f'config_{cover.source.id}_{cover.target.id}.txt' cover_constraint_file = covers_dir / f'constraint_{cover.source.id}_{cover.target.id}.txt' - subst_equalities = flatten_label('#And', cover.csubst.subst.ml_pred) + subst_equalities = flatten_label( + '#And', cover.csubst.pred(sort_with=self.kprint.definition, constraints=False) + ) if not cover_file.exists(): cover_file.write_text('\n'.join(self.kprint.pretty_print(se) for se in subst_equalities)) diff --git a/pyk/src/pyk/kcfg/tui.py b/pyk/src/pyk/kcfg/tui.py index 128c377b537..f346d81113c 100644 --- a/pyk/src/pyk/kcfg/tui.py +++ b/pyk/src/pyk/kcfg/tui.py @@ -309,7 +309,12 @@ def _cterm_text(cterm: CTerm) -> tuple[str, str]: term_str, constraint_str = _cterm_text(crewrite) elif type(self._element) is KCFG.Cover: - subst_equalities = map(_boolify, flatten_label('#And', self._element.csubst.subst.ml_pred)) + subst_equalities = map( + _boolify, + flatten_label( + '#And', self._element.csubst.pred(sort_with=self._kprint.definition, constraints=False) + ), + ) constraints = map(_boolify, flatten_label('#And', self._element.csubst.constraint)) term_str = '\n'.join(self._kprint.pretty_print(se) for se in subst_equalities) constraint_str = '\n'.join(self._kprint.pretty_print(c) for c in constraints) @@ -320,7 +325,10 @@ def _cterm_text(cterm: CTerm) -> tuple[str, str]: term_strs.append('') term_strs.append(f' - {shorten_hashes(target_id)}') if len(csubst.subst) > 0: - subst_equalities = map(_boolify, flatten_label('#And', csubst.subst.ml_pred)) + subst_equalities = map( + _boolify, + flatten_label('#And', csubst.pred(sort_with=self._kprint.definition, constraints=False)), + ) term_strs.extend(f' {self._kprint.pretty_print(cline)}' for cline in subst_equalities) if len(csubst.constraints) > 0: constraints = map(_boolify, flatten_label('#And', csubst.constraint)) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 9244a0c8500..62f5956f915 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -487,14 +487,16 @@ def from_spec_modules( return res - def path_constraints(self, final_node_id: NodeIdLike) -> KInner: + def path_constraints(self, final_node_id: NodeIdLike, sort_with: KDefinition | None = None) -> KInner: path = self.shortest_path_to(final_node_id) curr_constraint: KInner = mlTop() for edge in reversed(path): if type(edge) is KCFG.Split: assert len(edge.targets) == 1 csubst = edge.splits[edge.targets[0].id] - curr_constraint = mlAnd([csubst.subst.minimize().ml_pred, csubst.constraint, curr_constraint]) + curr_constraint = mlAnd( + [csubst.pred(sort_with=sort_with, constraints=False), csubst.constraint, curr_constraint] + ) if type(edge) is KCFG.Cover: curr_constraint = mlAnd([edge.csubst.constraint, edge.csubst.subst.apply(curr_constraint)]) return mlAnd(flatten_label('#And', curr_constraint)) From 7b9bbdf8ef87799932488e66cc1c04c21610b494 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 18:43:38 +0000 Subject: [PATCH 08/14] pyk/tests/unit/{kast/test_subst,test_cterm}: adapt tests of Subst.ml_pred to tests of CSubst.pred --- pyk/src/tests/unit/kast/test_subst.py | 20 ------------------ pyk/src/tests/unit/test_cterm.py | 30 +++++++++++++++++++++++---- 2 files changed, 26 insertions(+), 24 deletions(-) diff --git a/pyk/src/tests/unit/kast/test_subst.py b/pyk/src/tests/unit/kast/test_subst.py index fa5fd1c628c..d8fe816605c 100644 --- a/pyk/src/tests/unit/kast/test_subst.py +++ b/pyk/src/tests/unit/kast/test_subst.py @@ -7,7 +7,6 @@ from pyk.kast.inner import KApply, KLabel, KVariable, Subst from pyk.kast.manip import extract_subst -from pyk.prelude.kbool import TRUE from pyk.prelude.kint import INT, intToken from pyk.prelude.ml import mlAnd, mlEquals, mlEqualsTrue, mlOr, mlTop @@ -108,25 +107,6 @@ def test_unapply(term: KInner, subst: dict[str, KInner], expected: KInner) -> No assert actual == expected -ML_PRED_TEST_DATA: Final = ( - ('empty', Subst({}), KApply('#Top')), - ('singleton', Subst({'X': TRUE}), KApply('#Equals', [KVariable('X'), TRUE])), - ( - 'double', - Subst({'X': TRUE, 'Y': intToken(4)}), - KApply( - '#And', - [KApply('#Equals', [KVariable('X'), TRUE]), KApply('#Equals', [KVariable('Y'), intToken(4)])], - ), - ), -) - - -@pytest.mark.parametrize('test_id,subst,pred', ML_PRED_TEST_DATA, ids=[test_id for test_id, *_ in ML_PRED_TEST_DATA]) -def test_ml_pred(test_id: str, subst: Subst, pred: KInner) -> None: - assert subst.ml_pred == pred - - _0 = intToken(0) _EQ = KLabel('_==Int_') EXTRACT_SUBST_TEST_DATA: Final[tuple[tuple[KInner, dict[str, KInner], KInner], ...]] = ( diff --git a/pyk/src/tests/unit/test_cterm.py b/pyk/src/tests/unit/test_cterm.py index c9991f9fcde..e2364f73457 100644 --- a/pyk/src/tests/unit/test_cterm.py +++ b/pyk/src/tests/unit/test_cterm.py @@ -5,13 +5,14 @@ import pytest -from pyk.cterm import CTerm, cterm_build_claim, cterm_build_rule +from pyk.cterm import CSubst, CTerm, cterm_build_claim, cterm_build_rule from pyk.kast import Atts, KAtt -from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KVariable +from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KVariable, Subst from pyk.kast.outer import KClaim -from pyk.prelude.k import GENERATED_TOP_CELL +from pyk.prelude.k import GENERATED_TOP_CELL, K +from pyk.prelude.kbool import TRUE from pyk.prelude.kint import INT, intToken -from pyk.prelude.ml import mlAnd, mlEqualsTrue +from pyk.prelude.ml import mlAnd, mlEquals, mlEqualsTrue, mlTop from .utils import a, b, c, f, g, h, k, x, y, z @@ -186,3 +187,24 @@ def test_from_kast(test_id: str, kast: KInner, expected: CTerm) -> None: # Then assert cterm == expected + + +ML_PRED_TEST_DATA: Final = ( + ('empty', CSubst(Subst({})), mlTop()), + ('singleton', CSubst(Subst({'X': TRUE})), mlEquals(KVariable('X', sort=K), TRUE, arg_sort=K)), + ( + 'double', + CSubst(Subst({'X': TRUE, 'Y': intToken(4)})), + mlAnd( + [ + mlEquals(KVariable('X', sort=K), TRUE, arg_sort=K), + mlEquals(KVariable('Y', sort=K), intToken(4), arg_sort=K), + ] + ), + ), +) + + +@pytest.mark.parametrize('test_id,csubst,pred', ML_PRED_TEST_DATA, ids=[test_id for test_id, *_ in ML_PRED_TEST_DATA]) +def test_ml_pred(test_id: str, csubst: CSubst, pred: KInner) -> None: + assert csubst.pred() == pred From e8675c09e136a6e58d9544528f37119fa8d33305 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 18:43:57 +0000 Subject: [PATCH 09/14] pyk/kast/inner: remove poorly defined Subst.ml_pred method --- pyk/src/pyk/kast/inner.py | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/pyk/src/pyk/kast/inner.py b/pyk/src/pyk/kast/inner.py index b27a0d3153e..e034c048e7a 100644 --- a/pyk/src/pyk/kast/inner.py +++ b/pyk/src/pyk/kast/inner.py @@ -749,20 +749,6 @@ def from_pred(pred: KInner) -> Subst: raise ValueError(f'Invalid substitution predicate: {conjunct}') return Subst(subst) - @property - def ml_pred(self) -> KInner: - """Turn this `Subst` into a matching logic predicate using `{_#Equals_}` operator.""" - items = [] - for k in self: - if KVariable(k) != self[k]: - items.append(KApply('#Equals', [KVariable(k), self[k]])) - if len(items) == 0: - return KApply('#Top') - ml_term = items[0] - for _i in items[1:]: - ml_term = KApply('#And', [ml_term, _i]) - return ml_term - @property def pred(self) -> KInner: """Turn this `Subst` into a boolean predicate using `_==K_` operator.""" From 494652acb26a128ef3e8f18b9de85be939384181 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 21:59:02 +0000 Subject: [PATCH 10/14] Revert "pyk/cterm/cterm: only compute self_unique_constraints and other_unique_constraints if needed" This reverts commit 766c5392f8a6b889d5f86faf394a2b67a24ae1d5. --- pyk/src/pyk/cterm/cterm.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index e48cc1aae2d..a469a402db6 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -204,15 +204,15 @@ def anti_unify( """ new_config, self_subst, other_subst = anti_unify(self.config, other.config, kdef=kdef) common_constraints = [constraint for constraint in self.constraints if constraint in other.constraints] + self_unique_constraints = [ + ml_pred_to_bool(constraint) for constraint in self.constraints if constraint not in other.constraints + ] + other_unique_constraints = [ + ml_pred_to_bool(constraint) for constraint in other.constraints if constraint not in self.constraints + ] new_cterm = CTerm(config=new_config, constraints=()) if keep_values: - self_unique_constraints = [ - ml_pred_to_bool(constraint) for constraint in self.constraints if constraint not in other.constraints - ] - other_unique_constraints = [ - ml_pred_to_bool(constraint) for constraint in other.constraints if constraint not in self.constraints - ] disjunct_lhs = andBool([self_subst.pred] + self_unique_constraints) disjunct_rhs = andBool([other_subst.pred] + other_unique_constraints) if KToken('true', 'Bool') not in [disjunct_lhs, disjunct_rhs]: From 738ccf8658b13f74ea601e7fe78b9bbd87e82c2e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 22:26:56 +0000 Subject: [PATCH 11/14] pyk/cterm/cterm: use imported sort K instead of manually --- pyk/src/pyk/cterm/cterm.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index a469a402db6..14652361bdd 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -6,7 +6,7 @@ from typing import TYPE_CHECKING from ..kast import KInner -from ..kast.inner import KApply, KRewrite, KSort, KToken, KVariable, Subst, bottom_up +from ..kast.inner import KApply, KRewrite, KToken, KVariable, Subst, bottom_up from ..kast.manip import ( abstract_term_safely, build_claim, @@ -21,7 +21,7 @@ split_config_and_constraints, split_config_from, ) -from ..prelude.k import GENERATED_TOP_CELL +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 @@ -324,7 +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 = KSort('K') + sort = K if sort_with is not None: _sort = sort_with.sort(v) sort = _sort if _sort is not None else sort From 5d00f3c60b525a39533500e64f266f7e44e22689 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 22:32:06 +0000 Subject: [PATCH 12/14] cterm/cterm: simplify expression of sort for predicate equalities --- pyk/src/pyk/cterm/cterm.py | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 14652361bdd..baa9b7c13e7 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -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 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: _preds.extend(self.constraints) From 8757594842a364961e4af4d3f6d403b8ede82072 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 6 Sep 2024 00:52:15 +0000 Subject: [PATCH 13/14] 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 baa9b7c13e7..ce9b5ac688b 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 e2364f73457..df4849673d0 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)})), From 0e6ba9887c49336b4e95052489f2c43a807a7bc3 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 9 Sep 2024 15:45:10 +0000 Subject: [PATCH 14/14] pyk/cterm/cterm.py: only call sort_with once --- pyk/src/pyk/cterm/cterm.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index fe63d84ebc4..0c04e0ff207 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -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 not_none, unique +from ..utils import unique if TYPE_CHECKING: from collections.abc import Iterable, Iterator @@ -343,7 +343,10 @@ def pred(self, sort_with: KDefinition | None = None, subst: bool = True, constra _preds: list[KInner] = [] if subst: 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)) + sort = K + if sort_with is not None: + _sort = sort_with.sort(v) + sort = _sort if _sort is not None else sort _preds.append(mlEquals(KVariable(k, sort=sort), v, arg_sort=sort)) if constraints: _preds.extend(self.constraints)