[Why3-club] Is this goal really (un)tractable ?

Frédéric Besson frederic.besson at inria.fr
Fri Feb 24 10:41:35 CET 2012


On 23 févr. 2012, at 09:50, Jean-Christophe Filliatre wrote:

> Hi Frédéric,
> 
> On 22/02/2012 16:48, Jean-Christophe Filliatre wrote:
>> On my machine, using the git version of Why3, your goal is proved in no
>> time (under 0.04s) by Alt-ergo 0.94, CVC3 2.2, Yices 1.0.25, and Z3 2.19.
> 
> Oups, I took another goal by accident; my mistake.
> 
> With the right one, only Z3 (2.19) proves it.
> 
> I attach the input file for Alt-ergo on that goal. The issue is axiom "value_inversion". Alt-ergo finds no appropriate trigger for it, so it simply discards it. Therefore it gives up immediately.
> 
> If you manually give "u" as a trigger for this axiom, that is
> 
>  axiom value_inversion :
>    (forall u:value [u].
>    ((u = Int(Int_proj_1(u))) or (u = Loc(Loc_proj_1(u)))))
> 
> then Alt-ergo easily proves it. I've CC'ed Sylvain.
Thanks for the hint. That's a step forward...

> Such an axiom is generated automatically by Why3, to encode the algebraic data type "value". So we should do something to add such a trigger automatically.
For efficiency, triggers seem to be instrumental but also a kind of dark art.

Btw, would it make sense to be able to annotate functions definitions with a trigger annotations ?
In my case, I know that certain arguments will be known in the goal and I would like to instruct the prover that it would be wise to symbolically unfold the function/predicate...

Anyway, I am sure I will come back with more questions :)

Thanks

--
Frédéric


More information about the Why3-club mailing list