Skip to content

GitLab

why3
why3
Commit c364ad1a authored by Johannes Kanig's avatar Johannes Kanig
Browse files
Options

simplify limits objects to not use option types anymore

parent 88ce0c36
Hide whitespace changes
Inline Side-by-side
Showing with 84 additions and 102 deletions
examples/use_api/create_session.ml
View file @ c364ad1a
......@@ -92,9 +92,9 @@ let add_proofs_attempts g =
~keygen:dummy_keygen
~obsolete:true
~archived:false
~limit:{Call_provers.limit_time = Some 5;
limit_steps = None;
limit_mem = Some 1000 }
~limit:{Call_provers.empty_limit with
Call_provers.limit_time = 5;
limit_mem = 1000 }
~edit:None
g p.Whyconf.prover Session.Scheduled
in ())
......
examples/use_api/logic.ml
View file @ c364ad1a
......@@ -105,9 +105,7 @@ let () = printf "@[On task 1, alt-ergo answers %a@."
let result2 : Call_provers.prover_result =
Call_provers.wait_on_call
(Driver.prove_task ~command:alt_ergo.Whyconf.command
~limit:{Call_provers.limit_time = Some 10;
limit_mem = None ;
limit_steps = None}
~limit:{Call_provers.empty_limit with Call_provers.limit_time = 10}
alt_ergo_driver task2 ()) ()
let () = printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
......
src/coq-tactic/why3tac.ml4
View file @ c364ad1a
......@@ -1307,9 +1307,7 @@ let why3tac ?(timelimit=timelimit) s gl =
if debug then Format.printf "@[%a@]@\n---@." Pretty.print_task !task;
if debug then Format.printf "@[%a@]@\n---@." (Driver.print_task drv) !task;
let limit =
{ Call_provers.limit_time = Some timelimit;
limit_mem = None;
limit_steps = None } in
{ Call_provers.empty_limit with Call_provers.limit_time = timelimit } in
let call = Driver.prove_task ~command ~limit drv !task () in
wait_on_call call ()
with
......
src/driver/call_provers.ml
View file @ c364ad1a
......@@ -41,28 +41,19 @@ type prover_result = {
type resource_limit =
{
limit_time : int option;
limit_mem : int option;
limit_steps : int option;
limit_time : int;
limit_mem : int;
limit_steps : int;
}
let empty_limit =
{ limit_time = None ; limit_mem = None; limit_steps = None }
let empty_limit = { limit_time = 0 ; limit_mem = 0; limit_steps = 0 }
let get_time x = Opt.get_def 0 x.limit_time
let get_mem x = Opt.get_def 0 x.limit_mem
let get_steps x = Opt.get_def 0 x.limit_steps
let mk_limit t m s =
{ limit_time = if t = 0 then None else Some t;
limit_mem = if m = 0 then None else Some m;
limit_steps = if s = 0 then None else Some s
}
let limit_max a b =
mk_limit (max (get_time a) (get_time b))
(max (get_mem a) (get_mem b))
(max (get_steps a) (get_steps b))
let limit_max =
let single_limit_max a b = if a = 0 || b = 0 then 0 else max a b in
fun a b ->
{ limit_time = single_limit_max a.limit_time b.limit_time;
limit_steps = single_limit_max a.limit_steps b.limit_steps;
limit_mem = single_limit_max a.limit_mem b.limit_mem; }
type timeunit =
| Hour
......@@ -225,7 +216,7 @@ let parse_prover_run res_parser time out ret limit ~printer_mapping =
| Unknown (s, _) -> Unknown (s, Some reason_unknown)
| _ -> ans in
let ans = match ans, limit with
| (Unknown _ | HighFailure), { limit_time = Some tlimit }
| (Unknown _ | HighFailure), { limit_time = tlimit }
when time >= (0.9 *. float tlimit) -> Timeout
| _ -> ans in
let model = res_parser.prp_model_parser out printer_mapping in
......@@ -240,11 +231,8 @@ let parse_prover_run res_parser time out ret limit ~printer_mapping =
}
let actualcommand command limit file =
let timelimit = get_time limit in
let memlimit = get_mem limit in
let steplimit = get_steps limit in
let stime = string_of_int timelimit in
let smem = string_of_int memlimit in
let stime = string_of_int limit.limit_time in
let smem = string_of_int limit.limit_mem in
let arglist = Cmdline.cmdline_split command in
let use_stdin = ref true in
let on_timelimit = ref false in
......@@ -259,7 +247,7 @@ let actualcommand command limit file =
to prepare the command line in a separate function? *)
| "l" -> Config.libdir
| "d" -> Config.datadir
| "S" -> string_of_int steplimit
| "S" -> string_of_int limit.limit_steps
| _ -> failwith "unknown specifier, use %%, %f, %t, %T, %U, %m, %l, %d or %S"
in
let args =
......@@ -275,15 +263,14 @@ let actualcommand ~cleanup ~inplace command limit file =
raise e
let adapt_limits limit on_timelimit =
let new_time_limit =
let timelimit = get_time limit in
{ limit with limit_time =
(* for steps limit use 2 * t + 1 time *)
if limit.limit_steps <> None then (2 * timelimit + 1)
if limit.limit_steps <> empty_limit.limit_steps
then (2 * limit.limit_time + 1)
(* if prover implements time limit, use t + 1 *)
else if on_timelimit then succ timelimit
else if on_timelimit then succ limit.limit_time
(* otherwise use t *)
else timelimit in
{ limit with limit_time = Some new_time_limit }
else limit.limit_time }
let set_socket_name =
Prove_client.set_socket_name
......@@ -357,10 +344,11 @@ let call_on_file ~command ~limit ~res_parser ~printer_mapping
res_parser = res_parser;
printer_mapping = printer_mapping } in
Hashtbl.add saved_data id save;
let timelimit = get_time limit in
let memlimit = get_mem limit in
let use_stdin = if use_stdin then Some fin else None in
Prove_client.send_request ~use_stdin ~id ~timelimit ~memlimit ~cmd;
Prove_client.send_request ~use_stdin ~id
~timelimit:limit.limit_time
~memlimit:limit.limit_mem
~cmd;
ServerCall id
let get_new_results ~blocking =
......
src/driver/call_provers.mli
View file @ c364ad1a
......@@ -120,31 +120,22 @@ type post_prover_call = unit -> prover_result
type resource_limit =
{
limit_time : int option;
limit_mem : int option;
limit_steps : int option;
limit_time : int;
limit_mem : int;
limit_steps : int;
}
(* represents the three ways a prover run can be limited: in time, memory
and/or steps *)
val empty_limit : resource_limit
(* the limit object which imposes no limits *)
(* the limit object which imposes no limits. Use this object to impose no
limits, but also to know if some concrete time, steps or memlimit actually
means "no limit" *)
val limit_max : resource_limit -> resource_limit -> resource_limit
(* return the limit object whose components represent the maximum of the
corresponding components of the arguments *)
val get_time : resource_limit -> int
(* return time, return default value 0 if not set *)
val get_mem : resource_limit -> int
(* return time, return default value 0 if not set *)
val get_steps : resource_limit -> int
(* return time, return default value 0 if not set *)
val mk_limit : int -> int -> int -> resource_limit
(* build a limit object, transforming the default values into None on the fly
*)
val call_editor : command : string -> string -> pre_prover_call
val call_on_file :
......
src/ide/gmain.ml
View file @ c364ad1a
......@@ -490,7 +490,7 @@ let set_proof_state a =
let s =
if gconfig.show_time_limit then
Format.sprintf "%.2f [%d.0]" time
(Call_provers.get_time a.S.proof_limit)
(a.S.proof_limit.Call_provers.limit_time)
else
Format.sprintf "%.2f" time
in
......@@ -504,8 +504,8 @@ let set_proof_state a =
| S.Interrupted -> "(interrupted)"
| S.Scheduled | S.Running ->
Format.sprintf "[limit=%d sec., %d M]"
(Call_provers.get_time a.S.proof_limit)
(Call_provers.get_mem a.S.proof_limit)
(a.S.proof_limit.Call_provers.limit_time)
(a.S.proof_limit.Call_provers.limit_mem)
in
let t = if obsolete then t ^ " (obsolete)" else t in
(* TODO find a better way to signal archived row *)
......@@ -1019,9 +1019,9 @@ let prover_on_selected_goals pr =
(env_session()) sched
~context_unproved_goals_only:!context_unproved_goals_only
~cntexample
~limit:{Call_provers.limit_time = Some timelimit;
limit_mem = Some memlimit;
limit_steps = None}
~limit:{Call_provers.empty_limit with
Call_provers.limit_time = timelimit;
limit_mem = memlimit }
pr a
with e ->
eprintf "@[Exception raised while running a prover:@ %a@.@]"
......@@ -1136,9 +1136,9 @@ let bisect_proof_attempt pa =
assert (not lp.S.prover_config.C.in_place); (* TODO do this case *)
M.schedule_proof_attempt
~cntexample
~limit:{Call_provers.limit_time = Some !timelimit;
limit_mem = pa.S.proof_limit.Call_provers.limit_mem;
limit_steps = None}
~limit:{Call_provers.empty_limit with
Call_provers.limit_time = !timelimit;
limit_mem = pa.S.proof_limit.Call_provers.limit_mem }
?old:(S.get_edited_as_abs eS.S.session pa)
(* It is dangerous, isn't it? to be in place for bisecting? *)
~inplace:lp.S.prover_config.C.in_place
......@@ -1176,8 +1176,9 @@ let bisect_proof_attempt pa =
M.schedule_proof_attempt
~cntexample
~limit:{pa.S.proof_limit with
Call_provers.limit_steps = None;
limit_time = Some !timelimit}
Call_provers.limit_steps =
Call_provers.empty_limit.Call_provers.limit_steps;
limit_time = !timelimit}
?old:(S.get_edited_as_abs eS.S.session pa)
~inplace:lp.S.prover_config.C.in_place
~command:(C.get_complete_command lp.S.prover_config
......
src/session/session.ml
View file @ c364ad1a
......@@ -496,9 +496,9 @@ let get_used_provers_with_stats session =
PHprover.add prover_table prover x;
x
in
let lim_time = Call_provers.get_time pa.proof_limit in
let lim_mem = Call_provers.get_mem pa.proof_limit in
let lim_steps = Call_provers.get_steps pa.proof_limit in
let lim_time = pa.proof_limit.Call_provers.limit_time in
let lim_mem = pa.proof_limit.Call_provers.limit_mem in
let lim_steps = pa.proof_limit.Call_provers.limit_steps in
let tf = try Hashtbl.find timelimits lim_time with Not_found -> 0 in
let sf = try Hashtbl.find steplimits lim_steps with Not_found -> 0 in
let mf = try Hashtbl.find memlimits lim_mem with Not_found -> 0 in
......@@ -580,9 +580,9 @@ let save_proof_attempt fmt ((id,tl,sl,ml),a) =
fprintf fmt
"@\n@[<h><proof@ prover=\"%i\"%a%a%a%a%a%a>"
id
(save_int_def "timelimit" tl) (Call_provers.get_time a.proof_limit)
(save_int_def "steplimit" sl) (Call_provers.get_steps a.proof_limit)
(save_int_def "memlimit" ml) (Call_provers.get_mem a.proof_limit)
(save_int_def "timelimit" tl) (a.proof_limit.Call_provers.limit_time)
(save_int_def "steplimit" sl) (a.proof_limit.Call_provers.limit_steps)
(save_int_def "memlimit" ml) (a.proof_limit.Call_provers.limit_mem)
(opt_string "edited") a.proof_edited_as
(save_bool_def "obsolete" false) a.proof_obsolete
(save_bool_def "archived" false) a.proof_archived;
......@@ -987,10 +987,10 @@ let set_edited_as edited_as a = a.proof_edited_as <- edited_as
let set_timelimit timelimit a =
a.proof_limit <-
{ a.proof_limit with Call_provers.limit_time = Some timelimit}
{ a.proof_limit with Call_provers.limit_time = timelimit}
let set_memlimit memlimit a =
a.proof_limit <-
{ a.proof_limit with Call_provers.limit_mem = Some memlimit}
{ a.proof_limit with Call_provers.limit_mem = memlimit}
let set_obsolete ?(notify=notify) a =
a.proof_obsolete <- true;
......@@ -1293,7 +1293,9 @@ and load_proof_or_transf ctxt mg a =
let timelimit = int_attribute_def "timelimit" a timelimit in
let steplimit = int_attribute_def "steplimit" a steplimit in
let memlimit = int_attribute_def "memlimit" a memlimit in
let limit = Call_provers.mk_limit timelimit memlimit steplimit in
let limit = { Call_provers.limit_time = timelimit;
Call_provers.limit_mem = memlimit;
Call_provers.limit_steps = steplimit } in
(*
if timelimit < 0 then begin
eprintf "[Error] incorrect or unspecified timelimit '%i'@."
......@@ -2039,9 +2041,9 @@ let print_external_proof fmt p =
fprintf fmt "%a - %a (%i, %i, %i)%s%s%s"
Whyconf.print_prover p.proof_prover
print_attempt_status p.proof_state
(Call_provers.get_time p.proof_limit)
(Call_provers.get_steps p.proof_limit)
(Call_provers.get_mem p.proof_limit)
(p.proof_limit.Call_provers.limit_time)
(p.proof_limit.Call_provers.limit_steps)
(p.proof_limit.Call_provers.limit_mem)
(if p.proof_obsolete then " obsolete" else "")
(if p.proof_archived then " archived" else "")
(if p.proof_edited_as <> None then " edited" else "")
......
src/session/session_scheduler.ml
View file @ c364ad1a
......@@ -395,8 +395,8 @@ let find_prover eS a =
to the time or mem limits, we adapt these limits when we replay a
proof *)
let adapt_limits ~use_steps a =
let timelimit = (Call_provers.get_time a.proof_limit) in
let memlimit = (Call_provers.get_mem a.proof_limit) in
let timelimit = (a.proof_limit.Call_provers.limit_time) in
let memlimit = (a.proof_limit.Call_provers.limit_mem) in
match a.proof_state with
| Done { Call_provers.pr_answer = r;
Call_provers.pr_time = t;
......@@ -431,7 +431,7 @@ let adapt_limits ~use_steps a =
let adapt_limits ~use_steps a =
let t, m, s = adapt_limits ~use_steps a in
Call_provers.mk_limit t m s
{ Call_provers.limit_time = t; limit_mem = m; limit_steps = s }
type run_external_status =
| Starting
......@@ -472,7 +472,8 @@ let run_external_proof_v3 ~use_steps eS eT a ?(cntexample=false) callback =
let inplace = npc.prover_config.Whyconf.in_place in
let command =
Whyconf.get_complete_command npc.prover_config
~with_steps:(limit.Call_provers.limit_steps <> None) in
~with_steps:(limit.Call_provers.limit_steps <>
Call_provers.empty_limit.Call_provers.limit_steps) in
let cb result =
let result = fuzzy_proof_time result previous_result in
callback a ap limit
......@@ -548,8 +549,8 @@ let prover_on_goal eS eT ?callback ?(cntexample=false) ~limit p g =
let a =
try
let a = PHprover.find g.goal_external_proofs p in
set_timelimit (Call_provers.get_time limit) a;
set_memlimit (Call_provers.get_mem limit) a;
set_timelimit (limit.Call_provers.limit_time) a;
set_memlimit (limit.Call_provers.limit_mem) a;
a
with Not_found ->
let ep = add_external_proof ~keygen:O.create ~obsolete:false
......@@ -953,7 +954,9 @@ let convert_unknown_prover =
(* should not happen *)
assert false
in
let limit = Call_provers.mk_limit timelimit memlimit (-1) in
let limit = { Call_provers.empty_limit with
Call_provers.limit_time = timelimit;
limit_mem = memlimit} in
prover_on_goal es sched ~callback ~limit p g
| Itransform(trname,pcsuccess) ->
let callback ntr =
......
src/tools/why3prove.ml
View file @ c364ad1a
......@@ -278,9 +278,9 @@ let output_theory drv fname _tname th task dir =
let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
let limit =
{ Call_provers.limit_time = Some timelimit;
limit_mem = Some memlimit;
limit_steps = None } in
{ Call_provers.empty_limit with
Call_provers.limit_time = timelimit;
limit_mem = memlimit } in
match !opt_output, !opt_command with
| None, Some command ->
let call =
......
src/tools/why3replay.ml
View file @ c364ad1a
......@@ -252,16 +252,17 @@ let print_report (g,p,l,r) =
| M.Result(new_res,old_res) ->
(* begin match !opt_smoke with *)
(* | Session.SD_None -> *)
let t = Call_provers.get_time l in
let m = Call_provers.get_mem l in
let s = Call_provers.get_steps l in
printf "%a instead of %a (timelimit=%d, memlimit=%d, steplimit=%d)@."
print_result new_res print_result old_res t m s
print_result new_res print_result old_res
l.Call_provers.limit_time
l.Call_provers.limit_mem
l.Call_provers.limit_steps
(* | _ -> *)
(* printf "Smoke detected!!!@." *)
(* end *)
| M.No_former_result new_res ->
printf "no former result available, new result is: %a@." print_result new_res
printf "no former result available, new result is: %a@."
print_result new_res
| M.CallFailed msg ->
printf "internal failure '%a'@." Exn_printer.exn_printer msg;
| M.Edited_file_absent f ->
......@@ -400,7 +401,7 @@ let run_as_bench env_session =
eprintf " done.@.";
exit 0
in
let limit = Call_provers.mk_limit 2 0 0 in
let limit = { Call_provers.empty_limit with Call_provers.limit_time = 2} in
M.play_all env_session sched ~callback ~limit provers;
main_loop ();
eprintf "main replayer (in bench mode) exited unexpectedly@.";
......
src/why3session/why3session_html.ml
View file @ c364ad1a
......@@ -133,10 +133,10 @@ let print_results fmt provers proofs =
fprintf fmt "FF0000\">Invalid"
| Call_provers.Timeout ->
fprintf fmt "FF8000\">Timeout (%ds)"
(Call_provers.get_time pr.S.proof_limit)
pr.S.proof_limit.Call_provers.limit_time
| Call_provers.OutOfMemory ->
fprintf fmt "FF8000\">Out Of Memory (%dM)"
(Call_provers.get_time pr.S.proof_limit)
pr.S.proof_limit.Call_provers.limit_mem
| Call_provers.StepLimitExceeded ->
fprintf fmt "FF8000\">Step limit exceeded"
| Call_provers.Unknown _ ->
......
src/why3session/why3session_latex.ml
View file @ c364ad1a
......@@ -132,10 +132,10 @@ let print_result_prov proofs prov fmt=
fprintf fmt "& \\invalid{%.2f} " res.Call_provers.pr_time
| Call_provers.Timeout ->
fprintf fmt "& \\timeout{%ds} "
(Call_provers.get_time pr.S.proof_limit)
pr.S.proof_limit.Call_provers.limit_time
| Call_provers.OutOfMemory ->
fprintf fmt "& \\outofmemory{%dM} "
(Call_provers.get_mem pr.S.proof_limit)
pr.S.proof_limit.Call_provers.limit_mem
| Call_provers.StepLimitExceeded ->
fprintf fmt "& \\steplimitexceeded "
| Call_provers.Unknown _ ->
......
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