[Why3-club] Is this goal really (un)tractable ?
Jean-Christophe.Filliatre at lri.fr
Wed Feb 22 16:48:57 CET 2012
> 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,
> 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
> goal eval_case : forall p p':pc, x:value.
> evalcond 1 x 4 = Some p' ->
> p' = 1 \/ p' = 4
> 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!
> Frédéric Besson
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
-------------- 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