Maketrue/false/unknown do not check arity

[Broes De Cat]

Resulting in a segfault if the arity is wrong.

[Ingmar Dasseville]

An error is thrown in the PredInter::moveTupleFromTo function which is called from maketrue/false/unknown

[Broes De Cat]

Please test properly ;) An error is thrown if the code gets to moveFrom..., but it can crash earlier.

[Ingmar Dasseville]

I cannot reproduce the issue, it works when I test with this:

// c++
vocabulary V{
    type Large isa nat
    Z : Large
    P(Large)
}

structure S:V{
    Large={1..10}
}

theory T:V{
}


include <mx>
procedure main(){
    maketrue(S[V::P],{}) --throws error
    maketrue(S[V::Z].graph,{1,2}) --throws error
}

[Broes De Cat]

MakeTrueAtLeast and makeFalseAtLeast call istrue/isfalse, which I think will crash. They are called, e.g., when adding to a function interpretation directly.

[Ingmar Dasseville]

these are not available publicly, so an Assert should suffice?

[Broes De Cat]

I looked up my mails.

The issue was created because a call

makefalse(S[goal::I_XCoor].graph,{5,4})

segfaulted, where I_XCoor has arity 2.

As far as I can see, the relevant c++ code predates the issue, so I expected it to still hold (but did not check).

[Ingmar Dasseville]

ingmar@forty-two ~/b/idpRelease> idp /tmp/rommel.idp 
Warning: Verifying and/or autocompleting structure S
Error: Adding a tuple of size 2 to a predicate with arity 1

vocabulary goal {
    type XCo isa nat
    I_XCoor : XCo
}

theory T : goal{

}

structure S : goal{
    XCo = {1..10}
}

procedure main(){
    makefalse(S[goal::I_XCoor].graph,{5,4})
    print(S)
}

I know the behaviour of makefalse has changed at some point from makefalse -> makefalseExactly. Maybe that caused it to solve the issue

[Broes De Cat]

mm, okay then :)