Skip to content
This repository was archived by the owner on Apr 25, 2024. It is now read-only.

Commit d5895f9

Browse files
nwatson22nwatson22
authored
Merge 28157b5 into 97a9a21 
2 parents 97a9a21 + 28157b5 commit d5895f9

File tree

4 files changed

+146
-155
lines changed

4 files changed

+146
-155
lines changed

‎src/pyk/kast/manip.py‎

Lines changed: 1 addition & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66

77
from ..prelude.k import DOTS, GENERATED_TOP_CELL
88
from ..prelude.kbool import FALSE, TRUE, andBool, impliesBool, notBool, orBool
9-
from ..prelude.ml import mlAnd, mlEqualsTrue, mlImplies, mlOr, mlTop
9+
from ..prelude.ml import mlAnd, mlEqualsTrue, mlOr
1010
from ..utils import find_common_items, hash_str
1111
from .inner import KApply, KRewrite, KSequence, KToken, KVariable, Subst, bottom_up, top_down, var_occurrences
1212
from .kast import EMPTY_ATT, KAtt, WithKAtt
@@ -582,58 +582,6 @@ def _abstract(k: KInner) -> KVariable:
582582
return new_var
583583

584584

585-
def anti_unify(state1: KInner, state2: KInner) -> tuple[KInner, Subst, Subst]:
586-
def _rewrites_to_abstractions(_kast: KInner) -> KInner:
587-
if type(_kast) is KRewrite:
588-
return abstract_term_safely(_kast)
589-
return _kast
590-
591-
minimized_rewrite = push_down_rewrites(KRewrite(state1, state2))
592-
abstracted_state = bottom_up(_rewrites_to_abstractions, minimized_rewrite)
593-
subst1 = abstracted_state.match(state1)
594-
subst2 = abstracted_state.match(state2)
595-
if subst1 is None or subst2 is None:
596-
raise ValueError('Anti-unification failed to produce a more general state!')
597-
return (abstracted_state, subst1, subst2)
598-
599-
600-
def anti_unify_with_constraints(
601-
constrained_term_1: KInner,
602-
constrained_term_2: KInner,
603-
implications: bool = False,
604-
constraint_disjunct: bool = False,
605-
abstracted_disjunct: bool = False,
606-
) -> KInner:
607-
def disjunction_from_substs(subst1: Subst, subst2: Subst) -> KInner:
608-
if KToken('true', 'Bool') in [subst1.pred, subst2.pred]:
609-
return mlTop()
610-
return mlEqualsTrue(orBool([subst1.pred, subst2.pred]))
611-
612-
state1, constraint1 = split_config_and_constraints(constrained_term_1)
613-
state2, constraint2 = split_config_and_constraints(constrained_term_2)
614-
constraints1 = flatten_label('#And', constraint1)
615-
constraints2 = flatten_label('#And', constraint2)
616-
state, subst1, subst2 = anti_unify(state1, state2)
617-
618-
constraints = [c for c in constraints1 if c in constraints2]
619-
constraint1 = mlAnd([c for c in constraints1 if c not in constraints])
620-
constraint2 = mlAnd([c for c in constraints2 if c not in constraints])
621-
implication1 = mlImplies(constraint1, subst1.ml_pred)
622-
implication2 = mlImplies(constraint2, subst2.ml_pred)
623-
624-
if abstracted_disjunct:
625-
constraints.append(disjunction_from_substs(subst1, subst2))
626-
627-
if implications:
628-
constraints.append(implication1)
629-
constraints.append(implication2)
630-
631-
if constraint_disjunct:
632-
constraints.append(mlOr([constraint1, constraint2]))
633-
634-
return mlAnd([state] + constraints)
635-
636-
637585
def apply_existential_substitutions(constrained_term: KInner) -> KInner:
638586
state, constraint = split_config_and_constraints(constrained_term)
639587
constraints = flatten_label('#And', constraint)

‎src/pyk/kast/outer.py‎

Lines changed: 73 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,8 @@
1010
from functools import cached_property
1111
from typing import TYPE_CHECKING, final
1212

