Commit c2ef95ac authored by Andrei Paskevich's avatar Andrei Paskevich

Call_provers: set on_timelimit to true if why3cpulimit is used

also, drop command-line tags %T and %U which were only used
with why3cpulimit and never as an actual prover parameter.
parent 4035a124
......@@ -220,9 +220,6 @@ exec = "metis"
version_switch = "-v"
version_regexp = "metis \\([^ \n,]+\\)"
version_ok = "2.3"
# %U means 2*timelimit+1. Required because Metis tends to
# react very slowly to the time limit given, hence answers
# oscillate between Timeout and Unknown
command = "%e --time-limit %t %f"
driver = "drivers/metis.drv"
......
......@@ -236,8 +236,7 @@ let parse_prover_run res_parser time out ret on_timelimit limit ~printer_mapping
let ans = match ans, limit with
| (Unknown _ | HighFailure), { limit_time = Some tlimit }
when on_timelimit && time >= (0.9 *. float tlimit) -> Timeout
| _ -> ans
in
| _ -> ans in
let model = res_parser.prp_model_parser out printer_mapping in
Debug.dprintf debug "Call_provers: model:@.";
debug_print_model model;
......@@ -253,8 +252,6 @@ let actualcommand command ~use_why3cpulimit limit interactive file =
let timelimit = get_time limit in
let memlimit = get_mem limit in
let steplimit = get_steps limit in
let utime = string_of_int (2 * timelimit + 1) in
let ttime = string_of_int (succ timelimit) in
let stime = string_of_int timelimit in
let smem = string_of_int memlimit in
let arglist = Cmdline.cmdline_split command in
......@@ -264,9 +261,7 @@ let actualcommand command ~use_why3cpulimit limit interactive file =
let replace s = match Str.matched_group 1 s with
| "%" -> "%"
| "f" -> use_stdin := false; file
| "t" -> on_timelimit := true; string_of_int timelimit
| "T" -> ttime
| "U" -> utime
| "t" -> on_timelimit := true; stime
| "m" -> smem
(* FIXME: libdir and datadir can be changed in the configuration file
Should we pass them as additional arguments? Or would it be better
......@@ -284,11 +279,12 @@ let actualcommand command ~use_why3cpulimit limit interactive file =
let cpulimit_bin = Filename.concat Config.libdir "why3-cpulimit" in
let cpulimit_time =
(* for steps limit use 2 * t + 1 time *)
if limit.limit_steps <> None then utime
if limit.limit_steps <> None then string_of_int (2 * timelimit + 1)
(* if prover implements time limit, use t + 1 *)
else if !on_timelimit then ttime
else if !on_timelimit then string_of_int (succ timelimit)
(* otherwise use t *)
else stime in
on_timelimit := true;
cpulimit_bin :: cpulimit_time :: smem :: "-s" :: args
else
args 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