julia.lawall at lip6.fr
Mon Mar 25 10:35:32 CET 2019
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?
> 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.
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
More information about the Why3-club