CBMC
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 <
solvers/prop/literal.h
>
18
19
#include <memory>
20
21
struct
solver_hardnesst
;
22
23
class
clause_hardness_collectort
24
{
25
public
:
33
virtual
void
register_clause
(
34
const
bvt
&bv,
35
const
bvt
&cnf,
36
const
size_t
cnf_clause_index,
37
bool
register_cnf) = 0;
38
39
virtual
~clause_hardness_collectort
()
40
{
41
}
42
};
43
44
class
hardness_collectort
45
{
46
public
:
47
std::unique_ptr<clause_hardness_collectort>
solver_hardness
;
48
};
49
50
#endif // CPROVER_SOLVERS_HARDNESS_COLLECTOR_H
clause_hardness_collectort::register_clause
virtual void register_clause(const bvt &bv, const bvt &cnf, const size_t cnf_clause_index, bool register_cnf)=0
Called e.g.
hardness_collectort::solver_hardness
std::unique_ptr< clause_hardness_collectort > solver_hardness
Definition:
hardness_collector.h:47
bvt
std::vector< literalt > bvt
Definition:
literal.h:201
clause_hardness_collectort
Definition:
hardness_collector.h:23
literal.h
solver_hardnesst
A structure that facilitates collecting the complexity statistics from a decision procedure.
Definition:
solver_hardness.h:42
hardness_collectort
Definition:
hardness_collector.h:44
clause_hardness_collectort::~clause_hardness_collectort
virtual ~clause_hardness_collectort()
Definition:
hardness_collector.h:39
src
solvers
hardness_collector.h
Generated by
1.8.17