Program Listing for File statistics.h

↰ Return to documentation for file (src/statistics.h)

#ifndef STATISTICS_H_
#define STATISTICS_H_

#include <gmpxx.h>

#include <string>
#include <cstdint>
#include <vector>
#include <cfloat>

#include "structures.h"
#include "component_types/cacheable_component.h"

#include "primitive_types.h"
#include "solver_config.h"


class DataAndStatistics {
 public:
  DataAndStatistics() {
    time(&start_time_);
    for (unsigned i = 0; i < static_cast<unsigned>(TopTreeNodeType::NUM_TREE_NODE_TYPES); i++) {
      num_models_by_tree_node_type_[i] = 0;
      num_tree_nodes_by_type_[i] = 0;
    }
  }
  std::string input_file_;
  //double time_elapsed_ = 0.0;
  time_t start_time_;
  uint64_t maximum_cache_size_bytes_ = 0;

  SolverExitState exit_state_ = SolverExitState::NO_STATE;
  // different variable counts
  // number of variables  and clauses before preprocessing
  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;
  VariableIndex num_used_variables_ = 0;
  VariableIndex num_free_variables_ = 0;
  VariableIndex num_indep_support_variables_ = 0;
  ClauseIndex num_long_clauses_ = 0;
  ClauseIndex num_binary_clauses_ = 0;

  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;
  uint64_t num_failed_literals_detected_ = 0;
  uint64_t num_failed_literal_tests_ = 0;
  uint64_t num_conflicts_ = 0;

  // number of clauses overall learned
  uint64_t num_clauses_learned_ = 0;
  VariableIndex max_component_split_depth_ = 0;
  VariableIndex max_branch_var_depth_ = 0;
  TreeNodeIndex num_top_tree_nodes_ = 0;
  TreeNodeIndex num_tree_nodes_by_type_[static_cast<long>(TopTreeNodeType::NUM_TREE_NODE_TYPES)];
  mpz_class num_models_by_tree_node_type_[static_cast<long>(TopTreeNodeType::NUM_TREE_NODE_TYPES)];
  void UpdateNodeTypeStatistics(TopTreeNodeType node_type, const mpz_class & num_models) {
    auto node_type_id = static_cast<long>(node_type);
    num_tree_nodes_by_type_[node_type_id]++;
    num_models_by_tree_node_type_[node_type_id] += num_models;
  }
  TreeNodeIndex num_tree_nodes(TopTreeNodeType node_type) {
    auto node_type_id = static_cast<long>(node_type);
    return num_tree_nodes_by_type_[node_type_id];
  }
  mpz_class num_tree_node_models(TopTreeNodeType node_type) {
    auto node_type_id = static_cast<long>(node_type);
    return num_models_by_tree_node_type_[node_type_id];
  }
  double percent_tree_node_models(TopTreeNodeType node_type) {
    if (final_solution_count_ == 0)
      return -1;
    mpf_class percent_models = num_tree_node_models(node_type);
    percent_models /= static_cast<mpf_class>(final_solution_count_);
    return percent_models.get_d();
  }

  /* cache statistics */
  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;
  // the same number, summing over all components ever stored
  uint64_t overall_bytes_components_stored_ = 0;

  // the above numbers, but without any overhead,
  // counting only the pure data size of the components - without model counts
  uint64_t sum_bytes_pure_cached_component_data_ = 0;
  // the same number, summing over all components ever stored
  uint64_t overall_bytes_pure_stored_component_data_ = 0;


  uint64_t sys_overhead_sum_bytes_cached_components_ = 0;
    // the same number, summing over all components ever stored
  uint64_t sys_overhead_overall_bytes_components_stored_ = 0;

  uint64_t cache_infrastructure_bytes_memory_usage_ = 0;

  uint64_t overall_num_cache_stores_ = 0;

  /*end statistics */

  void reset_statistics() {
    // Reset cache statistics
    num_cache_hits_ = 0;
    num_cache_look_ups_ = 0;

    // Reset literal search operations
    num_failed_literals_detected_ = 0;
    num_failed_literal_tests_ = 0;
    num_conflicts_ = 0;
    num_decisions_ = 0;
//    num_implications_ = 0;
    num_unit_clauses_ = 0;

    // Reset execution parameters
    sampler_time_elapsed_ = 0.0;
    exit_state_ = SolverExitState::NO_STATE;

    // Reset all sampler only variables
    numb_second_pass_vars_.clear();

    sampler_time_elapsed_ = DBL_MAX;
    sampler_pass_1_time_ = DBL_MAX;
    sampler_pass_2_time_ = DBL_MAX;
  }

  bool cache_full() const {
    return cache_bytes_memory_usage() >= maximum_cache_size_bytes_;
  }

  uint64_t cache_bytes_memory_usage() const {
    return cache_infrastructure_bytes_memory_usage_
           + sum_bytes_cached_components_;
  }

