CBMC
Loading...
Searching...
No Matches
Classes | Public Member Functions | Static Private Member Functions | Private Attributes | List of all members
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:
[フレーム]
[legend]
+ Collaboration diagram for solver_hardnesst:
[フレーム]
[legend]

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.
 
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.
 
void  register_clause (const bvt &bv, const bvt &cnf, const size_t cnf_clause_index, bool register_cnf)
  Called e.g.
 
void  set_outfile (const std::string &file_name)
 
void  produce_report ()
  Print the statistics to a JSON file (specified via command-line option).
 
  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
 
- 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_expression string representing the disjuction of SSA assertions
pcs all 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
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

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_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 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:

AltStyle によって変換されたページ (->オリジナル) /