Module Stat

module Stat: sig .. end
Statistics
Author(s): Christoph Sticksel

type int_item 
An integer statistics item
type float_item 
A float statistics item
type int_list_item 
An integer statistics list
type stat_item 
An generic statistics item

Accessor functions


val set : int -> int_item -> unit
Set an integer statistics item
val set_float : float -> float_item -> unit
Set a float statistics item
val set_int_list : int list -> int_list_item -> unit
Set an integer statistics list
val incr : ?by:int -> int_item -> unit
Increment an integers statistics item
val incr_last : ?by:int -> int_list_item -> unit
Increment the last element of an integers statistics list
val append : int -> int_list_item -> unit
Append at the end of an integers statistics list
val reset : int_item -> unit
Reset an integer statistics item to its initial value
val reset_float : float_item -> unit
Reset a float statistics item to its initial value
val reset_int_list : int_list_item -> unit
Reset an integer list statistics item to its initial value
val get : int_item -> int
Get the value of an integer statistics item
val get_float : float_item -> float
Get the value of a float statistics item
val get_int_list : int_list_item -> int list
Get the value of an integer statistics list
val start_timer : float_item -> unit
Start a timer for the float statistics item

The timer (re-)starts from zero, a previously started time will be reset.

val record_time : float_item -> unit
Record the time since the call to Stat.start_timer of this statistics item, stop the timer
val unpause_time : float_item -> unit
Unpauses a timer previously paused by record_time.
val update_time : float_item -> unit
Record the time since the call to Stat.start_timer of this statistics item, do not stop the timer
val time_fun : float_item -> (unit -> 'a) -> 'a
Time a function call and add to the statistics item

Pretty-printing



Statistics items


val pp_print_stats : Format.formatter -> stat_item list -> unit
Print statistics
val pp_print_stats_xml : Format.formatter -> stat_item list -> unit
Print statistics in XML
val pp_print_stats_json : Format.formatter -> stat_item list -> unit
Print statistics in JSON

BMC


val bmc_k : int_item
Highest k reached
val bmc_total_time : float_item
Total time in BMC
val bmc_stop_timers : unit -> unit
Stop and record all timers
val bmc_stats_title : string
Title for BMC statistics
val bmc_stats : stat_item list
BMC statistics
val pp_print_bmc_stats : Format.formatter -> unit
Print statistics for BMC

Inductive step


val ind_k : int_item
Highest k reached
val ind_compress_equal_mod_input : int_item
Number clauses to compress inductive counterexamples
val ind_compress_same_successors : int_item
Number clauses to compress inductive counterexamples
val ind_compress_same_predecessors : int_item
Number clauses to compress inductive counterexamples
val ind_restarts : int_item
Number of restarts
val ind_lazy_invariants_count : int_item
Total time in BMC
val ind_lazy_invariants_time : float_item
Total time in BMC
val ind_total_time : float_item
Total time in BMC
val ind_stop_timers : unit -> unit
Stop and record all timers
val ind_stats_title : string
Title for inductive step statistics
val ind_stats : stat_item list
Inductive step statistics
val pp_print_ind_stats : Format.formatter -> unit
Print statistics for inductive step

IC3


val ic3_k : int_item
Highest k reached
val ic3_restarts : int_item
Number of restarts
val ic3_frame_sizes : int_list_item
Frame sizes in
val ic3_fwd_propagated : int_item
Number of forward propagations
val ic3_fwd_gen_propagated : int_item
Number of forward propagations without generalization
val ic3_fwd_subsumed : int_item
Number of forward subsumed clauses
val ic3_back_subsumed : int_item
Number of backward subsumed clauses
val ic3_fwd_fixpoint : int_item
Fixpoint in forward propagation
val ic3_inductive_blocking_clauses : int_item
Blocking clauses proved inductive
val ic3_total_time : float_item
Total time in IC3
val ic3_fwd_prop_time : float_item
Time spent forward propagating
val ic3_strengthen_time : float_item
Time spent strengthening
val ic3_find_cex_time : float_item
Time spent searching counterexamples
val ic3_ind_gen_time : float_item
Time spent inductively generalizing counterexample
val ic3_generalize_time : float_item
Time spent generalizing
val ic3_inductive_check_time : float_item
Time checking inductiveness of blocking clauses
val ic3_activation_literals : int_item
Number of activation literals
val ic3_stale_activation_literals : int_item
Number of permanently false activation literals
val ic3_stop_timers : unit -> unit
Stop and record all timers
val ic3_stats_title : string
Title for IC3 statistics
val ic3_stats : stat_item list
IC3 statistics
val pp_print_ic3_stats : Format.formatter -> unit
Print statistics for IC3
val ic3ia_refinements : int_list_item
Indices of discoveredi interpolants relative to end of frame
val ic3ia_refinements_end : int_list_item
Indices of discoveredi interpolants relative to end of frame
val ic3ia_num_simulations : int_item
Number of abstraction refinements
val ic3ia_interpolation_time : float_item
Total time for interpolation
val ic3ia_stats_title : string
Title for IC3IA statistics
val ic3ia_stats : stat_item list
IC3IA statistics
val pp_print_ic3ia_stats : Format.formatter -> unit
Print statistics for IC3IA

INVGENOS


val invgengraph_os_k : int_item
Hightest k reached.
val invgengraph_os_candidate_term_count : int_item
Total number of candidate terms.
val invgengraph_os_invariant_count : int_item
Total number of invariants discovered by invariant generation for all systems.
val invgengraph_os_implication_count : int_item
Total number of invariants discovered by invariant generation which were implications.
val invgengraph_os_graph_rewriting_time : float_item
Time spent rewriting graphs.
val invgengraph_os_total_time : float_item
Time spent rewriting graphs.
val invgengraph_os_stats_title : string
Title for INVGENOS statistics
val invgengraph_os_stats : stat_item list
All INVGENOS statistics
val invgengraph_os_stop_timers : unit -> unit
Stop and record all timers
val pp_print_invgengraph_os_stats : Format.formatter -> unit
Pretty-print INVGENOS statistics items

INVGENTS


val invgengraph_ts_k : int_item
Hightest k reached.
val invgengraph_ts_candidate_term_count : int_item
Total number of candidate terms.
val invgengraph_ts_invariant_count : int_item
Total number of invariants discovered by invariant generation for all systems.
val invgengraph_ts_implication_count : int_item
Total number of invariants discovered by invariant generation which were implications.
val invgengraph_ts_graph_rewriting_time : float_item
Time spent rewriting graphs.
val invgengraph_ts_total_time : float_item
Time spent rewriting graphs.
val invgengraph_ts_stats_title : string
Title for INVGENTS statistics
val invgengraph_ts_stats : stat_item list
All INVGENTS statistics
val invgengraph_ts_stop_timers : unit -> unit
Stop and record all timers
val pp_print_invgengraph_ts_stats : Format.formatter -> unit
Pretty-print INVGENTS statistics items

C2I


val c2i_str_invs : int_item
Number of strengthening invariants found.
val c2i_zero_cost : int_item
Number of zero-cost candidates found.
val c2i_moves : int_item
Number of random moves made.
val c2i_move_time : float_item
Time spent in moving and evaluating.
val c2i_query_time : float_item
Time spent querying solvers.
val c2i_model_comp_time : float_item
Time spent comparing models.
val c2i_total_time : float_item
Total time.
val c2i_stats_title : string
Title for C2I statistics.
val c2i_stats : stat_item list
All C2I statistics.
val c2i_stop_timers : unit -> unit
Stop and record all timers.
val pp_print_c2i_stats : Format.formatter -> unit
Pretty-print C2I statistics items

Testgen


val testgen_testcases : int_item
val testgen_deadlocks : int_item
val testgen_restarts : int_item
val testgen_forward_time : float_item
Time spent going forward.
val testgen_backward_time : float_item
Time spent going backward.
val testgen_enumerate_time : float_item
Time spent enumerating.
val testgen_total_time : float_item
val testgen_stats_title : string
val testgen_stats : stat_item list
val testgen_stop_timers : unit -> unit
val pp_print_testgen_stats : Format.formatter -> unit

SMT


val smt_check_sat_time : float_item
Time in check-sat calls
val smt_get_value_time : float_item
Time in get-value calls
val smt_get_unsat_core_time : float_item
Time in get-unsat-core calls
val smt_stop_timers : unit -> unit
Stop and record all timers
val smt_stats_title : string
Title for SMT statistics
val smt_stats : stat_item list
SMT statistics
val pp_print_smt_stats : Format.formatter -> unit
Print statistics for SMT

Certificates


val certif_gen_time : float_item
val certif_min_time : float_item
val certif_frontend_time : float_item
val certif_cvc4_time : float_item
val certif_k : int_item
val certif_size : int_item
val certif_old_k : int_item
val certif_old_size : int_item
val certif_stop_timers : unit -> unit
val certif_stats_title : string
Title for certificate statistics
val certif_stats : stat_item list
Certificate statistics
val pp_print_certif_stats : Format.formatter -> unit
Print statistics for certificate

Misc.


val total_time : float_item
Total time
val analysis_time : float_item
val clause_of_term_time : float_item
val smtexpr_of_term_time : float_item
val term_of_smtexpr_time : float_item
val misc_stop_timers : unit -> unit
Stop and record all timers
val misc_stats_title : string
Title of the general statistics section
val misc_stats : stat_item list
General statistics
val pp_print_misc_stats : Format.formatter -> unit
Print general statistics