dReal4
icp_stat.h
1 #pragma once
2 
3 #include <atomic>
4 
5 #include "dreal/util/stat.h"
6 #include "dreal/util/timer.h"
7 
8 namespace dreal {
9 
10 /// A class to show statistics information at destruction. We have a
11 /// static instance in Icp::CheckSat() to keep track of the numbers of
12 /// branching and pruning operations.
13 class IcpStat : public Stat {
14  public:
15  explicit IcpStat(const bool enabled, int id = 0)
16  : Stat{enabled}, thread_id_{id} {}
17  IcpStat(const IcpStat&) = delete;
18  IcpStat(IcpStat&&) = delete;
19  IcpStat& operator=(const IcpStat&) = delete;
20  IcpStat& operator=(IcpStat&&) = delete;
21  ~IcpStat() override;
22 
23  const int thread_id_;
24 
25  std::atomic<int> num_branch_{0};
26  std::atomic<int> num_prune_{0};
27 
28  Timer timer_branch_;
29  Timer timer_prune_;
30  Timer timer_eval_;
31 };
32 } // namespace dreal
bool enabled() const
Returns true if the logging is enabled.
Definition: stat.h:20
Sum type of symbolic::Expression and symbolic::Formula.
Definition: api.cc:9
A class to show statistics information at destruction.
Definition: icp_stat.h:13
Base class for statistics.
Definition: stat.h:8
Simple timer class to profile performance.
Definition: timer.h:10