Class DataAndStatistics¶
- Defined in File statistics.h
Class Documentation¶
-
class
DataAndStatistics
¶ statistics.h
Purpose: Defines the DataAndStatistics() class.
Copyright (C) 2018 Zayd Hammoudeh. All rights reserved.
- Author
- Zayd Hammoudeh zayd@ucsc.edu
- Version
- 0.00.00
This software may be modified and distributed under the terms of the MIT license. See the LICENSE file for details.
Original Author: Marc Thurley.
Public Functions
-
DataAndStatistics
()¶
-
void
UpdateNodeTypeStatistics
(TopTreeNodeType node_type, const mpz_class &num_models)¶ Updates the number of nodes and total model count based on the top tree node type.
- Parameters
node_type
: Type of top tree nodenum_models
: Number of new models for the specified node type.
-
TreeNodeIndex
num_tree_nodes
(TopTreeNodeType node_type)¶ Accesor for the number of top tree nodes of a specified type.
- Return
- Total number of top tree nodes of the specified type.
- Parameters
node_type
: Type of top tree node.
-
mpz_class
num_tree_node_models
(TopTreeNodeType node_type)¶ Accessor for the total number of models associated with a specified type of top tree node.
- Return
- Total number of models associated with the specific top tree node type.
- Parameters
node_type
: Type of top tree node.
-
double
percent_tree_node_models
(TopTreeNodeType node_type)¶ Calculates the percentage of all models that are of a specific type.
- Return
- Percent of all models that fall under the specified node type
- Parameters
node_type
: Type of top tree node (e.g., cylinder, max depth, component split, etc.)
-
void
reset_statistics
()¶
-
bool
cache_full
() const¶ Checks whether the cache is full (i.e., exceeds 100% capacity).
- Return
- true if the cache is full and false otherwise.
-
uint64_t
cache_bytes_memory_usage
() const¶ - Return
- Sum of the infrastructure bytes and the sized of the cached components.
-
uint64_t
overall_cache_bytes_memory_stored
()¶
-
void
incorporate_cache_store
(CacheableComponent &ccomp)¶
-
void
incorporate_cache_erase
(CacheableComponent &ccomp)¶
-
void
incorporate_cache_hit
(CacheableComponent &ccomp)¶
-
unsigned long
cache_MB_memory_usage
()¶
-
double
implicitBCP_miss_rate
()¶
-
unsigned long
num_clauses
() const¶
-
unsigned long
num_conflict_clauses
()¶
-
unsigned long
clause_deletion_interval
()¶
-
void
set_final_solution_count
(const mpz_class &count)¶ Updates the solver field “final_solution_count_” with the solution count multiplied by 2^{#unused variables}. Hence:
final_solution_count_ = count * 2^(num_variables_ - num_used_variables_)
- Parameters
count
: model count.
-
const mpz_class &
final_solution_count
() const¶ Accessor for the final solution count
- Return
- Final solution count.
-
void
printShort
()¶ statistics.cpp
Purpose: Defines methods for the DataAndStatistics() class.
Copyright (C) 2018 Zayd Hammoudeh. All rights reserved.
- Author
- Zayd Hammoudeh zayd@ucsc.edu
- Version
- 0.00.00
This software may be modified and distributed under the terms of the MIT license. See the LICENSE file for details.
Original Author: Marc Thurley.
-
void
printShortFormulaInfo
()¶ Prints to the console information about the formula including: number of long, binary, & unit clauses, number of used variables, and total number of variables.
-
unsigned long
getTime
() const¶ Number of decisions (i.e., branch variable selections) made. This is used for determining when to remove components from the cache.
- Return
- Number of branch variable selections
-
long double
getAvgComponentSize
()¶
-
unsigned long
cached_component_count
()¶ Access the number of components in the cache.
- Return
-
unsigned long
cache_hits
()¶ Number of cache look-ups where the component requested was in the cache.
- Return
- Cache look-up count.
-
double
cache_miss_rate
()¶ The rate of cache look-ups where the requested component was not in the cache.
- Return
- 0 if a cache look-up never occurred. Otherwise, it is the number of caches misses divided by the total number of cache look-ups.
-
long double
getAvgCacheHitSize
()¶ The average size of a reused (i.e., hit) components in the cache.
- Return
- 0 if a cache hit has never occurred. Otherwise, it is the average size of cached components that have ever been HIT.
Public Members
-
std::string
input_file_
¶ Path to the file containing the CNF formula used in the current run.
-
time_t
start_time_
¶
-
uint64_t
maximum_cache_size_bytes_
= 0¶
-
SolverExitState
exit_state_
= SolverExitState::NO_STATE¶
-
VariableIndex
num_original_variables_
= 0¶
-
ClauseIndex
num_original_clauses_
= 0¶
-
ClauseIndex
num_original_binary_clauses_
= 0¶
-
ClauseIndex
num_original_unit_clauses_
= 0¶
-
VariableIndex
num_variables_
= 0¶ number of variables remaining
-
VariableIndex
num_used_variables_
= 0¶ Number of variables that actually occurs in clauses
-
VariableIndex
num_free_variables_
= 0¶ Number of variables that do not appear in any clause.
-
VariableIndex
num_indep_support_variables_
= 0¶ Number of variables in the independent support.
-
ClauseIndex
num_long_clauses_
= 0¶ Number of long clauses (i.e., greater than 3 unique literals) after pre-processing.
-
ClauseIndex
num_binary_clauses_
= 0¶ Number of binary clauses after pre-processing.
-
ClauseIndex
num_long_conflict_clauses_
= 0¶
-
ClauseIndex
num_binary_conflict_clauses_
= 0¶
-
ClauseIndex
times_conflict_clauses_cleaned_
= 0¶
-
ClauseIndex
num_unit_clauses_
= 0¶
-
uint64_t
num_decisions_
= 0¶ number of all decisions made - MT
Number of times a branch variable is set. It does not include BCP variable setting.
-
uint64_t
num_failed_literals_detected_
= 0¶ Number of all failed literal detected.
-
uint64_t
num_failed_literal_tests_
= 0¶
-
uint64_t
num_conflicts_
= 0¶ Number of all conflicts encountered.
-
uint64_t
num_clauses_learned_
= 0¶
-
VariableIndex
max_component_split_depth_
= 0¶ Maximum number of embedded components splits.
-
VariableIndex
max_branch_var_depth_
= 0¶ Maximum depth of branch variable setting. This excludes variables implied via UP or implied BCP.
-
TreeNodeIndex
num_top_tree_nodes_
= 0¶ Number of top tree nodes observed.
-
TreeNodeIndex
num_tree_nodes_by_type_
[static_cast<long>(NUM_TREE_NODE_TYPES
)]¶ Number of nodes of each of the top tree node types
-
mpz_class
num_models_by_tree_node_type_
[static_cast<long>(NUM_TREE_NODE_TYPES
)]¶ Number of models for each of the top tree node types.
-
uint64_t
num_cache_hits_
= 0¶
-
uint64_t
num_cache_look_ups_
= 0¶
-
uint64_t
sum_cache_hit_sizes_
= 0¶
-
uint64_t
num_cached_components_
= 0¶
-
uint64_t
sum_size_cached_components_
= 0¶
-
uint64_t
sum_bytes_cached_components_
= 0¶ Number of bytes occupied by all cached components.
-
uint64_t
overall_bytes_components_stored_
= 0¶
-
uint64_t
sum_bytes_pure_cached_component_data_
= 0¶
-
uint64_t
overall_bytes_pure_stored_component_data_
= 0¶
-
uint64_t
sys_overhead_sum_bytes_cached_components_
= 0¶
-
uint64_t
sys_overhead_overall_bytes_components_stored_
= 0¶
-
uint64_t
cache_infrastructure_bytes_memory_usage_
= 0¶
-
uint64_t
overall_num_cache_stores_
= 0¶
-
mpz_class
final_solution_count_
= 0¶
-
double
sampler_time_elapsed_
= DBL_MAX¶ Amount of time required to complete the full sampling.
-
double
sampler_pass_1_time_
= DBL_MAX¶ Amount of time required to complete phase 1 and build all partial assignments (or just the time required to collect a single sample when two pass is disabled).
-
double
sampler_pass_2_time_
= DBL_MAX¶ Time required to convert all partial assignments into complete assignments. This represents “pass 2” of the sampler.
-
std::vector<VariableIndex>
numb_second_pass_vars_
¶ When performing two pass testing, this records the number of variables that remain to be set at the start of the second pass for each sample.