ROSE  0.9.10.91
Public Attributes | List of all members
Rose::BinaryAnalysis::SmtSolver::Stats Struct Reference

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 87 of file BinarySmtSolver.h.

#include <BinarySmtSolver.h>

Public Attributes

size_t ncalls
 Number of times satisfiable() was called. More...
 
size_t input_size
 Bytes of input generated for satisfiable(). More...
 
size_t output_size
 Amount of output produced by the SMT solver. More...
 
size_t memoizationHits
 Number of times memoization supplied a result. More...
 
size_t nSolversCreated
 Number of solvers created. More...
 
size_t nSolversDestroyed
 Number of solvers destroyed. More...
 
double prepareTime
 Time spent creating assertions before solving. More...
 
double solveTime
 Seconds spent in solver's solve function. More...
 
double evidenceTime
 Seconds to retrieve evidence of satisfiability. More...
 

Member Data Documentation

size_t Rose::BinaryAnalysis::SmtSolver::Stats::ncalls

Number of times satisfiable() was called.

Definition at line 88 of file BinarySmtSolver.h.

size_t Rose::BinaryAnalysis::SmtSolver::Stats::input_size

Bytes of input generated for satisfiable().

Definition at line 89 of file BinarySmtSolver.h.

size_t Rose::BinaryAnalysis::SmtSolver::Stats::output_size

Amount of output produced by the SMT solver.

Definition at line 90 of file BinarySmtSolver.h.

size_t Rose::BinaryAnalysis::SmtSolver::Stats::memoizationHits

Number of times memoization supplied a result.

Definition at line 91 of file BinarySmtSolver.h.

size_t Rose::BinaryAnalysis::SmtSolver::Stats::nSolversCreated

Number of solvers created.

Only for class statistics.

Definition at line 92 of file BinarySmtSolver.h.

size_t Rose::BinaryAnalysis::SmtSolver::Stats::nSolversDestroyed

Number of solvers destroyed.

Only for class statistics.

Definition at line 93 of file BinarySmtSolver.h.

double Rose::BinaryAnalysis::SmtSolver::Stats::prepareTime

Time spent creating assertions before solving.

Definition at line 94 of file BinarySmtSolver.h.

double Rose::BinaryAnalysis::SmtSolver::Stats::solveTime

Seconds spent in solver's solve function.

Definition at line 95 of file BinarySmtSolver.h.

double Rose::BinaryAnalysis::SmtSolver::Stats::evidenceTime

Seconds to retrieve evidence of satisfiability.

Definition at line 96 of file BinarySmtSolver.h.


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