Formalize LocSet as Set of Locations - #3962

Open

Drodt wants to merge 36 commits into

mainfrom

Commits on Aug 12, 2026

Start locset as set
Drodt
committed
2228091
Fix matching for ParametricSortInstance, start adjusting rules, unify functions and rules for LocSet and Set
Drodt
committed
4d64919
Unify rules
Drodt
committed
84fe216
Fix some tests
Drodt
committed
0b733cd

Commits on Aug 13, 2026

Fix matching
Drodt
committed
ec52c55
Fix logic printer and some proofs
Drodt
committed
1182d1e
Spotless
Drodt
committed
a4a4f72
Simplify rules, remove QualifierWrapper, fix match plans
Drodt
committed
69fddaa
Use switch
Drodt
committed
dc3112b
Merge branch 'main' into locset-as-set
Drodt
committed
dff6f0f
Remove proofs
Drodt
committed
8ea68fd
Fix proof
Drodt
committed
8d78080
Update oracle
Drodt
committed
2ea7421
Start of taclet proofs
Drodt
committed
1e728fc
Fix interpreter matching for parametric functions and matching of mixed concrete & generic sort (G) patterns: Pair<int, G> and nested Pair<int, Pair<int, G>>
unp1
committed
beecb26

Commits on Aug 14, 2026

Fix some taclet proofs and taclet PO generation for parametric sorts and functions
Drodt
committed
55b8b5a
Merge branch 'locset-as-set' of https://github.com/KeYProject/key into locset-as-set
Drodt
committed
fd5cbb9
Fix taclet proofs
Drodt
committed
3c29ae3
Merge branch 'main' into locset-as-set
Drodt
committed
8c9cbca
Fix tests
Drodt
committed
b67fb56
Fix taclet oracle and some rules
Drodt
committed
3e5e375
Fix JML translation and test
Drodt
committed
ff6e52b
Fix tests and taclets
Drodt
committed
311db60
Fix rule sets
Drodt
committed
add3f0c
Generate taclet oracle
Drodt
committed
474b2ee
Fix slicing test
Drodt
committed
26ea9b9
Fix set example
Drodt
committed
67fa061
Fix test
Drodt
committed
233632e
Fix tests
Drodt
committed
4615d57
Fix tests
Drodt
committed
67025dc
Fix wd rules
Drodt
committed
bfd727e

Commits on Aug 15, 2026

Move the succedent version of setEqualityToElementOfRight to setRules
unp1
committed
016c3be
Add component strategies for the set theories
unp1
committed
0f62a74
Regenerate taclets.old.txt
Drodt
committed
d7e0ea2
Avoid NPE
Drodt
committed
8a8536d
Give SetStrategy and LocSet something more to do
unp1
committed
288a848