13-
from ..prelude.kbool import TRUE
14-
from ..prelude.ml import ML_QUANTIFIERS
13+
from ..prelude.kbool import TRUE, orBool
14+
from ..prelude.ml import ML_QUANTIFIERS, mlAnd, mlEqualsTrue, mlImplies, mlOr, mlTop
1515
from ..utils import filter_none, single, unique
1616
from .inner import (
1717
KApply,
@@ -35,6 +35,8 @@
3535
from os import PathLike
3636
from typing import Any, Final, TypeVar
3737

38+
from ..cterm import CTerm
39+
3840
RL = TypeVar('RL', bound='KRuleLike')
3941

4042
_LOGGER: Final = logging.getLogger(__name__)
@@ -1057,6 +1059,61 @@ def production_for_klabel(self, klabel: KLabel) -> KProduction:
10571059
raise ValueError(f'Expected a single production for label {klabel}, not: {prods}') from err
10581060
return self._production_for_klabel[klabel]
10591061

1062+
def anti_unify(self, state1: KInner, state2: KInner) -> tuple[KInner, Subst, Subst]:
1063+
from .manip import abstract_term_safely, push_down_rewrites
1064+
1065+
def _rewrites_to_abstractions(_kast: KInner) -> KInner:
1066+
if type(_kast) is KRewrite:
1067+
return abstract_term_safely(_kast, sort=self.sort(_kast))
1068+
return _kast
1069+
1070+
minimized_rewrite = push_down_rewrites(KRewrite(state1, state2))
1071+
abstracted_state = bottom_up(_rewrites_to_abstractions, minimized_rewrite)
1072+
subst1 = abstracted_state.match(state1)
1073+
subst2 = abstracted_state.match(state2)
1074+
if subst1 is None or subst2 is None:
1075+
raise ValueError('Anti-unification failed to produce a more general state!')
1076+
return (abstracted_state, subst1, subst2)
1077+
1078+
def anti_unify_with_constraints(
1079+
self,
1080+
constrained_term_1: CTerm,
1081+
constrained_term_2: CTerm,
1082+
implications: bool = False,
1083+
constraint_disjunct: bool = False,
1084+
abstracted_disjunct: bool = False,
1085+
) -> KInner:
1086+
from .manip import flatten_label, split_config_and_constraints
1087+
1088+
def disjunction_from_substs(subst1: Subst, subst2: Subst) -> KInner:
1089+
if KToken('true', 'Bool') in [subst1.pred, subst2.pred]:
1090+
return mlTop()
1091+
return mlEqualsTrue(orBool([subst1.pred, subst2.pred]))
1092+
1093+
state1, constraint1 = split_config_and_constraints(constrained_term_1.kast)
1094+
state2, constraint2 = split_config_and_constraints(constrained_term_2.kast)
1095+
constraints1 = flatten_label('#And', constraint1)
1096+
constraints2 = flatten_label('#And', constraint2)
1097+
state, subst1, subst2 = self.anti_unify(state1, state2)
1098+
1099+
constraints = [c for c in constraints1 if c in constraints2]
1100+
constraint1 = mlAnd([c for c in constraints1 if c not in constraints])
1101+
constraint2 = mlAnd([c for c in constraints2 if c not in constraints])
1102+
implication1 = mlImplies(constraint1, subst1.ml_pred)
1103+
implication2 = mlImplies(constraint2, subst2.ml_pred)
1104+
1105+
if abstracted_disjunct:
1106+
constraints.append(disjunction_from_substs(subst1, subst2))
1107+
1108+
if implications:
1109+
constraints.append(implication1)
1110+
constraints.append(implication2)
1111+
1112+
if constraint_disjunct:
1113+
constraints.append(mlOr([constraint1, constraint2]))
1114+
1115+
return mlAnd([state] + constraints)
1116+
10601117
def production_for_cell_sort(self, sort: KSort) -> KProduction:
10611118
# Typical cell production has 3 productions:
10621119
# syntax KCell ::= "project:KCell" "(" K ")" [function, projection]
@@ -1101,8 +1158,11 @@ def sort(self, kast: KInner) -> KSort | None:
11011158
case KToken(_, sort) | KVariable(_, sort):
11021159
return sort
11031160
case KRewrite(lhs, rhs):
1104-
sort = self.sort(lhs)
1105-
return sort if sort == self.sort(rhs) else None
1161+
lhs_sort = self.sort(lhs)
1162+
rhs_sort = self.sort(rhs)
1163+
if lhs_sort and rhs_sort:
1164+
return self.least_common_supersort(lhs_sort, rhs_sort)
1165+
return None
11061166
case KSequence(_):
11071167
return KSort('K')
11081168
case KApply(label, _):
@@ -1128,6 +1188,15 @@ def sort_strict(self, kast: KInner) -> KSort:
11281188
raise ValueError(f'Could not determine sort of term: {kast}')
11291189
return sort
11301190

1191+
def least_common_supersort(self, sort1: KSort, sort2: KSort) -> KSort | None:
1192+
if sort1 == sort2:
1193+
return sort1
1194+
if sort1 in self.subsorts(sort2):
1195+
return sort2
1196+
if sort2 in self.subsorts(sort1):
1197+
return sort1
1198+
return None
1199+
11311200
def greatest_common_subsort(self, sort1: KSort, sort2: KSort) -> KSort | None:
11321201
if sort1 == sort2:
11331202
return sort1

‎src/tests/integration/kcfg/test_imp.py‎

Lines changed: 69 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@
88

99
from pyk.cterm import CSubst, CTerm
1010
from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst
11-
from pyk.kast.manip import minimize_term
11+
from pyk.kast.manip import get_cell, minimize_term
1212
from pyk.kcfg.semantics import KCFGSemantics
1313
from pyk.kcfg.show import KCFGShow
14-
from pyk.prelude.kbool import BOOL, notBool
14+
from pyk.prelude.kbool import BOOL, notBool, orBool
1515
from pyk.prelude.kint import intToken
1616
from pyk.prelude.ml import mlAnd, mlBottom, mlEqualsFalse, mlEqualsTrue, mlTop
1717
from pyk.proof import APRBMCProof, APRBMCProver, APRProof, APRProver, ProofStatus
@@ -1147,3 +1147,70 @@ def test_fail_fast(
11471147
assert len(proof.pending) == 1
11481148
assert len(proof.terminal) == 1
11491149
assert len(proof.failing) == 1
1150+
1151+
def test_anti_unify_with_constraints(
1152+
self,
1153+
kprint: KPrint,
1154+
) -> None:
1155+
cterm1 = self.config(
1156+
kprint=kprint,
1157+
k='int $n ; { }',
1158+
state='$s |-> 0',
1159+
constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]),
1160+
)
1161+
cterm2 = self.config(
1162+
kprint=kprint,
1163+
k='int $n ; { }',
1164+
state='$s |-> 1',
1165+
constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]),
1166+
)
1167+
1168+
anti_unifier = kprint.definition.anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True)
1169+
1170+
k_cell = get_cell(anti_unifier, 'STATE_CELL')
1171+
assert type(k_cell) is KApply
1172+
assert k_cell.label.name == '_|->_'
1173+
assert type(k_cell.args[1]) is KVariable
1174+
abstracted_var: KVariable = k_cell.args[1]
1175+
1176+
expected_anti_unifier = self.config(
1177+
kprint=kprint,
1178+
k='int $n ; { }',
1179+
state=f'$s |-> {abstracted_var.name}:Int',
1180+
constraint=mlAnd(
1181+
[
1182+
KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]),
1183+
mlEqualsTrue(
1184+
orBool(
1185+
[
1186+
KApply('_==K_', [KVariable(name=abstracted_var.name), intToken(0)]),
1187+
KApply('_==K_', [KVariable(name=abstracted_var.name), intToken(1)]),
1188+
]
1189+
)
1190+
),
1191+
]
1192+
),
1193+
).kast
1194+
1195+
assert anti_unifier == expected_anti_unifier
1196+
1197+
def test_anti_unify_with_constraints_subst_true(
1198+
self,
1199+
kprint: KPrint,
1200+
) -> None:
1201+
cterm1 = self.config(
1202+
kprint=kprint,
1203+
k='int $n ; { }',
1204+
state='$s |-> 0',
1205+
constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]),
1206+
)
1207+
cterm2 = self.config(
1208+
kprint=kprint,
1209+
k='int $n ; { }',
1210+
state='$s |-> 0',
1211+
constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]),
1212+
)
1213+
1214+
anti_unifier = kprint.definition.anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True)
1215+
1216+
assert anti_unifier == cterm1.kast

