Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Remove Subst.pred functionality #4626

Draft
wants to merge 3 commits into
base: develop
Choose a base branch
from
Draft

Remove Subst.pred functionality #4626

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8eff2fa
pyk/cterm/cterm: only compute self_unique_constraints and other_uniqu…
ehildenb Sep 5, 2024
f5be345
cterm/cterm, proof/test_imp: remove use of anti_unify keep_values arg…
ehildenb Sep 5, 2024
6427792
kast/inner: remove now unused Subst.pred
ehildenb Sep 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 3 additions & 20 deletions pyk/src/pyk/cterm/cterm.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,23 +6,21 @@
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,
split_config_and_constraints,
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:
Expand Down Expand Up @@ -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:
Expand All @@ -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
Expand Down
13 changes: 0 additions & 13 deletions pyk/src/pyk/kast/inner.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
81 changes: 3 additions & 78 deletions pyk/src/tests/integration/proof/test_imp.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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,
Expand All @@ -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

Expand Down
Loading