cprover
hardness_collector.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Capability to collect the statistics of the complexity of individual
4  solver queries.
5 
6 Author: Diffblue Ltd.
7 
8 \*******************************************************************/
9 
13 
14 #ifndef CPROVER_SOLVERS_HARDNESS_COLLECTOR_H
15 #define CPROVER_SOLVERS_HARDNESS_COLLECTOR_H
16 
17 #include <functional>
19 
20 class exprt;
21 
23 {
24 public:
25  using handlert = std::function<void(solver_hardnesst &)>;
26  virtual void with_solver_hardness(handlert handler) = 0;
27  virtual void enable_hardness_collection() = 0;
28  virtual ~hardness_collectort() = default;
29 };
30 
31 template <typename T>
33  T &maybe_hardness_collector,
35 {
36  // FIXME I am wondering if there is a way to do this that is a bit less
37  // dynamically typed.
38  if(
39  auto hardness_collector =
40  dynamic_cast<hardness_collectort *>(&maybe_hardness_collector))
41  {
42  hardness_collector->with_solver_hardness(handler);
43  }
44 }
45 #endif // CPROVER_SOLVERS_HARDNESS_COLLECTOR_H
hardness_collectort::enable_hardness_collection
virtual void enable_hardness_collection()=0
hardness_collectort::handlert
std::function< void(solver_hardnesst &)> handlert
Definition: hardness_collector.h:25
hardness_collectort::with_solver_hardness
virtual void with_solver_hardness(handlert handler)=0
solver_hardness.h
exprt
Base class for all expressions.
Definition: expr.h:53
hardness_collectort::~hardness_collectort
virtual ~hardness_collectort()=default
solver_hardnesst
A structure that facilitates collecting the complexity statistics from a decision procedure.
Definition: solver_hardness.h:45
hardness_collectort
Definition: hardness_collector.h:23
with_solver_hardness
void with_solver_hardness(T &maybe_hardness_collector, hardness_collectort::handlert handler)
Definition: hardness_collector.h:32