Description

SMT solver statistics.

Solver statistics get accumulted into the class statistics only when the solver is destroyed or the solver's resetStatistics method is invoked.

Definition at line 96 of file SmtSolver.h.

#include <Rose/BinaryAnalysis/SmtSolver.h>

Public Member Functions
void	print (std::ostream &, const std::string &prefix="") const

Public Attributes
size_t	ncalls = 0
	Number of times satisfiable() was called.

size_t	input_size = 0
	Bytes of input generated for satisfiable().

size_t	output_size = 0
	Amount of output produced by the SMT solver.

size_t	memoizationHits = 0
	Number of times memoization supplied a result.

size_t	nSolversCreated = 0
	Number of solvers created.

size_t	nSolversDestroyed = 0
	Number of solvers destroyed.

double	prepareTime = 0.0
	Total time in seconds spent creating assertions before solving.

double	longestPrepareTime = 0.0
	Longest of times added to prepareTime.

double	solveTime = 0.0
	Total time in seconds spent in solver's solve function.

double	longestSolveTime = 0.0
	Longest of times added to the solveTime total.

double	evidenceTime = 0.0
	Total time in seconds to retrieve evidence of satisfiability.

double	longestEvidenceTime = 0.0
	Longest of times added to evidenceTime.

size_t	nSatisfied = 0
	Number of times the solver returned "satisified".

size_t	nUnsatisfied = 0
	Number of times the solver returned "unsatisfied".

size_t	nUnknown = 0
	Number of times the solver returned "unknown".

Member Data Documentation

◆ ncalls

size_t Rose::BinaryAnalysis::SmtSolver::Stats::ncalls = 0

Number of times satisfiable() was called.

Definition at line 97 of file SmtSolver.h.

◆ input_size

size_t Rose::BinaryAnalysis::SmtSolver::Stats::input_size = 0

Bytes of input generated for satisfiable().

Definition at line 98 of file SmtSolver.h.

◆ output_size

size_t Rose::BinaryAnalysis::SmtSolver::Stats::output_size = 0

Amount of output produced by the SMT solver.

Definition at line 99 of file SmtSolver.h.

◆ memoizationHits

size_t Rose::BinaryAnalysis::SmtSolver::Stats::memoizationHits = 0

Number of times memoization supplied a result.

Definition at line 100 of file SmtSolver.h.

◆ nSolversCreated

size_t Rose::BinaryAnalysis::SmtSolver::Stats::nSolversCreated = 0

Number of solvers created.

Only for class statistics.

Definition at line 101 of file SmtSolver.h.

◆ nSolversDestroyed

size_t Rose::BinaryAnalysis::SmtSolver::Stats::nSolversDestroyed = 0

Number of solvers destroyed.

Only for class statistics.

Definition at line 102 of file SmtSolver.h.

◆ prepareTime

double Rose::BinaryAnalysis::SmtSolver::Stats::prepareTime = 0.0

Total time in seconds spent creating assertions before solving.

Definition at line 103 of file SmtSolver.h.

◆ longestPrepareTime

double Rose::BinaryAnalysis::SmtSolver::Stats::longestPrepareTime = 0.0

Longest of times added to prepareTime.

Definition at line 104 of file SmtSolver.h.

◆ solveTime

double Rose::BinaryAnalysis::SmtSolver::Stats::solveTime = 0.0

Total time in seconds spent in solver's solve function.

Definition at line 105 of file SmtSolver.h.

◆ longestSolveTime

double Rose::BinaryAnalysis::SmtSolver::Stats::longestSolveTime = 0.0

Longest of times added to the solveTime total.

Definition at line 106 of file SmtSolver.h.

◆ evidenceTime

double Rose::BinaryAnalysis::SmtSolver::Stats::evidenceTime = 0.0

Total time in seconds to retrieve evidence of satisfiability.

Definition at line 107 of file SmtSolver.h.

◆ longestEvidenceTime

double Rose::BinaryAnalysis::SmtSolver::Stats::longestEvidenceTime = 0.0

Longest of times added to evidenceTime.

Definition at line 108 of file SmtSolver.h.

◆ nSatisfied

size_t Rose::BinaryAnalysis::SmtSolver::Stats::nSatisfied = 0

Number of times the solver returned "satisified".

Definition at line 109 of file SmtSolver.h.

◆ nUnsatisfied

size_t Rose::BinaryAnalysis::SmtSolver::Stats::nUnsatisfied = 0

Number of times the solver returned "unsatisfied".

Definition at line 110 of file SmtSolver.h.

◆ nUnknown

size_t Rose::BinaryAnalysis::SmtSolver::Stats::nUnknown = 0

Number of times the solver returned "unknown".

Definition at line 111 of file SmtSolver.h.

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

SmtSolver.h