[Why3-club] Is this goal really (un)tractable ?
Frédéric Besson
frederic.besson at inria.fr
Wed Feb 22 15:53:07 CET 2012
Hello,
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].
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
More information about the Why3-club
mailing list