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  std::vector<size_t> clause_set = {};
54 
55  sat_hardnesst &operator+=(const sat_hardnesst &other);
56  };
57 
58  // Associate an SSA step expression (the one passed to the solver: the guard
59  // for GOTO; equality for ASSIGN, etc.) with the SAT hardness of the resulting
60  // query. The GOTO and source level instructions are stored as \ref
61  // goto_programt::const_targett.
63  {
64  std::string ssa_expression;
66 
67  bool operator==(const hardness_ssa_keyt &other) const;
68  };
69 
70  // As above but for the special case of multiple assertions, which are
71  // presented to the solver as a single disjunction. Hence we have one SSA
72  // expression (the whole disjunction) and multiple program counters.
74  {
76  std::string ssa_expression;
77  std::vector<goto_programt::const_targett> pcs;
78 
79  bool empty() const;
80  };
81 
88  void register_ssa(
89  std::size_t ssa_index,
90  const exprt ssa_expression,
92 
93  void register_ssa_size(std::size_t size);
94 
103  const exprt ssa_expression,
104  const std::vector<goto_programt::const_targett> &pcs);
105 
113  void register_clause(
114  const bvt &bv,
115  const bvt &cnf,
116  const size_t cnf_clause_index,
117  bool register_cnf);
118 
119  void set_outfile(const std::string &file_name);
120 
122  void produce_report();
123 
124  solver_hardnesst() = default;
125 
126  // copying this isn’t really a meaningful operation
129 
130  // copying this isn’t really a meaningful operation
133 
134 private:
135  // A minor modification of \ref goto_programt::output_instruction
137 
138  static std::string expr2string(const exprt expr);
139 
140  std::string outfile;
141  std::vector<std::unordered_map<hardness_ssa_keyt, sat_hardnesst>>
146  std::size_t max_ssa_set_size;
147 };
148 
149 // NOLINTNEXTLINE(readability/namespace)
150 namespace std
151 {
152 template <>
153 // NOLINTNEXTLINE(readability/identifiers)
154 struct hash<solver_hardnesst::hardness_ssa_keyt>
155 {
156  std::size_t
158  {
159  return std::hash<std::string>{}(
160  hashed_stats.ssa_expression +
161  hashed_stats.pc->source_location.as_string());
162  }
163 };
164 } // namespace std
165 
166 #endif // CPROVER_SOLVERS_SOLVER_HARDNESS_H
solver_hardnesst::register_ssa_size
void register_ssa_size(std::size_t size)
Definition: solver_hardness.cpp:69
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:157
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:381
solver_hardnesst::goto_instruction2string
static std::string goto_instruction2string(goto_programt::const_targett pc)
Definition: solver_hardness.cpp:228
exprt
Base class for all expressions.
Definition: expr.h:54
solver_hardnesst::solver_hardnesst
solver_hardnesst(solver_hardnesst &&)=default
solver_hardnesst::solver_hardnesst
solver_hardnesst(const solver_hardnesst &)=delete
solver_hardnesst::register_clause
void register_clause(const bvt &bv, const bvt &cnf, const size_t cnf_clause_index, bool register_cnf)
Called e.g.
Definition: solver_hardness.cpp:92
solver_hardnesst::assertion_stats
assertion_statst assertion_stats
Definition: solver_hardness.h:145
solver_hardnesst::current_ssa_key
hardness_ssa_keyt current_ssa_key
Definition: solver_hardness.h:143
solver_hardnesst::hardness_ssa_keyt::ssa_expression
std::string ssa_expression
Definition: solver_hardness.h:64
solver_hardnesst::assertion_statst::pcs
std::vector< goto_programt::const_targett > pcs
Definition: solver_hardness.h:77
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::sat_hardnesst::clause_set
std::vector< size_t > clause_set
Definition: solver_hardness.h:53
solver_hardnesst::operator=
solver_hardnesst & operator=(solver_hardnesst &&)=default
solver_hardnesst::outfile
std::string outfile
Definition: solver_hardness.h:140
solver_hardnesst::assertion_statst::sat_hardness
sat_hardnesst sat_hardness
Definition: solver_hardness.h:75
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:142
solver_hardnesst::assertion_statst
Definition: solver_hardness.h:74
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:48
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:78
literal.h
goto_program.h
Concrete Goto Program.
solver_hardnesst::set_outfile
void set_outfile(const std::string &file_name)
Definition: solver_hardness.cpp:118
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:146
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:35
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:551
solver_hardnesst::hardness_ssa_keyt::pc
goto_programt::const_targett pc
Definition: solver_hardness.h:65
solver_hardnesst::produce_report
void produce_report()
Print the statistics to a JSON file (specified via command-line option).
Definition: solver_hardness.cpp:123
solver_hardnesst::assertion_statst::empty
bool empty() const
Definition: solver_hardness.cpp:43
solver_hardnesst::hardness_ssa_keyt
Definition: solver_hardness.h:63
solver_hardnesst::current_hardness
sat_hardnesst current_hardness
Definition: solver_hardness.h:144
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:76