SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
VSStatistics.h
Go to the documentation of this file.
1 #pragma once
2 
4 
5 #ifdef SMTRAT_DEVOPTION_Statistics
6 
7 namespace smtrat {
8 namespace mcsat {
9 
10 class VSStatistics : public Statistics {
11 private:
12  std::size_t mExplanationCalled = 0;
13  std::size_t mExplanationSuccess = 0;
14 
15 public:
16  bool enabled() const {
17  return (mExplanationCalled > 0) || (mExplanationSuccess > 0);
18  }
19  void collect() {
20  Statistics::addKeyValuePair("explanation_called", mExplanationCalled);
21  Statistics::addKeyValuePair("explanation_success", mExplanationSuccess);
22  }
23 
24  void explanationCalled() {
25  ++mExplanationCalled;
26  }
27 
28  void explanationSuccess() {
29  ++mExplanationSuccess;
30  }
31 };
32 
33 } // namespace mcsat
34 } // namespace smtrat
35 
36 #endif
Class to create the formulas for axioms.
carl::statistics::Statistics Statistics
Definition: Statistics.h:7