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

/home/runner/work/cbmc/cbmc/src/goto-symex/solver_hardness.h
/home/runner/work/cbmc/cbmc/src/goto-symex/solver_hardness.cpp

Classes

Public Member Functions

Static Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ solver_hardnesst() [1/3]

◆ solver_hardnesst() [2/3]

◆ solver_hardnesst() [3/3]

Member Function Documentation

◆ expr2string()

◆ goto_instruction2string()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ produce_report()

◆ register_assertion_ssas()

◆ register_clause()

◆ register_ssa()

◆ register_ssa_size()

◆ set_outfile()

Member Data Documentation

◆ assertion_stats

◆ current_hardness

◆ current_ssa_key

◆ hardness_stats

◆ max_ssa_set_size

◆ outfile