[Why3-club] Is this goal really (un)tractable ?
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 :)
More information about the Why3-club