0

我的配置文件包括不同证明者的替代条目。当我使用该证明者执行为什么 3 证明时，为什么 3 的输出是一条消息，通知我的配置文件中有多个具有给定名称的证明者，这些证明者的列表。

/home/xyz> why3 prove --prover Z3 afile.why
More than one prover in /home/xyz/.why3.conf correspond to "Z3":
Z3 (4.4.1), Z3 (4.4.1 noBV)

如果可能的话，我想知道如何在该证明者的特定替代方案上调用Why3。

4

1 回答 1

0

最终我偷看了Why3的源代码得到了答案。它可以在why3/src/driver/whyconf.mli 和why3/src/driver/whyconf.ml 中找到。

一种解决方案是在Why3 的​​配置文件中使用证明者条目的版本和替代字段。例如，如果此文件包含 Z3 的以下两个条目：

[prover]
alternative = "noBV"
command = "%l/why3-cpulimit %t %m -s z3 -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%l/why3-cpulimit %U %m -s z3 -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
driver = "/home/ddeharbe/.opam/system/share/why3/drivers/z3_432.drv"
editor = ""
in_place = false
interactive = false
name = "Z3"
version = "4.4.1"

[prover]
command = "%l/why3-cpulimit %t %m -s z3 -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
command_steps = "%l/why3-cpulimit %U %m -s z3 -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 memory_max_alloc_count=%S %f"
driver = "/home/ddeharbe/.opam/system/share/why3/drivers/z3_440.drv"
editor = ""
in_place = false
interactive = false
name = "Z3"
shortcut = "z3"
version = "4.4.1"

“替代”字段在条目之间有所不同。所以要调用第一个条目，命令是：

why3 prove afile.why --prover Z3,4.4.1,

要调用第二个条目，命令是：

why3 prove afile.why --prover Z3,4.4.1,noBV
于 2017-07-04T06:13:21.027 回答