9 #ifndef CPROVER_SOLVERS_SOLVER_HARDNESS_H
10 #define CPROVER_SOLVERS_SOLVER_HARDNESS_H
17 #include <unordered_map>
18 #include <unordered_set>
77 std::vector<goto_programt::const_targett>
pcs;
89 std::size_t ssa_index,
90 const exprt ssa_expression,
103 const exprt ssa_expression,
104 const std::vector<goto_programt::const_targett> &pcs);
116 const size_t cnf_clause_index,
141 std::vector<std::unordered_map<hardness_ssa_keyt, sat_hardnesst>>
159 return std::hash<std::string>{}(
161 hashed_stats.
pc->source_location.as_string());
Base class for all expressions.
instructionst::const_iterator const_targett
std::vector< literalt > bvt
std::vector< goto_programt::const_targett > pcs
sat_hardnesst sat_hardness
std::string ssa_expression
goto_programt::const_targett pc
bool operator==(const hardness_ssa_keyt &other) const
std::string ssa_expression
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)
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
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
solver_hardnesst & operator=(solver_hardnesst &&)=default
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