ROSE
0.9.10.44

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...  
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.