Statistics.hpp File Reference

Plans regarding statistics for clause-sets. More...

Go to the source code of this file.

Detailed Description

Plans regarding statistics for clause-sets.

Comprehensive statistics
  • We need a tool which allows us to compute really *all* our statistics.
  • See "Comprehensive statistics" in Interfaces/InputOutput/plans/general.hpp for the C++ implementation.
  • We have extended_statistics_fcs, but this just collects a few statistics, and extensions would break applications.
  • Likely extended_statistics_fcs should just stay as it is, and we need another, more general method.
  • Introduce comprehensive_statistics_fcs(L,F), where L is a list of statistics functions f(F), taking an fcs F as argument.
  • The output is a the collection of statistics-descriptions and values.
  • This could either be a string, or it prints out all the values.
  • The variables all_fcs_statistics is a list of all our statistics.
  • comprehensive_statistics_all_fcs(F) : comprehensive_statistics_fcs(all_fcs_statistics,F).
  • The output of f(F) is a pair [description-string,value].
  • We use a new file, "ComprehensiveStatistics.mac".
  • There then also the wrappers for ordinary statistics (which just yield values) are provided.
  • The wrappers have the name-suffix "_sw" (for "statistics wrapper").
Further statistics
  • DONE A map from literals to literal-degrees.
  • DONE A map from variables to variable-degrees.
  • DONE (as a sorted list) Inversely, for every variable- resp. literal degree the number of variables resp. literals with that degree.
  • DONE Tests whether a clause-set is variable-regular or literal-regular.
  • variable_degree_cs should become var_deg_cs.
  • variable_degrees_cs perhaps should become var_degs_cs; or perhaps var_deg_hm_cs.
  • min_variable_degree_cs should become min_var_deg_cs.
  • max_variable_degree_cs should become max_var_deg_cs.
  • variableregularcsp should become varregcsp.
  • mean_variable_degree_cs should become mean_var_deg_cs.
  • variable_degrees_list_cs perhaps sould become var_deg_l_cs.

Definition in file Statistics.hpp.