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 
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 
40  {
41  }
42 };
43 
45 {
46 public:
47  std::unique_ptr<clause_hardness_collectort> solver_hardness;
48 };
49 
50 #endif // CPROVER_SOLVERS_HARDNESS_COLLECTOR_H
virtual void register_clause(const bvt &bv, const bvt &cnf, const size_t cnf_clause_index, bool register_cnf)=0
Called e.g.
std::unique_ptr< clause_hardness_collectort > solver_hardness
std::vector< literalt > bvt
Definition: literal.h:201
A structure that facilitates collecting the complexity statistics from a decision procedure.