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

Commit 34f35cf

Browse files
nwatson22nwatson22
committed
Incorporarte code from #544 which removes constraints for variables that no longer appear after abstraction during merge
1 parent fee00bb commit 34f35cf

File tree

2 files changed

+112
-24
lines changed

2 files changed

+112
-24
lines changed

‎src/pyk/cterm.py‎

Lines changed: 30 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -142,16 +142,41 @@ def _ml_impl(antecedents: Iterable[KInner], consequents: Iterable[KInner]) -> KI
142142
def add_constraint(self, new_constraint: KInner) -> CTerm:
143143
return CTerm(self.config, [new_constraint] + list(self.constraints))
144144

145-
def anti_unify(self, other_term: CTerm, kdef: KDefinition | None = None) -> KInner:
145+
def anti_unify(
146+
self, other: CTerm, keep_values: bool = False, kdef: KDefinition | None = None
147+
) -> tuple[CTerm, CSubst, CSubst]:
146148
def disjunction_from_substs(subst1: Subst, subst2: Subst) -> KInner:
147149
if KToken('true', 'Bool') in [subst1.pred, subst2.pred]:
148150
return mlTop()
149151
return mlEqualsTrue(orBool([subst1.pred, subst2.pred]))
150152

151-
new_config, self_subst, other_subst = anti_unify(self.config, other_term.config, kdef)
152-
constraints = [c for c in self.constraints if c in other_term.constraints]
153-
constraints.append(disjunction_from_substs(self_subst, other_subst))
154-
return mlAnd([new_config] + constraints)
153+
new_config, self_subst, other_subst = anti_unify(self.config, other.config, kdef=kdef)
154+
common_constraints = [constraint for constraint in self.constraints if constraint in other.constraints]
155+
156+
if keep_values:
157+
new_constraints = common_constraints
158+
new_constraints.append(disjunction_from_substs(self_subst, other_subst))
159+
else:
160+
new_constraints = []
161+
fvs = free_vars(new_config)
162+
len_fvs = 0
163+
while len_fvs < len(fvs):
164+
len_fvs = len(fvs)
165+
for constraint in common_constraints:
166+
if constraint not in new_constraints:
167+
constraint_fvs = free_vars(constraint)
168+
if any(fv in fvs for fv in constraint_fvs):
169+
new_constraints.append(constraint)
170+
fvs.extend(constraint_fvs)
171+
172+
new_cterm = CTerm(config=new_config, constraints=new_constraints)
173+
self_csubst = new_cterm.match_with_constraint(self)
174+
other_csubst = new_cterm.match_with_constraint(other)
175+
if self_csubst is None or other_csubst is None:
176+
raise ValueError(
177+
f'Anti-unification failed to produce a more general state: {(new_cterm, (self, self_csubst), (other, other_csubst))}'
178+
)
179+
return (new_cterm, self_csubst, other_csubst)
155180

156181

157182
def anti_unify(state1: KInner, state2: KInner, kdef: KDefinition | None = None) -> tuple[KInner, Subst, Subst]:

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

Lines changed: 82 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1148,26 +1148,86 @@ def test_fail_fast(
11481148
assert len(proof.terminal) == 1
11491149
assert len(proof.failing) == 1
11501150

1151-
def test_anti_unify(
1151+
def test_anti_unify_forget_values(
11521152
self,
1153+
kcfg_explore: KCFGExplore,
1154+
kprint: KPrint,
1155+
) -> None:
1156+
cterm1 = self.config(
1157+
kprint=kprint,
1158+
k='int $n ; { }',
1159+
state='N |-> X:Int',
1160+
constraint=mlAnd(
1161+
[
1162+
mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
1163+
mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])),
1164+
mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])),
1165+
]
1166+
),
1167+
)
1168+
cterm2 = self.config(
1169+
kprint=kprint,
1170+
k='int $n ; { }',
1171+
state='N |-> Y:Int',
1172+
constraint=mlAnd(
1173+
[
1174+
mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
1175+
mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])),
1176+
mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])),
1177+
]
1178+
),
1179+
)
1180+
1181+
anti_unifier, subst1, subst2 = cterm1.anti_unify(cterm2, keep_values=False, kdef=kprint.definition)
1182+
1183+
k_cell = get_cell(anti_unifier.kast, 'STATE_CELL')
1184+
assert type(k_cell) is KApply
1185+
assert k_cell.label.name == '_|->_'
1186+
assert type(k_cell.args[1]) is KVariable
1187+
abstracted_var: KVariable = k_cell.args[1]
1188+
1189+
expected_anti_unifier = self.config(
1190+
kprint=kprint,
1191+
k='int $n ; { }',
1192+
state=f'N |-> {abstracted_var.name}:Int',
1193+
constraint=mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
1194+
)
1195+
1196+
assert anti_unifier.kast == expected_anti_unifier.kast
1197+
1198+
def test_anti_unify_keep_values(
1199+
self,
1200+
kcfg_explore: KCFGExplore,
11531201
kprint: KPrint,
11541202
) -> None:
11551203
cterm1 = self.config(
11561204
kprint=kprint,
11571205
k='int $n ; { }',
1158-
state='$s |-> 0',
1159-
constraint=mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
1206+
state='N |-> X:Int',
1207+
constraint=mlAnd(
1208+
[
1209+
mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
1210+
mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])),
1211+
mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])),
1212+
]
1213+
),
11601214
)
11611215
cterm2 = self.config(
11621216
kprint=kprint,
11631217
k='int $n ; { }',
1164-
state='$s |-> 1',
1165-
constraint=mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
1218+
state='N |-> Y:Int',
1219+
constraint=mlAnd(
1220+
[
1221+
mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
1222+
mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])),
1223+
mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])),
1224+
]
1225+
),
11661226
)
11671227

1168-
anti_unifier = cterm1.anti_unify(cterm2, kprint.definition)
1228+
anti_unifier, subst1, subst2 = cterm1.anti_unify(cterm2, keep_values=True, kdef=kprint.definition)
11691229

1170-
k_cell = get_cell(anti_unifier, 'STATE_CELL')
1230+
k_cell = get_cell(anti_unifier.kast, 'STATE_CELL')
11711231
assert type(k_cell) is KApply
11721232
assert k_cell.label.name == '_|->_'
11731233
assert type(k_cell.args[1]) is KVariable
@@ -1176,41 +1236,44 @@ def test_anti_unify(
11761236
expected_anti_unifier = self.config(
11771237
kprint=kprint,
11781238
k='int $n ; { }',
1179-
state=f'$s |-> {abstracted_var.name}:Int',
1239+
state=f'N |-> {abstracted_var.name}:Int',
11801240
constraint=mlAnd(
11811241
[
1182-
mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
1242+
mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
1243+
mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])),
1244+
mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])),
11831245
mlEqualsTrue(
11841246
orBool(
11851247
[
1186-
KApply('_==K_', [KVariable(name=abstracted_var.name), intToken(0)]),
1187-
KApply('_==K_', [KVariable(name=abstracted_var.name), intToken(1)]),
1248+
KApply('_==K_', [KVariable(name=abstracted_var.name), KVariable('X', 'Int')]),
1249+
KApply('_==K_', [KVariable(name=abstracted_var.name), KVariable('Y', 'Int')]),
11881250
]
11891251
)
11901252
),
11911253
]
11921254
),
1193-
).kast
1255+
)
11941256

1195-
assert anti_unifier == expected_anti_unifier
1257+
assert anti_unifier.kast == expected_anti_unifier.kast
11961258

11971259
def test_anti_unify_subst_true(
11981260
self,
1261+
kcfg_explore: KCFGExplore,
11991262
kprint: KPrint,
12001263
) -> None:
12011264
cterm1 = self.config(
12021265
kprint=kprint,
12031266
k='int $n ; { }',
1204-
state='$s |-> 0',
1205-
constraint=mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
1267+
state='N |-> 0',
1268+
constraint=mlEqualsTrue(KApply('_==K_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
12061269
)
12071270
cterm2 = self.config(
12081271
kprint=kprint,
12091272
k='int $n ; { }',
1210-
state='$s |-> 0',
1211-
constraint=mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])),
1273+
state='N |-> 0',
1274+
constraint=mlEqualsTrue(KApply('_==K_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
12121275
)
12131276

1214-
anti_unifier = cterm1.anti_unify(cterm2, kprint.definition)
1277+
anti_unifier, _, _ = cterm1.anti_unify(cterm2, keep_values=True, kdef=kprint.definition)
12151278

1216-
assert anti_unifier == cterm1.kast
1279+
assert anti_unifier.kast == cterm1.kast

0 commit comments

Comments
 (0)