[Why3-club] predicates

Andrei Paskevich andrei.paskevich at lri.fr
Mon Mar 25 15:47:18 CET 2019


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.

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
> >       >
> >       >
> >       >
> >
> >
> >
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190325/ee6bba6c/attachment.html>


More information about the Why3-club mailing list