Predicate interpretations should be lua functions

[Bart Bogaerts]

Similar to how function interpretations are lua functions and can be called, so should predicate interpretations

(non-working example attached)

[Bart Bogaerts]

A problem with this is that we still would want .ct and .cf to work.

Maybe it would be better to have something like

S[V::P].value(3)

In that case, a predicate interpretation consists of ct table, cf table, pt table, pf table, and an extra lua function return true false or unknown...