Commit 742f0819 authored by MARCHE Claude's avatar MARCHE Claude

improved histograms

parent c4e7e01d
......@@ -112,22 +112,26 @@ let specialize_ls ls =
let spec ty = if ty_closed ty then Duty ty else spec ty in
List.map spec ls.ls_args, Opt.map spec ls.ls_value
(* dead code
let specialize_fs ls =
let dtyl, dty = specialize_ls ls in
match dty with
| Some dty -> dtyl, dty
| None -> raise (FunctionSymbolExpected ls)
*)
let specialize_cs ls =
if ls.ls_constr = 0 then raise (ConstructorExpected ls);
let dtyl, dty = specialize_ls ls in
dtyl, Opt.get dty
(* dead code
let specialize_ps ls =
let dtyl, dty = specialize_ls ls in
match dty with
| Some _ -> raise (PredicateSymbolExpected ls)
| None -> dtyl
*)
(** Patterns, terms, and formulas *)
......
......@@ -20,7 +20,9 @@ open Task
(** TODO use this label in the following function *)
(* dead code
let label_induction = create_label "induction"
*)
(*
let desc_labels = [label_induction,
......@@ -144,13 +146,14 @@ let print_lex lexl =
(************************* WITH LEXICOGRAPHIC ORDER **************************)
(*****************************************************************************)
(* dead code
let split_quantifiers x qvl =
let rec aux left = function
| hd :: tl when vs_equal x hd -> List.rev left, tl
| hd :: tl -> aux (hd :: left) tl
| [] -> assert false
in aux [] qvl
*)
(*INITIAL FORMULA SPLIT*)
let decompose_forall t =
......@@ -363,17 +366,20 @@ the induction hypothesis are the variables on the right of the rightmost
induction variable.*)
(* separate prenex universal quantification from the body of the formula*)
(* dead code
let decompose_int_forall t =
let rec aux qvl_acc t = match t.t_node with
| Tquant (Tforall, qt) ->
let qvl, _, t = t_open_quant qt in aux (qvl_acc @ qvl) t
| _ -> qvl_acc, t
in aux [] t
*)
(* find labeled variables (for induction variables),
and the rest of the quantified variables after the last labeled variable
(for the variables to generalize inside induction hypothesis).
Ex: the result of Va.x1.b.x2.c.x3.d.P is [a.x1.b.x2.c.x3][x1.x2.x3][d]*)
(* dead code
let split_int_qlv_labeled qvl =
let rec aux left_acc ind_acc gen_acc = function
| [] -> List.rev left_acc, List.rev ind_acc, gen_acc
......@@ -384,6 +390,7 @@ let split_int_qlv_labeled qvl =
then aux (v :: (gen_acc @ left_acc)) (v :: ind_acc) [] tl
else aux left_acc ind_acc (v :: gen_acc) tl
in aux [] [] [] qvl
*)
(*
input: ordered induction variables, rightmost neutral variables
......@@ -397,6 +404,7 @@ then output:
(d',e') ~ 'generalization variables',
(x1',x2',x3') ~ 'induction variables'
(0 <= x1'/\0 <= x2'/\(x1' < x1 \/ x1' = x1 /\ x2' < x2) ~ 'hyp. condition' *)
(* dead code
let lex_order_ivl (le_int,lt_int) ivl rvl =
let gen_rvl, (hd,hd',tl,tl') =
let create_v v = Term.create_vsymbol (Ident.id_clone v.vs_name) ty_int in
......@@ -423,10 +431,12 @@ let lex_order_ivl (le_int,lt_int) ivl rvl =
| _ -> assert false
in lex_ord (hd, hd', [],[]) lt_hd (tl, tl') in
gen_rvl, (hd' :: tl'), t_and nonneg_ivl' lt_lex
*)
(*returns the resulting formula with induction hypothesis.
The formula however is still not closed (by the quantifiers before
the rightmost neutral quantifiers). *)
(* dead code
let int_strong_induction_lex (le_int,lt_int) ivl rvl t =
let (gen_rvl, ind_ivl, hyp_cond) =
lex_order_ivl (le_int,lt_int) ivl rvl in
......@@ -437,7 +447,9 @@ let int_strong_induction_lex (le_int,lt_int) ivl rvl t =
let ind_hyp =
t_forall_close (ind_ivl @ gen_rvl) [] (t_implies hyp_cond hyp_goal) in
let open_t = t_implies ind_hyp (t_forall_close rvl [] t) in open_t
*)
(* dead code
let induction_int_lex _km (le_int,lt_int) t0 =
let qvl, t = decompose_int_forall t0 in
let lvl,ivl, genl = split_int_qlv_labeled qvl in
......@@ -452,7 +464,9 @@ let induction_int_lex _km (le_int,lt_int) t0 =
Format.printf "New Task: %a \n@." Pretty.print_term t);
[t]
end
*)
(* dead code
let induction_int_lex th_int = function
| Some
{ task_decl = { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
......@@ -466,6 +480,7 @@ let induction_int_lex th_int = function
(induction_int_lex km (le_int, lt_int) f)
with Exit -> [t] end
| _ -> assert false
*)
(*
let () =
......
......@@ -374,34 +374,34 @@ let run_one stats r0 r1 fname =
(**** print histograms ******)
let print_hist stats =
let main_ch = open_out "why3session.gnuplot" in
let main_file,main_ch =
Filename.open_temp_file "why3session" ".gnuplot"
in
let main_fmt = formatter_of_out_channel main_ch in
fprintf main_fmt "set logscale y@\n";
fprintf main_fmt "set logscale@\n";
fprintf main_fmt "set key rmargin@\n";
let (_:int) =
Hprover.fold
(fun p h acc ->
let pf = (string_of_int acc) ^ ".plot" in
let pf,ch = Filename.open_temp_file "why3session" ".data" in
if acc = 1 then
fprintf main_fmt "plot [0:%d] [0.01:%.2f] "
fprintf main_fmt "plot [1:%d] [0.01:%.2f] "
(stats.nb_proved_sub_goals + stats.nb_proved_root_goals)
(stats.max_time)
else
fprintf main_fmt "replot";
fprintf main_fmt " \"%s\" using 2:1 title \"%s\" with linespoints ps 0.2@\n"
fprintf main_fmt
" \"%s\" using 2:1 title \"%s\" with linespoints ps 0.2@\n"
pf (string_of_prover p);
let ch = open_out pf in
let fmt = formatter_of_out_channel ch in
(*
fprintf fmt "0.00 0@\n";
*)
let (_ :int) =
let (_ : float * int) =
Mfloat.fold
(fun t c acc ->
let acc = c + acc in
fprintf fmt "%.2f %d@\n" t acc;
acc)
h 0
(fun t c (acct,accc) ->
let accc = c + accc in
let acct = t +. acct in
fprintf fmt "%.2f %d@\n" acct accc;
(acct,accc))
h (0.0,0)
in
fprintf fmt "@.";
close_out ch;
......@@ -412,8 +412,14 @@ let print_hist stats =
fprintf main_fmt "set terminal pdfcairo@\n";
fprintf main_fmt "set output \"why3session.pdf\"@\n";
fprintf main_fmt "replot@.";
close_out main_ch
close_out main_ch;
let cmd = "gnuplot " ^ main_file in
eprintf "Running command %s@." cmd;
let ret = Sys.command cmd in
if ret <> 0 then
eprintf "Command %s failed@." cmd
else
eprintf "See also results in file why3session.pdf@."
(****** run on all files ******)
......
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