cprover
solver_hardness.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: measure and track the complexity of solver queries
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
9#ifndef CPROVER_SOLVERS_SOLVER_HARDNESS_H
10#define CPROVER_SOLVERS_SOLVER_HARDNESS_H
11
14
15#include <fstream>
16#include <string>
17#include <unordered_map>
18#include <unordered_set>
19#include <vector>
20
22
23#include <util/optional.h>
24
43{
44 // From SAT solver we collect the number of clauses, the number of literals
45 // and the number of distinct variables that were used in all clauses.
47 {
48 size_t clauses = 0;
49 size_t literals = 0;
50 std::unordered_set<size_t> variables = {};
51 std::vector<size_t> clause_set = {};
52
54 };
55
56 // Associate an SSA step expression (the one passed to the solver: the guard
57 // for GOTO; equality for ASSIGN, etc.) with the SAT hardness of the resulting
58 // query. The GOTO and source level instructions are stored as \ref
59 // goto_programt::const_targett.
61 {
62 std::string ssa_expression;
64
65 bool operator==(const hardness_ssa_keyt &other) const;
66 };
67
68 // As above but for the special case of multiple assertions, which are
69 // presented to the solver as a single disjunction. Hence we have one SSA
70 // expression (the whole disjunction) and multiple program counters.
72 {
74 std::string ssa_expression;
75 std::vector<goto_programt::const_targett> pcs;
76
77 bool empty() const;
78 };
79
86 void register_ssa(
87 std::size_t ssa_index,
88 const exprt ssa_expression,
90
91 void register_ssa_size(std::size_t size);
92
101 const exprt ssa_expression,
102 const std::vector<goto_programt::const_targett> &pcs);
103
111 void register_clause(
112 const bvt &bv,
113 const bvt &cnf,
114 const size_t cnf_clause_index,
115 bool register_cnf);
116
117 void set_outfile(const std::string &file_name);
118
120 void produce_report();
121
122 solver_hardnesst() = default;
123
124 // copying this isn’t really a meaningful operation
127
128 // copying this isn’t really a meaningful operation
131
132private:
133 // A minor modification of \ref goto_programt::output_instruction
135
136 static std::string expr2string(const exprt expr);
137
138 std::string outfile;
139 std::vector<std::unordered_map<hardness_ssa_keyt, sat_hardnesst>>
144 std::size_t max_ssa_set_size;
145};
146
147// NOLINTNEXTLINE(readability/namespace)
148namespace std
149{
150template <>
151// NOLINTNEXTLINE(readability/identifiers)
152struct hash<solver_hardnesst::hardness_ssa_keyt>
153{
154 std::size_t
156 {
157 return std::hash<std::string>{}(
158 hashed_stats.ssa_expression +
159 hashed_stats.pc->source_location().as_string());
160 }
161};
162} // namespace std
163
164static inline void with_solver_hardness(
165 decision_proceduret &maybe_hardness_collector,
166 std::function<void(solver_hardnesst &hardness)> handler)
167{
168 // FIXME I am wondering if there is a way to do this that is a bit less
169 // dynamically typed.
170 if(
171 auto prop_conv_solver =
172 dynamic_cast<prop_conv_solvert *>(&maybe_hardness_collector))
173 {
174 if(auto hardness_collector = prop_conv_solver->get_hardness_collector())
175 {
176 if(hardness_collector->solver_hardness)
177 {
178 auto &solver_hardness = static_cast<solver_hardnesst &>(
179 *(hardness_collector->solver_hardness));
180 handler(solver_hardness);
181 }
182 }
183 }
184}
185
186#endif // CPROVER_SOLVERS_SOLVER_HARDNESS_H
Base class for all expressions.
Definition: expr.h:54
instructionst::const_iterator const_targett
Definition: goto_program.h:593
Concrete Goto Program.
Capability to collect the statistics of the complexity of individual solver queries.
std::vector< literalt > bvt
Definition: literal.h:201
STL namespace.
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
assertion_statst assertion_stats
void set_outfile(const std::string &file_name)
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...
static std::string expr2string(const exprt expr)
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
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...
solver_hardnesst()=default
std::string outfile
solver_hardnesst & operator=(solver_hardnesst &&)=default
solver_hardnesst & operator=(const solver_hardnesst &)=delete
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