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>
18
#include <
solvers/solver_hardness.h
>
19
20
class
exprt
;
21
22
class
hardness_collectort
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>
32
void
with_solver_hardness
(
33
T &maybe_hardness_collector,
34
hardness_collectort::handlert
handler)
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
solvers
hardness_collector.h
Generated by
1.8.20