CBMC
solver_hardnesst Struct Reference

A structure that facilitates collecting the complexity statistics from a decision procedure. More...

#include <solver_hardness.h>

+ Inheritance diagram for solver_hardnesst:
+ Collaboration diagram for solver_hardnesst:

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_hardnesstoperator= (const solver_hardnesst &)=delete
 
solver_hardnesstoperator= (solver_hardnesst &&)=default
 
- Public Member Functions inherited from clause_hardness_collectort
virtual ~clause_hardness_collectort ()
 

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
 

Detailed Description

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 39 of file solver_hardness.h.

Constructor & Destructor Documentation

◆ solver_hardnesst() [1/3]

solver_hardnesst::solver_hardnesst ( )
default

◆ solver_hardnesst() [2/3]

solver_hardnesst::solver_hardnesst ( const solver_hardnesst )
delete

◆ solver_hardnesst() [3/3]

solver_hardnesst::solver_hardnesst ( solver_hardnesst &&  )
default

Member Function Documentation

◆ expr2string()

std::string solver_hardnesst::expr2string ( const exprt expr)
staticprivate

Definition at line 382 of file solver_hardness.cpp.

◆ goto_instruction2string()

std::string solver_hardnesst::goto_instruction2string ( goto_programt::const_targett  pc)
staticprivate

Definition at line 226 of file solver_hardness.cpp.

◆ operator=() [1/2]

solver_hardnesst& solver_hardnesst::operator= ( const solver_hardnesst )
delete

◆ operator=() [2/2]

solver_hardnesst& solver_hardnesst::operator= ( solver_hardnesst &&  )
default

◆ produce_report()

void solver_hardnesst::produce_report ( )

Print the statistics to a JSON file (specified via command-line option).

Definition at line 121 of file solver_hardness.cpp.

◆ register_assertion_ssas()

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.

Parameters
ssa_expressionstring representing the disjuction of SSA assertions
pcsall GOTO instruction iterators that contributed in the disjunction

Definition at line 75 of file solver_hardness.cpp.

◆ register_clause()

void solver_hardnesst::register_clause ( const bvt bv,
const bvt cnf,
const size_t  cnf_clause_index,
bool  register_cnf 
)
virtual

Called e.g.

from the satcheck_minisat2::lcnf, this function adds the complexity statistics from the last SAT query to the current_ssa_key.

Parameters
bvthe clause (vector of literals)
cnfprocessed clause
cnf_clause_indexindex of clause in dimacs output
register_cnfnegation of boolean variable tracking if the clause can be eliminated

Implements clause_hardness_collectort.

Definition at line 90 of file solver_hardness.cpp.

◆ register_ssa()

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.

Parameters
ssa_indexposition (of this step) in the SSA equation
ssa_expressionstring representing the SSA step expression
pcthe GOTO instruction iterator for this SSA step

Definition at line 45 of file solver_hardness.cpp.

◆ register_ssa_size()

void solver_hardnesst::register_ssa_size ( std::size_t  size)

Definition at line 66 of file solver_hardness.cpp.

◆ set_outfile()

void solver_hardnesst::set_outfile ( const std::string &  file_name)

Definition at line 116 of file solver_hardness.cpp.

Member Data Documentation

◆ assertion_stats

assertion_statst solver_hardnesst::assertion_stats
private

Definition at line 140 of file solver_hardness.h.

◆ current_hardness

sat_hardnesst solver_hardnesst::current_hardness
private

Definition at line 139 of file solver_hardness.h.

◆ current_ssa_key

hardness_ssa_keyt solver_hardnesst::current_ssa_key
private

Definition at line 138 of file solver_hardness.h.

◆ hardness_stats

std::vector<std::unordered_map<hardness_ssa_keyt, sat_hardnesst> > solver_hardnesst::hardness_stats
private

Definition at line 137 of file solver_hardness.h.

◆ max_ssa_set_size

std::size_t solver_hardnesst::max_ssa_set_size
private

Definition at line 141 of file solver_hardness.h.

◆ outfile

std::string solver_hardnesst::outfile
private

Definition at line 135 of file solver_hardness.h.


The documentation for this struct was generated from the following files: