Как позвонить Why3 из командной строки, чтобы получить доступ к проверщику с альтернативами?

Question

Мой конфигурационный файл содержит альтернативные записи для разных пруверов. Когда я выполняю подтверждение Why3 с этим проверяющим устройством, выводом Why3 является сообщение о том, что у меня в файле конфигурации более одного проверяющего с заданным именем, список этих проверяющих.

/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 на конкретной альтернативе этого средства проверки, если это возможно.

Answer 1

В конце концов я заглянул в исходный код 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