Error with symmetry breaking

[Former user]

Without symmetrybreaking models are generated normally. When symmetrybreaking is set to static, problem is classified as unsatisfiable.

[JoD]

De gedetecteerde inwisselbare domeinelementen zijn: {R1; R2; R3} met types {Room} {C31;C32} met types {Lecture}

Op het eerste gezicht is {C31;C32} correct, maar {R1; R2; R3} niet, aangezien de subtypes van Room een niet-symmetrische interpretatie hebben. Er loopt waarschijnlijk iets fout met de subtypedetectie van het symmetriedetectie-algoritme. Onlangs gerefactord?

[Broes De Cat]

Op het eerste zicht zie ik geen recente veranderingen aan de symmetrie-code (zeer weinig sowieso al) die aanleiding zouden kunnen geven tot deze bug. Wat doet de subtype detectie juist?

[JoD]

hmm, ik bedoelde eerder: is het subtypesysteem van idp onlangs gerefactord, waardoor de symmetriedetectie niet meer goed werkt.

Maar om op je vraag te antwoorden: er worden verzamelingen van domeinelementen gecreëerd op basis van de (sub)types waar ze in voorkomen. Vervolgens wordt gecheckt of de inputstructuur verandert als er twee omgewisseld worden. Het is waarschijnlijk die eerste stap die misloopt (bvb er wordt niet gedetecteerd dat twee domeinelementen van hetzelfde type in een verschillend subtype voorkomen).

Edit: waarschijnlijk niet gedetailleerd genoeg. Ben in de code aan het duiken...

[JoD]

Het loopt ergens mis in Symmetry.cpp lijn 870. Daar worden potentiële verzamelingen interchangeable domain elements geïnitialiseerd op basis van de sorts die voorkomen in gebruikte relaties in de theorie. Wat er waarschijnlijk mis loopt: er is geen relatie over LargeRoom of MultimediaRoom, dus er wordt (incorrect) afgeleid dat die types niet gebruikt worden in de theorie, en bijgevolg zijn R1-3 enkel van het type Room, en inwisselbaar.

Morgen eens zien hoe het opgelost kan worden...

[Broes De Cat]

Proposal to fix refs #556.

→ <<cset cb77f8cb87da>>

[JoD]

by pull request #389