[Why3-club] always inline a predicate

Andrei Paskevich andrei.paskevich at lri.fr
Thu Mar 7 17:22:20 CET 2019


On Thu, 7 Mar 2019 at 17:12, Jean-Christophe Filliatre <
Jean-Christophe.Filliatre at lri.fr> wrote:

> Dear Julia,
>
> There is a meta "inline:no" which can be used to indicate that a
> function/predicate *must not* be inlined (by inline_all or inline_goal).
> Use it like this
>
>   meta "inline:no" predicate foo
>
> Unless I'm mistaken, there is no way to indicate the opposite i.e. that
> a symbol must always be inlined.
>

We could add this functionality to "inline_trivial" (which is used in the
majority of provers' transformation chains), via an attribute attached to
the function/predicate symbol to force the inlining. In the IDE, however,
the symbol will not be inlined until the task is sent to a prover. To the
best of my knowledge, we do not have a transformation "inline this symbol
everywhere in the task", to do it easily in IDE. However, one could always
use "inline_trivial" from IDE to force inlining early.

Best,
Andrei


> On 3/3/19 8:18 AM, Julia Lawall wrote:
> > Hello,
> >
> > Is there an annotation that can be put in a .mlw to cause a predicate
> > always to be inlined?  Currently, I have to guess when inline_goal or
> > inline_all would be useful, and neither is really satisfactory, because I
> > don't want to inline everything, but just this one predicate.
> >
> > thanks,
> > julia
> > _______________________________________________
> > Why3-club mailing list
> > Why3-club at lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190307/505a46de/attachment.html>


More information about the Why3-club mailing list