Skip to content

GitLab

why3
why3
Commit 4922dbf0 authored by François Bobot's avatar François Bobot
Browse files
Options

remove polymorphism in bench/prepare db incorporation

parent e16b146a
Hide whitespace changes
Inline Side-by-side
Showing with 156 additions and 102 deletions
Makefile.in
View file @ 4922dbf0
......@@ -485,7 +485,7 @@ BENCH_FILES = bench benchrc whybench
BENCHMODULES := $(addprefix src/bench/, $(BENCH_FILES))
BENCHMODULES := src/ide/worker $(BENCHMODULES)
BENCHMODULES := src/ide/worker src/ide/db $(BENCHMODULES)
BENCHML = $(addsuffix .ml, $(BENCHMODULES))
BENCHMLI = $(addsuffix .mli, $(BENCHMODULES))
......@@ -499,8 +499,8 @@ $(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I @SQLITE3LIB@
byte: bin/why3bench.byte
opt: bin/why3bench.opt
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I +sqlite3
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3
bin/why3bench.opt: src/why.cmxa $(PGMCMX) $(BENCHCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
......
src/bench/bench.ml
View file @ 4922dbf0
......@@ -27,20 +27,36 @@ open Driver
open Call_provers
open Scheduler
type 'a tool = {
tval : 'a;
ttrans : task trans;
type tool_id = {
tool_name : string;
prover_name : string;
tool_db : Db.prover_id option;
}
(* tool_name, prover_name *)
type prob_id = {
prob_name : string;
prob_file : string;
prob_theory : string;
prob_db : Db.goal option;
}
(* prob_name, file_name, theory name *)
type tool = {
tval : tool_id;
ttrans : (task trans * (Db.transf_id option)) list;
tdriver : driver;
tcommand : string;
tenv : env;
tuse : task;
tuse_trans : Db.transf_id option;
ttime : int;
tmem : int;
}
type 'a prob = {
ptask : env -> task -> ('a * task) list; (** needed for tenv *)
ptrans : env -> task list trans;
type prob = {
ptask : env -> task -> (prob_id * task) list; (** needed for tenv *)
ptrans : env -> (task list trans * (Db.transf_id option)) list;
}
......@@ -48,20 +64,19 @@ type why_result =
| InternalFailure of exn
| Done of prover_result
let print_why_result fmt = function
| InternalFailure exn ->
Format.fprintf fmt "InternalFailure %a" Exn_printer.exn_printer exn
| Done pr -> Call_provers.print_prover_result fmt pr
type result = {tool : tool_id;
prob : prob_id;
task : Decl.prsymbol;
idtask : int;
result : why_result}
type ('a,'b) result = {tool : 'a;
prob : 'b;
task : Decl.prsymbol;
idtask : int;
result : why_result}
type ('a,'b) callback = 'a -> 'b -> task -> int -> why_result -> unit
type callback = tool_id -> prob_id ->
task -> int -> why_result -> unit
let debug_call = Debug.register_flag "call"
let debug = Debug.register_flag "bench_core"
......@@ -118,6 +133,23 @@ let new_external_proof =
Mutex.unlock queue_lock;
done
let apply_trans (task,_db_goal) (trans,_db_trans) =
let task = Trans.apply trans task in
((task:task),None)
let apply_transl (task,_db_goal) (trans,_db_trans) =
let tasks = Trans.apply trans task in
List.map (fun task -> (task:task),None) tasks
let rec apply_transll trl acc (task,db_goal) =
match trl with
| [] -> (task,db_goal)::acc
| tr::trl ->
let tl = apply_transl (task,db_goal) tr in
List.fold_left (apply_transll trl) acc tl
let call callback tool prob =
(** Prove goal *)
let call pval i task =
......@@ -133,11 +165,12 @@ let call callback tool prob =
in
(** Apply trans *)
let iter_task (pval,task) =
let trans = Trans.compose_l (prob.ptrans tool.tenv)
(Trans.singleton tool.ttrans) in
let tl = Trans.apply trans task in
let iter i task = call pval i task; succ i in
ignore (List.fold_left iter 0 (List.rev tl)) in
let translist = prob.ptrans tool.tenv in
let tasks = apply_transll translist [] (task,pval.prob_db) in
let tasks = List.map
(fun task -> List.fold_left apply_trans task tool.ttrans) tasks in
let iter i (task,_db_goal) = call pval i task; succ i in
ignore (List.fold_left iter 0 (List.rev tasks)) in
(** Split *)
let ths = prob.ptask tool.tenv tool.tuse in
List.iter iter_task ths
......@@ -210,11 +243,11 @@ type output =
(** In a file *)
|Csv of string
type ('a,'b) bench =
type bench =
{
bname : string;
btools : 'a tool list;
bprobs : 'b prob list;
btools : tool list;
bprobs : prob list;
boutputs : output list;
}
......
src/bench/bench.mli
View file @ 4922dbf0
......@@ -31,21 +31,37 @@ val maximum_running_proofs: int ref
(** bound on the number of prover processes running in parallel.
default is 2 *)
type 'a tool = {
tval : 'a;
ttrans : task trans;
type tool_id = {
tool_name : string;
prover_name : string;
tool_db : Db.prover_id option;
}
(* tool_name, prover_name *)
type prob_id = {
prob_name : string;
prob_file : string;
prob_theory : string;
prob_db : Db.goal option;
}
(* prob_name, file_name, theory name *)
type tool = {
tval : tool_id;
ttrans : (task trans * (Db.transf_id option)) list;
tdriver : driver;
tcommand : string;
tenv : env; (** Allow to compare axiomatic easily *)
tuse : task;
tuse_trans : Db.transf_id option;
ttime : int;
tmem : int;
}
type 'a prob = {
ptask : env -> task -> ('a * task) list; (** needed for tenv and tuse *)
ptrans : env -> task list trans; (** perhaps should be merged in
ptask *)
type prob = {
ptask : env -> task -> (prob_id * task) list;
(** needed for tenv and tuse *)
ptrans : env -> (task list trans * (Db.transf_id option)) list;
}
type why_result =
......@@ -53,35 +69,35 @@ type why_result =
| Done of prover_result
val print_why_result : Format.formatter -> why_result -> unit
type result = {tool : tool_id;
prob : prob_id;
task : Decl.prsymbol;
idtask : int;
result : why_result}
type ('a,'b) result = {tool : 'a;
prob : 'b;
task : Decl.prsymbol;
idtask : int;
result : why_result}
type ('a,'b) callback = 'a -> 'b -> task -> int -> why_result -> unit
type callback = tool_id -> prob_id ->
task -> int -> why_result -> unit
val all_list_tp :
?callback:('a,'b) callback ->
'a tool list -> 'b prob list -> ('a,'b) result list
?callback:callback ->
tool list -> prob list -> result list
val all_list_pt :
?callback:('a,'b) callback ->
'a tool list -> 'b prob list -> ('a,'b) result list
?callback:callback ->
tool list -> prob list -> result list
val all_array :
?callback:('a,'b) callback ->
'a tool array -> 'b prob array -> ('a,'b) result list array array
?callback:callback ->
tool array -> prob array -> result list array array
val any :
?callback:('a,'b) callback ->
('a tool * 'b prob) list -> ('a,'b) result list
?callback:callback ->
(tool * prob) list -> result list
val all_list_tools :
?callback:('a,'b) callback ->
'a tool list -> 'b prob list -> ('a * ('a,'b) result list) list
?callback:callback ->
tool list -> prob list -> (tool_id * result list) list
type output =
......@@ -91,25 +107,25 @@ type output =
(** In a file *)
|Csv of string
type ('a,'b) bench =
type bench =
{
bname : string;
btools : 'a tool list;
bprobs : 'b prob list;
btools : tool list;
bprobs : prob list;
boutputs : output list;
}
val run_bench :
?callback:('a,'b) callback -> ('a,'b) bench -> ('a,'b) result list
?callback:callback -> bench -> result list
val run_benchs :
?callback:('a,'b) callback -> ('a,'b) bench list ->
(('a,'b) bench * ('a,'b) result list) list
?callback:callback -> bench list ->
(bench * result list) list
val run_benchs_tools :
?callback:('a,'b) callback -> ('a,'b) bench list ->
(('a,'b) bench * ('a * ('a,'b) result list) list) list
?callback:callback -> bench list ->
(bench * (tool_id * result list) list) list
type nb_avg = int * float
......@@ -125,25 +141,26 @@ type tool_res =
val print_tool_res : Format.formatter -> tool_res -> unit
val compute_average : ('a,'b) result list -> tool_res
val compute_average : result list -> tool_res
val compute_timeline :
float -> float -> float -> ('a,'b) result list -> int list
float -> float -> float -> result list -> int list
(** [compute_timeline start end step results] *)
val filter_timeline : ('a,'b) result list -> ('a,'b) result list
val filter_timeline : result list -> result list
val max_time : ('a,'b) result list -> float
val max_time : result list -> float
open Format
val print_csv :
('b -> 'b -> int) ->
(formatter -> 'a -> unit) ->
(formatter -> 'b -> unit) ->
(prob_id -> prob_id -> int) ->
(formatter -> tool_id -> unit) ->
(formatter -> prob_id -> unit) ->
formatter ->
('a * ('a,'b) result list) list -> unit
(tool_id * result list) list -> unit
val print_output :
('b -> 'b -> int) ->
(formatter -> 'a -> unit) ->
(formatter -> 'b -> unit) ->
('a,'b) bench * ('a * ('a,'b) result list) list -> unit
(prob_id -> prob_id -> int) ->
(formatter -> tool_id -> unit) ->
(formatter -> prob_id -> unit) ->
bench * (tool_id * result list) list -> unit
src/bench/benchrc.ml
View file @ 4922dbf0
......@@ -27,9 +27,9 @@ open Theory
type id_tool = (string * string)
type id_prob = (string * string * string)
type benchrc = { tools : id_tool tool list Mstr.t;
probs : id_prob prob list Mstr.t;
benchs : (id_tool,id_prob) bench Mstr.t
type benchrc = { tools : tool list Mstr.t;
probs : prob list Mstr.t;
benchs : bench Mstr.t
}
open Whyconf
......@@ -54,9 +54,9 @@ let read_tools absf wc map (name,section) =
let env = Lexer.create_env loadpath in
(* transformations *)
let transforms = get_stringl ~default:[] section "transform" in
let lookup acc t = Trans.compose (Trans.lookup_transform t env) acc in
let transforms = List.fold_left lookup Trans.identity transforms
in
let lookup acc t = (Trans.lookup_transform t env,None)::acc in
let transforms = List.fold_left lookup [] transforms in
let transforms = List.rev transforms in
(* use *)
let use = get_stringl ~default:[] section "use" in
let load_use task s =
......@@ -84,12 +84,13 @@ let read_tools absf wc map (name,section) =
let load_driver (n,d,c) = n,Driver.load_driver env d,c in
let provers = List.map load_driver provers in
let create_tool (n,driver,command) =
{ tval = name,n ;
{ tval = {tool_name = name; prover_name = n;tool_db = None} ;
ttrans = transforms;
tdriver = driver;
tcommand = command;
tenv = env;
tuse = use;
tuse_trans = None;
ttime = timelimit;
tmem = memlimit
} in
......@@ -99,12 +100,12 @@ let read_probs absf map (name,section) =
(* transformations *)
let transforms = get_stringl ~default:[] section "transform" in
let gen_trans env =
let lookup acc t = Trans.compose_l
(try Trans.singleton (Trans.lookup_transform t env) with
Trans.UnknownTrans _ -> Trans.lookup_transform_l t env) acc
let lookup acc t =
((try Trans.singleton (Trans.lookup_transform t env) with
Trans.UnknownTrans _ -> Trans.lookup_transform_l t env),None)::acc
in
let transforms = List.fold_left lookup Trans.identity_l transforms in
transforms
let transforms = List.fold_left lookup [] transforms in
List.rev transforms
in
(* format *)
let format = get_stringo section "format" in
......@@ -117,7 +118,9 @@ let read_probs absf map (name,section) =
let m = Env.read_channel ?format:format env fname cin in
close_in cin;
let ths = Mnm.bindings m in
List.rev_map (fun (n,th) -> ((name,fname,n),th)) ths
let prob_id n = {prob_name = name;prob_file = fname; prob_theory = n;
prob_db = None} in
List.rev_map (fun (n,th) -> (prob_id n,th)) ths
in
let map (name,th) = name,Task.split_theory th None task in
let fold acc (n,l) =
......
src/bench/benchrc.mli
View file @ 4922dbf0
......@@ -44,15 +44,9 @@ open Why
open Util
type id_tool = (string * string)
(* tool_name, prover_name *)
type id_prob = (string * string * string)
(* prob_name, file_name, theory name *)
type benchrc = { tools : id_tool tool list Mstr.t;
probs : id_prob prob list Mstr.t;
benchs : (id_tool,id_prob) bench Mstr.t
type benchrc = { tools : tool list Mstr.t;
probs : prob list Mstr.t;
benchs : bench Mstr.t
}
val read_file : Whyconf.config -> string -> benchrc
src/bench/whybench.ml
View file @ 4922dbf0
......@@ -310,12 +310,13 @@ let () =
let prover = try Mstr.find s (get_provers config) with
| Not_found -> eprintf "Prover %s not found.@." s; exit 1
in
{ B.tval = "cmdline",s;
ttrans = Trans.identity;
{ B.tval = {B.tool_name = "cmdline"; prover_name = s; tool_db = None};
ttrans = [Trans.identity,None];
tdriver = load_driver env prover.driver;
tcommand = prover.command;
tenv = env;
tuse = !opt_task;
tuse_trans = None;
ttime = of_option !opt_timelimit;
tmem = of_option !opt_memlimit;
} in
......@@ -324,11 +325,11 @@ let () =
Debug.dprintf debug "Load transformations@.";
let transl =
let lookup acc t = Trans.compose_l
(try Trans.singleton (Trans.lookup_transform t env) with
Trans.UnknownTrans _ -> Trans.lookup_transform_l t env) acc
let lookup acc t =
((try Trans.singleton (Trans.lookup_transform t env) with
Trans.UnknownTrans _ -> Trans.lookup_transform_l t env),None)::acc
in
List.fold_left lookup Trans.identity_l !opt_trans in
List.rev (List.fold_left lookup [] !opt_trans) in
let fold_prob acc = function
| None, _ -> acc
......@@ -343,7 +344,10 @@ let () =
let th = Mnm.bindings m in
let map (name,th) = name,Task.split_theory th None task in
let fold acc (n,l) =
List.rev_append (List.map (fun v -> (("cmdline","",n),v)) l) acc in
let prob_id = {B.prob_name = "cmdline";prob_file = "";
prob_theory = n;
prob_db = None} in
List.rev_append (List.map (fun v -> (prob_id,v)) l) acc in
th |> List.map map |> List.fold_left fold [] in
{ B.ptask = gen;
ptrans = fun _ -> transl;
......@@ -375,7 +379,7 @@ let () =
let nb_done = ref 0 in
let nb_valid = ref 0 in
let nb_failure = ref 0 in
let callback (_,tool) (_,file,prob) task i res =
let callback tool_id prob_id task i res =
if not !opt_quiet then
begin begin match res with
| B.Done {Call_provers.pr_answer = ans} -> incr nb_done;
......@@ -388,15 +392,18 @@ let () =
!nb_done !nb_valid !nb_failure
end;
Debug.dprintf debug "%s.%s %a %i with %s : %a@."
file prob Pretty.print_pr (task_goal task) i tool
prob_id.B.prob_file prob_id.B.prob_theory
Pretty.print_pr (task_goal task) i tool_id.B.tool_name
B.print_why_result res;
in
let benchs =
List.map (fun b -> List.map snd (Mstr.bindings b.Benchrc.benchs))
!benchs in
let bl = B.run_benchs_tools ~callback (list_flatten_rev benchs) in
let print_tool fmt (t,s) = fprintf fmt "%s.%s" t s in
let print_prob fmt (b,f,t) = fprintf fmt "%s.%s.%s" b f t in
let print_tool fmt tool_id = fprintf fmt "%s.%s"
tool_id.B.tool_name tool_id.B.prover_name in
let print_prob fmt prob_id = fprintf fmt "%s.%s.%s"
prob_id.B.prob_name prob_id.B.prob_file prob_id.B.prob_theory in
let cmp = compare in
List.iter (B.print_output cmp print_tool print_prob) bl
......
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