From 39b964135c503fc4c9f5a7c598cfe44b44a28c55 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 9 Oct 2023 11:11:32 +0200 Subject: [PATCH] Rewording and poetry --- src/bin/common/solving_loop.ml | 12 +++- src/lib/structures/profiling.ml | 118 +++++++++++++++++++++++-------- src/lib/structures/profiling.mli | 4 +- 3 files changed, 99 insertions(+), 35 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index bc2d9ac43..da7943625 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -392,6 +392,7 @@ let main () = let handle_option st_loc name (value : DStd.Term.t) = match name, value.term with + (* Smtlib2 regular options *) | ":regular-output-channel", Symbol { name = Simple name; _ } -> Options.Output.create_channel name |> Options.Output.set_regular @@ -444,6 +445,13 @@ let main () = | ":random-seed"), _ -> unsupported_opt name + (* Alt-Ergo custom options *) + | ":profiling", Symbol { name = Simple level; _ } -> + begin + match float_of_string_opt level with + | None -> print_wrn_opt ~name st_loc "nonnegative integer" value + | Some i -> Options.set_profiling true i + end | _ -> unsupported_opt name in @@ -486,9 +494,9 @@ let main () = print_std Fmt.string Version._version | ":all-statistics" -> if Options.get_profiling () then - Printer.print_std "%t" Profiling.print_get_statistics + Printer.print_std "%t" Profiling.print_statistics else - Printer.print_smtlib_err "Profiling disactivated (try --profiling)" + warning "Profiling disactivated (try --profiling)" | ":assertion-stack-levels" -> unsupported_opt name | _ -> diff --git a/src/lib/structures/profiling.ml b/src/lib/structures/profiling.ml index 365807b8d..d5ec1f211 100644 --- a/src/lib/structures/profiling.ml +++ b/src/lib/structures/profiling.ml @@ -66,8 +66,7 @@ type t = { mutable b_elim : int; mutable instances_map : inst_info MS.t; mutable instances_map_printed : bool; - - timers : Timers.t Lazy.t + timers : Timers.t } type mode = @@ -85,7 +84,7 @@ let nb_prints = ref max_nb_prints let initial_info = ref true -let state = { +let state = lazy { decisions = 0; assumes = 0; assumes_current_lvl = 0; @@ -108,10 +107,16 @@ let state = { instances_map = MS.empty; instances_map_printed = false; - timers = lazy (Timers.empty ()) + timers = Timers.empty () } -let get_timers () = Lazy.force state.timers +(** Calls the continuation only when the profiling is on. + This allows to only force the state when the profiling is on. *) +let (let*) state f = + if Options.get_profiling () then + f (Lazy.force state) + +let get_timers () = (Lazy.force state).timers let set_sigprof () = let tm = @@ -123,6 +128,7 @@ let set_sigprof () = { Unix.it_value = tm; Unix.it_interval = 0. }) let init () = + let state = Lazy.force state in state.decisions <- 0; state.assumes <- 0; state.queries <- 0; @@ -151,15 +157,20 @@ let init () = (* update functions of the internal state *) let assume nb = + let* state = state in state.assumes <- nb + state.assumes; state.assumes_current_lvl <- nb + state.assumes_current_lvl -let query () = state.queries <- state.queries + 1 +let query () = + let* state = state in + state.queries <- state.queries + 1 let instances l = + let* state = state in state.instances <- state.instances + List.length l let instantiation ilvl = + let* state = state in state.instantiation_rounds <- state.instantiation_rounds + 1; state.instantiation_lvl <- state.instantiation_lvl + 1; if not (state.instantiation_lvl = ilvl) then begin @@ -170,12 +181,15 @@ let instantiation ilvl = end let bool_conflict () = + let* state = state in state.b_conflicts <- state.b_conflicts + 1 let theory_conflict () = + let* state = state in state.th_conflicts <- state.th_conflicts + 1 let bcp_conflict b1 b2 = + let* state = state in if b1 && b2 then state.bcp_b_conflicts <- state.bcp_b_conflicts + 1 else if (not b1) && (not b2) then @@ -184,20 +198,24 @@ let bcp_conflict b1 b2 = state.bcp_mix_conflicts <- state.bcp_mix_conflicts + 1 let red b = + let* state = state in if b then state.b_red <- state.b_red + 1 else state.t_red <- state.t_red + 1 let elim b = + let* state = state in if b then state.b_elim <- state.b_elim + 1 else state.t_elim <- state.t_elim + 1 -let reset_ilevel n = state.instantiation_lvl <- n +let reset_ilevel n = + let* state = state in state.instantiation_lvl <- n -let reset_dlevel n = state.decision_lvl <- n +let reset_dlevel n = + let* state = state in state.decision_lvl <- n let empty_inst_info loc = { @@ -214,6 +232,7 @@ let empty_inst_info loc = } let new_instance_of axiom inst loc kept = + let* state = state in let () = state.instances_map_printed <- false in let ii = try MS.find axiom state.instances_map @@ -229,6 +248,7 @@ let new_instance_of axiom inst loc kept = state.instances_map <- MS.add axiom ii state.instances_map let conflicting_instance axiom loc = + let* state = state in let ii = try MS.find axiom state.instances_map with Not_found -> empty_inst_info loc @@ -238,6 +258,7 @@ let conflicting_instance axiom loc = state.instances_map <- MS.add axiom ii state.instances_map let decision_on_instance axiom_name = + let* state = state in try let ii = MS.find axiom_name state.instances_map @@ -249,6 +270,7 @@ let decision_on_instance axiom_name = let decision d origin = + let* state = state in state.decisions <- state.decisions + 1; state.decision_lvl <- state.decision_lvl + 1; if state.decision_lvl <> d then begin @@ -265,6 +287,7 @@ let decision d origin = let register_produced_terms axiom loc consumed all produced _new = + let* state = state in let ii = try MS.find axiom state.instances_map with Not_found -> empty_inst_info loc @@ -304,8 +327,7 @@ let current_timer () = Timers.current_timer (get_timers ()) - Is the column linked to a statistic (Some true), a timer (Some false) or not (None)? - Data formatter - Todo(Steven): use Pierre's solution with Printbox and put these function where - they belong (the trash). + Todo(Steven): use Pierre's solution with Printbox *) let columns : (string * string * int * bool option * 'a) list = [ @@ -341,63 +363,97 @@ let columns : (string * string * int * bool option * 'a) list = (*-----------------------------------------------------------------*) "ilvl", "Current Instantiaton level", 6, Some true, - (fun _ _ sz -> int_resize state.instantiation_lvl sz); + (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.instantiation_lvl sz); "#i rnds", "Number of intantiation rounds", 8, Some true, (fun _ _ sz -> + let state = Lazy.force state in int_resize state.instantiation_rounds sz); "#insts", "Number of generated instances", 8, Some true, - (fun _ _ sz -> int_resize state.instances sz); + (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.instances sz); "i/r", "AVG number of generated instances per instantiation rounds", 8, Some true, (fun _ _ sz -> + let state = Lazy.force state in int_resize (state.instances / (max 1 state.instantiation_rounds)) sz); "dlvl", "Current Decision level", 6, Some true, - (fun _ _ sz -> int_resize state.decision_lvl sz); + (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.decision_lvl sz); "#decs", "Number of decisions", 6, Some true, - (fun _ _ sz -> int_resize state.decisions sz); + (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.decisions sz); "T-asm", "Number of calls to Theory.assume", 6, Some true, - (fun _ _ sz -> int_resize state.assumes sz); + (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.assumes sz); "T/d", "Number of Theory.assume after last decision", 6, Some true, - (fun _ _ sz -> int_resize state.assumes_current_lvl sz); + (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.assumes_current_lvl sz); "T-qr", "Number of calls to Theory.query", 15, Some true, - (fun _ _ sz -> int_resize state.queries sz); + (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.queries sz); "B-R", "Number of reduced clauses by Boolean propagation", 6, Some true, - (fun _ _ sz -> int_resize state.b_red sz); + (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.b_red sz); "B-E", "Number of eliminated clauses by Boolean propagation", 6, - Some true, (fun _ _ sz -> int_resize state.b_elim sz); + Some true, (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.b_elim sz); "T-R", "Number of reduced clauses by Theory propagation", 6, Some true, - (fun _ _ sz -> int_resize state.t_red sz); + (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.t_red sz); "T-E", "Number of eliminated clauses by Theory propagation", 6, - Some true, (fun _ _ sz -> int_resize state.t_elim sz); + Some true, (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.t_elim sz); "B-!", "Number of direct Boolean conflicts", 5, Some true, - (fun _ _ sz -> int_resize state.b_conflicts sz); + (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.b_conflicts sz); "T-!", "Number of direct Theory conflicts" , 5, Some true, - (fun _ _ sz -> int_resize state.th_conflicts sz); + (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.th_conflicts sz); "B>!", "Number of Boolean conflicts deduced by BCP", 5, Some true, - (fun _ _ sz -> int_resize state.bcp_b_conflicts sz); + (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.bcp_b_conflicts sz); "T>!", "Number of Theory conflicts deduced by BCP", 5, Some true, - (fun _ _ sz -> int_resize state.bcp_th_conflicts sz); + (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.bcp_th_conflicts sz); "M>!", "Number of Mix conflicts deduced by BCP", 5, Some true, - (fun _ _ sz -> int_resize state.bcp_mix_conflicts sz); + (fun _ _ sz -> + let state = Lazy.force state in + int_resize state.bcp_mix_conflicts sz); (*-----------------------------------------------------------------*) "SAT", "Time spent in SAT module(s)", 16, Some false, @@ -714,14 +770,14 @@ let register_float_stat (key : string) (getter : unit -> float) = (fun () -> Format.sprintf "%.9f" (getter ())) -let print_get_statistics fmt = - Format.fprintf fmt "(@[@,"; +let print_statistics fmt = + Fmt.pf fmt "(@[@,"; Hashtbl.iter - (fun key getter -> Format.fprintf fmt ":%s %s@," key (getter ())) + (fun key getter -> Fmt.pf fmt ":%s %s@," key (getter ())) statistics_table; - Format.fprintf fmt "@])@," + Fmt.pf fmt "@])@," -(* Now, registering the statistics we want in get-statistics. *) +(* Now, registering the statistics we want in (get-info :all-statistics). *) let () = register_int_stat "steps" (fun () -> Steps.get_steps ()); List.iter diff --git a/src/lib/structures/profiling.mli b/src/lib/structures/profiling.mli index 6431ee291..d640d09b3 100644 --- a/src/lib/structures/profiling.mli +++ b/src/lib/structures/profiling.mli @@ -66,5 +66,5 @@ val switch : Format.formatter -> unit val get_timers : unit -> Timers.t -(** Prints the statistics for the SMT instruction get-statistics *) -val print_get_statistics : Format.formatter -> unit +(** Prints the statistics for the SMT statement (get-info :all-statistics). *) +val print_statistics : Format.formatter -> unit