solver_hardness.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: measure and track the complexity of solver queries
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
#ifndef CPROVER_SOLVERS_SOLVER_HARDNESS_H
#define CPROVER_SOLVERS_SOLVER_HARDNESS_H
 
#include <solvers/hardness_collector.h>
#include <solvers/prop/prop_conv_solver.h>
 
#include <fstream>
#include <string>
#include <unordered_map>
#include <unordered_set>
#include <vector>
 
#include <goto-programs/goto_program.h>
 
#include <util/optional.h>
 
struct solver_hardnesst : public clause_hardness_collectort
{
  // From SAT solver we collect the number of clauses, the number of literals
  // and the number of distinct variables that were used in all clauses.
  struct sat_hardnesst
  {
    size_t clauses = 0;
    size_t literals = 0;
    std::unordered_set<size_t> variables = {};
    std::vector<size_t> clause_set = {};
 
    sat_hardnesst &operator+=(const sat_hardnesst &other);
  };
 
  // Associate an SSA step expression (the one passed to the solver: the guard
  // for GOTO; equality for ASSIGN, etc.) with the SAT hardness of the resulting
  // query. The GOTO and source level instructions are stored as \ref
  // goto_programt::const_targett.
  struct hardness_ssa_keyt
  {
    std::string ssa_expression;
    goto_programt::const_targett pc;
 
    bool operator==(const hardness_ssa_keyt &other) const;
  };
 
  // As above but for the special case of multiple assertions, which are
  // presented to the solver as a single disjunction. Hence we have one SSA
  // expression (the whole disjunction) and multiple program counters.
  struct assertion_statst
  {
    sat_hardnesst sat_hardness;
    std::string ssa_expression;
    std::vector<goto_programt::const_targett> pcs;
 
    bool empty() const;
  };
 
  void register_ssa(
    std::size_t ssa_index,
    const exprt ssa_expression,
    goto_programt::const_targett pc);
 
  void register_ssa_size(std::size_t size);
 
  void register_assertion_ssas(
    const exprt ssa_expression,
    const std::vector<goto_programt::const_targett> &pcs);
 
  void register_clause(
    const bvt &bv,
    const bvt &cnf,
    const size_t cnf_clause_index,
    bool register_cnf);
 
  void set_outfile(const std::string &file_name);
 
  void produce_report();
 
  solver_hardnesst() = default;
 
  // copying this isn’t really a meaningful operation
  solver_hardnesst(const solver_hardnesst &) = delete;
  solver_hardnesst(solver_hardnesst &&) = default;
 
  // copying this isn’t really a meaningful operation
  solver_hardnesst &operator=(const solver_hardnesst &) = delete;
  solver_hardnesst &operator=(solver_hardnesst &&) = default;
 
private:
  // A minor modification of \ref goto_programt::output_instruction
  static std::string goto_instruction2string(goto_programt::const_targett pc);
 
  static std::string expr2string(const exprt expr);
 
  std::string outfile;
  std::vector<std::unordered_map<hardness_ssa_keyt, sat_hardnesst>>
    hardness_stats;
  hardness_ssa_keyt current_ssa_key;
  sat_hardnesst current_hardness;
  assertion_statst assertion_stats;
  std::size_t max_ssa_set_size;
};
 
// NOLINTNEXTLINE(readability/namespace)
namespace std
{
template <>
// NOLINTNEXTLINE(readability/identifiers)
struct hash<solver_hardnesst::hardness_ssa_keyt>
{
  std::size_t
  operator()(const solver_hardnesst::hardness_ssa_keyt &hashed_stats) const
  {
    return std::hash<std::string>{}(
      hashed_stats.ssa_expression +
      hashed_stats.pc->source_location().as_string());
  }
};
} // namespace std
 
static inline void with_solver_hardness(
  decision_proceduret &maybe_hardness_collector,
  std::function<void(solver_hardnesst &hardness)> handler)
{
  // FIXME I am wondering if there is a way to do this that is a bit less
  // dynamically typed.
  if(
    auto prop_conv_solver =
      dynamic_cast<prop_conv_solvert *>(&maybe_hardness_collector))
  {
    if(auto hardness_collector = prop_conv_solver->get_hardness_collector())
    {
      if(hardness_collector->solver_hardness)
      {
        auto &solver_hardness = static_cast<solver_hardnesst &>(
          *(hardness_collector->solver_hardness));
        handler(solver_hardness);
      }
    }
  }
}
 
#endif // CPROVER_SOLVERS_SOLVER_HARDNESS_H