Plans regarding statistics for clausesets.
More...
Go to the source code of this file.
Detailed Description
Plans regarding statistics for clausesets.
 Todo:
 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 statisticsdescriptions 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 [descriptionstring,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 namesuffix "_sw" (for "statistics wrapper").
 Todo:
 Further statistics

DONE A map from literals to literaldegrees.

DONE A map from variables to variabledegrees.

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 clauseset is variableregular or literalregular.
 Todo:
 Naming

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.