Previous  Up  Next

Module Statistic (.ml)


module Statistic: sig .. end
derivation statistic

manages information about the derivation like number of inference rules applied, number of candidates computed, ...


Types

type config = Config.config 
type statistic

Functions


Creation


val create : config -> statistic

Derivation Rules 


val inc_close : statistic -> unit
val get_close : statistic -> int
val inc_assert : statistic -> unit
val get_assert : statistic -> int
val inc_split : statistic -> unit
val get_split : statistic -> int
val inc_resolve : statistic -> unit
val get_resolve : statistic -> int
val inc_subsume : statistic -> unit
val get_subsume : statistic -> int
val inc_compact : statistic -> unit
val get_compact : statistic -> int

Misc 


val inc_filtered_by_productivity : statistic -> unit
val get_filtered_by_productivity : statistic -> int
candidates ignored because of productivity.
val inc_computed_assert_candidates : statistic -> unit
val get_computed_assert_candidates : statistic -> int
computed assert candidates within the deepening bound.
val inc_computed_split_candidates : statistic -> unit
val get_computed_split_candidates : statistic -> int
computed split candidates (remainders) within the deeping bound.
val inc_jump : statistic -> unit
val get_jump : statistic -> int
executed jumps (Jumping).

Debug



for free use during development
val inc_debug : statistic -> unit
val get_debug : statistic -> int
val inc_global_debug : unit -> unit
val get_global_debug : unit -> int64
val inc_global_debug2 : unit -> unit
val get_global_debug2 : unit -> int
val set_global_debug2 : int -> unit

Representation


val print : statistic -> unit
string representation of the statistics (Print.print_label).