‎src/tests/unit/kast/test_manip.py‎

Lines changed: 3 additions & 96 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,8 @@
55

66
import pytest
77

8-
from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KToken, KVariable, Subst
8+
from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KVariable, Subst
99
from pyk.kast.manip import (
10-
anti_unify_with_constraints,
1110
bool_to_ml_pred,
1211
collapse_dots,
1312
minimize_term,
@@ -16,13 +15,12 @@
1615
remove_generated_cells,
1716
rename_generated_vars,
1817
simplify_bool,
19-
split_config_and_constraints,
2018
split_config_from,
2119
)
2220
from pyk.prelude.k import DOTS, GENERATED_TOP_CELL
23-
from pyk.prelude.kbool import BOOL, FALSE, TRUE, andBool, notBool, orBool
21+
from pyk.prelude.kbool import BOOL, FALSE, TRUE, andBool, notBool
2422
from pyk.prelude.kint import INT, intToken
25-
from pyk.prelude.ml import mlAnd, mlEqualsTrue, mlTop
23+
from pyk.prelude.ml import mlEqualsTrue, mlTop
2624

2725
from ..utils import a, b, c, f, k, x
2826

@@ -341,94 +339,3 @@ def test_split_config_from(term: KInner, expected_config: KInner, expected_subst
341339
# Then
342340
assert actual_config == expected_config
343341
assert actual_subst == expected_subst
344-
345-
346-
def test_anti_unify_with_constraints() -> None:
347-
cterm1 = mlAnd(
348-
[
349-
KApply(
350-
'<generatedTop>',
351-
[
352-
KApply('<k>', KToken('1', 'Int')),
353-
KApply('<generatedCounter>', KVariable('GENERATEDCOUNTER_CELL')),
354-
],
355-
),
356-
mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
357-
]
358-
)
359-
cterm2 = mlAnd(
360-
[
361-
KApply(
362-
'<generatedTop>',
363-
[
364-
KApply('<k>', KToken('2', 'Int')),
365-
KApply('<generatedCounter>', KVariable('GENERATEDCOUNTER_CELL')),
366-
],
367-
),
368-
mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
369-
]
370-
)
371-
372-
anti_unifier = anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True)
373-
374-
config, constraints = split_config_and_constraints(anti_unifier)
375-
376-
assert type(config) is KApply
377-
assert type(config.args[0]) is KApply
378-
assert type(config.args[0].args[0]) is KVariable
379-
var_name = config.args[0].args[0].name
380-
381-
expected = mlAnd(
382-
[
383-
mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
384-
mlEqualsTrue(
385-
orBool(
386-
[
387-
KApply('_==K_', [KVariable(var_name), KToken('1', 'Int')]),
388-
KApply('_==K_', [KVariable(var_name), KToken('2', 'Int')]),
389-
]
390-
)
391-
),
392-
]
393-
)
394-
395-
assert expected == constraints
396-
397-
398-
def test_anti_unify_with_constraints_subst_true() -> None:
399-
cterm1 = mlAnd(
400-
[
401-
KApply(
402-
'<generatedTop>',
403-
[
404-
KApply('<k>', KToken('1', 'Int')),
405-
KApply('<generatedCounter>', KVariable('GENERATEDCOUNTER_CELL')),
406-
],
407-
),
408-
mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
409-
]
410-
)
411-
cterm2 = mlAnd(
412-
[
413-
KApply(
414-
'<generatedTop>',
415-
[
416-
KApply('<k>', KToken('1', 'Int')),
417-
KApply('<generatedCounter>', KVariable('GENERATEDCOUNTER_CELL')),
418-
],
419-
),
420-
mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
421-
]
422-
)
423-
424-
anti_unifier = anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True)
425-
426-
config, constraints = split_config_and_constraints(anti_unifier)
427-
428-
expected = mlAnd(
429-
[
430-
mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
431-
]
432-
)
433-
434-
assert expected == constraints

0 commit comments

Comments
 (0)