diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 10f9f1cb52..44a9416fbb 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -6,14 +6,13 @@ 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, Subst, bottom_up from ..kast.manip import ( abstract_term_safely, build_claim, build_rule, flatten_label, free_vars, - ml_pred_to_bool, normalize_constraints, push_down_rewrites, remove_useless_constraints, @@ -21,8 +20,7 @@ split_config_from, ) 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, mlImplies, mlTop from ..utils import unique if TYPE_CHECKING: @@ -184,9 +182,7 @@ def add_constraint(self, new_constraint: KInner) -> CTerm: """Return a new `CTerm` with the additional constraints.""" 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 anti_unify(self, other: CTerm, kdef: KDefinition | None = None) -> tuple[CTerm, CSubst, CSubst]: """Given two `CTerm` instances, find a more general `CTerm` which can instantiate to both. Args: @@ -203,20 +199,7 @@ 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: - 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]: - new_cterm = new_cterm.add_constraint(mlEqualsTrue(orBool([disjunct_lhs, disjunct_rhs]))) - new_constraints = [] fvs = new_cterm.free_vars len_fvs = 0 diff --git a/pyk/src/pyk/kast/inner.py b/pyk/src/pyk/kast/inner.py index b27a0d3153..fc0d6a701e 100644 --- a/pyk/src/pyk/kast/inner.py +++ b/pyk/src/pyk/kast/inner.py @@ -763,19 +763,6 @@ def ml_pred(self) -> KInner: 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.""" - conjuncts = [ - KApply('_==K_', KVariable(name), val) - for name, val in self.items() - if type(val) is not KVariable or val.name != name - ] - if not conjuncts: - return KToken('true', 'Bool') - - return reduce(KLabel('_andBool_'), conjuncts) - @property def is_identity(self) -> bool: return len(self.minimize()) == 0 diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 8acbcd60cc..980e24c887 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -12,7 +12,7 @@ from pyk.kast.manip import minimize_term, sort_ac_collections from pyk.kcfg.semantics import KCFGSemantics from pyk.kcfg.show import KCFGShow -from pyk.prelude.kbool import FALSE, andBool, orBool +from pyk.prelude.kbool import FALSE from pyk.prelude.kint import intToken from pyk.prelude.ml import mlAnd, mlBottom, mlEquals, mlEqualsFalse, mlEqualsTrue, mlTop from pyk.proof import APRProver, ProofStatus @@ -1276,7 +1276,7 @@ def test_anti_unify_forget_values( ), ) - anti_unifier, subst1, subst2 = cterm1.anti_unify(cterm2, keep_values=False, kdef=kprove.definition) + anti_unifier, subst1, subst2 = cterm1.anti_unify(cterm2, kdef=kprove.definition) k_cell = anti_unifier.cell('STATE_CELL') assert type(k_cell) is KApply @@ -1293,81 +1293,6 @@ def test_anti_unify_forget_values( assert anti_unifier == expected_anti_unifier - def test_anti_unify_keep_values( - self, - kcfg_explore: KCFGExplore, - kprove: KProve, - ) -> None: - cterm1 = self.config( - kprint=kprove, - 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')])), - mlEqualsTrue(KApply('_>Int_', [KVariable('R', 'Int'), KToken('1', 'Int')])), - ] - ), - ) - cterm2 = self.config( - kprint=kprove, - 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')])), - mlEqualsTrue(KApply('_<=Int_', [KVariable('R', 'Int'), KToken('1', 'Int')])), - ] - ), - ) - - anti_unifier, subst1, subst2 = cterm1.anti_unify(cterm2, keep_values=True, kdef=kprove.definition) - - k_cell = anti_unifier.cell('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=kprove, - 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( - [ - andBool( - [ - KApply('_==K_', [KVariable(name=abstracted_var.name), KVariable('X', 'Int')]), - KApply('_>Int_', [KVariable('R', 'Int'), KToken('1', 'Int')]), - ] - ), - andBool( - [ - KApply('_==K_', [KVariable(name=abstracted_var.name), KVariable('Y', 'Int')]), - KApply('_<=Int_', [KVariable('R', 'Int'), KToken('1', 'Int')]), - ] - ), - ] - ) - ), - ] - ), - ) - - assert anti_unifier == expected_anti_unifier - def test_anti_unify_subst_true( self, kcfg_explore: KCFGExplore, @@ -1386,7 +1311,7 @@ def test_anti_unify_subst_true( constraint=mlEqualsTrue(KApply('_==K_', [KVariable('N', 'Int'), KToken('1', 'Int')])), ) - anti_unifier, _, _ = cterm1.anti_unify(cterm2, keep_values=True, kdef=kprove.definition) + anti_unifier, _, _ = cterm1.anti_unify(cterm2, kdef=kprove.definition) assert anti_unifier == cterm1