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

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Wed Feb 22 16:48:57 CET 2012


Hi Frédéric,

> I am trying to prove simple properties about an interpreter of a simple language.
> My goals, which (to me) are straightforward, are not discharged by provers [alt-ergo, cvc3,eprover,vampire,yices].

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.

Could you please run the following command

	why3 -P alt-ergo your-file -o tmp/

to get the input file for Alt-ergo generated by Why3?
(Alternatively, you can do that in why3ide using the "Edit" button on 
the line corresponding to the call to Alt-Ergo.)

Mine is attached. It indeed contains a trivial goal. Let's compare the 
two files. I can do that if you send me your file.

Hope this will help,
--
Jean-Christophe



> This is the case for the following simplistic theory.
>
> Theory T
>   use import int.Int
>   use import option.Option
>
> type location
> type value = Int int | Loc location
> type pc = int
>
> function evalcond (p:pc)  (x:value) (jmp:pc) : option pc =
>       match x with
>        | Loc _ ->  None
>        | Int i ->  if i>= 0 then Some p else Some jmp
>      end
>
> goal eval_case : forall p p':pc, x:value.
>     evalcond 1  x 4 = Some p' ->
>     p' = 1 \/ p' = 4
>
> end
>
> Could you tell me what I am doing wrong ?
> This is so simple, I almost suspect a bug...
>
> Actually, I also have a non-monotonicity problem.
> * Provers do not discharge my initial problem
> * Provers do discharge a cut-down version [alt-ergo.cvc3]
> * Provers do not discharge the previous minimal goal
>
> Are there known tricks to minimize the source of such erratic behaviors ?
> Are there ways to provide hints to the provers.
> For instance, is there a way to instruct the prover to
> * recursively inline certain definitions (something like the simpl Coq tactic)
> * when it is done, do a case analysis over the match statements
>
> A that point, the previous goal is quantifier-free and falls in a decidable fragment...
>
> I almost lost faith in those provers :(
> Any insight would be much appreciated!
>
> Best,
>
> --
> Frédéric Besson
>
>
>
>
>
>
>
>
>
>
>
>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club


-------------- section suivante --------------
Un texte encapsul? et encod? dans un jeu de caract?res inconnu a ?t? nettoy?...
Nom : goal.why
URL : <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20120222/cc7070c6/attachment.txt>


More information about the Why3-club mailing list