Issues with constructed types unless constructors are ordered alphabetically.

[Matthias van der Hallen]

No description provided.

[Bart Bogaerts]

Example?

[Matthias van der Hallen]

Sorry, I was still minimizing it, having previously done so with my thesis student but without saving it. I had problems reconstructing it, because I forgot about the inductive definition. It seems to be crucial to the buggy behavior. Some other things seem to be crucial as well, so the title might be incorrect.

So, the example: While the following theory would require every Installatie to be mapped to 1 by HeeftVermogen, Vaatwasmachine(1) is mapped to 0.

vocabulary V{
    type num isa nat
    type ID isa int
    type Installatie constructed from {Stopcontact(ID), Wasmachine(ID), Vaatwasmachine(ID)}

    partial HeeftVermogen(Installatie):num
    occurs(num)
//    res:num
}


theory T: V{
    {occurs(p)<- ?x[Installatie]: HeeftVermogen(x)=p.}
    !i : HeeftVermogen(i)=1.
//    HeeftVermogen(Vaatwasmachine(1))=res.
}


structure S:V{
    num = {0..1} 
    ID = {1}
}

procedure main(){
    stdoptions.nbmodels = 1
    printmodels(modelexpand(T,S)) 
}

Test it at: http://dtai.cs.kuleuven.be/krr/idp-ide/?src=91faf9f6051f2ba776193296f1586b73

The bug disappears when you either:

• Remove the inductive definition of occurs, or
• set stdoptions.nbmodels to 0, 2, … or
• order the constructors of Installatie alphabetically.

Adding the commented constraint and the res function constant surprisingly says res is 1!

‌

[Bart Bogaerts]

Also the bootstrapping might be related

[Bart Bogaerts]

Making the function non-partial even gives more fishy things!

[Matthias van der Hallen]

Oh indeed, we noticed but forgot to mention

[Matthias van der Hallen]

Just adding the sentence !x : occurs(x)=>true. makes the bug disappear.
So, adding a constraint over occurs seems to ‘solve' the issue, so it’s probably bootstrapping related?

[Bart Bogaerts]

Looks like it might be… But… I don’t really have a clue why things would go wrong here.

[Bart Bogaerts]

Dummy commit to removve spam issues

fixes #962 fixes #963 fixes #964 fixes #965 fixes #966 fixes #967 fixes #968 fixes #969 fixes #970 fixes #971 fixes #972 fixes #973 fixes #974 fixes #975 fixes #976

→ <<cset 672e55adb463>>