I'm experimenting with why3 by following their tutorial, but I get the message Unknown logical symbol map.Map.const for multiple provers. Here are the contents of the theory I'm trying to prove:
theory List
type list 'a = Nil | Cons 'a (list 'a)
predicate mem(x: 'a) (l: list 'a) = match l with
| Nil -> false
| Cons y r -> x = y || mem x r
end
goal G1: mem 2 (Cons 1 (Cons 2 (Cons 3 Nil)))
end
Here are the results of a variety of provers:
z3:
▶ why3 prove -P z3 demo_logic.why
File "/usr/local/share/why3/drivers/z3_bare.drv", line 172, characters 36-41:
Unknown logical symbol map.Map.const
cvc4:
▶ why3 prove -P cvc4 demo_logic.why
File "/usr/local/share/why3/drivers/cvc4_bare.drv", line 180, characters 36-41:
Unknown logical symbol map.Map.const
pvs:
▶ why3 prove -P pvs demo_logic.why
File "/usr/local/share/why3/drivers/pvs-common.gen", line 41, characters 18-23:
Unknown logical symbol map.Map.const
This is my why3 version information:
▶ why3 --version
Why3 platform, version -n 0.85+git (build date: Tue Mar 10 08:27:47 EDT 2015)
The timestamps on the .drv files mentioned in the error messages match the timestamp on my why3 executable.
Is there something wrong with my theory or my installation?
Edit to add: In the tutorial itself it says to use why3 demo_logic.why to prove the theory, but when I try that I get this result:
▶ why3 demo_logic.why
'demo_logic.why' is not a Why3 command.
If instead I just do why3 prove demo_logic.why, the result is just (approximately) an echo of the theory:
▶ why3 prove demo_logic.why
theory List
(* use why3.BuiltIn.BuiltIn *)
type list 'a =
| Nil
| Cons 'a (list 'a)
predicate mem (x:'a) (l:list 'a) =
match l with
| Nil -> false
| Cons y r -> x = y || mem x r
end
goal G1 : mem 2 (Cons 1 (Cons 2 (Cons 3 (Nil:list int))))
end
Do you installed a previous version of why3? Problems in the execution of provers are often due to a new why3 using a configuration file of an old why3. And I have seen your particular instance fixed by this:
rm ~/.why3.conf
why3 config --detect