[Why3-club] Why3-club Digest, Vol 95, Issue 7

Claude Marche Claude.Marche at inria.fr
Fri Mar 29 17:06:38 CET 2019



Le 29/03/2019 à 14:56, Sandrine Blazy a écrit :
> Dear Claude,
> 
>> Le 15 nov. 2018 à 12:01, why3-club-request at lists.gforge.inria.fr 
>> <mailto:why3-club-request at lists.gforge.inria.fr> a écrit :
>>
>> Since Why3 1.0 we wanted to disencourage users to intentionally choose a
>> particular prover to discharge a goal. We want to encourage instead the
>> use of the shortcut "0" "1" and "2" that selects a "strategy" which will
>> try several provers.
>>
>> In essence, for begineers we suggest to try first "0", if it fails use
>> "s" to split, then "0" again on subgoals. Then on each specific unproved
>> subgoals, an option is to try "1" or "2 ».
> 
> Thanks for the advice; we asked our students to follow this strategy which
> worked very well until now.
> However, the proof window shows that  "s" calls the transformation
> split_vc, and strategy   « 1 » uses the transformation split_all_full.
> 
> What is the difference between both transformations, and when should I try
> to split again instead of using strategy 1 ? Indeed, on some examples,
> « 1 » followed by « 2 » does not help, but splitting again followed by 
> « 0 »
> is enough to prove the VCs.

Indded we would like the strategies "1" and "2" to use 'split_vc' 
instead of 'split_all_full'. there is already a ticket for that ...

https://gitlab.inria.fr/why3/why3/issues/282

split_all_full should be used only by advanced users.

- Claude


More information about the Why3-club mailing list