[Why3-club] strategy definitions in the config file

Julia Lawall julia.lawall at lip6.fr
Mon Mar 18 13:39:06 CET 2019



On Mon, 18 Mar 2019, Claude Marche wrote:

>
> Sorry for the late answer.
>
> Please look at the manual http://why3.lri.fr/doc/technical.html#sec137
> for a description of the language of proof strategies.
>
> As shown by Mario's answer, the "t" instruction requires both a
> transformation name and a label. You did not give any label. The
> newlines are not significant so in your case the "c" on the next line is
> taken as the label, and then the next token "Alt-Ergo,2.0" is not
> understood as a command, which can be only c, p, t or a label.

Thanks for the explanation and the pointer to the relevant section of the
manual.

julia

>
> - Claude
>
> Le 16/03/2019 à 09:17, Julia Lawall a écrit :
> > Often I do split_vc and the alt-ergo.  How would I define such a strategy
> > in the configuration file?
> >
> > I tried:
> >
> > [strategy]
> > code = "start:
> > t split_all_full
> > c Alt-Ergo,2.0 40 10000
> >
> > But it says "Fatal: loading strategy 'Auto_level_1' failed: syntax error
> > on character 'A' at position 26"
> >
> > I see examples with Eprover where the value in the name keyval pair is
> > used to name the prover.  Alt-Ergo has Alt-Ergo in this line, but it
> > doesn't work.
> >
> > thanks,
> > julia
> > _______________________________________________
> > Why3-club mailing list
> > Why3-club at lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >
> _______________________________________________
> 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