ROSE  0.11.98.0
Public Member Functions | 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 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...
 

Member Data Documentation

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

Number of solvers created.

Only for class statistics.

Definition at line 101 of file SmtSolver.h.

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

Number of solvers destroyed.

Only for class statistics.

Definition at line 102 of file SmtSolver.h.

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.


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