diff --git a/src/core/dterm.ml b/src/core/dterm.ml index 7a2fd08d532ee270e818030c489d3df436d578b2..e1c6570ccd2c4ac347ca91b27720267d605e408e 100644 --- a/src/core/dterm.ml +++ b/src/core/dterm.ml @@ -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 *) diff --git a/src/transform/induction.ml b/src/transform/induction.ml index 3108a043f587bf1b94d16457d110ee48c2f3a603..324b420c99ed4cdfbcf601592c17f4ef3fbab299 100644 --- a/src/transform/induction.ml +++ b/src/transform/induction.ml @@ -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 () = diff --git a/src/why3session/why3session_info.ml b/src/why3session/why3session_info.ml index 81ab4d3886c05c1872d4d54d36b20ded1766f5cc..27f505f87c6cda9cf2f2cc363513fbcfdcbb4071 100644 --- a/src/why3session/why3session_info.ml +++ b/src/why3session/why3session_info.ml @@ -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 ******)