[Why3-club] predicates

Julia Lawall julia.lawall at lip6.fr
Mon Mar 25 15:50:33 CET 2019



On Mon, 25 Mar 2019, Andrei Paskevich wrote:

> Commited in 5e93e6d7 in master. You can put the attribute [@inline:trivial] over the predicate symbol (right after the name) or over its definition (right before the formula). The symbol will be inlined automatically for the majority
> of the automated provers via their drivers. Alternatively, you can call apply "inline_trivial" in the IDE to force the inlining during the interactive phase.

Great!  Thanks so much for taking care of it quickly.

julia

>
> Best,
> Andrei
>
> On Mon, 25 Mar 2019 at 10:43, Julia Lawall <julia.lawall at lip6.fr> wrote:
>       On Mon, 25 Mar 2019, Andrei Paskevich wrote:
>
>       > The change in the master branch I can do today, if you are okay with using a development version.
>
>       That would be wonderful.  I would be much better than rewriting all of my
>       predicates :)
>
>       Thanks very much.
>       julia
>
>       >
>       > Best,
>       > Andrei
>       >
>       > On Mon, 25 Mar 2019 at 10:35, Julia Lawall <julia.lawall at lip6.fr> wrote:
>       >
>       >
>       >       On Mon, 25 Mar 2019, Andrei Paskevich wrote:
>       >
>       >       > Hi Julia,
>       >       >
>       >       > would it help to label such predicates explicitly in order to always inline them when passing the task to a prover (as you suggested in an earlier mail)? I am inclined to add this functionality to the
>       "inline_trivial"
>       >       transformation.
>       >       > One downside of this is that the predicate is not inlined while you are in the interactive phase, so, for example, "split_goal" will not work on it, unless you call inline on it.
>       >
>       >       I would be completely happy to label the predicates with inline.  I know
>       >       up front that they only exist to collect information and reduce code size.
>       >       The split_goal limitation is not a problem.
>       >
>       >       Could this be done quickly, or would it have to wait for the next release?
>       >
>       >       Thanks,
>       >       julia
>       >
>       >       >
>       >       > Best,
>       >       > Andrei
>       >       >
>       >       > On Mon, 25 Mar 2019 at 08:57, Julia Lawall <julia.lawall at lip6.fr> wrote:
>       >       >       My natural inclination is to make predicates that combine other
>       >       >       predicates, in order to avoid massive code duplication.  But it seems that
>       >       >       doing so makes it very hard for why3 to find the information it needs.  So
>       >       >       to get the proof to go through, I have to manually inline the predicates,
>       >       >       which clutters the code and is quite unsatisfying.
>       >       >
>       >       >       These predicates are not in the goal, but rather in the hypotheses, eg in
>       >       >       the ensures of a function I am calling.  Inline goal is thus of no use,
>       >       >       and Inline all inlines far too much, and seems to make it impossible to
>       >       >       get the proof to go through for other reasons.
>       >       >
>       >       >       Is there some intuition about when it is possible to define predicates
>       >       >       that wrap other predicates and when it is not?  Is there some level of
>       >       >       nesting that one should not exceed, or is there a distinction between
>       >       >       predicates defined in the current module or some other module?
>       >       >
>       >       >       I have tried meta rewrite_def predicate XXX but it doesn't seem to give
>       >       >       much benefit.
>       >       >
>       >       >       thanks,
>       >       >       julia
>       >       >       _______________________________________________
>       >       >       Why3-club mailing list
>       >       >       Why3-club at lists.gforge.inria.fr
>       >       >       https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>       >       >
>       >       >
>       >       >
>       >
>       >
>       >
>
>
>


More information about the Why3-club mailing list