SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
CoveringNGStatistics.h
Go to the documentation of this file.
1 #pragma once
2 
3 
5 #include "types.h"
6 
7 #ifdef SMTRAT_DEVOPTION_Statistics
8 
9 
10 namespace smtrat::covering_ng {
11 
12 class CoveringNGStatistics : public Statistics {
13  carl::statistics::Timer m_formula_evaluation;
14  carl::statistics::Series m_implicant_sotd;
15  std::size_t m_num_implicants_used;
16  std::size_t m_num_implicants_found;
17  std::size_t m_num_intervals_used;
18  std::size_t m_num_intervals_found;
19  std::size_t m_bool_var_not_at_end;
20 
21 public:
22  bool enabled() const {
23  return true;
24  }
25 
26  void collect() {
27  Statistics::addKeyValuePair("formula_evaluation", m_formula_evaluation);
28  Statistics::addKeyValuePair("implicants.used.sotd", m_implicant_sotd);
29  Statistics::addKeyValuePair("implicants.used.num", m_num_implicants_used);
30  Statistics::addKeyValuePair("implicants.found.num", m_num_implicants_found);
31  Statistics::addKeyValuePair("intervals.used.num", m_num_intervals_used);
32  Statistics::addKeyValuePair("intervals.found.num", m_num_intervals_found);
33  Statistics::addKeyValuePair("var_order.bool_var_not_at_end.num", m_bool_var_not_at_end);
34  }
35 
36  void implicant_used(std::size_t sotd) {
37  m_num_implicants_used++;
38  m_implicant_sotd.add(sotd);
39  }
40  void implicants_found(std::size_t num) {
41  m_num_implicants_found+=num;
42  }
43  void intervals_used(std::size_t num) {
44  m_num_intervals_used+=num;
45  }
46  void intervals_found(std::size_t num) {
47  m_num_intervals_found+=num;
48  }
49 
50  void formula_evaluation_start() {
51  m_formula_evaluation.start_this();
52  }
53  void formula_evaluation_end() {
54  m_formula_evaluation.finish();
55  }
56 
57  void variable_ordering(const cadcells::VariableOrdering& var_order, const std::map<carl::Variable, carl::Variable>& var_mapping) {
58  bool last_block_bool = true;
59  for (auto it = var_order.rbegin(); it != var_order.rend(); it++) {
60  if (last_block_bool) {
61  // if we are in the last block of booleans and see a non-Boolean variable, then we just left the last block consisting of booleans
62  if (var_mapping.find(*it) == var_mapping.end()) last_block_bool = false;
63  } else {
64  // if we are not in the last block of booleans and we see a Boolean variable, then we increase the counter
65  if (var_mapping.find(*it) != var_mapping.end()) m_bool_var_not_at_end++;
66  }
67  }
68  }
69 
70 };
71 
72 CoveringNGStatistics &statistics();
73 
74 }
75 
76 #endif
std::vector< carl::Variable > VariableOrdering
Definition: common.h:11
bool sotd(cadcells::datastructures::Projections &proj, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &a, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &b)
Dolzmann et al 2004.
std::vector< carl::Variable > variable_ordering(const carl::QuantifierPrefix &quantifiers, const FormulaT &formula)
Calculates a variable ordering based on the given quantifier blocks and the given formula.
carl::statistics::Statistics Statistics
Definition: Statistics.h:7