diff --git a/package/version b/package/version index 5bb6eae1e..0892550dd 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.415 +0.1.416 diff --git a/pyproject.toml b/pyproject.toml index 6272a7533..5c06d1e5b 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.415" +version = "0.1.416" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/src/pyk/cterm.py b/src/pyk/cterm.py index d02542d2a..2b5b3aff0 100644 --- a/src/pyk/cterm.py +++ b/src/pyk/cterm.py @@ -5,9 +5,10 @@ from itertools import chain from typing import TYPE_CHECKING -from .kast.inner import KApply, KInner, KRewrite, KVariable, Subst +from .kast.inner import KApply, KInner, KRewrite, KToken, KVariable, Subst, bottom_up from .kast.kast import KAtt from .kast.manip import ( + abstract_term_safely, apply_existential_substitutions, count_vars, flatten_label, @@ -22,13 +23,16 @@ ) from .kast.outer import KClaim, KRule from .prelude.k import GENERATED_TOP_CELL -from .prelude.ml import is_top, mlAnd, mlImplies, mlTop +from .prelude.kbool import orBool +from .prelude.ml import is_top, mlAnd, mlEqualsTrue, mlImplies, mlTop from .utils import unique if TYPE_CHECKING: from collections.abc import Iterable, Iterator from typing import Any + from .kast.outer import KDefinition + @dataclass(frozen=True, order=True) class CTerm: @@ -56,7 +60,7 @@ def from_dict(dct: dict[str, Any]) -> CTerm: @staticmethod def _check_config(config: KInner) -> None: if not isinstance(config, KApply) or not config.is_cell: - raise ValueError('Expected cell label, found: {config.label.name}') + raise ValueError(f'Expected cell label, found: {config}') @staticmethod def _normalize_constraints(constraints: Iterable[KInner]) -> tuple[KInner, ...]: @@ -138,6 +142,59 @@ def _ml_impl(antecedents: Iterable[KInner], consequents: Iterable[KInner]) -> KI def add_constraint(self, new_constraint: KInner) -> CTerm: return CTerm(self.config, [new_constraint] + list(self.constraints)) + def anti_unify( + self, other: CTerm, keep_values: bool = False, kdef: KDefinition | None = None + ) -> tuple[CTerm, CSubst, CSubst]: + def disjunction_from_substs(subst1: Subst, subst2: Subst) -> KInner: + if KToken('true', 'Bool') in [subst1.pred, subst2.pred]: + return mlTop() + return mlEqualsTrue(orBool([subst1.pred, subst2.pred])) + + 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] + + new_cterm = CTerm( + config=new_config, constraints=([disjunction_from_substs(self_subst, other_subst)] if keep_values else []) + ) + + new_constraints = [] + fvs = free_vars(new_cterm.kast) + 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.extend(constraint_fvs) + + for constraint in new_constraints: + new_cterm = new_cterm.add_constraint(constraint) + self_csubst = new_cterm.match_with_constraint(self) + other_csubst = new_cterm.match_with_constraint(other) + if self_csubst is None or other_csubst is None: + raise ValueError( + f'Anti-unification failed to produce a more general state: {(new_cterm, (self, self_csubst), (other, other_csubst))}' + ) + return (new_cterm, self_csubst, other_csubst) + + +def anti_unify(state1: KInner, state2: KInner, kdef: KDefinition | None = None) -> tuple[KInner, Subst, Subst]: + def _rewrites_to_abstractions(_kast: KInner) -> KInner: + if type(_kast) is KRewrite: + sort = kdef.sort(_kast) if kdef else None + return abstract_term_safely(_kast, sort=sort) + return _kast + + minimized_rewrite = push_down_rewrites(KRewrite(state1, state2)) + abstracted_state = bottom_up(_rewrites_to_abstractions, minimized_rewrite) + subst1 = abstracted_state.match(state1) + subst2 = abstracted_state.match(state2) + if subst1 is None or subst2 is None: + raise ValueError('Anti-unification failed to produce a more general state!') + return (abstracted_state, subst1, subst2) + @dataclass(frozen=True, order=True) class CSubst: diff --git a/src/pyk/kast/manip.py b/src/pyk/kast/manip.py index e5fc13446..126cc201c 100644 --- a/src/pyk/kast/manip.py +++ b/src/pyk/kast/manip.py @@ -6,7 +6,7 @@ from ..prelude.k import DOTS, GENERATED_TOP_CELL from ..prelude.kbool import FALSE, TRUE, andBool, impliesBool, notBool, orBool -from ..prelude.ml import mlAnd, mlEqualsTrue, mlImplies, mlOr, mlTop +from ..prelude.ml import mlAnd, mlEqualsTrue, mlOr from ..utils import find_common_items, hash_str from .inner import KApply, KRewrite, KSequence, KToken, KVariable, Subst, bottom_up, top_down, var_occurrences from .kast import EMPTY_ATT, KAtt, WithKAtt @@ -582,58 +582,6 @@ def _abstract(k: KInner) -> KVariable: return new_var -def anti_unify(state1: KInner, state2: KInner) -> tuple[KInner, Subst, Subst]: - def _rewrites_to_abstractions(_kast: KInner) -> KInner: - if type(_kast) is KRewrite: - return abstract_term_safely(_kast) - return _kast - - minimized_rewrite = push_down_rewrites(KRewrite(state1, state2)) - abstracted_state = bottom_up(_rewrites_to_abstractions, minimized_rewrite) - subst1 = abstracted_state.match(state1) - subst2 = abstracted_state.match(state2) - if subst1 is None or subst2 is None: - raise ValueError('Anti-unification failed to produce a more general state!') - return (abstracted_state, subst1, subst2) - - -def anti_unify_with_constraints( - constrained_term_1: KInner, - constrained_term_2: KInner, - implications: bool = False, - constraint_disjunct: bool = False, - abstracted_disjunct: bool = False, -) -> KInner: - def disjunction_from_substs(subst1: Subst, subst2: Subst) -> KInner: - if KToken('true', 'Bool') in [subst1.pred, subst2.pred]: - return mlTop() - return mlEqualsTrue(orBool([subst1.pred, subst2.pred])) - - state1, constraint1 = split_config_and_constraints(constrained_term_1) - state2, constraint2 = split_config_and_constraints(constrained_term_2) - constraints1 = flatten_label('#And', constraint1) - constraints2 = flatten_label('#And', constraint2) - state, subst1, subst2 = anti_unify(state1, state2) - - constraints = [c for c in constraints1 if c in constraints2] - constraint1 = mlAnd([c for c in constraints1 if c not in constraints]) - constraint2 = mlAnd([c for c in constraints2 if c not in constraints]) - implication1 = mlImplies(constraint1, subst1.ml_pred) - implication2 = mlImplies(constraint2, subst2.ml_pred) - - if abstracted_disjunct: - constraints.append(disjunction_from_substs(subst1, subst2)) - - if implications: - constraints.append(implication1) - constraints.append(implication2) - - if constraint_disjunct: - constraints.append(mlOr([constraint1, constraint2])) - - return mlAnd([state] + constraints) - - def apply_existential_substitutions(constrained_term: KInner) -> KInner: state, constraint = split_config_and_constraints(constrained_term) constraints = flatten_label('#And', constraint) diff --git a/src/pyk/kast/outer.py b/src/pyk/kast/outer.py index 1f04a7b68..dc1ec0b96 100644 --- a/src/pyk/kast/outer.py +++ b/src/pyk/kast/outer.py @@ -1101,8 +1101,11 @@ def sort(self, kast: KInner) -> KSort | None: case KToken(_, sort) | KVariable(_, sort): return sort case KRewrite(lhs, rhs): - sort = self.sort(lhs) - return sort if sort == self.sort(rhs) else None + lhs_sort = self.sort(lhs) + rhs_sort = self.sort(rhs) + if lhs_sort and rhs_sort: + return self.least_common_supersort(lhs_sort, rhs_sort) + return None case KSequence(_): return KSort('K') case KApply(label, _): @@ -1128,6 +1131,17 @@ def sort_strict(self, kast: KInner) -> KSort: raise ValueError(f'Could not determine sort of term: {kast}') return sort + def least_common_supersort(self, sort1: KSort, sort2: KSort) -> KSort | None: + if sort1 == sort2: + return sort1 + if sort1 in self.subsorts(sort2): + return sort2 + if sort2 in self.subsorts(sort1): + return sort1 + # Computing least common supersort is not currently supported if sort1 is not a subsort of sort2 or + # vice versa. In that case there may be more than one LCS. + return None + def greatest_common_subsort(self, sort1: KSort, sort2: KSort) -> KSort | None: if sort1 == sort2: return sort1 @@ -1135,6 +1149,8 @@ def greatest_common_subsort(self, sort1: KSort, sort2: KSort) -> KSort | None: return sort1 if sort2 in self.subsorts(sort1): return sort2 + # Computing greatest common subsort is not currently supported if sort1 is not a subsort of sort2 or + # vice versa. In that case there may be more than one GCS. return None # Sorts like Int cannot be injected directly into sort K so they are embedded in a KSequence. diff --git a/src/tests/integration/kcfg/test_imp.py b/src/tests/integration/kcfg/test_imp.py index 4142b5ff4..9ce17ecf6 100644 --- a/src/tests/integration/kcfg/test_imp.py +++ b/src/tests/integration/kcfg/test_imp.py @@ -8,10 +8,10 @@ from pyk.cterm import CSubst, CTerm from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst -from pyk.kast.manip import minimize_term +from pyk.kast.manip import get_cell, minimize_term from pyk.kcfg.semantics import KCFGSemantics from pyk.kcfg.show import KCFGShow -from pyk.prelude.kbool import BOOL, notBool +from pyk.prelude.kbool import BOOL, notBool, orBool from pyk.prelude.kint import intToken from pyk.prelude.ml import mlAnd, mlBottom, mlEqualsFalse, mlEqualsTrue, mlTop from pyk.proof import APRBMCProof, APRBMCProver, APRProof, APRProver, ProofStatus @@ -1147,3 +1147,137 @@ def test_fail_fast( assert len(proof.pending) == 1 assert len(proof.terminal) == 1 assert len(proof.failing) == 1 + + def test_anti_unify_forget_values( + self, + kcfg_explore: KCFGExplore, + kprint: KPrint, + ) -> None: + cterm1 = self.config( + kprint=kprint, + k='int $n ; { }', + state='N |-> X:Int', + constraint=mlAnd( + [ + mlEqualsTrue(KApply('_>Int_', [KVariable('K', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])), + ] + ), + ) + cterm2 = self.config( + kprint=kprint, + k='int $n ; { }', + state='N |-> Y:Int', + constraint=mlAnd( + [ + mlEqualsTrue(KApply('_>Int_', [KVariable('K', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])), + ] + ), + ) + + anti_unifier, subst1, subst2 = cterm1.anti_unify(cterm2, keep_values=False, kdef=kprint.definition) + + k_cell = get_cell(anti_unifier.kast, 'STATE_CELL') + assert type(k_cell) is KApply + assert k_cell.label.name == '_|->_' + assert type(k_cell.args[1]) is KVariable + abstracted_var: KVariable = k_cell.args[1] + + expected_anti_unifier = self.config( + kprint=kprint, + k='int $n ; { }', + state=f'N |-> {abstracted_var.name}:Int', + constraint=mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), + ) + + assert anti_unifier.kast == expected_anti_unifier.kast + + def test_anti_unify_keep_values( + self, + kcfg_explore: KCFGExplore, + kprint: KPrint, + ) -> None: + cterm1 = self.config( + kprint=kprint, + k='int $n ; { }', + state='N |-> X:Int', + constraint=mlAnd( + [ + mlEqualsTrue(KApply('_>Int_', [KVariable('K', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])), + ] + ), + ) + cterm2 = self.config( + kprint=kprint, + k='int $n ; { }', + state='N |-> Y:Int', + constraint=mlAnd( + [ + mlEqualsTrue(KApply('_>Int_', [KVariable('K', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])), + ] + ), + ) + + anti_unifier, subst1, subst2 = cterm1.anti_unify(cterm2, keep_values=True, kdef=kprint.definition) + + k_cell = get_cell(anti_unifier.kast, 'STATE_CELL') + assert type(k_cell) is KApply + assert k_cell.label.name == '_|->_' + assert type(k_cell.args[1]) is KVariable + abstracted_var: KVariable = k_cell.args[1] + + expected_anti_unifier = self.config( + kprint=kprint, + k='int $n ; { }', + state=f'N |-> {abstracted_var.name}:Int', + constraint=mlAnd( + [ + mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue( + orBool( + [ + KApply('_==K_', [KVariable(name=abstracted_var.name), KVariable('X', 'Int')]), + KApply('_==K_', [KVariable(name=abstracted_var.name), KVariable('Y', 'Int')]), + ] + ) + ), + ] + ), + ) + + assert anti_unifier.kast == expected_anti_unifier.kast + + def test_anti_unify_subst_true( + self, + kcfg_explore: KCFGExplore, + kprint: KPrint, + ) -> None: + cterm1 = self.config( + kprint=kprint, + k='int $n ; { }', + state='N |-> 0', + constraint=mlEqualsTrue(KApply('_==K_', [KVariable('N', 'Int'), KToken('1', 'Int')])), + ) + cterm2 = self.config( + kprint=kprint, + k='int $n ; { }', + state='N |-> 0', + constraint=mlEqualsTrue(KApply('_==K_', [KVariable('N', 'Int'), KToken('1', 'Int')])), + ) + + anti_unifier, _, _ = cterm1.anti_unify(cterm2, keep_values=True, kdef=kprint.definition) + + assert anti_unifier.kast == cterm1.kast diff --git a/src/tests/integration/konvert/test_simple_proofs.py b/src/tests/integration/konvert/test_simple_proofs.py index dd9b05125..a40df4543 100644 --- a/src/tests/integration/konvert/test_simple_proofs.py +++ b/src/tests/integration/konvert/test_simple_proofs.py @@ -547,6 +547,75 @@ ), ) +SORT_TERM_DATA: Final = ( + ( + 'variable-int', + KVariable('X', 'Int'), + KSort('Int'), + ), + ( + 'variable-bool', + KVariable('X', 'Bool'), + KSort('Bool'), + ), + ( + 'variable-k', + KVariable('X', 'K'), + KSort('K'), + ), + ( + 'variable-kitem', + KVariable('X', 'KItem'), + KSort('KItem'), + ), + ( + 'int-token', + intToken(1), + KSort('Int'), + ), + ( + 'bool-token', + KToken('true', 'Bool'), + KSort('Bool'), + ), + ( + 'ksequence', + KSequence((intToken(0), intToken(1), intToken(2))), + KSort('K'), + ), + ( + 'krewrite-same-sort', + KRewrite(lhs=intToken(0), rhs=intToken(1)), + KSort('Int'), + ), + ( + 'krewrite-direct-supersort-lhs', + KRewrite(lhs=intToken(0), rhs=KVariable('X', 'KItem')), + KSort('KItem'), + ), + ( + 'krewrite-direct-supersort-rhs', + KRewrite(rhs=intToken(0), lhs=KVariable('X', 'KItem')), + KSort('KItem'), + ), + ( + 'sort-parametric-int', + KApply( + KLabel('#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort', [KSort('Int')]), + [KToken('true', 'Bool'), intToken(1), intToken(2)], + ), + KSort('Int'), + ), + ( + 'sort-parametric-bool', + KApply( + KLabel('#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort', [KSort('Bool')]), + [KToken('true', 'Bool'), KToken('true', 'Bool'), KToken('false', 'Bool')], + ), + KSort('Bool'), + ), +) + class TestKonvertSimpleProofs(KompiledTest): KOMPILE_MAIN_FILE = K_FILES / 'simple-proofs.k' @@ -639,3 +708,21 @@ def test_explicit_krule_to_kore( # Then assert actual_kore_text == kore_text + + @pytest.mark.parametrize( + 'test_id,kast,expected_sort', + SORT_TERM_DATA, + ids=[test_id for test_id, *_ in SORT_TERM_DATA], + ) + def test_sort_term( + self, + definition: KDefinition, + test_id: str, + kast: KInner, + expected_sort: KSort, + ) -> None: + # When + actual_sort = definition.sort(kast) + + # Then + assert actual_sort == expected_sort diff --git a/src/tests/unit/kast/test_manip.py b/src/tests/unit/kast/test_manip.py index 175c9370a..d898d19ed 100644 --- a/src/tests/unit/kast/test_manip.py +++ b/src/tests/unit/kast/test_manip.py @@ -5,9 +5,8 @@ import pytest -from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KToken, KVariable, Subst +from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KVariable, Subst from pyk.kast.manip import ( - anti_unify_with_constraints, bool_to_ml_pred, collapse_dots, minimize_term, @@ -16,13 +15,12 @@ remove_generated_cells, rename_generated_vars, simplify_bool, - split_config_and_constraints, split_config_from, ) from pyk.prelude.k import DOTS, GENERATED_TOP_CELL -from pyk.prelude.kbool import BOOL, FALSE, TRUE, andBool, notBool, orBool +from pyk.prelude.kbool import BOOL, FALSE, TRUE, andBool, notBool from pyk.prelude.kint import INT, intToken -from pyk.prelude.ml import mlAnd, mlEqualsTrue, mlTop +from pyk.prelude.ml import mlEqualsTrue, mlTop from ..utils import a, b, c, f, k, x @@ -341,94 +339,3 @@ def test_split_config_from(term: KInner, expected_config: KInner, expected_subst # Then assert actual_config == expected_config assert actual_subst == expected_subst - - -def test_anti_unify_with_constraints() -> None: - cterm1 = mlAnd( - [ - KApply( - '', - [ - KApply('', KToken('1', 'Int')), - KApply('', KVariable('GENERATEDCOUNTER_CELL')), - ], - ), - mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), - ] - ) - cterm2 = mlAnd( - [ - KApply( - '', - [ - KApply('', KToken('2', 'Int')), - KApply('', KVariable('GENERATEDCOUNTER_CELL')), - ], - ), - mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), - ] - ) - - anti_unifier = anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True) - - config, constraints = split_config_and_constraints(anti_unifier) - - assert type(config) is KApply - assert type(config.args[0]) is KApply - assert type(config.args[0].args[0]) is KVariable - var_name = config.args[0].args[0].name - - expected = mlAnd( - [ - mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), - mlEqualsTrue( - orBool( - [ - KApply('_==K_', [KVariable(var_name), KToken('1', 'Int')]), - KApply('_==K_', [KVariable(var_name), KToken('2', 'Int')]), - ] - ) - ), - ] - ) - - assert expected == constraints - - -def test_anti_unify_with_constraints_subst_true() -> None: - cterm1 = mlAnd( - [ - KApply( - '', - [ - KApply('', KToken('1', 'Int')), - KApply('', KVariable('GENERATEDCOUNTER_CELL')), - ], - ), - mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), - ] - ) - cterm2 = mlAnd( - [ - KApply( - '', - [ - KApply('', KToken('1', 'Int')), - KApply('', KVariable('GENERATEDCOUNTER_CELL')), - ], - ), - mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), - ] - ) - - anti_unifier = anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True) - - config, constraints = split_config_and_constraints(anti_unifier) - - expected = mlAnd( - [ - mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), - ] - ) - - assert expected == constraints