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

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Thu Feb 23 09:50:55 CET 2012


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.

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.

Regarding Z3, CVC3, and Yices, it is more tricky, since we don't pass 
them triggers (and we don't even have a way to do it in some cases). As 
you see, Z3 is able to use the axiom anyway, but CVC3 and Yices don't.

-- 
Jean-Christophe
-------------- section suivante --------------
Un texte encapsul? et encod? dans un jeu de caract?res inconnu a ?t? nettoy?...
Nom : test-T-eval_case.why
URL : <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20120223/c94a4802/attachment.txt>


More information about the Why3-club mailing list