  uint64_t overall_cache_bytes_memory_stored() {
      return cache_infrastructure_bytes_memory_usage_
             + overall_bytes_components_stored_;
    }

  void incorporate_cache_store(CacheableComponent &ccomp) {
    sum_bytes_cached_components_ += ccomp.SizeInBytes();
    sum_size_cached_components_ += ccomp.num_variables();
    num_cached_components_++;
    overall_bytes_components_stored_ += ccomp.SizeInBytes();
    overall_num_cache_stores_ += ccomp.num_variables();
    sys_overhead_sum_bytes_cached_components_ += ccomp.sys_overhead_SizeInBytes();
    sys_overhead_overall_bytes_components_stored_ += ccomp.sys_overhead_SizeInBytes();


    sum_bytes_pure_cached_component_data_ += ccomp.data_only_byte_size();
    overall_bytes_pure_stored_component_data_ += ccomp.data_only_byte_size();
  }
  void incorporate_cache_erase(CacheableComponent &ccomp) {
    sum_bytes_cached_components_ -= ccomp.SizeInBytes();
    sum_size_cached_components_ -= ccomp.num_variables();
    num_cached_components_--;
    sum_bytes_pure_cached_component_data_ -= ccomp.data_only_byte_size();

    sys_overhead_sum_bytes_cached_components_ -= ccomp.sys_overhead_SizeInBytes();
  }

  void incorporate_cache_hit(CacheableComponent &ccomp) {
    num_cache_hits_++;
    sum_cache_hit_sizes_ += ccomp.num_variables();
  }
  unsigned long cache_MB_memory_usage() {
    return cache_bytes_memory_usage() / 1000000;
  }
  mpz_class final_solution_count_ = 0;

  double implicitBCP_miss_rate() {
    if (num_failed_literal_tests_ == 0) return 0.0;
    return (num_failed_literal_tests_ - num_failed_literals_detected_)
           / static_cast<double>(num_failed_literal_tests_);
  }
  unsigned long num_clauses() const {
    return num_long_clauses_ + num_binary_clauses_ + num_unit_clauses_;
  }
  unsigned long num_conflict_clauses() {
    return num_long_conflict_clauses_ + num_binary_conflict_clauses_;
  }

  unsigned long clause_deletion_interval() {
    return 10000 + 10 * times_conflict_clauses_cleaned_;
  }
  void set_final_solution_count(const mpz_class &count) {
    // set final_solution_count_ = count * 2^(num_variables_ - num_used_variables_)
    mpz_mul_2exp(final_solution_count_.get_mpz_t(), count.get_mpz_t(),
                 num_variables_ - num_used_variables_);
  }
  const mpz_class &final_solution_count() const {
    return final_solution_count_;
  }

//  void incorporateConflictClauseData(const std::vector<LiteralID> &clause) {
//    if (clause.size() == 1)
//      num_unit_clauses_++;
//    else if (clause.size() == 2)
//      num_binary_conflict_clauses_++;
//    num_long_conflict_clauses_++;
//  }
  void incorporateClauseData(const std::vector<LiteralID> &clause) {
    if (clause.size() == 1)
      num_unit_clauses_++;
    else if (clause.size() == 2)
      num_binary_clauses_++;
    else
      num_long_clauses_++;
  }

  void printShort();
  void printShortFormulaInfo() {
    std::cout << "variables (all/used/free): \t"
              << num_variables_ << "/" << num_used_variables_ << "/"
              << num_variables_ - num_used_variables_ << "\n"
              << "independent support size:  \t" << num_indep_support_variables_ << "\n";

    std::cout << "clauses (all/long/binary/unit): "
              << num_clauses() << "/" << num_long_clauses_
              << "/" << num_binary_clauses_ << "/" << num_unit_clauses_ << std::endl;
  }
  unsigned long getTime() const {
    return num_decisions_;
  }

  long double getAvgComponentSize() {
    return sum_size_cached_components_ / static_cast<long double>(num_cached_components_);
  }
  unsigned long cached_component_count() {
    return num_cached_components_;
  }
  unsigned long cache_hits() {
    return num_cache_hits_;
  }
  double cache_miss_rate() {
    if (num_cache_look_ups_ == 0) return 0.0;
    return (num_cache_look_ups_ - num_cache_hits_) / static_cast<double>(num_cache_look_ups_);
  }
  long double getAvgCacheHitSize() {
    if (num_cache_hits_ == 0) return 0.0;
    return sum_cache_hit_sizes_ / static_cast<long double>(num_cache_hits_);
  }

  //-----------------------------------------//
  //        Sampler Fields and Methods       //
  //-----------------------------------------//
  double sampler_time_elapsed_ = DBL_MAX;
  double sampler_pass_1_time_ = DBL_MAX;
  double sampler_pass_2_time_ = DBL_MAX;
  std::vector<VariableIndex> numb_second_pass_vars_;
};

#endif /* STATISTICS_H_ */