ROSE
0.11.145.0

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. More...  
size_t  input_size = 0 
Bytes of input generated for satisfiable(). More...  
size_t  output_size = 0 
Amount of output produced by the SMT solver. More...  
size_t  memoizationHits = 0 
Number of times memoization supplied a result. More...  
size_t  nSolversCreated = 0 
Number of solvers created. More...  
size_t  nSolversDestroyed = 0 
Number of solvers destroyed. More...  
double  prepareTime = 0.0 
Total time in seconds spent creating assertions before solving. More...  
double  longestPrepareTime = 0.0 
Longest of times added to prepareTime. More...  
double  solveTime = 0.0 
Total time in seconds spent in solver's solve function. More...  
double  longestSolveTime = 0.0 
Longest of times added to the solveTime total. More...  
double  evidenceTime = 0.0 
Total time in seconds to retrieve evidence of satisfiability. More...  
double  longestEvidenceTime = 0.0 
Longest of times added to evidenceTime. More...  
size_t  nSatisfied = 0 
Number of times the solver returned "satisified". More...  
size_t  nUnsatisfied = 0 
Number of times the solver returned "unsatisfied". More...  
size_t  nUnknown = 0 
Number of times the solver returned "unknown". More...  
size_t Rose::BinaryAnalysis::SmtSolver::Stats::ncalls = 0 
Number of times satisfiable() was called.
Definition at line 97 of file SmtSolver.h.
size_t Rose::BinaryAnalysis::SmtSolver::Stats::input_size = 0 
Bytes of input generated for satisfiable().
Definition at line 98 of file SmtSolver.h.
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.
size_t Rose::BinaryAnalysis::SmtSolver::Stats::memoizationHits = 0 
Number of times memoization supplied a result.
Definition at line 100 of file SmtSolver.h.
size_t Rose::BinaryAnalysis::SmtSolver::Stats::nSolversCreated = 0 
size_t Rose::BinaryAnalysis::SmtSolver::Stats::nSolversDestroyed = 0 
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.
double Rose::BinaryAnalysis::SmtSolver::Stats::longestPrepareTime = 0.0 
Longest of times added to prepareTime.
Definition at line 104 of file SmtSolver.h.
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.
double Rose::BinaryAnalysis::SmtSolver::Stats::longestSolveTime = 0.0 
Longest of times added to the solveTime total.
Definition at line 106 of file SmtSolver.h.
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.
double Rose::BinaryAnalysis::SmtSolver::Stats::longestEvidenceTime = 0.0 
Longest of times added to evidenceTime.
Definition at line 108 of file SmtSolver.h.
size_t Rose::BinaryAnalysis::SmtSolver::Stats::nSatisfied = 0 
Number of times the solver returned "satisified".
Definition at line 109 of file SmtSolver.h.
size_t Rose::BinaryAnalysis::SmtSolver::Stats::nUnsatisfied = 0 
Number of times the solver returned "unsatisfied".
Definition at line 110 of file SmtSolver.h.
size_t Rose::BinaryAnalysis::SmtSolver::Stats::nUnknown = 0 
Number of times the solver returned "unknown".
Definition at line 111 of file SmtSolver.h.