“未知逻辑符号map.Map.const”消息在Why3中

Question

我正在通过跟踪why3来试验他们的教程，但是我得到了多个验证器的消息Unknown logical symbol map.Map.const。以下是我试图证明的理论的内容：

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

以下是各种证明文件的结果：

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

这是我的why3版本信息：

▶ why3 --version
Why3 platform, version -n 0.85+git (build date: Tue Mar 10 08:27:47 EDT 2015)

错误消息中提到的.drv文件上的时间戳与我的why3可执行文件上的时间戳匹配。

我的理论和装置有什么问题吗？

编辑以添加:在本教程中，它说要使用why3 demo_logic.why来证明这个理论，但是当我尝试得到这个结果时：

▶ why3 demo_logic.why             
'demo_logic.why' is not a Why3 command.

如果我只是做了why3 prove demo_logic.why，结果只是(大约)一个理论的呼应：

▶ 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

Answer 1

您是否安装了以前版本的why3？在执行验证程序时经常会出现问题，原因是使用旧why3的配置文件创建了新的why3。我见过你的特别例子是这样的

rm ~/.why3.conf
why3 config --detect