cprover
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 
12 #include <solvers/prop/literal.h>
13 
14 #include <fstream>
15 #include <sstream>
16 #include <string>
17 #include <unordered_map>
18 #include <unordered_set>
19 #include <vector>
20 
21 #include <iostream>
22 
24 
25 #include <util/optional.h>
26 
45 {
46  // From SAT solver we collect the number of clauses, the number of literals
47  // and the number of distinct variables that were used in all clauses.
49  {
50  size_t clauses = 0;
51  size_t literals = 0;
52  std::unordered_set<size_t> variables = {};
53 
54  sat_hardnesst &operator+=(const sat_hardnesst &other);
55  };
56 
57  // Associate an SSA step expression (the one passed to the solver: the guard
58  // for GOTO; equality for ASSIGN, etc.) with the SAT hardness of the resulting
59  // query. The GOTO and source level instructions are stored as \ref
60  // goto_programt::const_targett.
62  {
63  std::string ssa_expression;
65 
66  bool operator==(const hardness_ssa_keyt &other) const;
67  };
68 
69  // As above but for the special case of multiple assertions, which are
70  // presented to the solver as a single disjunction. Hence we have one SSA
71  // expression (the whole disjunction) and multiple program counters.
73  {
75  std::string ssa_expression;
76  std::vector<goto_programt::const_targett> pcs;
77 
78  bool empty() const;
79  };
80 
87  void register_ssa(
88  std::size_t ssa_index,
89  const exprt ssa_expression,
91 
92  void register_ssa_size(std::size_t size);
93 
102  const exprt ssa_expression,
103  const std::vector<goto_programt::const_targett> &pcs);
104 
108  void register_clause(const bvt &bv);
109 
110  void set_outfile(const std::string &file_name);
111 
113  void produce_report();
114 
115  solver_hardnesst() = default;
116 
117  // copying this isn’t really a meaningful operation
120 
121  // copying this isn’t really a meaningful operation
124 
125 private:
126  // A minor modification of \ref goto_programt::output_instruction
128 
129  static std::string expr2string(const exprt expr);
130 
131  std::string outfile;
132  std::vector<std::unordered_map<hardness_ssa_keyt, sat_hardnesst>>
137  std::size_t max_ssa_set_size;
138 };
139 
140 // NOLINTNEXTLINE(readability/namespace)
141 namespace std
142 {
143 template <>
144 // NOLINTNEXTLINE(readability/identifiers)
145 struct hash<solver_hardnesst::hardness_ssa_keyt>
146 {
147  std::size_t
149  {
150  return std::hash<std::string>{}(
151  hashed_stats.ssa_expression +
152  hashed_stats.pc->source_location.as_string());
153  }
154 };
155 } // namespace std
156 
157 #endif // CPROVER_SOLVERS_SOLVER_HARDNESS_H
solver_hardnesst::register_ssa_size
void register_ssa_size(std::size_t size)
Definition: solver_hardness.cpp:67
std::hash< solver_hardnesst::hardness_ssa_keyt >::operator()
std::size_t operator()(const solver_hardnesst::hardness_ssa_keyt &hashed_stats) const
Definition: solver_hardness.h:148
solver_hardnesst::sat_hardnesst
Definition: solver_hardness.h:49
bvt
std::vector< literalt > bvt
Definition: literal.h:201
optional.h
solver_hardnesst::expr2string
static std::string expr2string(const exprt expr)
Definition: solver_hardness.cpp:346
solver_hardnesst::goto_instruction2string
static std::string goto_instruction2string(goto_programt::const_targett pc)
Definition: solver_hardness.cpp:193
exprt
Base class for all expressions.
Definition: expr.h:53
solver_hardnesst::solver_hardnesst
solver_hardnesst(solver_hardnesst &&)=default
solver_hardnesst::solver_hardnesst
solver_hardnesst(const solver_hardnesst &)=delete
solver_hardnesst::assertion_stats
assertion_statst assertion_stats
Definition: solver_hardness.h:136
solver_hardnesst::current_ssa_key
hardness_ssa_keyt current_ssa_key
Definition: solver_hardness.h:134
solver_hardnesst::hardness_ssa_keyt::ssa_expression
std::string ssa_expression
Definition: solver_hardness.h:63
solver_hardnesst::assertion_statst::pcs
std::vector< goto_programt::const_targett > pcs
Definition: solver_hardness.h:76
solver_hardnesst::sat_hardnesst::variables
std::unordered_set< size_t > variables
Definition: solver_hardness.h:52
solver_hardnesst::sat_hardnesst::clauses
size_t clauses
Definition: solver_hardness.h:50
solver_hardnesst::register_clause
void register_clause(const bvt &bv)
Called e.g.
Definition: solver_hardness.cpp:90
solver_hardnesst::operator=
solver_hardnesst & operator=(solver_hardnesst &&)=default
solver_hardnesst::outfile
std::string outfile
Definition: solver_hardness.h:131
solver_hardnesst::assertion_statst::sat_hardness
sat_hardnesst sat_hardness
Definition: solver_hardness.h:74
solver_hardnesst::operator=
solver_hardnesst & operator=(const solver_hardnesst &)=delete
solver_hardnesst::hardness_stats
std::vector< std::unordered_map< hardness_ssa_keyt, sat_hardnesst > > hardness_stats
Definition: solver_hardness.h:133
solver_hardnesst::assertion_statst
Definition: solver_hardness.h:73
solver_hardnesst::register_ssa
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...
Definition: solver_hardness.cpp:46
solver_hardnesst::register_assertion_ssas
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...
Definition: solver_hardness.cpp:76
literal.h
goto_program.h
Concrete Goto Program.
solver_hardnesst::set_outfile
void set_outfile(const std::string &file_name)
Definition: solver_hardness.cpp:100
solver_hardnesst
A structure that facilitates collecting the complexity statistics from a decision procedure.
Definition: solver_hardness.h:45
solver_hardnesst::solver_hardnesst
solver_hardnesst()=default
solver_hardnesst::max_ssa_set_size
std::size_t max_ssa_set_size
Definition: solver_hardness.h:137
solver_hardnesst::sat_hardnesst::literals
size_t literals
Definition: solver_hardness.h:51
solver_hardnesst::hardness_ssa_keyt::operator==
bool operator==(const hardness_ssa_keyt &other) const
Definition: solver_hardness.cpp:33
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
solver_hardnesst::hardness_ssa_keyt::pc
goto_programt::const_targett pc
Definition: solver_hardness.h:64
solver_hardnesst::produce_report
void produce_report()
Print the statistics to a JSON file (specified via command-line option).
Definition: solver_hardness.cpp:105
solver_hardnesst::assertion_statst::empty
bool empty() const
Definition: solver_hardness.cpp:41
solver_hardnesst::hardness_ssa_keyt
Definition: solver_hardness.h:62
solver_hardnesst::current_hardness
sat_hardnesst current_hardness
Definition: solver_hardness.h:135
solver_hardnesst::sat_hardnesst::operator+=
sat_hardnesst & operator+=(const sat_hardnesst &other)
Definition: solver_hardness.cpp:24
solver_hardnesst::assertion_statst::ssa_expression
std::string ssa_expression
Definition: solver_hardness.h:75