cprover
|
A structure that facilitates collecting the complexity statistics from a decision procedure. More...
#include <solver_hardness.h>
Classes | |
struct | assertion_statst |
struct | hardness_ssa_keyt |
struct | sat_hardnesst |
Public Member Functions | |
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 solver queries collected since the last call. More... | |
void | register_ssa_size (std::size_t size) |
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 of assertions to all the solver queries collected since the last call. More... | |
void | register_clause (const bvt &bv, const bvt &cnf, const size_t cnf_clause_index, bool register_cnf) |
Called e.g. More... | |
void | set_outfile (const std::string &file_name) |
void | produce_report () |
Print the statistics to a JSON file (specified via command-line option). More... | |
solver_hardnesst ()=default | |
solver_hardnesst (const solver_hardnesst &)=delete | |
solver_hardnesst (solver_hardnesst &&)=default | |
solver_hardnesst & | operator= (const solver_hardnesst &)=delete |
solver_hardnesst & | operator= (solver_hardnesst &&)=default |
Static Private Member Functions | |
static std::string | goto_instruction2string (goto_programt::const_targett pc) |
static std::string | expr2string (const exprt expr) |
Private Attributes | |
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 |
A structure that facilitates collecting the complexity statistics from a decision procedure.
The idea is to associate some solver complexity metric with each line-of-code, GOTO instruction, and SSA step. The motivation is to be able to track the impact of (1) which C instruction to use on the code level, (2) which GOTO instruction to generate when parsing the source or running internal optimisations, (3) which SSA step to produce for each GOTO instruction, etc.
In terms of a SAT solver the complexity metric can be number of clauses/literals/variables.
The object of this type should be visible from the symex_target_equationt (so that we can register which SSA/GOTO/program counter was passed to the solver) and from some decision procedure (e.g. a derived class of cnft for SAT solving). For this purpose the object lives in the solver_factoryt::solvert and pointers are passed to both decision_proceduret and propt.
Definition at line 41 of file solver_hardness.h.
|
default |
|
delete |
|
default |
|
staticprivate |
Definition at line 379 of file solver_hardness.cpp.
|
staticprivate |
Definition at line 223 of file solver_hardness.cpp.
|
delete |
|
default |
void solver_hardnesst::produce_report | ( | ) |
Print the statistics to a JSON file (specified via command-line option).
Definition at line 118 of file solver_hardness.cpp.
void solver_hardnesst::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 of assertions to all the solver queries collected since the last call.
ssa_expression | string representing the disjuction of SSA assertions |
pcs | all GOTO instruction iterators that contributed in the disjunction |
Definition at line 73 of file solver_hardness.cpp.
void solver_hardnesst::register_clause | ( | const bvt & | bv, |
const bvt & | cnf, | ||
const size_t | cnf_clause_index, | ||
bool | register_cnf | ||
) |
Called e.g.
from the satcheck_minisat2::lcnf
, this function adds the complexity statistics from the last SAT query to the current_ssa_key
.
bv | the clause (vector of literals) |
cnf | processed clause |
cnf_clause_index | index of clause in dimacs output |
register_cnf | negation of boolean variable tracking if the clause can be eliminated |
Definition at line 87 of file solver_hardness.cpp.
void solver_hardnesst::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 solver queries collected since the last call.
ssa_index | position (of this step) in the SSA equation |
ssa_expression | string representing the SSA step expression |
pc | the GOTO instruction iterator for this SSA step |
Definition at line 43 of file solver_hardness.cpp.
void solver_hardnesst::register_ssa_size | ( | std::size_t | size | ) |
Definition at line 64 of file solver_hardness.cpp.
void solver_hardnesst::set_outfile | ( | const std::string & | file_name | ) |
Definition at line 113 of file solver_hardness.cpp.
|
private |
Definition at line 142 of file solver_hardness.h.
|
private |
Definition at line 141 of file solver_hardness.h.
|
private |
Definition at line 140 of file solver_hardness.h.
|
private |
Definition at line 139 of file solver_hardness.h.
|
private |
Definition at line 143 of file solver_hardness.h.
|
private |
Definition at line 137 of file solver_hardness.h.