7 #ifdef SMTRAT_DEVOPTION_Statistics
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;
22 bool enabled()
const {
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);
36 void implicant_used(std::size_t
sotd) {
37 m_num_implicants_used++;
38 m_implicant_sotd.add(
sotd);
40 void implicants_found(std::size_t num) {
41 m_num_implicants_found+=num;
43 void intervals_used(std::size_t num) {
44 m_num_intervals_used+=num;
46 void intervals_found(std::size_t num) {
47 m_num_intervals_found+=num;
50 void formula_evaluation_start() {
51 m_formula_evaluation.start_this();
53 void formula_evaluation_end() {
54 m_formula_evaluation.finish();
58 bool last_block_bool =
true;
59 for (
auto it = var_order.rbegin(); it != var_order.rend(); it++) {
60 if (last_block_bool) {
62 if (var_mapping.find(*it) == var_mapping.end()) last_block_bool =
false;
65 if (var_mapping.find(*it) != var_mapping.end()) m_bool_var_not_at_end++;
72 CoveringNGStatistics &statistics();
std::vector< carl::Variable > VariableOrdering
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