[Why3-club] inlining functions or explicit predicates

Claude Marche Claude.Marche at inria.fr
Fri Feb 15 17:08:33 CET 2019


Dear JJ,

As you remark, Why3 0.88 is now quite outdated and my answer may not be 
very accurate. As far as I remember, the former "Inline" button was 
applying the transformation "inline_goal" which has the effect of 
inlining the defined function symbols appearing in an outermost position 
in the goal.

The doc for the transformations are obtained when typing `why3 
--list-transforms', and some of them are documented in a bit more 
details in the manual : "inline_*" are documented at the beginning of 
http://why3.lri.fr/doc/technical.html#sec128

In Why3 1.x, the user interface for applying transformations is much 
more powerful, in your case you would probably want to type "unfold foo" 
where "foo" is your function symbol. The documentation is also visible 
interactively.

I don't know how to help more without seeing the exact example you have.

- Claude



Le 14/02/2019 à 16:20, Jean-Jacques Levy a écrit :
> Dear Why3 Friends,
> 
> is there any doc about the functionality of the  "Inline"  button in the Why3 IDE ?
> 
> Same for inline_all, inline_goal, inline_trivial..
> 
> My current problem is that the inlined version of a trivial function works with automatic provers, but I cannot find a way of forcing that inlining.
> 
> Many many thanks for you help!
> 
> -JJ-
> 
> ps/ I’m using old release 0.88.3 :-(
> _______________________________________________
> 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