CBMC
solver_hardness.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: measure and track the complexity of solver queries
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_SOLVERS_SOLVER_HARDNESS_H
10 #define CPROVER_SOLVERS_SOLVER_HARDNESS_H
11 
14 
15 #include <string>
16 #include <unordered_map>
17 #include <unordered_set>
18 #include <vector>
19 
21 
40 {
41  // From SAT solver we collect the number of clauses, the number of literals
42  // and the number of distinct variables that were used in all clauses.
44  {
45  size_t clauses = 0;
46  size_t literals = 0;
47  std::unordered_set<size_t> variables = {};
48  std::vector<size_t> clause_set = {};
49 
50  sat_hardnesst &operator+=(const sat_hardnesst &other);
51  };
52 
53  // Associate an SSA step expression (the one passed to the solver: the guard
54  // for GOTO; equality for ASSIGN, etc.) with the SAT hardness of the resulting
55  // query. The GOTO and source level instructions are stored as \ref
56  // goto_programt::const_targett.
58  {
59  std::string ssa_expression;
61 
62  bool operator==(const hardness_ssa_keyt &other) const;
63  };
64 
65  // As above but for the special case of multiple assertions, which are
66  // presented to the solver as a single disjunction. Hence we have one SSA
67  // expression (the whole disjunction) and multiple program counters.
69  {
71  std::string ssa_expression;
72  std::vector<goto_programt::const_targett> pcs;
73 
74  bool empty() const;
75  };
76 
83  void register_ssa(
84  std::size_t ssa_index,
85  const exprt &ssa_expression,
87 
88  void register_ssa_size(std::size_t size);
89 
98  const exprt &ssa_expression,
99  const std::vector<goto_programt::const_targett> &pcs);
100 
108  void register_clause(
109  const bvt &bv,
110  const bvt &cnf,
111  const size_t cnf_clause_index,
112  bool register_cnf);
113 
114  void set_outfile(const std::string &file_name);
115 
117  void produce_report();
118 
119  solver_hardnesst() = default;
120 
121  // copying this isn’t really a meaningful operation
124 
125  // copying this isn’t really a meaningful operation
128 
129 private:
130  // A minor modification of \ref goto_programt::output_instruction
132 
133  static std::string expr2string(const exprt &expr);
134 
135  std::string outfile;
136  std::vector<std::unordered_map<hardness_ssa_keyt, sat_hardnesst>>
141  std::size_t max_ssa_set_size;
142 };
143 
144 // NOLINTNEXTLINE(readability/namespace)
145 namespace std
146 {
147 template <>
148 // NOLINTNEXTLINE(readability/identifiers)
149 struct hash<solver_hardnesst::hardness_ssa_keyt>
150 {
151  std::size_t
153  {
154  return std::hash<std::string>{}(
155  hashed_stats.ssa_expression +
156  hashed_stats.pc->source_location().as_string());
157  }
158 };
159 } // namespace std
160 
161 static inline void with_solver_hardness(
162  decision_proceduret &maybe_hardness_collector,
163  std::function<void(solver_hardnesst &hardness)> handler)
164 {
165  // FIXME I am wondering if there is a way to do this that is a bit less
166  // dynamically typed.
167  if(
168  auto prop_conv_solver =
169  dynamic_cast<prop_conv_solvert *>(&maybe_hardness_collector))
170  {
171  if(auto hardness_collector = prop_conv_solver->get_hardness_collector())
172  {
173  if(hardness_collector->solver_hardness)
174  {
175  auto &solver_hardness = static_cast<solver_hardnesst &>(
176  *(hardness_collector->solver_hardness));
177  handler(solver_hardness);
178  }
179  }
180  }
181 }
182 
183 #endif // CPROVER_SOLVERS_SOLVER_HARDNESS_H
An interface for a decision procedure for satisfiability problems.
Base class for all expressions.
Definition: expr.h:56
instructionst::const_iterator const_targett
Definition: goto_program.h:615
Concrete Goto Program.
Capability to collect the statistics of the complexity of individual solver queries.
std::vector< literalt > bvt
Definition: literal.h:201
static void with_solver_hardness(decision_proceduret &maybe_hardness_collector, std::function< void(solver_hardnesst &hardness)> handler)
std::vector< goto_programt::const_targett > pcs
goto_programt::const_targett pc
bool operator==(const hardness_ssa_keyt &other) const
sat_hardnesst & operator+=(const sat_hardnesst &other)
std::vector< size_t > clause_set
std::unordered_set< size_t > variables
A structure that facilitates collecting the complexity statistics from a decision procedure.
sat_hardnesst current_hardness
static std::string expr2string(const exprt &expr)
assertion_statst assertion_stats
void set_outfile(const std::string &file_name)
solver_hardnesst & operator=(const solver_hardnesst &)=delete
void register_clause(const bvt &bv, const bvt &cnf, const size_t cnf_clause_index, bool register_cnf)
Called e.g.
hardness_ssa_keyt current_ssa_key
solver_hardnesst()=default
void register_ssa(std::size_t ssa_index, const exprt &ssa_expression, goto_programt::const_targett pc)
Called from the symtex_target_equationt::convert_*, this function associates an SSA step to all the s...
solver_hardnesst & operator=(solver_hardnesst &&)=default
std::string outfile
void register_assertion_ssas(const exprt &ssa_expression, const std::vector< goto_programt::const_targett > &pcs)
Called from the symtex_target_equationt::convert_assertions, this function associates the disjunction...
std::vector< std::unordered_map< hardness_ssa_keyt, sat_hardnesst > > hardness_stats
std::size_t max_ssa_set_size
void produce_report()
Print the statistics to a JSON file (specified via command-line option).
solver_hardnesst(solver_hardnesst &&)=default
static std::string goto_instruction2string(goto_programt::const_targett pc)
solver_hardnesst(const solver_hardnesst &)=delete
void register_ssa_size(std::size_t size)
std::size_t operator()(const solver_hardnesst::hardness_ssa_keyt &hashed_stats) const