Commit 841170c6 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'issue_299b' into 'master'

Add %t/%m for timelimit/memlimit in strategy definitions

See merge request !123
parents a3448b0a bf3b9624
......@@ -31,6 +31,8 @@ IDE
* auto jumping to next unproved goal can now be disabled in the preferences
* add a "reset proofs" command in the Tools menu. It removes all proofs in
the session
* strategies can now be defined using %t (resp. %m) for using a prover with
the default timelimit (resp. memlimit)
Realizations
* Added experimental realizations for new Set theories in both Isabelle and
......
......@@ -90,6 +90,20 @@ let set_session_max_tasks n =
session_max_tasks := n;
Prove_client.set_max_running_provers n
let set_session_memlimit c n =
let main = Whyconf.get_main c.controller_config in
let timelimit = Whyconf.timelimit main in
let run_max = Whyconf.running_provers_max main in
let main = Whyconf.set_limits main timelimit n run_max in
c.controller_config <- Whyconf.set_main c.controller_config main
let set_session_timelimit c n =
let main = Whyconf.get_main c.controller_config in
let memlimit = Whyconf.memlimit main in
let run_max = Whyconf.running_provers_max main in
let main = Whyconf.set_limits main n memlimit run_max in
c.controller_config <- Whyconf.set_main c.controller_config main
let set_session_prover_upgrade_policy c p u =
c.controller_config <- Whyconf.set_prover_upgrade_policy c.controller_config p u
......@@ -771,6 +785,9 @@ let run_strategy_on_goal
else
match Array.get strat pc with
| Icall_prover(p,timelimit,memlimit) ->
let main = Whyconf.get_main c.controller_config in
let timelimit = Opt.get_def (Whyconf.timelimit main) timelimit in
let memlimit = Opt.get_def (Whyconf.memlimit main) memlimit in
let callback panid res =
callback_pa panid res;
match res with
......
......@@ -102,11 +102,16 @@ val create_controller: Whyconf.config -> Env.env -> Session_itp.session -> contr
(** creates a controller for the given session.
The config and env is used to load the drivers for the provers. *)
val set_session_max_tasks : int -> unit
(** sets the maximum number of proof tasks that can be running at the
same time. Initially set to 1. *)
val set_session_memlimit: controller -> int -> unit
(** sets the default memlimit for proof attempts *)
val set_session_timelimit: controller -> int -> unit
(** sets the default timelimit for proof attempts *)
val set_session_prover_upgrade_policy :
controller -> Whyconf.prover -> Whyconf.prover_upgrade_policy -> unit
......
......@@ -1517,8 +1517,8 @@ end
begin
match s with
| "max_tasks" -> Controller_itp.set_session_max_tasks i
| "timelimit" -> Server_utils.set_session_timelimit i
| "memlimit" -> Server_utils.set_session_memlimit i
| "timelimit" -> Controller_itp.set_session_timelimit d.cont i
| "memlimit" -> Controller_itp.set_session_memlimit d.cont i
| _ -> P.notify (Message (Error ("Unknown config parameter "^s)))
end
| Set_prover_policy(p,u) ->
......
......@@ -266,12 +266,6 @@ let return_prover name config =
end else
Some (snd (Whyconf.Mprover.choose provers))
let session_timelimit = ref 2
let session_memlimit = ref 1000
let set_session_timelimit n = session_timelimit := n
let set_session_memlimit n = session_memlimit := n
type command_prover =
| Bad_Arguments of Whyconf.prover
| Not_Prover
......@@ -289,14 +283,18 @@ let parse_prover_name config name args : command_prover =
if (List.length args > 2) then Bad_Arguments prover else
match args with
| [] ->
let limit_time = Whyconf.timelimit (Whyconf.get_main config) in
let limit_mem = Whyconf.memlimit (Whyconf.get_main config) in
let default_limit = Call_provers.{empty_limit with
limit_time = !session_timelimit;
limit_mem = !session_memlimit} in
limit_time = limit_time;
limit_mem = limit_mem} in
Prover (prover_config, default_limit)
| [timeout] -> Prover (prover_config,
Call_provers.{empty_limit with
limit_time = int_of_string timeout;
limit_mem = !session_memlimit})
| [timeout] ->
let limit_mem = Whyconf.memlimit (Whyconf.get_main config) in
Prover (prover_config,
Call_provers.{empty_limit with
limit_time = int_of_string timeout;
limit_mem = limit_mem})
| [timeout; oom ] ->
Prover (prover_config, Call_provers.{empty_limit with
limit_time = int_of_string timeout;
......
......@@ -27,13 +27,6 @@ val get_session_dir : allow_mkdir:bool -> string Queue.t -> string
*)
val set_session_timelimit : int -> unit
(** sets the default timelimit in seconds. Initially set to 2. *)
val set_session_memlimit : int -> unit
(** sets the default mem in Mb. Initially set to 1000. *)
(** Simple queries *)
(* The id you are trying to use is undefined *)
......
......@@ -12,7 +12,9 @@
(** {2 User-defined strategies} *)
type instruction =
| Icall_prover of Whyconf.prover * int * int (** timelimit, memlimit *)
| Icall_prover of Whyconf.prover * int option * int option
(** timelimit (if none use default timelimit),
memlimit (if none use default memlimit) *)
| Itransform of string * int (** successor state on success *)
| Igoto of int (** goto state *)
......
......@@ -27,7 +27,9 @@
*)
type instruction =
| Icall_prover of Whyconf.prover * int * int (** timelimit, memlimit *)
| Icall_prover of Whyconf.prover * int option * int option
(** timelimit (if none use default timelimit),
memlimit (if none use default memlimit) *)
| Itransform of string * int (** successor state on success *)
| Igoto of int (** goto state *)
......
......@@ -89,8 +89,13 @@
error "Prover description %s is ambiguous" p
let integer msg s =
try int_of_string s
with Failure _ -> error "unable to parse %s argument '%s'" msg s
try Some (int_of_string s)
with Failure _ ->
match s with
| "%t" -> None
| "%m" -> None
| _ ->
error "unable to parse %s argument '%s'" msg s
let transform code t =
try
......@@ -109,6 +114,8 @@ let integer = ['0'-'9']+
let goto = 'g' | "goto"
let call = 'c' | "call"
let transform = 't' | "transform"
let timelimit = integer | "%t"
let memlimit = integer | "%m"
rule scan code = parse
| space+
......@@ -121,12 +128,14 @@ rule scan code = parse
| goto space+ (ident as id)
{ add_instr code (Igoto (find_label code id));
scan code lexbuf }
| call space+ (ident as p) space+ (integer as t) space+ (integer as m)
| call space+ (ident as p) space+ (timelimit as t) space+ (memlimit as m)
{ let p = prover code p in
let t = integer "timelimit" t in
if t <= 0 then error "timelimit %d is invalid" t;
if t <> None && Opt.get t <= 0 then
error "timelimit %d is invalid" (Opt.get t);
let m = integer "memlimit" m in
if m <= 0 then error "memlimit %d is invalid" m;
if m <> None && Opt.get m <= 0 then
error "memlimit %d is invalid" (Opt.get m);
add_instr code (Icall_prover (p.Whyconf.prover, t, m));
scan code lexbuf }
| transform space+ (ident as t) space+ (ident as l)
......
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