Commit 5f6dc23b authored by MARCHE Claude's avatar MARCHE Claude

detection of multiple versions of Z3, CVC3 and Alt-Ergo

parent 3b2c1733
[ATP alt-ergo-0.93.1]
name = "Alt-Ergo"
exec = "alt-ergo-0.93.1"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_ok = "0.93.1"
version_bad = "0.93"
version_bad = "0.92.3"
version_bad = "0.92.2"
version_bad = "0.92.1"
version_bad = "0.92"
version_bad = "0.91"
version_bad = "0.9"
version_bad = "0.8"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
driver = "drivers/alt_ergo_trunk.drv"
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
version_switch = "-version"
version_regexp = "\\([0-9.]+\\)"
version_ok = "0.93.1"
version_ok = "0.93"
version_bad = "0.92.3"
version_bad = "0.92.2"
......@@ -31,9 +47,9 @@ version_old = "0.8"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
driver = "drivers/alt_ergo.drv"
[ATP cvc3]
[ATP cvc3-2.4]
name = "CVC3"
exec = "cvc3"
exec = "cvc3-2.4.1"
version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
version_ok = "2.4.1"
......@@ -141,9 +157,9 @@ command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
driver = "drivers/verit.drv"
[ATP z3]
[ATP z3-3]
name = "Z3"
exec = "z3"
exec = "z3-3.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "3.2"
......@@ -165,7 +181,7 @@ name = "Z3"
exec = "z3"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_old = "2.19"
version_ok = "2.19"
version_old = "2.18"
version_old = "2.17"
version_old = "2.16"
......
......@@ -177,12 +177,25 @@ let detect_prover main acc l =
try
let detect_execs data =
try Some (Util.list_first (detect_exec main data) data.execs)
with Not_found -> None in
with Not_found -> None
in
let prover = Util.list_first detect_execs l in
Mstr.add prover_id prover acc
with Not_found ->
eprintf "Prover %s not found.@." prover_id;
acc
(* does not work
List.fold_left
(fun acc data ->
List.fold_left
(fun acc e ->
eprintf "Trying executable %s@." e;
match detect_exec main data e with
| None -> acc
| Some prover -> Mstr.add prover_id prover acc)
acc data.execs)
acc l
*)
let run_auto_detection config =
let main = get_main config in
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment